Nuprl Lemma : int_formulaco-ext

int_formulaco() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
if lbl =a "le" then left:int_term() × int_term()
if lbl =a "eq" then left:int_term() × int_term()

                             if lbl =a "and" then left:int_formulaco() × int_formulaco()

                             if lbl =a "or" then left:int_formulaco() × int_formulaco()

                             if lbl =a "implies" then left:int_formulaco() × int_formulaco()

                             if lbl =a "not" then int_formulaco()
                             else Void
                             fi

Proof

Definitions occuring in Statement : int_formulaco: int_formulaco(), int_term: int_term(), ifthenelse: if b then t else f fi , eq_atom: x =a y, ext-eq: A ≡ B, product: x:A × B[x], token: "$token", atom: Atom, void: Void
Definitions unfolded in proof : int_formulaco: int_formulaco(), uall: ∀[x:A]. B[x], so_lambda: λ₂x.t[x], member: t ∈ T, all: ∀x:A. B[x], implies: P ⇒ Q, bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, ifthenelse: if b then t else f fi , uiff: uiff(P;Q), and: P ∧ Q, uimplies: b supposing a, bfalse: ff, exists: ∃x:A. B[x], prop: ℙ, or: P ∨ Q, sq_type: SQType(T), guard: {T}, bnot: ¬_bb, assert: ↑b, false: False, so_apply: x[s], continuous-monotone: ContinuousMonotone(T.F[T]), type-monotone: Monotone(T.F[T]), subtype_rel: A ⊆r B, so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], strong-type-continuous: Continuous+(T.F[T]), type-continuous: Continuous(T.F[T])
Lemmas referenced : corec-ext, eq_atom_wf, bool_wf, eqtt_to_assert, assert_of_eq_atom, int_term_wf, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, neg_assert_of_eq_atom, subtype_rel_product, subtype_rel_self, subtype_rel_wf, strong-continuous-depproduct, continuous-constant, strong-continuous-product, continuous-id, subtype_rel_weakening, nat_wf
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, sqequalRule, lambdaEquality, productEquality, atomEquality, hypothesisEquality, tokenEquality, hypothesis, lambdaFormation, unionElimination, equalityElimination, productElimination, independent_isectElimination, because_Cache, equalityTransitivity, equalitySymmetry, dependent_pairFormation, promote_hyp, dependent_functionElimination, instantiate, cumulativity, independent_functionElimination, voidElimination, voidEquality, universeEquality, independent_pairFormation, isect_memberFormation, axiomEquality, isect_memberEquality, isectEquality, applyEquality, functionExtensionality, functionEquality

Latex:
int\_formulaco() \mequiv{} lbl:Atom \mtimes{} if lbl =a "less" then left:int\_term() \mtimes{} int\_term() if lbl =a "le" then left:int\_term() \mtimes{} int\_term() if lbl =a "eq" then left:int\_term() \mtimes{} int\_term() if lbl =a "and" then left:int\_formulaco() \mtimes{} int\_formulaco() if lbl =a "or" then left:int\_formulaco() \mtimes{} int\_formulaco() if lbl =a "implies" then left:int\_formulaco() \mtimes{} int\_formulaco() if lbl =a "not" then int\_formulaco() else Void fi Date html generated: 2017_04_14-AM-08_59_45 Last ObjectModification: 2017_02_27-PM-03_43_05 Theory : omega Home Index