Certificate for #4110 ⟨a, b | aababaaab=ba⟩

Back:⟨a, b | aababaaab=ba⟩

Completion settings:

[1] aababaaab=ba

Axiom: aababaaab=ba.

Referenced by [3].

[2] aabab=c

Axiom: aabab=c.

Referenced by [3], [4].

[3] ba=caaab

Overlap of [1] aababaaab=ba with [2] aabab=c:

aababaaab aabab

Critical pair: caaab=ba.

Flip LHS and RHS.

Defines rule #2.

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

[4] aacaaabb=c

Overlap of [2] aabab=c with [3] ba=caaab:

aa bab ba

Critical pair: aacaaabb=c.

Defines rule #4.

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

[5] caaacaaabcaaabb=bc

Overlap of [3] ba=caaab with [4] aacaaabb=c:

b a aacaaabb

Critical pair: bc=caaabacaaabb.

Reduce RHS:

[3]caaa(ba)caaabb
⇒ caaacaaabcaaabb

Flip LHS and RHS.

Referenced by [7].

[6] aacaaabcaaab=ca

Overlap of [4] aacaaabb=c with [3] ba=caaab:

aacaaab b ba

Critical pair: aacaaabcaaab=ca.

Referenced by [7], [8].

[7] bc=cacab

Simplify [5] caaacaaabcaaabb=bc.

Reduce LHS:

[6]ca(aacaaabcaaab)b
⇒ cacab

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] aacaaacacacaaacac=ca

Overlap of [6] aacaaabcaaab=ca with [7] bc=cacab:

aacaaa bcaaab bc

Critical pair: aacaaacacabaaab=ca.

Reduce LHS:

[3]aacaaacaca(ba)aab
[3]⇒ aacaaacacacaaa(ba)ab
[3]⇒ aacaaacacacaaacaaa(ba)b
[4]⇒ aacaaacacacaaaca(aacaaabb)
⇒ aacaaacacacaaacac

Defines rule #1.