### Nuprl Lemma : full-omega_wf

`∀[fmla:int_formula()]. (full-omega(fmla) ∈ {b:𝔹| b = ff `` (¬satisfiable_int_formula(fmla))} )`

Proof

Definitions occuring in Statement :  full-omega: `full-omega(fmla)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` int_formula: `int_formula()` bfalse: `ff` bool: `𝔹` uall: `∀[x:A]. B[x]` not: `¬A` implies: `P `` Q` member: `t ∈ T` set: `{x:A| B[x]} ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` full-omega: `full-omega(fmla)` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` polynomial-constraints: `polynomial-constraints()` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iPolynomial: `iPolynomial()` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k` and: `P ∧ Q` squash: `↓T` guard: `{T}` iMonomial: `iMonomial()` subtype_rel: `A ⊆r B` istype: `istype(T)` prop: `ℙ` int_nzero: `ℤ-o` has-value: `(a)↓` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` tunion: `⋃x:A.B[x]` so_apply: `x[s1;s2]` bool: `𝔹` unit: `Unit` not: `¬A` l_exists: `(∃x∈L. P[x])` exists: `∃x:A. B[x]` top: `Top` bor: `p ∨bq` ifthenelse: `if b then t else f fi ` bfalse: `ff` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` cand: `A c∧ B` false: `False` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` true: `True` pi2: `snd(t)` int-constraint-problem: `IntConstraints` l_all: `(∀x∈L.P[x])` pi1: `fst(t)` nat: `ℕ` isr: `isr(x)`
Lemmas referenced :  satisfiable_int_formula_dnf int_formula_dnf_wf evalall-reduce list_wf polynomial-constraints_wf int_formula_wf list-valueall-type product-valueall-type iPolynomial_wf set-valueall-type iMonomial_wf all_wf int_seg_wf length_wf imonomial-less_wf select_wf sq_stable__le less_than_transitivity2 le_weakening2 int_nzero_wf sorted_wf istype-int nequal_wf int-valueall-type value-type-has-value list-value-type satisfiable_int_formula_wf l_exists_wf satisfiable_polynomial_constraints_wf l_member_wf eager-accum-list_accum bool_wf bfalse_wf bor_wf union-valueall-type unit_wf2 equal-valueall-type list_accum_wf list_induction equal-wf-T-base l_all_wf list_accum_nil_lemma istype-void l_all_nil list_accum_cons_lemma l_all_cons eqtt_to_assert btrue_neq_bfalse btrue_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal_wf squash_wf true_wf equal-wf-base-T testxxx_lemma pcs-to-integer-problem_wf omega_wf satisfiable-pcs-to-integer-problem sq_stable__all satisfiable-integer-problem_wf subtype_rel_list list_subtype_base int_subtype_base false_wf sq_stable_from_decidable decidable__false isr-omega not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination hypothesis Error :inhabitedIsType,  Error :lambdaFormation_alt,  sqequalRule independent_isectElimination Error :equalityIsType1,  equalityTransitivity equalitySymmetry independent_functionElimination axiomEquality Error :universeIsType,  Error :lambdaEquality_alt,  because_Cache natural_numberEquality setElimination rename productElimination imageMemberEquality baseClosed imageElimination setEquality intEquality callbyvalueReduce Error :productIsType,  Error :functionIsType,  Error :setIsType,  Error :dependent_set_memberEquality_alt,  Error :equalityIsType3,  functionEquality applyEquality Error :isect_memberEquality_alt,  voidElimination Error :equalityIsType4,  functionExtensionality unionElimination equalityElimination independent_pairFormation Error :dependent_pairFormation_alt,  promote_hyp instantiate cumulativity hyp_replacement universeEquality Error :equalityIsType2,  baseApply closedConclusion addEquality

Latex:
\mforall{}[fmla:int\_formula()].  (full-omega(fmla)  \mmember{}  \{b:\mBbbB{}|  b  =  ff  {}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla))\}  )

Date html generated: 2019_06_20-PM-00_51_40
Last ObjectModification: 2018_10_03-PM-03_00_23

Theory : omega

Home Index