`∀[a,b:ℤ].  (((a -- b) + b) = imax(a;b) ∈ ℤ)`

Proof

Definitions occuring in Statement :  ndiff: `a -- b` imax: `imax(a;b)` uall: `∀[x:A]. B[x]` add: `n + m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ndiff: `a -- b` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` subtract: `n - m` top: `Top`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis intEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality because_Cache applyEquality lambdaEquality imageElimination extract_by_obid equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination voidElimination voidEquality minusEquality

Latex:
\mforall{}[a,b:\mBbbZ{}].    (((a  --  b)  +  b)  =  imax(a;b))

Date html generated: 2017_04_14-AM-09_15_03
Last ObjectModification: 2017_02_27-PM-03_52_43

Theory : int_2

Home Index