---

Step * of Lemma radd_assoc

∀[a,b,c:ℝ].  (((a + b) + c) = (a + b + c))
BY
{ (Auto
   THEN (InstLemma `radd-list-cons` [⌜[b; c]⌝;⌜a⌝]⋅ THENA Auto)
   THEN (RWO "radd-as-radd-list<" (-1) THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)
   THEN (Subst ⌜((a + b) + c) = (c + a + b) ∈ ℝ⌝ 0⋅ THENA Auto)
   THEN (RW (AddrC [1;2] (LemmaC `radd-as-radd-list`)) 0 THENA Auto)
   THEN RWO "radd-list-cons<" 0
   THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. radd-list([a; b; c]) = (a + b + c)
⊢ radd-list([c; a; b]) = radd-list([a; b; c])

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbR{}].    (((a  +  b)  +  c)  =  (a  +  b  +  c))


By

---

Latex:
(Auto
  THEN  (InstLemma  `radd-list-cons`  [\mkleeneopen{}[b;  c]\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "radd-as-radd-list<"  (-1)  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}((a  +  b)  +  c)  =  (c  +  a  +  b)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RW  (AddrC  [1;2]  (LemmaC  `radd-as-radd-list`))  0  THENA  Auto)
  THEN  RWO  "radd-list-cons<"  0
  THEN  Auto)

---

Home Index