Certificate for #20235 ⟨a, b | aba=a, babb=aab⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

Defines rule #3.

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

[2] babb=aab

Axiom: babb=aab.

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

[3] abb=aaab

Overlap of [1] aba=a with [2] babb=aab:

a ba babb

Critical pair: aaab=abb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] baab=aaaab

Overlap of [2] babb=aab with [2] babb=aab:

bab b babb

Critical pair: babaab=aababb.

Reduce LHS:

[1]	b(aba)ab
	⇒ baab

Reduce RHS:

[1]	a(aba)bb
[3]	⇒ a(abb)
	⇒ aaaab

Referenced by [7].

[5] aaaaab=aab

Overlap of [3] abb=aaab with [2] babb=aab:

ab b babb

Critical pair: abaab=aaababb.

Reduce LHS:

[1]	(aba)ab
	⇒ aab

Reduce RHS:

[1]	aa(aba)bb
[3]	⇒ aa(abb)
	⇒ aaaaab

Flip LHS and RHS.

Referenced by [6].

[6] aaaaa=aa

Overlap of [5] aaaaab=aab with [1] aba=a:

aaaa ab aba

Critical pair: aaaaa=aaba.

Reduce RHS:

[1]	a(aba)
	⇒ aa

Defines rule #1.

[7] baa=aaaa

Overlap of [4] baab=aaaab with [1] aba=a:

ba ab aba

Critical pair: baa=aaaaba.

Reduce RHS:

[1]	aaa(aba)
	⇒ aaaa

Defines rule #2.