---

Step * 1 1 of Lemma radd_assoc


1. a : ℝ
2. b : ℝ
3. c : ℝ
4. radd-list([a; b; c]) = (a + b + c)
5. permutation(ℝ;[c; a; b];[a; b; c])
⊢ radd-list([c; a; b]) = radd-list([a; b; c])
BY
{ (RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  radd-list([a;  b;  c])  =  (a  +  b  +  c)
5.  permutation(\mBbbR{};[c;  a;  b];[a;  b;  c])
\mvdash{}  radd-list([c;  a;  b])  =  radd-list([a;  b;  c])


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)

---

Home Index