Certificate for #10729 ⟨a, b | aaab=baa, abab=1⟩

Completion settings:

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

[1] aaab=baa

Axiom: aaab=baa.

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

[2] abab=1

Axiom: abab=1.

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

[3] bbaa=aa

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

aa ab abab

Critical pair: aa=baaab.

Reduce RHS:

[1]	b(aaab)
	⇒ bbaa

Flip LHS and RHS.

Referenced by [4].

[4] bba=a

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

bba a abab

Critical pair: bba=aabab.

Reduce RHS:

[2]	a(abab)
	⇒ a

Referenced by [5].

[5] bb=1

Overlap of [4] bba=a with [2] abab=1:

bb a abab

Critical pair: bb=abab.

Reduce RHS:

[2]	(abab)
	⇒ 1

Defines rule #3.

Referenced by [6], [7].

[6] baab=aaa

Overlap of [1] aaab=baa with [5] bb=1:

aaa b bb

Critical pair: aaa=baab.

Flip LHS and RHS.

Referenced by [10].

[7] aba=b

Overlap of [2] abab=1 with [5] bb=1:

aba b bb

Critical pair: aba=b.

Referenced by [8], [9].

[8] aab=baaa

Overlap of [1] aaab=baa with [7] aba=b:

aa ab aba

Critical pair: aab=baaa.

Referenced by [9].

[9] ab=baaaa

Overlap of [8] aab=baaa with [7] aba=b:

a ab aba

Critical pair: ab=baaaa.

Defines rule #2.

Referenced by [10].

[10] aaaaa=1

Overlap of [2] abab=1 with [9] ab=baaaa:

abab ab

Critical pair: baaaaab=1.

Reduce LHS:

[1]	baa(aaab)
[6]	⇒ (baab)aa
	⇒ aaaaa

Defines rule #1.