Certificate for #15933 ⟨a, b | aba=bb, baaab=a⟩

Completion settings:

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

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #4.

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

[2] baaab=a

Axiom: baaab=a.

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

[3] abaaaab=ba

Overlap of [1] bb=aba with [2] baaab=a:

b b baaab

Critical pair: ba=abaaaab.

Flip LHS and RHS.

Referenced by [8].

[4] baaaaba=ab

Overlap of [2] baaab=a with [1] bb=aba:

baaa b bb

Critical pair: baaaaba=ab.

Referenced by [6].

[5] aaaab=baaaa

Overlap of [2] baaab=a with [2] baaab=a:

baaa b baaab

Critical pair: baaaa=aaaab.

Flip LHS and RHS.

Referenced by [6], [8].

[6] abaaaaaa=ab

Simplify [4] baaaaba=ab.

Reduce LHS:

[5]	b(aaaab)a
[1]	⇒ (bb)aaaaa
	⇒ abaaaaaa

Defines rule #2.

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

[7] aaaaaaa=a

Overlap of [2] baaab=a with [6] abaaaaaa=ab:

baa ab abaaaaaa

Critical pair: baaab=aaaaaaa.

Reduce LHS:

[2]	(baaab)
	⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [11].

[8] aabaaaaa=ba

Simplify [3] abaaaab=ba.

Reduce LHS:

[5]	ab(aaaab)
[1]	⇒ a(bb)aaaa
	⇒ aabaaaaa

Referenced by [9], [10].

[9] baba=aaaaaa

Overlap of [2] baaab=a with [8] aabaaaaa=ba:

ba aab aabaaaaa

Critical pair: baba=aaaaaa.

Referenced by [11].

[10] aab=baa

Overlap of [8] aabaaaaa=ba with [6] abaaaaaa=ab:

a abaaaaa abaaaaaa

Critical pair: aab=baa.

Defines rule #3.

[11] bab=aaaaa

Overlap of [9] baba=aaaaaa with [6] abaaaaaa=ab:

b aba abaaaaaa

Critical pair: bab=aaaaaaaaaaa.

Reduce RHS:

[7]	(aaaaaaa)aaaa
	⇒ aaaaa

Defines rule #5.