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

Proving  (3.84a)  e = f ∧ E[z := e] ≡ e = f ∧ E[z := f]

    e = f ⇒ (E[z := e] ≡ E[z := f])   ─ This is:   (3.83)  Leibniz Axiom
  =   〈 Definition of $\implies$ (3.60) 〉
       ─ CalcCheck: (3.60) Definition of ⇒   ─   OK
    e = f ∧ (E[z := e] ≡ E[z := f]) ≡ e = f
  =   〈 (3.49) 〉
       ─ CalcCheck: (3.49) p ∧ (q ≡ r) ≡ p ∧ q ≡ p ∧ r ≡ p   ─   OK
    e = f ∧ E[z := e] ≡ e = f ∧ E[z := f]

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



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

Proving  (3.84b)  e = f ⇒ E[z := e] ≡ e = f ⇒ E[z := f]

    e = f ⇒ E[z := e] ≡ e = f ⇒ E[z := f]
  =   〈 (3.63) 〉
       ─ CalcCheck: (3.63) Distributivity of ⇒ over ≡   ─   OK
    e = f ⇒ (E[z := e] ≡ E[z := f])
  =   〈 (3.62) 〉
       ─ CalcCheck: (3.62) p ⇒ (q ≡ r) ≡ p ∧ q ≡ p ∧ r   ─   OK
    e = f ∧ E[z := e] ≡ e = f ∧ E[z := f]   ─ This is:   (3.84a)

 ─ CalcCheck: All steps OK
Final \ThisIs{  (3.84a)} matches ─ OK
Proof matches goal ─ OK



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

Proving  (3.84c)  q ∧ e = f ⇒ E[z := e] ≡ q ∧ e = f ⇒ E[z := f]

    q ∧ e = f ⇒ E[z := e]
  =   〈 (3.65) Shunting 〉
       ─ CalcCheck: (3.65) Shunting   ─   OK
    q ⇒ (e = f ⇒ E[z := e])
  =   〈 (3.84b) 〉
       ─ CalcCheck: (3.84b) e = f ⇒ E[z := e] ≡ e = f ⇒ E[z := f]   ─   OK
    q ⇒ (e = f ⇒ E[z := f])
  =   〈 (3.65) Shunting 〉
       ─ CalcCheck: (3.65) Shunting   ─   OK
    q ∧ e = f ⇒ E[z := f]

 ─ CalcCheck: All steps OK
Proof matches goal ─ OK



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