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

    (p ≢ q) ≡ ¬p ≡ q

    ¬p ≡ q
  =   〈 Distributivity of $\neg$ over $\equiv$ (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    ¬(p ≡ q)
  =   〈 Definition of $\nequiv$ (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    p ≢ q

 ─ CalcCheck: All steps OK



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

    (p ≢ q) ≡ r ≡ (p ≢ (q ≡ r))

    p ≢ (q ≡ r)
  =   〈 Definition of $\nequiv$ (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    ¬(p ≡ q ≡ r)
  =   〈 Associativity of $\equiv$ (3.1) 〉
       ─ CalcCheck: (3.1) Associativity of ≡   ─   OK
    ¬(p ≡ q ≡ r)
  =   〈 Distributivity of $\neg$ over $\equiv$ (3.9) 〉
       ─ CalcCheck: (3.9) Distributivity of ¬ over ≡   ─   OK
    ¬(p ≡ q) ≡ r
  =   〈 Definition of $\nequiv$ (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢   ─   OK
    (p ≢ q) ≡ r

 ─ CalcCheck: All steps OK



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

    ((p ≢ q) ≡ r ≡ p ≡ q) ≢ r

    (p ≡ q) ≢ r
  =   〈 (3.14) 〉
       ─ CalcCheck: (3.14) (p ≢ q) ≡ ¬p ≡ q; could not justify this step!
    ¬(q ≡ q) ≡ r
  =   〈 Definition of $\nequiv$ (3.10) 〉
       ─ CalcCheck: (3.10) Definition of ≢; could not justify this step!
    (p ≢ q) ≡ r
  =   〈 Removing unnecessary brackets 〉
       ─ CalcCheck: Could not extract information   ─   OK (no change)
    (p ≢ q) ≡ r

 ─ CalcCheck: 2 out of 3 steps not justified



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

    p ∨ q ∨ r ≡ p ∨ q ∨ p ∨ r

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

 ─ CalcCheck: All steps OK



CalcCheck: Finished checking Test/Test002.ltx
CalcCheck: 7 out of 8 calculations fully checked
CalcCheck: 1 out of 8 calculations not fully justified
CalcCheck: Wrote Test/Test002.ltx.html
