### Nuprl Lemma : isaxiom-implies

`∀[t:Base]. (t ~ Ax) supposing ((↑isaxiom(t)) and (t)↓)`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` assert: `↑b` bfalse: `ff` btrue: `tt` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` isaxiom: `if z = Ax then a otherwise b` base: `Base` sqequal: `s ~ t` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` implies: `P `` Q` prop: `ℙ` bfalse: `ff` false: `False` top: `Top`
Lemmas referenced :  base_wf bfalse_wf top_wf btrue_wf is-exception_wf has-value_wf_base assert_wf false_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin isaxiomCases divergentSqle hypothesis because_Cache sqequalRule lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination sqequalAxiom isect_memberEquality hypothesisEquality voidElimination independent_functionElimination baseClosed voidEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[t:Base].  (t  \msim{}  Ax)  supposing  ((\muparrow{}isaxiom(t))  and  (t)\mdownarrow{})

Date html generated: 2016_05_13-PM-03_27_10
Last ObjectModification: 2016_01_14-PM-06_43_52

Theory : call!by!value_1

Home Index