Certificate for #5408 ⟨a, b | aab=bb, abb=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], [6], [9].

[2] aaab=aa

Axiom: abb=aa.

Reduce LHS:

[1]	a(bb)
	⇒ aaab

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

[3] baab=aaa

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

b b bb

Critical pair: baab=aabb.

Reduce RHS:

[1]	aa(bb)
[2]	⇒ a(aaab)
	⇒ aaa

Referenced by [5].

[4] aab=aaaa

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

aaa b bb

Critical pair: aaaaab=aab.

Reduce LHS:

[2]	aa(aaab)
	⇒ aaaa

Flip LHS and RHS.

Defines rule #3.

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

[5] baaaa=aaa

Simplify [3] baab=aaa.

Reduce LHS:

[4]	b(aab)
	⇒ baaaa

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

[6] baaa=aaaaa

Overlap of [1] bb=aab with [5] baaaa=aaa:

b b baaaa

Critical pair: baaa=aabaaaa.

Reduce RHS:

[5]	aa(baaaa)
	⇒ aaaaa

Referenced by [7].

[7] aaaaa=aa

Overlap of [5] baaaa=aaa with [2] aaab=aa:

ba aaa aaab

Critical pair: baaa=aaab.

Reduce LHS:

[6]	(baaa)
	⇒ aaaaa

Reduce RHS:

[2]	(aaab)
	⇒ aa

Defines rule #1.

Referenced by [8].

[8] baa=aaaa

Overlap of [5] baaaa=aaa with [2] aaab=aa:

baaa a aaab

Critical pair: baaaaa=aaaaab.

Reduce LHS:

[7]	b(aaaaa)
	⇒ baa

Reduce RHS:

[7]	(aaaaa)b
[4]	⇒ (aab)
	⇒ aaaa

Defines rule #2.

[9] bb=aaaa

Simplify [1] bb=aab.

Reduce RHS:

[4]	(aab)
	⇒ aaaa

Defines rule #4.