Nuprl Lemma : trivial-int-eq-test
∀P:ℤ ⟶ ℙ
∀[x,y:ℤ].
(((P ((x - y) + y)) ⇒ (P x))
∧ ((P (y + (x - y))) ⇒ (P x))
∧ ((P ((x + y) - y)) ⇒ (P x))
∧ ((P (y - y - x)) ⇒ (P x)))
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
and: P ∧ Q,
cand: A c∧ B,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
subtract: n - m,
top: Top
Lemmas referenced :
subtract-add-cancel,
subtract_wf,
minus-one-mul,
add-swap,
add-mul-special,
zero-mul,
add-zero,
and_wf,
equal_wf,
add-subtract-cancel,
minus-add,
minus-minus,
add-associates,
add-commutes
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
sqequalHypSubstitution,
sqequalRule,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
functionExtensionality,
intEquality,
addEquality,
independent_pairFormation,
because_Cache,
isect_memberEquality,
voidElimination,
voidEquality,
dependent_set_memberEquality,
equalityTransitivity,
equalitySymmetry,
lambdaEquality,
setElimination,
rename,
productElimination,
setEquality,
hyp_replacement,
Error :applyLambdaEquality,
multiplyEquality,
natural_numberEquality,
functionEquality,
cumulativity,
universeEquality
Latex:
\mforall{}P:\mBbbZ{} {}\mrightarrow{} \mBbbP{}
\mforall{}[x,y:\mBbbZ{}].
(((P ((x - y) + y)) {}\mRightarrow{} (P x))
\mwedge{} ((P (y + (x - y))) {}\mRightarrow{} (P x))
\mwedge{} ((P ((x + y) - y)) {}\mRightarrow{} (P x))
\mwedge{} ((P (y - y - x)) {}\mRightarrow{} (P x)))
Date html generated:
2016_10_25-AM-10_43_58
Last ObjectModification:
2016_07_12-AM-06_54_19
Theory : general
Home
Index