Certificate for #15797 ⟨a, b | aab=bb, bbbba=a⟩

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 #3.

Referenced by [2], [3], [4], [8], [9].

[2] aaaaaaba=a

Axiom: bbbba=a.

Reduce LHS:

[1]	(bb)bba
[1]	⇒ aa(bb)ba
[1]	⇒ aaaa(bb)a
	⇒ aaaaaaba

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

[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], [5], [6].

[4] baaaab=aaaaaab

Overlap of [1] bb=aab with [3] baab=aaaab:

b b baab

Critical pair: baaaab=aabaab.

Reduce RHS:

[3]	aa(baab)
	⇒ aaaaaab

Referenced by [6], [8].

[5] aaaaaaaaaab=aab

Overlap of [2] aaaaaaba=a with [3] baab=aaaab:

aaaaaa ba baab

Critical pair: aaaaaaaaaab=aab.

Referenced by [6].

[6] baaaaaaaab=aab

Overlap of [3] baab=aaaab with [4] baaaab=aaaaaab:

baa b baaaab

Critical pair: baaaaaaaab=aaaabaaaab.

Reduce RHS:

[4]	aaaa(baaaab)
[5]	⇒ (aaaaaaaaaab)
	⇒ aab

Referenced by [7].

[7] aaba=baaa

Overlap of [6] baaaaaaaab=aab with [2] aaaaaaba=a:

baa aaaaaab aaaaaaba

Critical pair: baaa=aaba.

Flip LHS and RHS.

Referenced by [8], [9].

[8] baaaaaaa=a

Overlap of [4] baaaab=aaaaaab with [7] aaba=baaa:

baa aab aaba

Critical pair: baabaaa=aaaaaaba.

Reduce LHS:

[7]	b(aaba)aa
[1]	⇒ (bb)aaaaa
[7]	⇒ (aaba)aaaa
	⇒ baaaaaaa

Reduce RHS:

[2]	(aaaaaaba)
	⇒ a

Referenced by [9], [10].

[9] ba=aaa

Overlap of [1] bb=aab with [8] baaaaaaa=a:

b b baaaaaaa

Critical pair: ba=aabaaaaaaa.

Reduce RHS:

[7]	(aaba)aaaaaa
[8]	⇒ (baaaaaaa)aa
	⇒ aaa

Defines rule #2.

Referenced by [10].

[10] aaaaaaaaa=a

Overlap of [8] baaaaaaa=a with [2] aaaaaaba=a:

baaaaaa a aaaaaaba

Critical pair: baaaaaaa=aaaaaaba.

Reduce LHS:

[9]	(ba)aaaaaa
	⇒ aaaaaaaaa

Reduce RHS:

[2]	(aaaaaaba)
	⇒ a

Defines rule #1.