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:
2019_10_31-AM-07_23_21
Last ObjectModification:
2019_08_16-PM-03_31_50
Theory : free!groups
Home
Index