---

Step * 1 of Lemma radd-list_functionality_wrt_permutation


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)) ∈ ℝ
BY
{ (EqCD THEN EAuto 1) }

---

Latex:

---

Latex:

1.  L1  :  \mBbbR{}  List
2.  ||L1||  \mneq{}  0
3.  L2  :  \mBbbR{}  List
4.  permutation(\mBbbR{};L1;L2)
5.  ||L1||  =  ||L2||
\mvdash{}  accelerate(||L1||;reg-seq-list-add(L1))  =  accelerate(||L2||;reg-seq-list-add(L2))


By

---

Latex:
(EqCD  THEN  EAuto  1)

---

Home Index