---

Step * of Lemma star-append-iff

∀[T:Type]. ∀[P,Q:(T List) ⟶ ℙ].
  ∀L:T List
    (star-append(T;P;Q) L ⇐⇒ (Q L) ∨ (∃L1,L2:T List. ((L = (L1 @ L2) ∈ (T List)) ∧ (P L1) ∧ (star-append(T;P;Q) L2))))
BY
{ xxx(Unfold `star-append` 0 THEN Reduce 0 THEN Auto THEN ExRepD)xxx }

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

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P,Q:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L:T  List
        (star-append(T;P;Q)  L
        \mLeftarrow{}{}\mRightarrow{}  (Q  L)  \mvee{}  (\mexists{}L1,L2:T  List.  ((L  =  (L1  @  L2))  \mwedge{}  (P  L1)  \mwedge{}  (star-append(T;P;Q)  L2))))


By

---

Latex:
xxx(Unfold  `star-append`  0  THEN  Reduce  0  THEN  Auto  THEN  ExRepD)xxx

---

Home Index