3 Bool eval(const Wff wff, const Bool e[])
5 case truth: return true;
6 case falsity: return false;
7 case prop(x): return e[x];
8 case implies(x, y): return ! eval(x,e) || eval(y,e);
9 case disj(x, y): return eval(x,e) || eval(y,e);
10 case conj(x, y): return eval(x,e) && eval(y,e);
11 case not(a): return ! eval(a,e);
17 case implies(x, y): x = simplify(x); y = simplify(y);
18 case disj(x, y): x = simplify(x); y = simplify(y);
19 case conj(x, y): x = simplify(x); y = simplify(y);
20 case not(a): a = simplify(a);
25 case implies(truth, a): wff = a;
26 case implies(falsity, a): return truth;
27 case implies(a, falsity): wff = not(a);
28 case implies(a, truth): return truth;
29 case disj(truth, a): return truth;
30 case disj(falsity, a): wff = a;
31 case disj(a, truth): return truth;
32 case disj(a, falsity): wff = a;
33 case conj(truth, a): wff = a;
34 case conj(falsity, a): return falsity;
35 case conj(a, truth): wff = a;
36 case conj(a, falsity): return falsity;
37 case not(not(a)): wff = a;