%Patch files loaded: patch2 version 1.2.2.36

$$$a4.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.

$$$a4.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|)