### Nuprl Lemma : cbv-sqequal0

`∀[a:Base]. eval x = a in 0 ~ 0 supposing (a)↓`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` callbyvalue: callbyvalue uimplies: `b supposing a` uall: `∀[x:A]. B[x]` natural_number: `\$n` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  base_wf exception-not-value is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle callbyvalueCallbyvalue sqequalHypSubstitution hypothesis sqequalRule callbyvalueReduce sqleReflexivity lemma_by_obid isectElimination thin baseClosed callbyvalueExceptionCases axiomSqleEquality hypothesisEquality independent_isectElimination independent_functionElimination voidElimination baseApply closedConclusion sqequalAxiom isect_memberEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a:Base].  eval  x  =  a  in  0  \msim{}  0  supposing  (a)\mdownarrow{}

Date html generated: 2016_05_13-PM-03_28_41
Last ObjectModification: 2016_01_14-PM-06_41_58

Theory : arithmetic

Home Index