---

Step * of Lemma radd-list_functionality_wrt_permutation

∀[L1,L2:ℝ List].  radd-list(L1) = radd-list(L2) ∈ ℝ supposing permutation(ℝ;L1;L2)
BY
{ (Auto
   THEN Unfold `radd-list` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (FLemma `permutation-length` [-1] THENA Auto)
   THEN AutoSplit) }

1
1. L1 : ℝ List
2. ||L1|| ≠ 0
3. L2 : ℝ List
4. permutation(ℝ;L1;L2)
5. ||L1|| = ||L2|| ∈ ℤ
⊢ accelerate(||L1||;reg-seq-list-add(L1)) = accelerate(||L2||;reg-seq-list-add(L2)) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].    radd-list(L1)  =  radd-list(L2)  supposing  permutation(\mBbbR{};L1;L2)


By

---

Latex:
(Auto
  THEN  Unfold  `radd-list`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (FLemma  `permutation-length`  [-1]  THENA  Auto)
  THEN  AutoSplit)

---

Home Index