Step
*
2
1
of Lemma
decidable__exists_iseg
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. ∃L':T List. (L' ≤ firstn(||L|| - 1;L) ∧ P[L'])
⊢ Dec(∃L':T List. (L' ≤ firstn(||L|| - 1;L) @ [last(L)] ∧ P[L']))
BY
{ ((OrLeft THEN Auto) THEN ParallelLast THEN Auto) }
1
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. L' : T List
8. L' ≤ firstn(||L|| - 1;L)
9. P[L']
⊢ L' ≤ firstn(||L|| - 1;L) @ [last(L)]
Latex:
Latex:
1. [T] : Type
2. [P] : (T List) {}\mrightarrow{} \mBbbP{}
3. \mforall{}L:T List. Dec(P[L])
4. L : T List
5. \mneg{}\muparrow{}null(L)
6. ||L|| \mgeq{} 1
7. \mexists{}L':T List. (L' \mleq{} firstn(||L|| - 1;L) \mwedge{} P[L'])
\mvdash{} Dec(\mexists{}L':T List. (L' \mleq{} firstn(||L|| - 1;L) @ [last(L)] \mwedge{} P[L']))
By
Latex:
((OrLeft THEN Auto) THEN ParallelLast THEN Auto)
Home
Index