---

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


1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. 0 < n
6. n ≤ ||L||
7. 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;[];λi,l. (l @ [L[f i]]))) ~ primrec(n;[];λi,l. (l @ [map(g;L)[f i]]))
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

1
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)]]

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index