Certificate for #16540 ⟨a, b | aba=ab, bba=aaa⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aba=ab

Axiom: aba=ab.

Defines rule #2.

Referenced by [3], [4].

[2] bba=aaa

Axiom: bba=aaa.

Defines rule #3.

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

[3] aaaa=abb

Overlap of [1] aba=ab with [1] aba=ab:

ab a aba

Critical pair: abab=abba.

Reduce LHS:

[1]	(aba)b
	⇒ abb

Reduce RHS:

[2]	a(bba)
	⇒ aaaa

Flip LHS and RHS.

Defines rule #4.

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

[4] abbb=ab

Overlap of [1] aba=ab with [3] aaaa=abb:

ab a aaaa

Critical pair: ababb=abaaa.

Reduce LHS:

[1]	(aba)bb
	⇒ abbb

Reduce RHS:

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

Defines rule #5.

Referenced by [6], [7].

[5] aaabb=abb

Overlap of [2] bba=aaa with [3] aaaa=abb:

bb a aaaa

Critical pair: bbabb=aaaaaa.

Reduce LHS:

[2]	(bba)bb
	⇒ aaabb

Reduce RHS:

[3]	(aaaa)aa
[2]	⇒ a(bba)a
[3]	⇒ (aaaa)a
[2]	⇒ a(bba)
[3]	⇒ (aaaa)
	⇒ abb

Referenced by [6].

[6] aaab=ab

Overlap of [2] bba=aaa with [4] abbb=ab:

bb a abbb

Critical pair: bbab=aaabbb.

Reduce LHS:

[2]	(bba)b
	⇒ aaab

Reduce RHS:

[5]	(aaabb)b
[4]	⇒ (abbb)
	⇒ ab

Referenced by [7].

[7] aab=ab

Overlap of [3] aaaa=abb with [6] aaab=ab:

a aaa aaab

Critical pair: aab=abbb.

Reduce RHS:

[4]	(abbb)
	⇒ ab

Defines rule #1.