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

equality_example  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  x,y:VAR real
  a:real=1
  f(x,y):real = x+y
  g(x,y):real = x+y

  IbEx: THEOREM f(y,a)=g(y,1)
END equality_example


E11  % [ parameters ]
		: THEORY
% Theory for Rubin Chapter 11 Question E11 on p. 244
  BEGIN

  A:TYPE+

  P:PRED[A]
  A,B,C,D:PRED[A]

  a, b:A

  x,y : VAR A

  formulas: THEOREM (forall x: P(x)) => P(a) & P(b)


  E11_example: THEOREM (FORALL x,y:A(x)&B(y)=> x=y)&(EXISTS x:A(x)&C(x))&
	(EXISTS x:B(x)&D(x))
	=>(EXISTS x:C(x)&D(x))

  END E11


%% To get you started on 2(a)
q2a  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  U:TYPE+
  x,y: VAR U
  P,Q,R:PRED[U] 
  %P(x):bool
  a:U
  f(x):U
  g:[[U,U]->U]
  h(x,y):U

  B2:THEOREM (forall x:P(x) => NOT Q(x)) & (forall x: Q(x)  OR NOT R(x))
& ((exists x: NOT Q(f(x))) OR (exists x: Q(f(x)))) 
 => (exists x: NOT P(f(x)) OR NOT R(f(x)))

  END q2a


% Fill in the rest below.




predicate  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  A:TYPE+

  x,y:VAR A

  P(x):bool
  Q(x):bool

  I1:PROPOSITION (FORALL x:P(x) OR Q(x))&
      (FORALL y:NOT P(y) => NOT Q(y)) &
  	(EXISTS x:NOT P(x)) => FALSE

  END predicate




equality  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  x,y:VAR real
  A:TYPE = real
  a:real=1
  f(x,y):real=x+y
  g(x,y):A=x+y

  Ia:THEOREM f(y,a)=g(1,y)
  

  END equality






counter  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  A:TYPE+
  x,y:VAR A
  E,F,H:PRED[A]
  G(x,y):bool % G:PRED[[A,A]]

  END counter




counter_model  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  A:TYPE+={a1,a2}
  x,y:VAR A
  E(x):bool = TRUE
  H(x):bool = TRUE
  F(x):bool = FALSE
  G(x,y):bool = TRUE


  NOTHmmm:PROPOSITION
  NOT((EXISTS x:E(x) & (FORALL y: F(y)=>G(x,y))) &
  (FORALL x,y:(E(x)=>(G(x,y)<=>H(y))))
	=> (FORALL x:F(x)<=>H(x)))

  

  END counter_model

counter_model2  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  A:TYPE+={a1,a2}
  x,y:VAR A
  E(x):bool = x=a1
  H(x):bool = x=a2
  F(x):bool = FALSE
  G(x,y):bool = x=a1 & y=a2


  NOTHmmm:PROPOSITION
  NOT((EXISTS x:E(x) & (FORALL y: F(y)=>G(x,y))) &
  (FORALL x,y:(E(x)=>(G(x,y)<=>H(y))))
	=> (FORALL x:F(x)<=>H(x)))

  z:VAR real
  
  Stupid: THEOREM exists z: z>2

  END counter_model2




example04  % [ parameters ]
		: THEORY

  BEGIN

x,y:VAR nat
f(x,y):nat = x + y

T1: THEOREM f(x,y)=f(y,x)

 P1: PROPOSITION x+x>x
 WrongNotP1: PROPOSITION NOT(x+x>x)
 NotP1: PROPOSITION NOT(FORALL (x:nat): (x+x>x))

  

  END example04