Certificate for #16503 ⟨a, b | aab=ab, bab=aaa⟩

Back:⟨a, b | aab=ab, bab=aaa⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

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

[2] bab=aaa

Axiom: bab=aaa.

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

[3] aaaaa=aaaa

Overlap of [1] aab=ab with [2] bab=aaa:

aa b bab

Critical pair: aaaaa=abab.

Reduce RHS:

[2]a(bab)
⇒ aaaa

Referenced by [5].

[4] ab=baaaa

Overlap of [2] bab=aaa with [2] bab=aaa:

ba b bab

Critical pair: baaaa=aaaab.

Reduce RHS:

[1]aa(aab)
[1]⇒ a(aab)
[1]⇒ (aab)
⇒ ab

Flip LHS and RHS.

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

[5] aaaa=aaa

Overlap of [4] ab=baaaa with [2] bab=aaa:

a b bab

Critical pair: aaaa=baaaaab.

Reduce RHS:

[3]b(aaaaa)b
[1]⇒ baa(aab)
[1]⇒ ba(aab)
[1]⇒ b(aab)
[2]⇒ (bab)
⇒ aaa

Defines rule #1.

Referenced by [6], [7].

[6] bbaaa=aaa

Overlap of [2] bab=aaa with [4] ab=baaaa:

b ab ab

Critical pair: bbaaaa=aaa.

Reduce LHS:

[5]bb(aaaa)
⇒ bbaaa

Defines rule #3.

[7] ab=baaa

Simplify [4] ab=baaaa.

Reduce RHS:

[5]b(aaaa)
⇒ baaa

Defines rule #2.