---

Step * of Lemma map_is_append

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[L:A List]. ∀[L1,L2:B List].
  {(map(f;firstn(||L1||;L)) = L1 ∈ (B List)) ∧ (map(f;nth_tl(||L1||;L)) = L2 ∈ (B List))} 
  supposing map(f;L) = (L1 @ L2) ∈ (B List)
BY
{ xxx(Unfold `guard` 0 THEN InductionOnList)xxx }

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

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. u : A
5. v : A List
6. ∀[L1,L2:B List].
     (map(f;firstn(||L1||;v)) = L1 ∈ (B List)) ∧ (map(f;nth_tl(||L1||;v)) = L2 ∈ (B List)) 
     supposing map(f;v) = (L1 @ L2) ∈ (B List)
⊢ ∀[L1,L2:B List].
    (map(f;firstn(||L1||;[u / v])) = L1 ∈ (B List)) ∧ (map(f;nth_tl(||L1||;[u / v])) = L2 ∈ (B List)) 
    supposing map(f;[u / v]) = (L1 @ L2) ∈ (B List)

---

Latex:

---

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


By

---

Latex:
xxx(Unfold  `guard`  0  THEN  InductionOnList)xxx

---

Home Index