Nuprl Lemma : cbv-sqequal0

[a:Base]. eval in supposing (a)↓


Proof




Definitions occuring in Statement :  has-value: (a)↓ callbyvalue: callbyvalue uimplies: supposing a uall: [x:A]. B[x] natural_number: $n base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ implies:  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