Certificate for #13182 ⟨a, b | abb=aaa, bab=aa⟩

Completion settings:

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

[1] abb=aaa

Axiom: abb=aaa.

Defines rule #7.

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

[2] bab=aa

Axiom: bab=aa.

Defines rule #6.

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

[3] aaab=baaa

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

ba b bab

Critical pair: baaa=aaab.

Flip LHS and RHS.

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

[4] abaaa=abaa

Overlap of [1] abb=aaa with [2] bab=aa:

ab b bab

Critical pair: abaa=aaaab.

Reduce RHS:

[3]	a(aaab)
	⇒ abaaa

Flip LHS and RHS.

Referenced by [8], [9].

[5] aab=baaa

Overlap of [2] bab=aa with [1] abb=aaa:

b ab abb

Critical pair: baaa=aab.

Flip LHS and RHS.

Defines rule #4.

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

[6] bbaaa=aaaa

Overlap of [5] aab=baaa with [1] abb=aaa:

a ab abb

Critical pair: aaaa=baaab.

Reduce RHS:

[3]	b(aaab)
	⇒ bbaaa

Flip LHS and RHS.

Defines rule #5.

[7] aaaaa=aaaa

Overlap of [5] aab=baaa with [2] bab=aa:

aa b bab

Critical pair: aaaa=baaaab.

Reduce RHS:

[3]	ba(aaab)
[2]	⇒ (bab)aaa
	⇒ aaaaa

Flip LHS and RHS.

Defines rule #1.

[8] abaa=baaa

Simplify [3] aaab=baaa.

Reduce LHS:

[5]	a(aab)
[4]	⇒ (abaaa)
	⇒ abaa

Defines rule #3.

Referenced by [9].

[9] baaaa=baaa

Simplify [4] abaaa=abaa.

Reduce LHS:

[8]	(abaa)a
	⇒ baaaa

Reduce RHS:

[8]	(abaa)
	⇒ baaa

Defines rule #2.