Nuprl Lemma : general_arith_equation2
∀[b:ℤ]. ∀[a,c:Top].  ((a - b - c) + b ~ a - c)
Proof
Definitions occuring in Statement : 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
subtract: n - m
, 
add: n + m
, 
int: ℤ
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
subtract: n - 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