Certificate for #15794 ⟨a, b | aab=bb, bbbaa=b⟩

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.

Referenced by [2], [3], [4], [5], [7], [8].

[2] aaaabaa=b

Axiom: bbbaa=b.

Reduce LHS:

[1]	(bb)baa
[1]	⇒ aa(bb)aa
	⇒ aaaabaa

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

[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].

[4] aaaaaab=b

Overlap of [2] aaaabaa=b with [2] aaaabaa=b:

aaaab aa aaaabaa

Critical pair: aaaabb=baabaa.

Reduce LHS:

[1]	aaaa(bb)
	⇒ aaaaaab

Reduce RHS:

[3]	(baab)aa
[2]	⇒ (aaaabaa)
	⇒ b

Referenced by [5], [6].

[5] baaaab=b

Overlap of [2] aaaabaa=b with [4] aaaaaab=b:

aaaab aa aaaaaab

Critical pair: aaaabb=baaaab.

Reduce LHS:

[1]	aaaa(bb)
[4]	⇒ (aaaaaab)
	⇒ b

Flip LHS and RHS.

Referenced by [7].

[6] aab=baa

Overlap of [4] aaaaaab=b with [2] aaaabaa=b:

aa aaaab aaaabaa

Critical pair: aab=baa.

Defines rule #2.

Referenced by [7], [8].

[7] baaaaaa=b

Simplify [5] baaaab=b.

Reduce LHS:

[6]	baa(aab)
[6]	⇒ b(aab)aa
[1]	⇒ (bb)aaaa
[6]	⇒ (aab)aaaa
	⇒ baaaaaa

Defines rule #1.

[8] bb=baa

Simplify [1] bb=aab.

Reduce RHS:

[6]	(aab)
	⇒ baa

Defines rule #3.