prop-src/T7.pcc

   1 datatype Wff :: rewrite
   2              = T | F
   3              | VAR Quark
   4              | NOT Wff
   5              | AND Wff, Wff
   6              | OR  Wff, Wff
   7              ;
   8
   9 Wff dnf (Wff wff)
  10 {
  11    rewrite (wff) type (Wff)
  12    {  NOT T: F
  13    |  NOT F: T
  14    |  NOT NOT X: X
  15    |  OR(T,_): T
  16    |  OR(_,T): T
  17    |  OR(F,X): X
  18    |  OR(X,F): X
  19    |  AND(T,X): X
  20    |  AND(X,T): X
  21    |  AND(F,_): F
  22    |  AND(_,F): F
  23
  24    |  NOT(OR(X,Y)):   AND(NOT X,NOT Y)
  25
  26    |  AND(OR(X,Y),Z): OR(AND(X,Z),AND(Y,Z))
  27    |  AND(X,OR(Y,Z)): OR(AND(X,Y),AND(X,Z))
  28    |  OR(OR(X,Y),Z):  OR(X,OR(Y,Z))
  29    |  AND(AND(X,Y),Z): AND(X,AND(Y,Z))
  30    }
  31    return wff;
  32 }