============ Es. 2, 13/01/2017 ============ F ::= A | B | F /\ F | F \/ F g(A) = A g(B) = B g(F1 \/ F2) = g(F1) \/ g(F2) g(F1 /\ F2) = if g(F1) == g(F2) then g(F1) else g(F1) /\ g(F2) A == A = true A == B = false B == A = false B == B = true (F1 /\ F2) == (G1 /\ G2) = F1 == G1 && F2 == G2 (F1 \/ F2) == (G1 \/ G2) = F1 == G1 && F2 == G2 (F1 /\ F2) == A = false (F1 /\ F2) == B = false (F1 /\ F2) == (G1 \/ G2) = false ... Test: g((A /\ A) /\ (A /\ A) --> if g(A /\ A) == g(A /\ A) then g(A /\ A) else ... --> if (if g(A) == g(A) then g(A) else ...) == (if g(A) == g(A) then g(A) else ...) then (if g(A) == g(A) then g(A) else ...) else ... --> if (if A == A then A else ...) == (if A == A then A else ...) then (if A == A then A else ...) else ... --> if A == A then A else ... --> A