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