---

Step * 1 of Lemma radd_assoc


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])
BY
{ (Assert permutation(ℝ;[c; a; b];[a; b; c]) BY
         ((RW (AddrC [2] (LemmaC `permutation-rotate-cons`)) 0 THENM Reduce 0) THEN Auto)) }

1
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])

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  permutation(\mBbbR{};[c;  a;  b];[a;  b;  c])  BY
              ((RW  (AddrC  [2]  (LemmaC  `permutation-rotate-cons`))  0  THENM  Reduce  0)  THEN  Auto))

---

Home Index