Certificate for #16329 ⟨a, b | aab=bb, bbba=aa⟩

Completion settings:

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

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #4.

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

[2] aaaaba=aa

Axiom: bbba=aa.

Reduce LHS:

[1]	(bb)ba
[1]	⇒ aa(bb)a
	⇒ aaaaba

Referenced by [4], [5], [6], [7], [8], [9].

[3] baab=aaaab

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

b b bb

Critical pair: baab=aabb.

Reduce RHS:

[1]	aa(bb)
	⇒ aaaab

Referenced by [4], [7].

[4] baaaaaab=aaab

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

baa b baab

Critical pair: baaaaaab=aaaabaab.

Reduce RHS:

[2]	(aaaaba)ab
	⇒ aaab

Referenced by [5].

[5] aaaba=baaaa

Overlap of [4] baaaaaab=aaab with [2] aaaaba=aa:

baa aaaab aaaaba

Critical pair: baaaa=aaaba.

Flip LHS and RHS.

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

[6] aaaaaaa=aa

Overlap of [2] aaaaba=aa with [5] aaaba=baaaa:

aaaab a aaaba

Critical pair: aaaabbaaaa=aaaaba.

Reduce LHS:

[1]	aaaa(bb)aaaa
[2]	⇒ aa(aaaaba)aaa
	⇒ aaaaaaa

Reduce RHS:

[2]	(aaaaba)
	⇒ aa

Defines rule #1.

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

[7] baaaaa=aa

Overlap of [5] aaaba=baaaa with [2] aaaaba=aa:

aaab a aaaaba

Critical pair: aaabaa=baaaaaaaba.

Reduce LHS:

[5]	(aaaba)a
	⇒ baaaaa

Reduce RHS:

[6]	b(aaaaaaa)ba
[3]	⇒ (baab)a
[2]	⇒ (aaaaba)
	⇒ aa

Referenced by [8].

[8] baaaa=aaaaaa

Overlap of [5] aaaba=baaaa with [5] aaaba=baaaa:

aaab a aaaba

Critical pair: aaabbaaaa=baaaaaaba.

Reduce LHS:

[1]	aaa(bb)aaaa
[2]	⇒ a(aaaaba)aaa
	⇒ aaaaaa

Reduce RHS:

[7]	(baaaaa)aba
[5]	⇒ (aaaba)
	⇒ baaaa

Flip LHS and RHS.

Referenced by [10].

[9] aaba=aaaaa

Overlap of [6] aaaaaaa=aa with [2] aaaaba=aa:

aaa aaaa aaaaba

Critical pair: aaaaa=aaba.

Flip LHS and RHS.

Defines rule #3.

[10] baa=aaaa

Overlap of [5] aaaba=baaaa with [8] baaaa=aaaaaa:

aaa ba baaaa

Critical pair: aaaaaaaaa=baaaaaaa.

Reduce LHS:

[6]	(aaaaaaa)aa
	⇒ aaaa

Reduce RHS:

[6]	b(aaaaaaa)
	⇒ baa

Flip LHS and RHS.

Defines rule #2.