---

Step * 2 of Lemma star-append-iff


1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. [Q] : (T List) ⟶ ℙ
4. L : T List
5. (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))))))
⊢ ∃LL:T List List. ∃L':T List. ((∀X∈LL.P X) ∧ (Q L') ∧ (L = (concat(LL) @ L') ∈ (T List)))
BY
{ ((D (-1))
   THENL [((InstConcl [⌜[]⌝; ⌜L⌝])⋅ THEN Reduce 0 THEN Auto THEN Try ((BLemma `l_all_nil` THEN Auto)))
         ; (ExRepD THEN (InstConcl [⌜[L1 / LL]⌝; ⌜L'⌝])⋅ THEN Auto)]
) }

1
1. T : Type
2. P : (T List) ⟶ ℙ
3. Q : (T List) ⟶ ℙ
4. L : T List
5. L1 : T List
6. L2 : T List
7. L = (L1 @ L2) ∈ (T List)
8. P L1
9. LL : T List List
10. L' : T List
11. (∀X∈LL.P X)
12. Q L'
13. L2 = (concat(LL) @ L') ∈ (T List)
14. (∀X∈[L1 / LL].P X)
15. Q L'
⊢ L = (concat([L1 / LL]) @ L') ∈ (T List)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  L  :  T  List
5.  (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'))))))
\mvdash{}  \mexists{}LL:T  List  List.  \mexists{}L':T  List.  ((\mforall{}X\mmember{}LL.P  X)  \mwedge{}  (Q  L')  \mwedge{}  (L  =  (concat(LL)  @  L')))


By

---

Latex:
((D  (-1))
  THENL  [((InstConcl  [\mkleeneopen{}[]\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{}  THEN  Reduce  0  THEN  Auto  THEN  Try  ((BLemma  `l\_all\_nil`  THEN  Auto)))
              ;  (ExRepD  THEN  (InstConcl  [\mkleeneopen{}[L1  /  LL]\mkleeneclose{};  \mkleeneopen{}L'\mkleeneclose{}])\mcdot{}  THEN  Auto)]
)

---

Home Index