A5Q1 : THEORY

 BEGIN

 x: VAR real
                      
 g(x): real =   TABLE  
		%--------------% 
		|[ x<0 | x>=0 ]|
                %--------------%
                |  x   | 2*x  ||
                %--------------% 
		ENDTABLE 

 h(x): real =   TABLE  
		%--------------% 
		|[ x<=0 | x>=0 ]|
                %--------------%
                |  x   | 2*x  ||
                %--------------% 
		ENDTABLE 

 same: THEOREM FORALL (x:real): g(x)=h(x)  

  END A5Q1


A5Q2  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  


  PwrCond(Prev:bool, Power, Kin, Kout:posreal):bool = TABLE
   %-----------------------------------------------%
   |[Power<=Kout|Power>Kout & Power<Kin|Power>=Kin]|
   %-----------------------------------------------%
   | TRUE       | Prev                 | FALSE    ||
   %-----------------------------------------------%
   ENDTABLE


  END A5Q2


A5Q3: THEORY
 BEGIN

 n: VAR nat

 Q3d: THEOREM (forall (n:nat): (exists (i:nat) : (4^n-1) = 3*i))

% Sample PVS for Rubin p. 302 A2.  Uncomment and edit for Question 3 f
% sum2(n): RECURSIVE nat =
%  (IF n = 0 THEN 0 ELSE n^2 + sum2(n - 1) ENDIF)
%  MEASURE id

% closed_form2: THEOREM sum2(n) = (n * (n + 1)*(2*n+1))/6


 END A5Q3