### Nuprl Lemma : full-omega-unsat

`∀[fmla:int_formula()]. ¬satisfiable_int_formula(fmla) supposing inr Ax  ≤ full-omega(fmla)`

Proof

Definitions occuring in Statement :  full-omega: `full-omega(fmla)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` int_formula: `int_formula()` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` inr: `inr x ` sqle: `s ≤ t` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` bool: `𝔹` isl: `isl(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff`
Lemmas referenced :  satisfiable-full-omega-tt satisfiable_int_formula_wf sqle_wf_base int_formula-subtype-base int_formula_wf full-omega_wf set_wf bool_wf equal-wf-T-base not_wf equal_wf true_wf unit_subtype_base false_wf has-value_wf_base is-exception_wf not-bfalse-sqle-btrue
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality independent_isectElimination hypothesis because_Cache independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination baseClosed baseApply closedConclusion applyEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality setElimination rename unionElimination divergentSqle sqleRule sqleReflexivity

Latex:
\mforall{}[fmla:int\_formula()].  \mneg{}satisfiable\_int\_formula(fmla)  supposing  inr  Ax    \mleq{}  full-omega(fmla)

Date html generated: 2017_09_29-PM-05_56_26
Last ObjectModification: 2017_06_01-AM-10_01_56

Theory : omega

Home Index