---

Step * 1 1 of Lemma map-permute_list


1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
⊢ map(g;primrec(||L||;[];λi,l. (l @ [L[f i]]))) ~ primrec(||L||;[];λi,l. (l @ [map(g;L)[f i]]))
BY
{ Assert ⌜∀n:ℕ. ((n ≤ ||L||) ⇒ (map(g;primrec(n;[];λi,l. (l @ [L[f i]]))) ~ primrec(n;[];λi,l. (l @ [map(g;L)[f i]]))))\000C⌝⋅ }

1
.....assertion..... 
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
⊢ ∀n:ℕ. ((n ≤ ||L||) ⇒ (map(g;primrec(n;[];λi,l. (l @ [L[f i]]))) ~ primrec(n;[];λi,l. (l @ [map(g;L)[f i]]))))

2
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
4. ∀n:ℕ. ((n ≤ ||L||) ⇒ (map(g;primrec(n;[];λi,l. (l @ [L[f i]]))) ~ primrec(n;[];λi,l. (l @ [map(g;L)[f i]]))))
⊢ map(g;primrec(||L||;[];λi,l. (l @ [L[f i]]))) ~ primrec(||L||;[];λi,l. (l @ [map(g;L)[f i]]))

---

Latex:

---

Latex:

1.  g  :  Top
2.  L  :  Top  List
3.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
\mvdash{}  map(g;primrec(||L||;[];\mlambda{}i,l.  (l  @  [L[f  i]])))  \msim{}  primrec(||L||;[];\mlambda{}i,l.  (l  @  [map(g;L)[f  i]]))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}
                    ((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)\mkleeneclose{}\mcdot{}

---

Home Index