Nuprl Lemma : general_arith_equation2

[b:ℤ]. ∀[a,c:Top].  ((a c) c)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top subtract: m add: m int: sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtract: m top: Top
Lemmas referenced :  add-associates istype-void add-commutes istype-top istype-int add-inverse2 zero-add-sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin Error :isect_memberEquality_alt,  voidElimination hypothesis hypothesisEquality because_Cache axiomSqEquality Error :inhabitedIsType,  Error :isectIsTypeImplies

Latex:
\mforall{}[b:\mBbbZ{}].  \mforall{}[a,c:Top].    ((a  -  b  -  c)  +  b  \msim{}  a  -  c)



Date html generated: 2019_06_20-AM-11_26_21
Last ObjectModification: 2019_03_06-PM-10_44_18

Theory : arithmetic


Home Index