### Nuprl Lemma : decidable__exists_length_bool

`∀[P:(𝔹 List) ⟶ ℙ]. ((∀L:𝔹 List. Dec(P[L])) `` (∀n:ℕ. Dec(∃L:𝔹 List. ((||L|| = n ∈ ℤ) ∧ P[L]))))`

Proof

Definitions occuring in Statement :  length: `||as||` list: `T List` nat: `ℕ` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` exists: `∃x:A. B[x]` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  decidable__exists_length bool_wf false_wf le_wf equipollent-two equipollent_wf int_seg_wf all_wf list_wf decidable_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis isect_memberFormation hypothesisEquality lambdaFormation independent_functionElimination dependent_pairFormation dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation setElimination rename lambdaEquality applyEquality functionEquality cumulativity universeEquality

Latex:
\mforall{}[P:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}L:\mBbbB{}  List.  Dec(P[L]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(\mexists{}L:\mBbbB{}  List.  ((||L||  =  n)  \mwedge{}  P[L]))))

Date html generated: 2016_05_14-PM-04_06_51
Last ObjectModification: 2015_12_26-PM-07_41_41

Theory : equipollence!!cardinality!

Home Index