---

Step * 1 of Lemma map_is_append


1. A : Type
2. B : Type
3. f : A ⟶ B
⊢ ∀[L1,L2:B List].
    (map(f;firstn(||L1||;[])) = L1 ∈ (B List)) ∧ (map(f;nth_tl(||L1||;[])) = L2 ∈ (B List)) 
    supposing map(f;[]) = (L1 @ L2) ∈ (B List)
BY
{ RepeatFor 2 ((D 0 THENA Auto)
               THEN D -1
               THEN (Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
\mvdash{}  \mforall{}[L1,L2:B  List].
        (map(f;firstn(||L1||;[]))  =  L1)  \mwedge{}  (map(f;nth\_tl(||L1||;[]))  =  L2) 
        supposing  map(f;[])  =  (L1  @  L2)


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto)
                          THEN  D  -1
                          THEN  (Reduce  0  THEN  Auto))

---

Home Index