---

Step * 1 of Lemma map-permute_list


1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
⊢ map(g;(L o f)) ~ (map(g;L) o f)
BY
{ xxx(RepUR ``permute_list mklist`` 0 THEN Subst' ||map(g;L)|| = ||L|| ∈ ℤ 0)xxx }

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

---

Latex:

---

Latex:

1.  g  :  Top
2.  L  :  Top  List
3.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||
\mvdash{}  map(g;(L  o  f))  \msim{}  (map(g;L)  o  f)


By

---

Latex:
xxx(RepUR  ``permute\_list  mklist``  0  THEN  Subst'  ||map(g;L)||  =  ||L||  0)xxx

---

Home Index