---

Step * of Lemma decidable__exists_iseg

No Annotations
∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ((∀L:T List. Dec(P[L])) ⇒ (∀L:T List. Dec(∃L':T List. (L' ≤ L ∧ P[L']))))
BY
{ (Auto THEN MoveToConcl (-1) THEN InductionOnLast) }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
⊢ Dec(∃L':T List. (L' ≤ [] ∧ P[L']))

2
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. L : T List
5. ¬↑null(L)
6. ||L|| ≥ 1 
7. Dec(∃L':T List. (L' ≤ firstn(||L|| - 1;L) ∧ P[L']))
⊢ Dec(∃L':T List. (L' ≤ firstn(||L|| - 1;L) @ [last(L)] ∧ P[L']))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}L:T  List.  Dec(P[L]))  {}\mRightarrow{}  (\mforall{}L:T  List.  Dec(\mexists{}L':T  List.  (L'  \mleq{}  L  \mwedge{}  P[L']))))


By

---

Latex:
(Auto  THEN  MoveToConcl  (-1)  THEN  InductionOnLast)

---

Home Index