Certificate for #3808 ⟨a, b | aaab=ba, abab=1⟩

Completion settings:

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

[1] aaab=ba

Axiom: aaab=ba.

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

[2] abab=1

Axiom: abab=1.

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

[3] baab=aa

Overlap of [1] aaab=ba with [2] abab=1:

aa ab abab

Critical pair: aa=baab.

Flip LHS and RHS.

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

[4] bba=aaaaa

Overlap of [1] aaab=ba with [3] baab=aa:

aaa b baab

Critical pair: aaaaa=baaab.

Reduce RHS:

[1]	b(aaab)
	⇒ bba

Flip LHS and RHS.

Referenced by [8], [10].

[5] aab=abaaa

Overlap of [2] abab=1 with [3] baab=aa:

aba b baab

Critical pair: abaaa=aab.

Flip LHS and RHS.

Referenced by [7].

[6] aba=baaaa

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

baa b baab

Critical pair: baaaa=aaaab.

Reduce RHS:

[1]	a(aaab)
	⇒ aba

Flip LHS and RHS.

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

[7] baaaaaaaaaa=baa

Overlap of [1] aaab=ba with [6] aba=baaaa:

aa ab aba

Critical pair: aabaaaa=baa.

Reduce LHS:

[5]	(aab)aaaa
[6]	⇒ (aba)aaaaaa
	⇒ baaaaaaaaaa

Referenced by [9].

[8] aaaaaaaa=1

Overlap of [2] abab=1 with [6] aba=baaaa:

abab aba

Critical pair: baaaab=1.

Reduce LHS:

[1]	ba(aaab)
[6]	⇒ b(aba)
[4]	⇒ (bba)aaa
	⇒ aaaaaaaa

Defines rule #1.

Referenced by [9], [10].

[9] ab=baaa

Overlap of [6] aba=baaaa with [8] aaaaaaaa=1:

ab a aaaaaaaa

Critical pair: ab=baaaaaaaaaaa.

Reduce RHS:

[7]	(baaaaaaaaaa)a
	⇒ baaa

Defines rule #2.

[10] bb=aaaa

Overlap of [4] bba=aaaaa with [8] aaaaaaaa=1:

bb a aaaaaaaa

Critical pair: bb=aaaaaaaaaaaa.

Reduce RHS:

[8]	(aaaaaaaa)aaaa
	⇒ aaaa

Defines rule #3.