`∀[x:Base]. x + 0 ~ 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` top: `Top` implies: `P `` Q` false: `False` prop: `ℙ`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalSqle divergentSqle callbyvalueAdd sqequalHypSubstitution hypothesis sqequalRule baseApply closedConclusion baseClosed hypothesisEquality thin productElimination lemma_by_obid isectElimination equalityTransitivity equalitySymmetry isect_memberEquality voidElimination voidEquality addExceptionCases axiomSqleEquality independent_isectElimination intEquality natural_numberEquality independent_functionElimination exceptionSqequal sqleReflexivity because_Cache sqequalAxiom functionEquality

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

Date html generated: 2016_05_13-PM-03_29_01
Last ObjectModification: 2016_01_14-PM-06_41_48

Theory : arithmetic

Home Index