---

Step * 2 of Lemma reg-seq-list-add_functionality_wrt_permutation


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)} 
BY
{ (EqTypeCD THEN Auto THEN Try ((GenConclTerm ⌜reg-seq-list-add(L)⌝⋅ THEN CompleteAuto)⋅))⋅ }

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

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  L'  :  \mBbbR{}  List
3.  permutation(\mBbbR{};L;L')
4.  \mneg{}(||L||  =  0)
\mvdash{}  reg-seq-list-add(L)  =  reg-seq-list-add(L')


By

---

Latex:
(EqTypeCD  THEN  Auto  THEN  Try  ((GenConclTerm  \mkleeneopen{}reg-seq-list-add(L)\mkleeneclose{}\mcdot{}  THEN  CompleteAuto)\mcdot{}))\mcdot{}

---

Home Index