Nuprl Lemma : implies-bar-equal
∀[T:Type]. ∀x,y:bar-base(T). (((∃a:T. (x↓a ∧ y↓a)) ∨ (x↑ ∧ y↑)) ⇒ bar-equal(T;x;y))
Proof
Definitions occuring in Statement :
bar-equal: bar-equal(T;x;y),
bar-diverges: x↑,
bar-converges: x↓a,
bar-base: bar-base(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
member: t ∈ T,
and: P ∧ Q,
exists: ∃x:A. B[x],
or: P ∨ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
bar-equal: bar-equal(T;x;y),
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
false: False,
not: ¬A
Lemmas referenced :
bar-base_wf,
bar-diverges_wf,
bar-converges_wf,
exists_wf,
or_wf,
bar-converges-unique,
squash_wf,
true_wf,
istype-universe,
subtype_rel_self,
iff_weakening_equal,
bar-converges-not-diverges
Rules used in proof :
universeEquality,
hypothesis,
productEquality,
lambdaEquality,
sqequalRule,
hypothesisEquality,
cumulativity,
isectElimination,
extract_by_obid,
introduction,
cut,
productElimination,
thin,
unionElimination,
sqequalHypSubstitution,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
independent_pairFormation,
independent_functionElimination,
applyEquality,
Error :lambdaEquality_alt,
imageElimination,
equalityTransitivity,
equalitySymmetry,
Error :universeIsType,
natural_numberEquality,
imageMemberEquality,
baseClosed,
instantiate,
independent_isectElimination,
voidElimination,
because_Cache
Latex:
\mforall{}[T:Type]. \mforall{}x,y:bar-base(T). (((\mexists{}a:T. (x\mdownarrow{}a \mwedge{} y\mdownarrow{}a)) \mvee{} (x\muparrow{} \mwedge{} y\muparrow{})) {}\mRightarrow{} bar-equal(T;x;y))
Date html generated:
2019_06_20-PM-00_37_06
Last ObjectModification:
2018_10_11-PM-04_08_48
Theory : co-recursion
Home
Index