### Nuprl Lemma : word-rel-confluent

`∀[X:Type]`
`  ∀b,w1,w:(X + X) List.`
`    ((λx,y. word-rel(X;x;y)^* b w1)`
`    `` (λx,y. word-rel(X;x;y)^* b w)`
`    `` (∃z:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 z) ∧ (λx,y. word-rel(X;x;y)^* w z))))`

Proof

Definitions occuring in Statement :  word-rel: `word-rel(X;w1;w2)` transitive-reflexive-closure: `R^*` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  rel-confluent: `rel-confluent(T;x,y.R[x; y])` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` rel-diamond-property: `rel-diamond-property(T;x,y.R[x; y])` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a`
Lemmas referenced :  diamond-implies-TC-confluent list_wf word-rel_wf istype-universe word-rel-diamond length_wf_nat istype-less_than istype-nat word-rel-length
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin unionEquality hypothesisEquality hypothesis lambdaEquality_alt inhabitedIsType universeIsType independent_functionElimination instantiate universeEquality dependent_pairFormation_alt lambdaFormation_alt functionIsType because_Cache applyEquality setElimination rename independent_isectElimination

Latex:
\mforall{}[X:Type]
\mforall{}b,w1,w:(X  +  X)  List.
((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w1)
{}\mRightarrow{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w)
{}\mRightarrow{}  (\mexists{}z:(X  +  X)  List.  ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  z)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w  z))))

Date html generated: 2020_05_20-AM-08_22_03
Last ObjectModification: 2019_08_16-PM-03_31_50

Theory : free!groups

Home Index