Nuprl Definition : word-equiv
word-equiv(X;w1;w2) == ∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w))
Definitions occuring in Statement :
word-rel: word-rel(X;w1;w2),
transitive-reflexive-closure: R^*,
list: T List,
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
union: left + right
Definitions occuring in definition :
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
transitive-reflexive-closure: R^*,
list: T List,
union: left + right,
lambda: λx.A[x],
word-rel: word-rel(X;w1;w2)
FDL editor aliases :
word-equiv
Latex:
word-equiv(X;w1;w2) == \mexists{}w:(X + X) List. ((\mlambda{}x,y. word-rel(X;x;y)\^{}* w1 w) \mwedge{} (\mlambda{}x,y. word-rel(X;x;y)\^{}* \000Cw2 w))
Date html generated:
2020_05_20-AM-08_22_05
Last ObjectModification:
2017_01_14-PM-05_10_39
Theory : free!groups
Home
Index