$$$PVSPredExamples.pvs
%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

  U:TYPE+

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

  x,y : VAR U

  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



$$$PVSPredExamples.prf
(|equality_example|
 (|IbEx| "" (SKOLEM!)
  (("" (EXPAND* "f" "g") (("" (EXPAND "a") (("" (PROPAX) NIL NIL)) NIL)) NIL))
  NIL))
(E11
 (|E11_example| "" (FLATTEN)
  (("" (SKOLEM!)
    (("" (SKOLEM!)
      (("" (INST -1 "x!1" "x!2")
        (("" (FLATTEN)
          (("" (INST 1 "x!1")
            (("" (SPLIT)
              (("1" (REPLACE -1 *)
                (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL))
                  NIL))
                NIL)
               ("2" (PROPAX) NIL NIL) ("3" (PROPAX) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|q2a|)
(|predicate|
 (I1 "" (FLATTEN)
  (("" (SKOLEM!)
    (("" (INST -1 "x!1") (("" (INST?) (("" (BDDSIMP) NIL NIL)) NIL)) NIL))
    NIL))
  NIL))
(|equality|
 (|Ia| "" (SKOLEM!) (("" (EXPAND "f") (("" (EXPAND* "g" "a") NIL NIL)) NIL))
  NIL))
(|counter|)
(|counter_model|
 (|NOTHmmm| "" (SPLIT)
  (("1" (INST -1 "a1") (("1" (EXPAND* "H" "F") NIL NIL)) NIL)
   ("2" (INST 1 "a1")
    (("2" (SPLIT)
      (("1" (EXPAND "E") (("1" (PROPAX) NIL NIL)) NIL)
       ("2" (SKOLEM!) (("2" (EXPAND* "F" "G") NIL NIL)) NIL))
      NIL))
    NIL)
   ("3" (SKOLEM!) (("3" (EXPAND* "E" "G" "H") NIL NIL)) NIL))
  NIL))
(|counter_model2|
 (|NOTHmmm| "" (AUTO-REWRITE-DEFS :ALWAYS? T)
  (("" (BDDSIMP)
    (("1" (ASSERT)
      (("1" (INST -1 "a2")
        (("1" (BDDSIMP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL)
     ("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL) ("3" (ASSERT) NIL NIL))
    NIL))
  NIL)
 (|Stupid| "" (INST 1 "2+5/10") (("" (ASSERT) NIL NIL)) NIL))