`∀[x:Base]. 0 + x ~ x supposing (x)↓ `` (x ∈ ℤ)`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` add: `n + m` natural_number: `\$n` int: `ℤ` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` and: `P ∧ Q` implies: `P `` 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