Certificate for #16071 ⟨a, b | aaa=bb, baab=aa⟩

Completion settings:

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

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

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

[2] baab=aa

Axiom: baab=aa.

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

[3] aaab=baaa

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

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

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

[4] aabaaa=baa

Overlap of [1] bb=aaa with [2] baab=aa:

b b baab

Critical pair: baa=aaaaab.

Reduce RHS:

[3]	aa(aaab)
	⇒ aabaaa

Flip LHS and RHS.

Referenced by [9].

[5] aab=baaaaa

Overlap of [2] baab=aa with [1] bb=aaa:

baa b bb

Critical pair: baaaaa=aab.

Flip LHS and RHS.

Referenced by [7], [8], [10], [12].

[6] abaaa=baaaa

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

baa b baab

Critical pair: baaaa=aaaab.

Reduce RHS:

[3]	a(aaab)
	⇒ abaaa

Flip LHS and RHS.

Referenced by [7], [9], [10], [11].

[7] baaaaaa=baaa

Simplify [3] aaab=baaa.

Reduce LHS:

[5]	a(aab)
[6]	⇒ (abaaa)aa
	⇒ baaaaaa

Referenced by [8].

[8] aaaaaaa=aaaa

Overlap of [5] aab=baaaaa with [2] baab=aa:

aa b baab

Critical pair: aaaa=baaaaaaab.

Reduce RHS:

[7]	(baaaaaa)ab
[5]	⇒ baa(aab)
[2]	⇒ (baab)aaaaa
	⇒ aaaaaaa

Flip LHS and RHS.

Referenced by [10].

[9] baaaaa=baa

Simplify [4] aabaaa=baa.

Reduce LHS:

[6]	a(abaaa)
[6]	⇒ (abaaa)a
	⇒ baaaaa

Referenced by [10], [11].

[10] aaaaa=aa

Overlap of [9] baaaaa=baa with [5] aab=baaaaa:

baaa aa aab

Critical pair: baaabaaaaa=baab.

Reduce LHS:

[6]	baa(abaaa)aa
[2]	⇒ (baab)aaaaaa
[8]	⇒ (aaaaaaa)a
	⇒ aaaaa

Reduce RHS:

[2]	(baab)
	⇒ aa

Defines rule #1.

Referenced by [12].

[11] abaa=baaa

Overlap of [6] abaaa=baaaa with [9] baaaaa=baa:

a baaa baaaaa

Critical pair: abaa=baaaaaa.

Reduce RHS:

[9]	(baaaaa)a
	⇒ baaa

Defines rule #2.

[12] aab=baa

Simplify [5] aab=baaaaa.

Reduce RHS:

[10]	b(aaaaa)
	⇒ baa

Defines rule #3.