---

Step * 2 1 of Lemma concat-decomp


1. [T] : Type
2. ll : T List List
3. x : T
4. ll1 : T List List
5. ll2 : T List List
6. l1 : T List
7. l2 : T List
8. concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List)
9. ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List)
⊢ ((l1 @ [x] @ l2 ∈ ll1)
∨ (((l1 @ [x] @ l2) = (l1 @ [x] @ l2) ∈ (T List)) ∨ (l1 @ [x] @ l2 ∈ []))
∨ (l1 @ [x] @ l2 ∈ ll2))
∧ ((x ∈ l1) ∨ ((x = x ∈ T) ∨ (x ∈ [])) ∨ (x ∈ l2))
BY
{ Obvious }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  ll  :  T  List  List
3.  x  :  T
4.  ll1  :  T  List  List
5.  ll2  :  T  List  List
6.  l1  :  T  List
7.  l2  :  T  List
8.  concat(ll)  =  (concat(ll1)  @  (l1  @  [x]  @  l2)  @  concat(ll2))
9.  ll  =  (ll1  @  [l1  @  [x]  @  l2]  @  ll2)
\mvdash{}  ((l1  @  [x]  @  l2  \mmember{}  ll1)
\mvee{}  (((l1  @  [x]  @  l2)  =  (l1  @  [x]  @  l2))  \mvee{}  (l1  @  [x]  @  l2  \mmember{}  []))
\mvee{}  (l1  @  [x]  @  l2  \mmember{}  ll2))
\mwedge{}  ((x  \mmember{}  l1)  \mvee{}  ((x  =  x)  \mvee{}  (x  \mmember{}  []))  \mvee{}  (x  \mmember{}  l2))


By

---

Latex:
Obvious

---

Home Index