### 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