### Nuprl Lemma : satisfiable-full-omega-tt

`∀[fmla:int_formula()]. ↑isl(full-omega(fmla)) supposing 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()` assert: `↑b` isl: `isl(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` assert: `↑b` ifthenelse: `if b then t else f fi ` isl: `isl(x)` true: `True` subtype_rel: `A ⊆r B` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` false: `False` not: `¬A`
Lemmas referenced :  full-omega_wf set_wf bool_wf equal-wf-T-base not_wf satisfiable_int_formula_wf eqtt_to_assert assert_witness isl_wf unit_wf2 btrue_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bfalse_wf int_formula_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality functionEquality baseClosed lambdaFormation setElimination rename unionElimination equalityElimination productElimination independent_isectElimination natural_numberEquality applyEquality independent_functionElimination dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry because_Cache voidElimination isect_memberEquality setEquality

Latex:
\mforall{}[fmla:int\_formula()].  \muparrow{}isl(full-omega(fmla))  supposing  satisfiable\_int\_formula(fmla)

Date html generated: 2017_09_29-PM-05_56_22
Last ObjectModification: 2017_07_26-PM-01_47_04

Theory : omega

Home Index