---

Step * 1 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
{ ((EqCD THEN Auto)
   THEN (FLemma `permutation-length` [-2] THENA Auto)
   THEN DVar `L'
   THEN DVar `L\''
   THEN All Reduce 
   THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((EqCD  THEN  Auto)
  THEN  (FLemma  `permutation-length`  [-2]  THENA  Auto)
  THEN  DVar  `L'
  THEN  DVar  `L\mbackslash{}''
  THEN  All  Reduce 
  THEN  Auto')

---

Home Index