Certificate for #16521 ⟨a, b | aab=bb, bab=aaa⟩

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.

Defines rule #4.

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

[2] bab=aaa

Axiom: bab=aaa.

Defines rule #5.

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

[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 [8].

[4] baaa=aaaaa

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

b b bab

Critical pair: baaa=aabab.

Reduce RHS:

[2]	aa(bab)
	⇒ aaaaa

Defines rule #2.

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

[5] aaaaab=aaab

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

ba b bb

Critical pair: baaab=aaab.

Reduce LHS:

[4]	(baaa)b
	⇒ aaaaab

Referenced by [9].

[6] aaaab=aaaaaa

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

ba b bab

Critical pair: baaaa=aaaab.

Reduce LHS:

[4]	(baaa)a
	⇒ aaaaaa

Flip LHS and RHS.

Referenced by [8].

[7] aaaaaaaa=aaaaaa

Overlap of [2] bab=aaa with [4] baaa=aaaaa:

ba b baaa

Critical pair: baaaaaa=aaaaaa.

Reduce LHS:

[4]	(baaa)aaa
	⇒ aaaaaaaa

Defines rule #1.

Referenced by [9].

[8] baab=aaaaaa

Simplify [3] baab=aaaab.

Reduce RHS:

[6]	(aaaab)
	⇒ aaaaaa

Defines rule #6.

Referenced by [9].

[9] aaab=aaaaaaa

Overlap of [2] bab=aaa with [8] baab=aaaaaa:

ba b baab

Critical pair: baaaaaaa=aaaaab.

Reduce LHS:

[4]	(baaa)aaaa
[7]	⇒ (aaaaaaaa)a
	⇒ aaaaaaa

Reduce RHS:

[5]	(aaaaab)
	⇒ aaab

Flip LHS and RHS.

Defines rule #3.