---

Step * 2 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)
⊢ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l))
BY
{ TACTIC:((((((((HypSubst (-1) 0) THENA Auto) THEN (InstConcl [⌜l1 @ [x] @ l2⌝])⋅) THENA Auto)
             THEN RWW "member_append" 0
             )
            THENA Auto
            )
           THEN RWW "cons_member" 0
           )
          THENA Auto
          ) }

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

---

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{}  \mexists{}l:T  List.  ((l  \mmember{}  ll)  \mwedge{}  (x  \mmember{}  l))


By

---

Latex:
TACTIC:((((((((HypSubst  (-1)  0)  THENA  Auto)  THEN  (InstConcl  [\mkleeneopen{}l1  @  [x]  @  l2\mkleeneclose{}])\mcdot{})  THENA  Auto)
                      THEN  RWW  "member\_append"  0
                      )
                    THENA  Auto
                    )
                  THEN  RWW  "cons\_member"  0
                  )
                THENA  Auto
                )

---

Home Index