---

Step * of Lemma add-associates

∀[x,y,z:Top].  ((x + y) + z ~ x + y + z)
BY
{ TACTIC:Assert ⌜∀x,y,z:ℤ.  (((x + y) + z) = (x + y + z) ∈ ℤ)⌝⋅ }

1
.....assertion..... 
∀x,y,z:ℤ.  (((x + y) + z) = (x + y + z) ∈ ℤ)

2
1. ∀x,y,z:ℤ.  (((x + y) + z) = (x + y + z) ∈ ℤ)
⊢ ∀[x,y,z:Top].  ((x + y) + z ~ x + y + z)

---

Latex:

---

Latex:
\mforall{}[x,y,z:Top].    ((x  +  y)  +  z  \msim{}  x  +  y  +  z)


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y,z:\mBbbZ{}.    (((x  +  y)  +  z)  =  (x  +  y  +  z))\mkleeneclose{}\mcdot{}

---

Home Index