%Please fill in the following table:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Partner| Last Name             | 1st Name              | Student #     |
%  1    |                       |                       |               |
%  2    |                       |                       |               |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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 : THEORY

 BEGIN

  U:TYPE
  a:U

% Add your definition of f(x,y) here




  END A5Q2


A5Q3: THEORY
 BEGIN

 n: VAR nat

 Q3d: THEOREM (forall (n:nat): (exists (i:nat) : (2^(2*n+1)+1) = 3*i))

 END A5Q3


% PVS for Question 4
sentrip  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  k_PressSP: int = 2450
  k_deadBand: int = 50
  KDB:int = k_deadBand 
  KHPSP:int = k_PressSP

  Trip:TYPE = {Tripped, NotTripped}

% Equivalent Vertical Condition Table for f_PressTrip
  f_PressTrip(Pressure:real,f_PressTripS1:Trip):Trip = TABLE
  | Pressure<=k_PressSP-k_deadBand                  | NotTripped  ||
  | k_PressSP-k_deadBand<Pressure&Pressure<k_PressSP|f_PressTripS1||
  | Pressure>=k_PressSP                             |Tripped      ||
  ENDTABLE

  AItype:TYPE = subrange(0,5000)%real
  PTRIP(PRES:AItype,PREV:bool):bool = TABLE
  |[PRES<=KHPSP-KDB|KHPSP-KDB<PRES & PRES<KHPSP|PRES>=KHPSP]|
  | FALSE         | PREV                       | TRUE     ||
  ENDTABLE

% Abstraction Functions
  Trip2bool(TripVal:Trip):bool = TABLE
  |[TripVal=Tripped|TripVal=NotTripped]|
  |  TRUE          |  FALSE           ||
  ENDTABLE

  real2AItype(x:real):AItype = TABLE
  |[x<=0|0<x&x<5000|x>=5000]|
  |  0  | floor(x) | 5000||
  ENDTABLE

  Sentrip1:THEOREM
  (FORALL (Pressure:real,f_PressTripS1:Trip):
  Trip2bool(f_PressTrip(Pressure,f_PressTripS1)) =
    PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1)))

% Add definitions for 4(d) starting here
% i.e., add Theorem Sentrip2 here
%
%  Sentrip2:THEOREM



%  Add definitions for 4(f) starting here
%
%  Add Definition of f_PressTrip2 here (make sure all TCCs are proved)







%  Add Definition of PTRIP2 here (make sure all TCCs are proved)


% add Theorem Sentrip3 here and prove it!
%
%  Sentrip3:THEOREM




% Add definitions for 4(d) starting here
% i.e., add Theorem Sentrip4 here and prove it!
%
%  Sentrip4:THEOREM


  END sentrip