---

Step * 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)
⊢ ∃ll1,ll2:T List List
   ∃l1,l2:T List
    ((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List))
    ∧ (ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List)))
BY
{ TACTIC:((((((((((((((((FLemma `l_member_decomp` [(-2)]) THENA Auto) THEN (FLemma `l_member_decomp` [(-2)]))
                      THENA Auto
                      )
                     THEN ExRepD
                     THEN WeakSubstFor ⌜ll⌝ 0⋅)
                    THENA Auto
                    )
                   THEN WeakSubstFor ⌜l⌝ 0⋅
                   )
                  THENA Auto
                  )
                 THEN RWW "concat_append" 0
                 )
                THENA Auto
                )
               THEN RWW "concat-cons" 0
               )
              THENA Auto
              )
             THEN RWW "concat-nil" 0
             )
            THENA Auto
            )
           THEN RWW "append_nil_sq" 0
           )
          THENA Auto
          ) }

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

---

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)
\mvdash{}  \mexists{}ll1,ll2:T  List  List
      \mexists{}l1,l2:T  List
        ((concat(ll)  =  (concat(ll1)  @  (l1  @  [x]  @  l2)  @  concat(ll2)))
        \mwedge{}  (ll  =  (ll1  @  [l1  @  [x]  @  l2]  @  ll2)))


By

---

Latex:
TACTIC:((((((((((((((((FLemma  `l\_member\_decomp`  [(-2)])  THENA  Auto)
                                          THEN  (FLemma  `l\_member\_decomp`  [(-2)])
                                          )
                                        THENA  Auto
                                        )
                                      THEN  ExRepD
                                      THEN  WeakSubstFor  \mkleeneopen{}ll\mkleeneclose{}  0\mcdot{})
                                    THENA  Auto
                                    )
                                  THEN  WeakSubstFor  \mkleeneopen{}l\mkleeneclose{}  0\mcdot{}
                                  )
                                THENA  Auto
                                )
                              THEN  RWW  "concat\_append"  0
                              )
                            THENA  Auto
                            )
                          THEN  RWW  "concat-cons"  0
                          )
                        THENA  Auto
                        )
                      THEN  RWW  "concat-nil"  0
                      )
                    THENA  Auto
                    )
                  THEN  RWW  "append\_nil\_sq"  0
                  )
                THENA  Auto
                )

---

Home Index