Nuprl Lemma : l_exists_wf_nil

[P:Void ⟶ Void]. ((∃x∈[]. P[x]) ∈ ℙ)


Proof




Definitions occuring in Statement :  l_exists: (∃x∈L. P[x]) nil: [] uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] void: Void
Definitions unfolded in proof :  l_exists: (∃x∈L. P[x]) select: L[n] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] nil: [] it: so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} int_seg: {i..j-} false: False lelt: i ≤ j < k and: P ∧ Q implies:  Q subtype_rel: A ⊆B
Lemmas referenced :  less_than_irreflexivity less_than_transitivity1 void_wf int_seg_wf exists_wf base_wf stuck-spread length_of_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin baseClosed independent_isectElimination lambdaFormation isect_memberEquality voidElimination voidEquality isect_memberFormation introduction natural_numberEquality because_Cache lambdaEquality applyEquality functionExtensionality hypothesisEquality instantiate setElimination rename productElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry functionEquality

Latex:
\mforall{}[P:Void  {}\mrightarrow{}  Void].  ((\mexists{}x\mmember{}[].  P[x])  \mmember{}  \mBbbP{})



Date html generated: 2016_05_14-AM-06_39_40
Last ObjectModification: 2016_01_14-PM-08_21_01

Theory : list_0


Home Index