Nuprl Lemma : sqeq-copath5
∀[n,m:Top]. ((m + 1) - n - 1 ~ m - n - 1 - 1)
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
top: Top,
subtract: n - m,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
not: ¬A,
is-exception: is-exception(t),
false: False,
implies: P ⇒ Q,
prop: ℙ,
top: Top,
subtype_rel: A ⊆r B,
uiff: uiff(P;Q),
uimplies: b supposing a,
and: P ∧ Q,
has-value: (a)↓,
subtract: n - m,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
exception-not-bottom,
bottom_diverge,
exception-not-value_1,
int_subtype_base,
sqle_wf_base,
minus-minus,
minus-add,
zero-add,
add-commutes,
minus-one-mul-top,
add-swap,
minus-one-mul,
base_wf,
add-associates,
add-is-int-iff,
minus-is-int-iff,
int-value-type,
value-type-has-value,
top_wf,
is-exception_wf,
has-value_wf_base
Rules used in proof :
exceptionAdd,
minusExceptionCases,
sqleRule,
independent_functionElimination,
exceptionSqequal,
axiomSqleEquality,
addExceptionCases,
applyLambdaEquality,
hyp_replacement,
sqleReflexivity,
natural_numberEquality,
minusEquality,
voidEquality,
voidElimination,
lambdaEquality,
applyEquality,
addEquality,
callbyvalueMinus,
equalitySymmetry,
equalityTransitivity,
independent_isectElimination,
intEquality,
productElimination,
callbyvalueAdd,
because_Cache,
isect_memberEquality,
sqequalAxiom,
hypothesis,
hypothesisEquality,
baseClosed,
closedConclusion,
baseApply,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
divergentSqle,
sqequalSqle,
thin,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[n,m:Top]. ((m + 1) - n - 1 \msim{} m - n - 1 - 1)
Date html generated:
2016_12_12-AM-09_16_29
Last ObjectModification:
2016_12_11-PM-05_22_46
Theory : co-recursion
Home
Index