---

Step * 1 of Lemma star-append-iff


1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. [Q] : (T List) ⟶ ℙ
4. L : T List
5. LL : T List List
6. L' : T List
7. (∀X∈LL.P X)
8. Q L'
9. L = (concat(LL) @ L') ∈ (T List)
⊢ (Q L)
∨ (∃L1,L2:T List
    ((L = (L1 @ L2) ∈ (T List))
    ∧ (P L1)
    ∧ (∃LL:T List List. ∃L':T List. ((∀X∈LL.P X) ∧ (Q L') ∧ (L2 = (concat(LL) @ L') ∈ (T List))))))
BY
{ (((DVar `LL' THEN All Reduce)
    THENL [(OrLeft THENM (HypSubst (-1) 0)); (OrRight THENM (InstConcl [⌜u⌝; ⌜concat(v) @ L'⌝])⋅)]
   )
   THEN (Auto
         THEN OnMaybeHyp 10 (\h. ((Unfold `concat` h)
                                  THEN (Reduce h)
                                  THEN (Fold `concat` h)
                                  THEN (RWO "append_assoc" h)
                                  THEN Auto)⋅)
         )
   THEN OnMaybeHyp 8 (\h. ((RWO "l_all_cons" h) THEN Auto THEN (InstConcl [⌜v⌝; ⌜L'⌝])⋅ THEN Auto)⋅)⋅) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  L  :  T  List
5.  LL  :  T  List  List
6.  L'  :  T  List
7.  (\mforall{}X\mmember{}LL.P  X)
8.  Q  L'
9.  L  =  (concat(LL)  @  L')
\mvdash{}  (Q  L)
\mvee{}  (\mexists{}L1,L2:T  List
        ((L  =  (L1  @  L2))
        \mwedge{}  (P  L1)
        \mwedge{}  (\mexists{}LL:T  List  List.  \mexists{}L':T  List.  ((\mforall{}X\mmember{}LL.P  X)  \mwedge{}  (Q  L')  \mwedge{}  (L2  =  (concat(LL)  @  L'))))))


By

---

Latex:
(((DVar  `LL'  THEN  All  Reduce)
    THENL  [(OrLeft  THENM  (HypSubst  (-1)  0));  (OrRight  THENM  (InstConcl  [\mkleeneopen{}u\mkleeneclose{};  \mkleeneopen{}concat(v)  @  L'\mkleeneclose{}])\mcdot{})]
  )
  THEN  (Auto
              THEN  OnMaybeHyp  10  (\mbackslash{}h.  ((Unfold  `concat`  h)
                                                                THEN  (Reduce  h)
                                                                THEN  (Fold  `concat`  h)
                                                                THEN  (RWO  "append\_assoc"  h)
                                                                THEN  Auto)\mcdot{})
              )
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  ((RWO  "l\_all\_cons"  h)  THEN  Auto  THEN  (InstConcl  [\mkleeneopen{}v\mkleeneclose{};  \mkleeneopen{}L'\mkleeneclose{}])\mcdot{}  THEN  Auto)\mcdot{})\mcdot{})

---

Home Index