### Nuprl Lemma : confluent-equiv-is-equiv

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (Refl(T;x,y.R[x;y])`
`  `` Trans(T;x,y.R[x;y])`
`  `` rel-confluent(T;x,y.R[x;y])`
`  `` 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-confluent: `rel-confluent(T;x,y.R[x; y])` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` 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` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` confluent-equiv: `confluent-equiv(T;x,y.R[x; y])` exists: `∃x:A. B[x]` member: `t ∈ T` cand: `A c∧ B` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` guard: `{T}` rel-confluent: `rel-confluent(T;x,y.R[x; y])`
Lemmas referenced :  subtype_rel_self rel-confluent_wf trans_wf refl_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt independent_pairFormation sqequalRule dependent_pairFormation_alt hypothesisEquality cut hypothesis productIsType universeIsType applyEquality thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination because_Cache productElimination lambdaEquality_alt inhabitedIsType functionIsType universeEquality dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(Refl(T;x,y.R[x;y])
{}\mRightarrow{}  Trans(T;x,y.R[x;y])
{}\mRightarrow{}  rel-confluent(T;x,y.R[x;y])
{}\mRightarrow{}  EquivRel(T;a,b.confluent-equiv(T;x,y.R[x;y])  a  b))

Date html generated: 2019_10_15-AM-10_24_48
Last ObjectModification: 2019_08_16-PM-03_12_27

Theory : relations2

Home Index