Certificate for #16228 ⟨a, b | aab=ba, abaa=bb⟩

Completion settings:

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

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

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

[2] bb=aaaaab

Axiom: abaa=bb.

Reduce LHS:

[1]	a(ba)a
[1]	⇒ aaa(ba)
	⇒ aaaaab

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aaaaaaaaab=aaaaaaab

Overlap of [2] bb=aaaaab with [1] ba=aab:

b b ba

Critical pair: baab=aaaaaba.

Reduce LHS:

[1]	(ba)ab
[1]	⇒ aa(ba)b
[2]	⇒ aaaa(bb)
	⇒ aaaaaaaaab

Reduce RHS:

[1]	aaaaa(ba)
	⇒ aaaaaaab

Referenced by [4].

[4] aaaaaaaab=aaaaaaab

Overlap of [2] bb=aaaaab with [2] bb=aaaaab:

b b bb

Critical pair: baaaaab=aaaaabb.

Reduce LHS:

[1]	(ba)aaaab
[1]	⇒ aa(ba)aaab
[1]	⇒ aaaa(ba)aab
[1]	⇒ aaaaaa(ba)ab
[1]	⇒ aaaaaaaa(ba)b
[3]	⇒ a(aaaaaaaaab)b
[2]	⇒ aaaaaaaa(bb)
[3]	⇒ aaaa(aaaaaaaaab)
[3]	⇒ aa(aaaaaaaaab)
[3]	⇒ (aaaaaaaaab)
	⇒ aaaaaaab

Reduce RHS:

[2]	aaaaa(bb)
[3]	⇒ a(aaaaaaaaab)
	⇒ aaaaaaaab

Flip LHS and RHS.

Defines rule #1.