---

Step * 1 1 of Lemma concat-decomp


1. [T] : Type
2. ll : T List List
3. x : T
4. l : T List
5. (l ∈ ll)
6. (x ∈ l)
7. l3 : T List List
8. l4 : T List List
9. ll = (l3 @ [l] @ l4) ∈ (T List List)
10. l1 : T List
11. l2 : T List
12. l = (l1 @ [x] @ l2) ∈ (T List)
⊢ ∃ll1,ll2:T List List
   ∃l1@0,l2@0:T List
    (((concat(l3) @ (l1 @ [x] @ l2) @ concat(l4)) = (concat(ll1) @ (l1@0 @ [x] @ l2@0) @ concat(ll2)) ∈ (T List))
    ∧ ((l3 @ [l1 @ [x] @ l2] @ l4) = (ll1 @ [l1@0 @ [x] @ l2@0] @ ll2) ∈ (T List List)))
BY
{ TACTIC:((InstConcl [⌜l3⌝; ⌜l4⌝; ⌜l1⌝; ⌜l2⌝])⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  ll  :  T  List  List
3.  x  :  T
4.  l  :  T  List
5.  (l  \mmember{}  ll)
6.  (x  \mmember{}  l)
7.  l3  :  T  List  List
8.  l4  :  T  List  List
9.  ll  =  (l3  @  [l]  @  l4)
10.  l1  :  T  List
11.  l2  :  T  List
12.  l  =  (l1  @  [x]  @  l2)
\mvdash{}  \mexists{}ll1,ll2:T  List  List
      \mexists{}l1@0,l2@0:T  List
        (((concat(l3)  @  (l1  @  [x]  @  l2)  @  concat(l4))
        =  (concat(ll1)  @  (l1@0  @  [x]  @  l2@0)  @  concat(ll2)))
        \mwedge{}  ((l3  @  [l1  @  [x]  @  l2]  @  l4)  =  (ll1  @  [l1@0  @  [x]  @  l2@0]  @  ll2)))


By

---

Latex:
TACTIC:((InstConcl  [\mkleeneopen{}l3\mkleeneclose{};  \mkleeneopen{}l4\mkleeneclose{};  \mkleeneopen{}l1\mkleeneclose{};  \mkleeneopen{}l2\mkleeneclose{}])\mcdot{}  THEN  Auto)

---

Home Index