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

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  P1,P2, Pn, Q1, Q2, Qm: bool

  DemoA: THEOREM P1 & P2 & Pn IMPLIES Q1 OR Q2 OR Qm

  DemoB: THEOREM P1 OR P2 IMPLIES Q1 AND Q2 

  Demorgan: THEOREM NOT(P1 OR P2) IFF (NOT P1 AND NOT P2)

  P,Q,R:bool

  BddSimpEx: PROPOSITION P IMPLIES Q AND R

  A,B,C,D,E,F,G,H:bool

  P48B15: PROPOSITION
    (A =>(B=>C)) & (NOT A => D & NOT E) & (A & B => NOT C)
   &(D => F OR G) & (B OR (G => H)) & (G => E OR H) & (G & NOT H)
	IMPLIES FALSE

   M, V: bool

   VALID: PROPOSITION
     (Q => M OR V) & M & (V => Q) => Q


  END demo1

$$$demo1.prf
(|demo1| (|DemoA| "" (FLATTEN) (("" (POSTPONE) NIL)))
 (|DemoB| "" (FLATTEN)
  (("" (SPLIT 1)
    (("1" (SPLIT) (("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL)))
     ("2" (SPLIT) (("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL)))))))
 (|Demorgan| "" (BDDSIMP) (("" (PROPAX) NIL)))
 (|BddSimpEx| "" (BDDSIMP) (("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL)))
 (P48B15 "" (BDDSIMP) (("" (PROPAX) NIL)))
 (VALID "" (BDDSIMP) (("" (POSTPONE) NIL))))