---

Step * 2 of Lemma split-at-first


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. u : T
5. v : T List
6. ∃X,Y:T List. ((v = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )
⊢ ∃X,Y:T List. (([u / v] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )
BY
{ xxx(ExRepD THEN (Decide P[u] THENA Auto))xxx }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. u : T
5. v : T List
6. X : T List
7. Y : T List
8. v = (X @ Y) ∈ (T List)
9. (∀x∈X.¬P[x])
10. P[hd(Y)] supposing ||Y|| ≥ 1 
11. P[u]
⊢ ∃X,Y:T List. (([u / v] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )

2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. u : T
5. v : T List
6. X : T List
7. Y : T List
8. v = (X @ Y) ∈ (T List)
9. (∀x∈X.¬P[x])
10. P[hd(Y)] supposing ||Y|| ≥ 1 
11. ¬P[u]
⊢ ∃X,Y:T List. (([u / v] = (X @ Y) ∈ (T List)) ∧ (∀x∈X.¬P[x]) ∧ P[hd(Y)] supposing ||Y|| ≥ 1 )

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  u  :  T
5.  v  :  T  List
6.  \mexists{}X,Y:T  List.  ((v  =  (X  @  Y))  \mwedge{}  (\mforall{}x\mmember{}X.\mneg{}P[x])  \mwedge{}  P[hd(Y)]  supposing  ||Y||  \mgeq{}  1  )
\mvdash{}  \mexists{}X,Y:T  List.  (([u  /  v]  =  (X  @  Y))  \mwedge{}  (\mforall{}x\mmember{}X.\mneg{}P[x])  \mwedge{}  P[hd(Y)]  supposing  ||Y||  \mgeq{}  1  )


By

---

Latex:
xxx(ExRepD  THEN  (Decide  P[u]  THENA  Auto))xxx

---

Home Index