Nuprl Lemma : zero-add-base

[x:Base]. supposing (x)↓  (x ∈ ℤ)


Proof




Definitions occuring in Statement :  has-value: (a)↓ uimplies: supposing a uall: [x:A]. B[x] implies:  Q member: t ∈ T add: m natural_number: $n int: base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ and: P ∧ Q implies:  Q false: False prop:
Lemmas referenced :  zero-add base_wf equal-wf-base is-exception_wf has-value_wf_base int-value-type value-type-has-value exception-not-value zero-add-sqle
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle callbyvalueAdd sqequalHypSubstitution hypothesis thin baseClosed sqequalRule baseApply closedConclusion hypothesisEquality productElimination lemma_by_obid isectElimination because_Cache addExceptionCases axiomSqleEquality exceptionSqequal sqleReflexivity independent_isectElimination intEquality independent_functionElimination voidElimination sqequalAxiom functionEquality isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[x:Base].  0  +  x  \msim{}  x  supposing  (x)\mdownarrow{}  {}\mRightarrow{}  (x  \mmember{}  \mBbbZ{})



Date html generated: 2016_05_13-PM-03_29_02
Last ObjectModification: 2016_01_14-PM-06_41_52

Theory : arithmetic


Home Index