CalcCheck: Test/Test003.ltx: No syntax errors.
CalcCheck: Now checking...

Proving  (3.14)  (p ≢ q) ≡ ¬p ≡ q

    p ≢ q
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    ¬(p ≡ q)
  =   〈 (3.9 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    ¬p ≡ q

 ─ CalcCheck: 1 out of 2 steps not justified
Proof matches goal ─ OK



=======================

Proving  (3.18)  Mutual associativity:  ((p ≢ q) ≡ r ≡ p) ≢ (q ≡ r)

    (p ≢ q) ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    ¬(p ≡ q) ≡ r
  =   〈 (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    ¬p ≡ q ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢; could not justify this step!
    (p ≢ q) ≡ r
  =   〈 (3.1) 〉
       ─ CalcCheck: (3.1) Associativity of ≡; could not justify this step!
    p ≢ (q ≡ r)

 ─ CalcCheck: 2 out of 4 steps not justified
Could not match proof with stated goal.



=======================

Proving  (3.19)  Mutual interchangeability:  (p ≢ q) ≡ r ≡ ((p ≡ q) ≢ r)

    (p ≢ q) ≡ r
  =   〈 (3.16) 〉
       ─ CalcCheck: (3.16) Symmetry of ≢   ─   OK
    (q ≢ p) ≡ r
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢; could not justify this step!
    ¬q ≡ p ≡ r
  =   〈 3.2 〉
       ─ CalcCheck: Could not extract information   ─   OK (no change)
    p ≡ ¬q ≡ r
  =   〈 (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    p ≡ ¬(q ≡ r)
  =   〈 (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    p ≡ (q ≢ r)
  =   〈 (3.17) 〉
       ─ CalcCheck: (3.17) Associativity of ≢; could not justify this step!
    (p ≡ q) ≢ r

 ─ CalcCheck: 2 out of 6 steps not justified
Proof matches goal ─ OK



=======================

Proving  (3.31)  Distributivity of $∨$ over $∨$:  p ∨ q ∨ r ≡ p ∨ q ∨ p ∨ r

    p ∨ q ∨ p ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ q ∨ p ∨ r
  =   〈 (3.24) 〉
       ─ CalcCheck: (3.24) Symmetry of ∨   ─   OK
    p ∨ p ∨ q ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ p ∨ q ∨ r
  =   〈 (3.26) 〉
       ─ CalcCheck: (3.26) Idempotency of ∨   ─   OK
    p ∨ q ∨ r
  =   〈 (3.25) 〉
       ─ CalcCheck: (3.25) Associativity of ∨   ─   OK
    p ∨ q ∨ r

 ─ CalcCheck: All steps OK
Proof matches goal ─ OK



=======================

Proving  (3.36)  Symmetry of $∧$:  p ∧ q ≡ q ∧ p

    p ∧ q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ q ≡ p ∧ q
  =   〈 (3.2) 〉
       ─ CalcCheck: (3.2) Symmetry of ≡   ─   OK (no change)
    p ≡ q ≡ q ∧ p
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    q ∧ p

 ─ CalcCheck: 2 out of 3 steps not justified
Proof matches goal ─ OK



=======================

Proving  (3.38)  Idempotency of $∧$:  p ∧ p ≡ p

    p ∧ p
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule   ─   OK
    p ≡ p ≡ p ∨ p
  =   〈 (3.26) 〉
       ─ CalcCheck: (3.26) Idempotency of ∨   ─   OK
    p ≡ p ≡ p
  =   〈 (3.2) 〉
       ─ CalcCheck: (3.2) Symmetry of ≡   ─   OK
    p

 ─ CalcCheck: All steps OK
Proof matches goal ─ OK



=======================

Proving  (3.40)  Zero of $∧$:  p ∧ false ≡ false

    p ∧ false
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule   ─   OK
    p ≡ false ≡ p ∨ false
  =   〈 (3.30) 〉
       ─ CalcCheck: (3.30) Identity of ∨   ─   OK
    p ≡ false ≡ p
  =   〈 3.15 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    ¬p ≡ p
  =   〈 (3.15) 〉
       ─ CalcCheck: (3.15) ¬p ≡ p ≡ false   ─   OK
    false

 ─ CalcCheck: 1 out of 4 steps not justified
Proof matches goal ─ OK



=======================

Proving  p ∨ (¬p ∧ q) ≡ p ∨ q

    p ∨ (¬p ∧ q)
  =   〈 (3.32) 〉
       ─ CalcCheck: (3.32) p ∨ q ≡ p ∨ ¬q ≡ p; could not justify this step!
    p ∨ (p ∧ q) ≡ p
  =   〈 (3.32) 〉
       ─ CalcCheck: (3.32) p ∨ q ≡ p ∨ ¬q ≡ p; could not justify this step!
    ¬p ∨ q

 ─ CalcCheck: 2 out of 2 steps not justified
Could not match proof with stated goal.



=======================

Proving  (3.48)  p ∧ q ≡ p ∧ ¬q ≡ ¬p

    p ∧ q ≡ p ∧ ¬q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ q ≡ p ∨ q
  =   〈 3.32 〉
       ─ CalcCheck: Could not extract information; could not justify this step!
    q ≡ p ∨ ¬q
  =   〈 (3.35) 〉
       ─ CalcCheck: (3.35) Golden Rule; could not justify this step!
    p ≡ p ∧ q
  =   〈 (3.40) 〉
       ─ CalcCheck: (3.40) Zero of ∧; could not justify this step!
    p ≡ false
  =   〈 (3.15) 〉
       ─ CalcCheck: (3.15) ¬p ≡ p ≡ false   ─   OK
    ¬p

 ─ CalcCheck: 4 out of 5 steps not justified
Proof matches goal ─ OK



CalcCheck: Finished checking Test/Test003.ltx
CalcCheck: 2 out of 9 calculations fully checked
CalcCheck: 7 out of 9 calculations not fully justified
CalcCheck: Wrote Test/Test003.ltx.html
