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

Proving  (3.29)  Zero of $∨$:  p ∨ true ≡ true

    p ∨ true
  =   〈 Identity of $\equiv$ (3.3) 〉
       ─ CalcCheck: (3.3) Identity of ≡   ─   OK
    p ∨ (p ≡ p)
  =   〈 Distributivity of $\lor$ over $\equiv$ (3.27) 〉
       ─ CalcCheck: (3.27) Distributivity of ∨ over ≡   ─   OK
    p ∨ p ≡ p ∨ p
  =   〈 Identity of $\equiv$ (3.3) 〉
       ─ CalcCheck: (3.3) Identity of ≡   ─   OK
    true

 ─ CalcCheck: All steps OK
Proof matches goal ─ OK



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

Proving  (3.29)  Zero of $∨$:  p ∨ true ≡ true

    true   ─ This is:   (3.4)
  =   〈 Identity of $\equiv$ (3.3) 〉
       ─ CalcCheck: (3.3) Identity of ≡   ─   OK
    p ∨ p ≡ p ∨ p
  =   〈 Distributivity of $\lor$ over $\equiv$ (3.27) 〉
       ─ CalcCheck: (3.27) Distributivity of ∨ over ≡   ─   OK
    p ∨ (p ≡ p)
  =   〈 Identity of $\equiv$ (3.3) 〉
       ─ CalcCheck: (3.3) Identity of ≡   ─   OK
    p ∨ true

 ─ CalcCheck: All steps OK
Initial \ThisIs{  (3.4)} matches ─ OK
Proof matches goal ─ OK



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

Proving  (3.82a)  Transitivity of $⇒$:  (p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)

    (p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)
  =   〈 Shunting (3.65) 〉
       ─ CalcCheck: (3.65) Shunting   ─   OK
    p ∧ (p ⇒ q) ∧ (q ⇒ r) ⇒ r
  =   〈 (3.66) $p \land (p \implies q) \equiv p \land q$ 〉
       ─ CalcCheck: (3.66) p ∧ (p ⇒ q) ≡ p ∧ q   ─   OK
    p ∧ q ∧ (q ⇒ r) ⇒ r
  =   〈 (3.66) $p \land (p \implies q) \equiv p \land q$ 〉
       ─ CalcCheck: (3.66) p ∧ (p ⇒ q) ≡ p ∧ q   ─   OK
    p ∧ q ∧ r ⇒ r   ─ This is:   (3.76b)  Strengthening

 ─ CalcCheck: All steps OK
Final \ThisIs{  (3.76b)  Strengthening} matches ─ OK
Proof matches goal ─ OK



CalcCheck: Finished checking Test/Test005.ltx
CalcCheck: 3 out of 3 calculations fully checked
CalcCheck: Wrote Test/Test005.ltx.html
