$$$PVS4propLogic.pvs
PVS4propLogic  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  p, q, r, s, t, u:bool

  Demorgan: THEOREM p & q <=> NOT(NOT p OR NOT q)

  ArrowE: THEOREM (p=>q) & p => q

  BDDSIMPex:PROPOSITION p => q&r

  Yuck: THEOREM (p & q <=> NOT(NOT p OR NOT q))& (s OR r => t) 
	    => FALSE

  m, v:bool
  q:int

  E1: THEOREM (q=>m OR v) & m & (v => q) => q

  CounterE1: THEOREM m & NOT v & NOT q =>
NOT((q=>m OR v) & m & (v => q) => q)

  CounterE1b: THEOREM m & NOT v & NOT q =>
(q=>m OR v) & m & (v => q) & NOT q

  a2i:THEOREM ((p=>q)=>q)=>((q=>p)=>p)

 a,b,c,d,e,f,g,h,i:bool

  
% Check consistency of premises.  This is true so premises are inconsistent.
  reallyugly:THEOREM
 (a=>c)&(a OR NOT b) & (c => d or e) & (d => f & NOT b)
  & (e => NOT a & f) & (a OR NOT f) & 
  (NOT b OR g => h & i) & (h=>b)
=> FALSE 

% Same as above but premise h=>b replaced with NOT(h=>b).  Theorem unprovable
% so there must be a counter example which we get from one of the unprovable 
% seqents.
  reallyugly2:THEOREM
 (a=>c)&(a OR NOT b) & (c => d or e) & (d => f & NOT b)
  & (e => NOT a & f) & (a OR NOT f) & 
  (NOT b OR g => h & i) & NOT (h=>b)
=> FALSE 

% Counter example to reallyugly2 is give by truth table row
% |a|b|c|d|e|f|g|h|i|a=>c|a OR NOT b|c=>d OR e| . . .
% |T|F|T|T|F|T|T|T|T| T  |   T      | T       | . . .
% Check this using PVS.
  Counterreallyugly2:THEOREM
  a&NOT b&c&d&NOT e&f&h&i =>
 (a=>c)&(a OR NOT b) & (c => d or e) & (d => f & NOT b)
  & (e => NOT a & f) & (a OR NOT f) & 
  (NOT b OR g => h & i) & NOT (h=>b)




  END PVS4propLogic

$$$PVS4propLogic.prf
(|PVS4propLogic|
 (|Demorgan| "" (SPLIT)
  (("1" (FLATTEN)
    (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)
   ("2" (FLATTEN) (("2" (BDDSIMP) NIL NIL)) NIL))
  NIL)
 (|ArrowE| "" (FLATTEN)
  (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)
 (|BDDSIMPex| "" (BDDSIMP) (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL))
  NIL)
 (|Yuck| "" (FLATTEN)
  (("" (BDDSIMP) (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)) NIL))
  NIL)
 (E1 "" (FLATTEN) (("" (BDDSIMP) (("" (POSTPONE) NIL NIL)) NIL)) NIL)
 (|CounterE1| "" (BDDSIMP) NIL NIL)
 (|CounterE1b| "" (FLATTEN) (("" (BDDSIMP) NIL NIL)) NIL)
 (|a2i| "" (FLATTEN)
  (("" (SPLIT -2)
    (("1" (PROPAX) NIL NIL)
     ("2" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (FLATTEN) NIL NIL)) NIL))
    NIL))
  NIL)
 (|reallyugly| "" (FLATTEN) (("" (BDDSIMP) NIL NIL)) NIL)
 (|reallyugly2| "" (FLATTEN)
  (("" (BDDSIMP) (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL)) NIL))
  NIL)
 (|Counterreallyugly2| "" (FLATTEN) (("" (BDDSIMP) NIL NIL)) NIL))