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 a well-founded relation.

In 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: a = -b, append: as @ bs, cons: [a / b], nil: [], list: T List, exists: ∃x:A. B[x], and: P ∧ Q, union: left + right, equal: s = t ∈ T
Definitions occuring in definition : exists: ∃x:A. B[x], inverse-letters: a = -b, and: P ∧ Q, cons: [a / b], nil: [], equal: s = t ∈ T, list: T List, union: left + right, append: as @ bs
FDL editor aliases : word-rel

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