$$$Assignment5.pvs
colors : THEORY
BEGIN

ryb: TYPE = {Red, Yellow, Blue}

bw : TYPE = {White, Black }

wh : TYPE = { c : bw | c = White }

ry : TYPE = { c : ryb | c = Red OR c = Yellow}

w : VAR wh
r1 : VAR ry
blorwh : VAR bw

white : THEOREM w = White

black_or_white : THEOREM blorwh = White OR blorwh = Black

red_or_yellow : THEOREM r1 = Red OR r1 = Yellow

END colors


invalid  % [ parameters ]
                : THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  A,B:VAR bool

  bad: AXIOM (A IMPLIES B) & B IMPLIES A

  P1: PROPOSITION (FALSE IMPLIES B) & B IMPLIES FALSE

  P2: PROPOSITION A IMPLIES FALSE

  P3: PROPOSITION 1=2

  END invalid



$$$Assignment5.prf
(|colors| (|white| "" (SKOLEM!) (("" (ASSERT) NIL)))
 (|black_or_white| "" (POSTPONE) NIL) (|red_or_yellow| "" (POSTPONE) NIL))(|invalid|
                                                                           (P1
                                                                            ""
                                                                            (POSTPONE)
                                                                            NIL)
                                                                           (P2
                                                                            ""
                                                                            (POSTPONE)
                                                                            NIL)
                                                                           (P3
                                                                            ""
                                                                            (POSTPONE)
                                                                            NIL))