Nuprl Definition : word-rel

This is the relation that says that word w2 is obtained from word w1 by 
deleting and adjacent pair of letters  x,y that are inverses.
This implies that the length of w2 is strictly less than the length of w1,
so it is well-founded relation.

In Error :word-rel-diamond we prove that is has the diamond property,
so its transitive closure is confluent, and we can get an equivalence
relation ⌜word-equiv(X;w1;w2)⌝.⋅

word-rel(X;w1;w2) ==
  ∃x,y:X X. ∃a,b:(X X) List. (x -y ∧ (w1 (a [x; y] b) ∈ ((X X) List)) ∧ (w2 (a b) ∈ ((X X) List)))

Definitions occuring in Statement :  inverse-letters: -b append: as bs cons: [a b] nil: [] list: List exists: x:A. B[x] and: P ∧ Q union: left right equal: t ∈ T
Definitions occuring in definition :  exists: x:A. B[x] inverse-letters: -b and: P ∧ Q cons: [a b] nil: [] equal: t ∈ T list: List union: left right append: as bs
FDL editor aliases :  word-rel

word-rel(X;w1;w2)  ==
    \mexists{}x,y:X  +  X.  \mexists{}a,b:(X  +  X)  List.  (x  =  -y  \mwedge{}  (w1  =  (a  @  [x;  y]  @  b))  \mwedge{}  (w2  =  (a  @  b)))

Date html generated: 2020_05_20-AM-08_21_45
Last ObjectModification: 2019_08_16-PM-03_39_18

Theory : free!groups

Home Index