---

Step * 1 1 1 2 2 1 of Lemma map-permute_list


1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. n ≤ ||L||
8. map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
⊢ map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]])) @ [L[f (n - 1)]]) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
@ [map(g;L)[f (n - 1)]]
BY
{ RWO "map_append_sq" 0 }

1
.....wf..... 
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. n ≤ ||L||
8. map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
⊢ g ∈ Top

2
.....wf..... 
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. n ≤ ||L||
8. map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
⊢ primrec(n - 1;[];λi,l. (l @ [L[f i]])) ∈ Top

3
.....wf..... 
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. n ≤ ||L||
8. map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
⊢ [L[f (n - 1)]] ∈ Top

4
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. n ≤ ||L||
8. map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
⊢ map(g;primrec(n - 1;[];λi,l. (l @ [L[f i]]))) @ map(g;[L[f (n - 1)]]) ~ primrec(n - 1;[];λi,l. (l @ [map(g;L)[f i]]))
@ [map(g;L)[f (n - 1)]]

---

Latex:

---

Latex:

1.  g  :  Top
2.  L  :  Top  List
3.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
4.  n  :  \mBbbZ{}
5.  n  \mneq{}  0
6.  0  <  n
7.  n  \mleq{}  ||L||
8.  map(g;primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [L[f  i]])))  \msim{}  primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [map(g;L)[f  i]]))
\mvdash{}  map(g;primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [L[f  i]]))  @  [L[f  (n  -  1)]]) 
\msim{}  primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [map(g;L)[f  i]]))  @  [map(g;L)[f  (n  -  1)]]


By

---

Latex:
RWO  "map\_append\_sq"  0

---

Home Index