---

Step * of Lemma map_permute_list

∀[A,B:Type]. ∀[f:B ⟶ A]. ∀[x:B List]. ∀[g:ℕ||x|| ⟶ ℕ||x||].  (map(f;(x o g)) = (map(f;x) o g) ∈ (A List))
BY
{ (Auto
   THEN (Assert ||map(f;x)|| = ||x|| ∈ ℤ BY
               (RWO "map_length" 0 THEN Auto))
   THEN (Assert ||map(f;(x o g))|| = ||x|| ∈ ℤ BY
               (RWO "map_length" 0 THEN Auto THEN RWO "permute_list_length" 0 THEN Auto))
   THEN (Assert ||(map(f;x) o g)|| = ||x|| ∈ ℤ BY
               (RWO "permute_list_length" 0 THEN Auto))
   THEN ((BLemma `list_extensionality` THEN Auto) THEN RWW "permute_list_select map_select" 0 THEN Auto THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:B  {}\mrightarrow{}  A].  \mforall{}[x:B  List].  \mforall{}[g:\mBbbN{}||x||  {}\mrightarrow{}  \mBbbN{}||x||].    (map(f;(x  o  g))  =  (map(f;x)  o  g))


By

---

Latex:
(Auto
  THEN  (Assert  ||map(f;x)||  =  ||x||  BY
                          (RWO  "map\_length"  0  THEN  Auto))
  THEN  (Assert  ||map(f;(x  o  g))||  =  ||x||  BY
                          (RWO  "map\_length"  0  THEN  Auto  THEN  RWO  "permute\_list\_length"  0  THEN  Auto))
  THEN  (Assert  ||(map(f;x)  o  g)||  =  ||x||  BY
                          (RWO  "permute\_list\_length"  0  THEN  Auto))
  THEN  ((BLemma  `list\_extensionality`  THEN  Auto)
              THEN  RWW  "permute\_list\_select  map\_select"  0
              THEN  Auto
              THEN  Auto')\mcdot{})

---

Home Index