Certificate for #16070 ⟨a, b | aaa=bb, abbb=bb⟩

Completion settings:

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

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

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

[2] aaaab=aaa

Axiom: abbb=bb.

Reduce LHS:

[1]	a(bb)b
	⇒ aaaab

Reduce RHS:

[1]	(bb)
	⇒ aaa

Referenced by [4].

[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 [4], [5], [6], [7], [8], [9].

[4] abaaa=aaa

Simplify [2] aaaab=aaa.

Reduce LHS:

[3]	a(aaab)
	⇒ abaaa

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

[5] baaa=aaaaaaa

Overlap of [4] abaaa=aaa with [3] aaab=baaa:

ab aaa aaab

Critical pair: abbaaa=aaab.

Reduce LHS:

[1]	a(bb)aaa
	⇒ aaaaaaa

Reduce RHS:

[3]	(aaab)
	⇒ baaa

Flip LHS and RHS.

Defines rule #2.

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

[6] aaaaaaaaaa=aaaaa

Overlap of [3] aaab=baaa with [4] abaaa=aaa:

aa ab abaaa

Critical pair: aaaaa=baaaaaa.

Reduce RHS:

[5]	(baaa)aaa
	⇒ aaaaaaaaaa

Flip LHS and RHS.

Referenced by [7].

[7] aaaaaaaaa=aaaa

Overlap of [6] aaaaaaaaaa=aaaaa with [3] aaab=baaa:

aaaaaaa aaa aaab

Critical pair: aaaaaaabaaa=aaaaab.

Reduce LHS:

[3]	aaaa(aaab)aaa
[3]	⇒ a(aaab)aaaaaa
[4]	⇒ (abaaa)aaaaaa
	⇒ aaaaaaaaa

Reduce RHS:

[3]	aa(aaab)
[4]	⇒ a(abaaa)
	⇒ aaaa

Referenced by [8].

[8] aaaaaaaa=aaa

Overlap of [7] aaaaaaaaa=aaaa with [3] aaab=baaa:

aaaaaa aaa aaab

Critical pair: aaaaaabaaa=aaaab.

Reduce LHS:

[3]	aaa(aaab)aaa
[3]	⇒ (aaab)aaaaaa
[7]	⇒ b(aaaaaaaaa)
[5]	⇒ (baaa)a
	⇒ aaaaaaaa

Reduce RHS:

[3]	a(aaab)
[4]	⇒ (abaaa)
	⇒ aaa

Defines rule #1.

[9] aaab=aaaaaaa

Simplify [3] aaab=baaa.

Reduce RHS:

[5]	(baaa)
	⇒ aaaaaaa

Defines rule #3.