Certificate for #16333 ⟨a, b | aab=bb, bbbb=aa⟩

Completion settings:

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

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

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

[2] aaaaaab=aa

Axiom: bbbb=aa.

Reduce LHS:

[1]	(bb)bb
[1]	⇒ aa(bb)b
[1]	⇒ aaaa(bb)
	⇒ aaaaaab

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

[3] baab=aaaab

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

b b bb

Critical pair: baab=aabb.

Reduce RHS:

[1]	aa(bb)
	⇒ aaaab

Referenced by [5].

[4] aab=aaaa

Overlap of [2] aaaaaab=aa with [1] bb=aab:

aaaaaa b bb

Critical pair: aaaaaaaab=aab.

Reduce LHS:

[2]	aa(aaaaaab)
	⇒ aaaa

Flip LHS and RHS.

Defines rule #3.

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

[5] baaaa=aaaaaa

Simplify [3] baab=aaaab.

Reduce LHS:

[4]	b(aab)
	⇒ baaaa

Reduce RHS:

[4]	aa(aab)
	⇒ aaaaaa

Referenced by [6], [7].

[6] baa=aaaa

Overlap of [5] baaaa=aaaaaa with [2] aaaaaab=aa:

b aaaa aaaaaab

Critical pair: baa=aaaaaaaab.

Reduce RHS:

[2]	aa(aaaaaab)
	⇒ aaaa

Defines rule #2.

Referenced by [7].

[7] aaaaaaaa=aa

Overlap of [5] baaaa=aaaaaa with [4] aab=aaaa:

baa aa aab

Critical pair: baaaaaa=aaaaaab.

Reduce LHS:

[6]	(baa)aaaa
	⇒ aaaaaaaa

Reduce RHS:

[2]	(aaaaaab)
	⇒ aa

Defines rule #1.

[8] bb=aaaa

Simplify [1] bb=aab.

Reduce RHS:

[4]	(aab)
	⇒ aaaa

Defines rule #4.