### Nuprl Lemma : not-bl-exists-eq-bl-all

[L,P:Top].  b(∃x∈L.P[x])_b (∀x∈L.¬bP[x])_b)

Proof

Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b bl-all: (∀x∈L.P[x])_b bnot: ¬bb uall: [x:A]. B[x] top: Top so_apply: x[s] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bl-all: (∀x∈L.P[x])_b bl-exists: (∃x∈L.P[x])_b reduce: reduce(f;k;as) list_ind: list_ind nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A all: x:A. B[x] top: Top and: P ∧ Q prop: bnot: ¬bb ifthenelse: if then else fi  so_lambda: λ2x.t[x] so_apply: x[s] decidable: Dec(P) or: P ∨ Q nat_plus: + subtype_rel: A ⊆B has-value: (a)↓ sq_type: SQType(T) guard: {T} uiff: uiff(P;Q) btrue: tt bor: p ∨bq bfalse: ff band: p ∧b q
Lemmas referenced :  has-value-band-type bottom_diverge has-value-implies-dec-isaxiom-2 assert_of_bnot eqff_to_assert eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases isl_wf injection-eta has-value-bor-type has-value-implies-dec-ispair-2 union-value-type value-type-has-value top_wf is-exception_wf has-value_wf_base int_subtype_base has-value-bnot-type fun_exp_unroll_1 int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le bottom-sqle strictness-decide strictness-apply fun_exp0_lemma base_wf less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin sqequalSqle fixpointLeast lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll independent_functionElimination axiomSqleEquality unionElimination dependent_set_memberEquality divergentSqle baseApply closedConclusion baseClosed applyEquality because_Cache equalityTransitivity equalitySymmetry decideExceptionCases callbyvalueCallbyvalue callbyvalueReduce callbyvalueExceptionCases exceptionSqequal sqleReflexivity sqequalAxiom unionEquality instantiate cumulativity productElimination

Latex:
\mforall{}[L,P:Top].    (\mneg{}\msubb{}(\mexists{}x\mmember{}L.P[x])\_b  \msim{}  (\mforall{}x\mmember{}L.\mneg{}\msubb{}P[x])\_b)

Date html generated: 2016_05_14-PM-02_11_22
Last ObjectModification: 2016_01_15-AM-08_03_46

Theory : list_1

Home Index