---

Step * 1 1 1 2 of Lemma map-permute_list

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

1
.....antecedent..... 
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. n : ℤ
5. 0 < n
6. n ≤ ||L||
⊢ (n - 1) ≤ ||L||

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

---

Latex:

---

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


By

---

Latex:
ParallelLast

---

Home Index