---

Step * of Lemma reg-seq-list-add_functionality_wrt_permutation

∀[L,L':ℝ List].
  reg-seq-list-add(L) = reg-seq-list-add(L') ∈ {f:ℕ+ ⟶ ℤ| ||L||-regular-seq(f)}  supposing permutation(ℝ;L;L')
BY
{ (Auto THEN (Decide ⌜||L|| = 0 ∈ ℤ⌝⋅ THENA Auto)) }

1
1. L : ℝ List
2. L' : ℝ List
3. permutation(ℝ;L;L')
4. ||L|| = 0 ∈ ℤ
⊢ reg-seq-list-add(L) = reg-seq-list-add(L') ∈ {f:ℕ+ ⟶ ℤ| ||L||-regular-seq(f)} 

2
1. L : ℝ List
2. L' : ℝ List
3. permutation(ℝ;L;L')
4. ¬(||L|| = 0 ∈ ℤ)
⊢ reg-seq-list-add(L) = reg-seq-list-add(L') ∈ {f:ℕ+ ⟶ ℤ| ||L||-regular-seq(f)} 

---

Latex:

---

Latex:
\mforall{}[L,L':\mBbbR{}  List].    reg-seq-list-add(L)  =  reg-seq-list-add(L')  supposing  permutation(\mBbbR{};L;L')


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}||L||  =  0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index