Nuprl Lemma : rleq2_functionality
∀x1,y1,x2,y2:ℕ+ ⟶ ℤ. (bdd-diff(x1;x2) ⇒ bdd-diff(y1;y2) ⇒ (rleq2(x1;y1) ⇐⇒ rleq2(x2;y2)))
Proof
Definitions occuring in Statement :
rleq2: rleq2(x;y),
bdd-diff: bdd-diff(f;g),
nat_plus: ℕ+,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
function: x:A ⟶ B[x],
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
guard: {T},
rminus: -(x),
reg-seq-add: reg-seq-add(x;y)
Lemmas referenced :
rleq2_wf,
bdd-diff_wf,
nat_plus_wf,
rleq2-iff-rnonneg2,
rnonneg2_functionality,
reg-seq-add_functionality_wrt_bdd-diff,
rminus_functionality_wrt_bdd-diff,
bdd-diff_inversion
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
functionEquality,
intEquality,
independent_pairFormation,
dependent_functionElimination,
independent_functionElimination,
productElimination,
sqequalRule,
lambdaEquality,
addEquality,
applyEquality,
minusEquality
Latex:
\mforall{}x1,y1,x2,y2:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}. (bdd-diff(x1;x2) {}\mRightarrow{} bdd-diff(y1;y2) {}\mRightarrow{} (rleq2(x1;y1) \mLeftarrow{}{}\mRightarrow{} rleq2(x2;y2)))
Date html generated:
2016_05_18-AM-07_15_22
Last ObjectModification:
2015_12_28-AM-00_42_47
Theory : reals
Home
Index