Nuprl Lemma : TC-equiv-is-equiv
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(rel-diamond-property(T;x,y.R x y)
⇒ (∃m:T ⟶ ℕ. ∀x,y:T. ((R x y) ⇒ m y < m x))
⇒ EquivRel(T;a,b.confluent-equiv(T;x,y.R^* x y) a b))
Proof
Definitions occuring in Statement :
confluent-equiv: confluent-equiv(T;x,y.R[x; y]),
rel-diamond-property: rel-diamond-property(T;x,y.R[x; y]),
transitive-reflexive-closure: R^*,
equiv_rel: EquivRel(T;x,y.E[x; y]),
nat: ℕ,
less_than: a < b,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
nat: ℕ,
refl: Refl(T;x,y.E[x; y]),
transitive-reflexive-closure: R^*,
or: P ∨ Q,
trans: Trans(T;x,y.E[x; y]),
infix_ap: x f y
Lemmas referenced :
confluent-equiv-is-equiv,
transitive-reflexive-closure_wf,
istype-nat,
subtype_rel_self,
istype-less_than,
rel-diamond-property_wf,
istype-universe,
transitive-closure_wf,
transitive-reflexive-closure_transitivity,
diamond-implies-TC-confluent,
eta_conv,
rel-confluent_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality_alt,
applyEquality,
hypothesis,
inhabitedIsType,
universeIsType,
independent_functionElimination,
productIsType,
functionIsType,
because_Cache,
instantiate,
universeEquality,
setElimination,
rename,
inlFormation_alt,
dependent_functionElimination,
functionExtensionality_alt,
cumulativity,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality
Latex:
\mforall{}[T:Type]. \mforall{}[R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
(rel-diamond-property(T;x,y.R x y)
{}\mRightarrow{} (\mexists{}m:T {}\mrightarrow{} \mBbbN{}. \mforall{}x,y:T. ((R x y) {}\mRightarrow{} m y < m x))
{}\mRightarrow{} EquivRel(T;a,b.confluent-equiv(T;x,y.R\^{}* x y) a b))
Date html generated:
2019_10_15-AM-10_24_51
Last ObjectModification:
2019_08_16-PM-03_32_51
Theory : relations2
Home
Index