Example 6.4 ~a v b |- ~(a & ~b) (0) Comment |a & ~b (1) Assumption |a (2) And-Elimination (Left) (1) Fail: a does not match m2 with { m1:a, m2:~b } False Example 6.5 |- ((a & ~b) v ~a) v b (0) Comment |~(((a & ~b) v ~a) v b) (1) Assumption ||b (2) Assumption ||((a & ~b) v ~a) v b (3) Or-Introduction (Right) (2) Fail: ((a & ~b) v ~a) v b does not match m1 v m2 with { m1:b, m2:b } False Example 6.7 erroneous a v b |- b, undischarged assumption (0) Comment a v b (1) Given |~b (2) Assumption ||~a (3) Assumption ||b (4) Or-Elimination (Right) (1) (3) Fail: ~a does not match ~m2 with { m1:a, m2:b } False Example 6.7a dead end a v b |- b, can't discharge assumption (0) Comment a v b (1) Given |~b (2) Assumption ||~a (3) Assumption ||b (4) Or-Elimination (Right) (1) (3) Fail: ~a does not match ~m2 with { m1:a, m2:b } False Example 6.8 erroneous a v b |- b, confusion about brackets (0) Comment a v b (1) Given |~a (2) Assumption |~a v b (3) Or-Introduction (Left) (2) Fail: ~a v b does not match m1 v m2 with { m2:~a, m1:~a } False Example 6.9 a & b |- ~(~a v ~b) (0) Comment a & b (1) Given a (2) And-Elimination (Left) (1) Fail: a does not match m2 with { m1:a, m2:b } False