Certificate for #24708 ⟨a, b | aa=a, babbab=ab⟩

Back:⟨a, b | aa=a, babbab=ab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [4].

[2] babbab=ab

Axiom: babbab=ab.

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

[3] babab=abbab

Overlap of [2] babbab=ab with [2] babbab=ab:

bab bab babbab

Critical pair: babab=abbab.

Referenced by [4], [7].

[4] abab=bab

Overlap of [3] babab=abbab with [2] babbab=ab:

ba bab babbab

Critical pair: baab=abbabbab.

Reduce LHS:

[1]b(aa)b
⇒ bab

Reduce RHS:

[2]ab(babbab)
⇒ abab

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [7], [8].

[5] babbbab=bab

Overlap of [2] babbab=ab with [4] abab=bab:

babb ab abab

Critical pair: babbbab=abab.

Reduce RHS:

[4](abab)
⇒ bab

Referenced by [6], [7].

[6] abbbab=ab

Overlap of [2] babbab=ab with [5] babbbab=bab:

bab bab babbbab

Critical pair: babbab=abbbab.

Reduce LHS:

[2](babbab)
⇒ ab

Flip LHS and RHS.

Referenced by [8], [10].

[7] babbbbab=abbab

Overlap of [5] babbbab=bab with [4] abab=bab:

babbb ab abab

Critical pair: babbbbab=babab.

Reduce RHS:

[3](babab)
⇒ abbab

Referenced by [9].

[8] abbbbab=bab

Overlap of [6] abbbab=ab with [4] abab=bab:

abbb ab abab

Critical pair: abbbbab=abab.

Reduce RHS:

[4](abab)
⇒ bab

Referenced by [9], [10].

[9] abbab=bbab

Simplify [7] babbbbab=abbab.

Reduce LHS:

[8]b(abbbbab)
⇒ bbab

Flip LHS and RHS.

Defines rule #3.

Referenced by [10].

[10] bbbab=ab

Overlap of [9] abbab=bbab with [8] abbbbab=bab:

abb ab abbbbab

Critical pair: abbbab=bbabbbbab.

Reduce LHS:

[6](abbbab)
⇒ ab

Reduce RHS:

[8]bb(abbbbab)
⇒ bbbab

Flip LHS and RHS.

Defines rule #4.