Certificate for #15515 ⟨a, b | aaa=bb, aabab=a⟩

Back:⟨a, b | aaa=bb, aabab=a⟩

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #3.

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

[2] aabab=a

Axiom: aabab=a.

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

[3] aaab=baaa

Overlap of [1] bb=aaa with [1] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

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

[4] aabaaaa=ab

Overlap of [2] aabab=a with [1] bb=aaa:

aaba b bb

Critical pair: aabaaaa=ab.

Referenced by [7].

[5] babaaa=aa

Overlap of [3] aaab=baaa with [2] aabab=a:

a aab aabab

Critical pair: aa=baaaab.

Reduce RHS:

[3]ba(aaab)
⇒ babaaa

Flip LHS and RHS.

Referenced by [6].

[6] aab=baaaaaaa

Overlap of [5] babaaa=aa with [3] aaab=baaa:

bab aaa aaab

Critical pair: babbaaa=aab.

Reduce LHS:

[1]ba(bb)aaa
⇒ baaaaaaa

Flip LHS and RHS.

Referenced by [7].

[7] ab=baaaaaaaaaaa

Simplify [4] aabaaaa=ab.

Reduce LHS:

[6](aab)aaaa
⇒ baaaaaaaaaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] aaaaaaaaaaaaaaaa=a

Overlap of [2] aabab=a with [7] ab=baaaaaaaaaaa:

a abab ab

Critical pair: abaaaaaaaaaaaab=a.

Reduce LHS:

[3]abaaaaaaaaa(aaab)
[3]⇒ abaaaaaa(aaab)aaa
[3]⇒ abaaa(aaab)aaaaaa
[3]⇒ ab(aaab)aaaaaaaaa
[1]⇒ a(bb)aaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaaa

Defines rule #1.