#5 ⟨a, b | baabababababa=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. dc6c [9]
3. abc [2]
4. bad [3]
5. caad [5]
6. dacac26 [17]
7. dadcac21 [15]
8. dad2cac16 [13]
9. dad3cac11 [11]
10. dad4cac6 [10]
11. dad5a [7]
12. da2a2d25 [18]
13. (da)2a2d20 [16]
14. dad2aa2d15 [14]
15. dad3aa2d10 [12]
16. dad4aa2d5 [8]
# ab:baabababababa=a bcd/a ab=c,ba=d custom:1
db=bc
dcccccc=c
ab=c
ba=d
ca=ad
dac=acccccccccccccccccccccccccc
dadc=accccccccccccccccccccc
daddc=acccccccccccccccc
dadddc=accccccccccc
daddddc=acccccc
daddddd=a
daa=aaddddddddddddddddddddddddd
dada=aadddddddddddddddddddd
dadda=aaddddddddddddddd
daddda=aadddddddddd
dadddda=aaddddd

Certificate

[1] baabababababa=a

Axiom: baabababababa=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] dccccca=a

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

1 baabababababa ba

Critical pair: dabababababa=a.

Reduce LHS:

[2]d(ab)ababababa
[2]dc(ab)abababa
[2]dcc(ab)ababa
[2]dccc(ab)aba
[2]dcccc(ab)a
dccccca

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] daddddd=a

Simplify [4] dccccca=a.

Reduce LHS:

[5]dcccc(ca)
[5]dccc(ca)d
[5]dcc(ca)dd
[5]dc(ca)ddd
[5]d(ca)dddd
daddddd

Defines rule #11.

Referenced by [8], [9], [10], [12], [14], [16], [18].

[8] dadddda=aaddddd

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

dadddd d daddddd

Critical pair: aaddddd=dadddda.

Flip LHS and RHS.

Defines rule #16.

Referenced by [12].

[9] dcccccc=c

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

dadddd d db

Critical pair: ab=daddddbc.

Reduce LHS:

[2](ab)
c

Reduce RHS:

[6]daddd(db)c
[6]dadd(db)cc
[6]dad(db)ccc
[6]da(db)cccc
[2]d(ab)ccccc
dcccccc

Flip LHS and RHS.

Defines rule #2.

Referenced by [10], [11], [13], [15], [17].

[10] daddddc=acccccc

Overlap of [7] daddddd=a with [9] dcccccc=c:

dadddd d dcccccc

Critical pair: acccccc=daddddc.

Flip LHS and RHS.

Defines rule #10.

Referenced by [11].

[11] dadddc=accccccccccc

Overlap of [10] daddddc=acccccc with [9] dcccccc=c:

daddd dc dcccccc

Critical pair: accccccccccc=dadddc.

Flip LHS and RHS.

Defines rule #9.

Referenced by [13].

[12] daddda=aadddddddddd

Overlap of [8] dadddda=aaddddd with [7] daddddd=a:

daddd da daddddd

Critical pair: aadddddddddd=daddda.

Flip LHS and RHS.

Defines rule #15.

Referenced by [14].

[13] daddc=acccccccccccccccc

Overlap of [11] dadddc=accccccccccc with [9] dcccccc=c:

dadd dc dcccccc

Critical pair: acccccccccccccccc=daddc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [15].

[14] dadda=aaddddddddddddddd

Overlap of [12] daddda=aadddddddddd with [7] daddddd=a:

dadd da daddddd

Critical pair: aaddddddddddddddd=dadda.

Flip LHS and RHS.

Defines rule #14.

Referenced by [16].

[15] dadc=accccccccccccccccccccc

Overlap of [13] daddc=acccccccccccccccc with [9] dcccccc=c:

dad dc dcccccc

Critical pair: accccccccccccccccccccc=dadc.

Flip LHS and RHS.

Defines rule #7.

Referenced by [17].

[16] dada=aadddddddddddddddddddd

Overlap of [14] dadda=aaddddddddddddddd with [7] daddddd=a:

dad da daddddd

Critical pair: aadddddddddddddddddddd=dada.

Flip LHS and RHS.

Defines rule #13.

Referenced by [18].

[17] dac=acccccccccccccccccccccccccc

Overlap of [15] dadc=accccccccccccccccccccc with [9] dcccccc=c:

da dc dcccccc

Critical pair: acccccccccccccccccccccccccc=dac.

Flip LHS and RHS.

Defines rule #6.

[18] daa=aaddddddddddddddddddddddddd

Overlap of [16] dada=aadddddddddddddddddddd with [7] daddddd=a:

da da daddddd

Critical pair: aaddddddddddddddddddddddddd=daa.

Flip LHS and RHS.

Defines rule #12.