#2 ⟨a, b | baababa=a

Quick links

  1. Properties
  2. Rewriting system
  3. Certificate

Properties

Rewriting system

Format:
Word to reduce:
Tips:
  • Lowercase letters stand for generators.
  • Spaces are ignored.
  • Numbers repeat the previous letter, e.g. b90.
Reduction strategy:
Path to normal form: 1
1
#RuleProof
1. dbbc [6]
2. dc3c [9]
3. abc [2]
4. bad [3]
5. caad [5]
6. dacac5 [11]
7. dadcac3 [10]
8. dad2a [7]
9. da2a2d4 [12]
10. (da)2a2d2 [8]
# ab:baababa=a bcd/a ab=c,ba=d custom:1
db=bc
dccc=c
ab=c
ba=d
ca=ad
dac=accccc
dadc=accc
dadd=a
daa=aadddd
dada=aadd

Certificate

[1] baababa=a

Axiom: baababa=a.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Defines rule #3.

Referenced by [4], [5], [6], [9].

[3] ba=d

Axiom: ba=d.

Defines rule #4.

Referenced by [4], [5], [6].

[4] dcca=a

Overlap of [1] baababa=a with [3] ba=d:

1 baababa ba

Critical pair: dababa=a.

Reduce LHS:

[2]d(ab)aba
[2]dc(ab)a
dcca

Referenced by [7].

[5] ca=ad

Overlap of [2] ab=c with [3] ba=d:

a b ba

Critical pair: ca=ad.

Defines rule #5.

Referenced by [7].

[6] db=bc

Overlap of [3] ba=d with [2] ab=c:

b a ab

Critical pair: db=bc.

Defines rule #1.

Referenced by [9].

[7] dadd=a

Simplify [4] dcca=a.

Reduce LHS:

[5]dc(ca)
[5]d(ca)d
dadd

Defines rule #8.

Referenced by [8], [9], [10], [12].

[8] dada=aadd

Overlap of [7] dadd=a with [7] dadd=a:

dad d dadd

Critical pair: aadd=dada.

Flip LHS and RHS.

Defines rule #10.

Referenced by [12].

[9] dccc=c

Overlap of [7] dadd=a with [6] db=bc:

dad d db

Critical pair: ab=dadbc.

Reduce LHS:

[2](ab)
c

Reduce RHS:

[6]da(db)c
[2]d(ab)cc
dccc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11].

[10] dadc=accc

Overlap of [7] dadd=a with [9] dccc=c:

dad d dccc

Critical pair: accc=dadc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [11].

[11] dac=accccc

Overlap of [10] dadc=accc with [9] dccc=c:

da dc dccc

Critical pair: accccc=dac.

Flip LHS and RHS.

Defines rule #6.

[12] daa=aadddd

Overlap of [8] dada=aadd with [7] dadd=a:

da da dadd

Critical pair: aadddd=daa.

Flip LHS and RHS.

Defines rule #9.