Certificate for #13127 ⟨a, b | aab=aaa, abb=bb⟩

Completion settings:

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

[1] aab=aaa

Axiom: aab=aaa.

Defines rule #3.

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

[2] abb=bb

Axiom: abb=bb.

Referenced by [3], [5].

[3] bb=aaaa

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

a ab abb

Critical pair: abb=aaab.

Reduce LHS:

[2]	(abb)
	⇒ bb

Reduce RHS:

[1]	a(aab)
	⇒ aaaa

Defines rule #4.

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

[4] aaaaaa=aaaa

Overlap of [1] aab=aaa with [3] bb=aaaa:

aa b bb

Critical pair: aaaaaa=aaab.

Reduce RHS:

[1]	a(aab)
	⇒ aaaa

Referenced by [7].

[5] abaaaa=aaaaa

Overlap of [2] abb=bb with [3] bb=aaaa:

ab b bb

Critical pair: abaaaa=bbb.

Reduce RHS:

[3]	(bb)b
[1]	⇒ aa(aab)
	⇒ aaaaa

Referenced by [7].

[6] baaaa=aaaaa

Overlap of [3] bb=aaaa with [3] bb=aaaa:

b b bb

Critical pair: baaaa=aaaab.

Reduce RHS:

[1]	aa(aab)
	⇒ aaaaa

Referenced by [7], [8].

[7] aaaaa=aaaa

Simplify [5] abaaaa=aaaaa.

Reduce LHS:

[6]	a(baaaa)
[4]	⇒ (aaaaaa)
	⇒ aaaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] baaaa=aaaa

Simplify [6] baaaa=aaaaa.

Reduce RHS:

[7]	(aaaaa)
	⇒ aaaa

Defines rule #2.