Certificate for #19009 ⟨a, b | aab=b, abbaaa=b⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(a) = 1

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abbaaa=b

Axiom: abbaaa=b.

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

[3] bbaaa=ab

Overlap of [1] aab=b with [2] abbaaa=b:

a ab abbaaa

Critical pair: ab=bbaaa.

Flip LHS and RHS.

Referenced by [7], [9].

[4] abbab=bb

Overlap of [2] abbaaa=b with [1] aab=b:

abba aa aab

Critical pair: abbab=bb.

Referenced by [6].

[5] bab=abbb

Overlap of [2] abbaaa=b with [1] aab=b:

abbaa a aab

Critical pair: abbaab=bab.

Reduce LHS:

[1]	abb(aab)
	⇒ abbb

Flip LHS and RHS.

Defines rule #2.

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

[6] bbbbb=bb

Simplify [4] abbab=bb.

Reduce LHS:

[5]	ab(bab)
[5]	⇒ a(bab)bb
[1]	⇒ (aab)bbbb
	⇒ bbbbb

Referenced by [7].

[7] abbbb=ab

Overlap of [6] bbbbb=bb with [3] bbaaa=ab:

bbb bb bbaaa

Critical pair: bbbab=bbaaa.

Reduce LHS:

[5]	bb(bab)
[5]	⇒ b(bab)bb
[6]	⇒ ba(bbbbb)
[5]	⇒ (bab)b
	⇒ abbbb

Reduce RHS:

[3]	(bbaaa)
	⇒ ab

Referenced by [8], [9].

[8] bbbb=b

Overlap of [1] aab=b with [7] abbbb=ab:

a ab abbbb

Critical pair: aab=bbbb.

Reduce LHS:

[1]	(aab)
	⇒ b

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[9] baaa=abb

Overlap of [8] bbbb=b with [3] bbaaa=ab:

bb bb bbaaa

Critical pair: bbab=baaa.

Reduce LHS:

[5]	b(bab)
[5]	⇒ (bab)bb
[7]	⇒ (abbbb)b
	⇒ abb

Flip LHS and RHS.

Defines rule #4.