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



a5solnQ1  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  
%PVS FOR Question 1 b goes here
% Put your definition of f(x) here
x:VAR real

f(x):{y:real|y>=-9} = x^2+4*x-5


% I fogot to say it, but you should put g(x) here

g(x:{x:real|x/=-2}):posreal = 1/(f(x)+9)


% Put you definition of h(x,y) here




  END a5solnQ1




a5solnQ2  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

n:VAR nat

% PVS for Huth+Ryan p. 56 #3.  
sum2(n): RECURSIVE nat =
  (IF n = 0 THEN 0 ELSE n^2 + sum2(n - 1) ENDIF)
  MEASURE id

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

Q2bii: THEOREM n>=4 IMPLIES 2^n>= n+10
  END a5solnQ2


% PVS for question 3 follows

sentripsoln % [ 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}

  AItype:TYPE = real

  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

  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 = x%floor(x)


% Prove this for Question 3 a

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


% Additional Definitions for status output

% Specification
  f_PressStatus(f_PressTrip:Trip,f_PressStatusS1,Transmit:bool):bool =
  TABLE
  | f_PressTrip=Tripped                    | TRUE           ||
  | NOT(f_PressTrip=Tripped)&Transmit      | FALSE          ||
  | NOT(f_PressTrip=Tripped)& NOT Transmit | f_PressStatusS1||
  ENDTABLE

% Implementation
  STATUS(PRES:AItype,PREV:bool):bool = TABLE
  |[PRES<KHPSP-KDB|KHPSP-KDB<=PRES & PRES<KHPSP|PRES>=KHPSP]|
  | PREV         | PREV                       | TRUE     ||
  ENDTABLE




  Status1:THEOREM
  (FORALL (Pressure:real,f_PressTripS1:Trip,f_PressStatusS1,Transmit:bool):
  f_PressStatus(f_PressTrip(Pressure,f_PressTripS1),f_PressStatusS1,Transmit) =
    IF NOT(Transmit) THEN STATUS(real2AItype(Pressure),f_PressStatusS1)
    ELSE FALSE %PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1))
    ENDIF)


Status2:THEOREM
(EXISTS (Pressure:real,f_PressTripS1:Trip,f_PressStatusS1,Transmit:bool):
f_PressStatus(f_PressTrip(Pressure,f_PressTripS1),f_PressStatusS1,Transmit) /=
IF NOT(Transmit) THEN STATUS(real2AItype(Pressure),f_PressStatusS1)
ELSE FALSE 
ENDIF)

%A2Q2h
%Here we can rewrite the status regarding the conclusion of the counter example.
%To judge "Tripped?" first instead of the Transmit, then the equation can be fine.

Status3:THEOREM
(FORALL (Pressure:real,f_PressTripS1:Trip,f_PressStatusS1,Transmit:bool):
f_PressStatus(f_PressTrip(Pressure,f_PressTripS1),f_PressStatusS1,Transmit) =
IF PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1)) THEN 
TRUE 
ELSE 
IF Transmit THEN
FALSE
ELSE
STATUS(real2AItype(Pressure),f_PressStatusS1)
ENDIF
ENDIF)



  END sentripsoln