---

Step * 1 of Lemma general_arith_equation2


1. b : ℤ
2. a : Top
3. c : Top
⊢ ((a + (-b)) + b) + (-c) ~ a + (-c)
BY
{ ((RW (AddrC [1;1] (LemmaC `add-associates`)) 0 THENA Auto) THEN (Subst' (-b) + b ~ 0 0 THENA Auto)) }

1
1. b : ℤ
2. a : Top
3. c : Top
⊢ (a + 0) + (-c) ~ a + (-c)

---

Latex:

---

Latex:

1.  b  :  \mBbbZ{}
2.  a  :  Top
3.  c  :  Top
\mvdash{}  ((a  +  (-b))  +  b)  +  (-c)  \msim{}  a  +  (-c)


By

---

Latex:
((RW  (AddrC  [1;1]  (LemmaC  `add-associates`))  0  THENA  Auto)  THEN  (Subst'  (-b)  +  b  \msim{}  0  0  THENA  Auto))

---

Home Index