Certificate for #16297 ⟨a, b | aab=bb, abba=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].

[2] aaaba=aa

Axiom: abba=aa.

Reduce LHS:

[1]	a(bb)a
	⇒ aaaba

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

[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] aaaaaaab=aaab

Overlap of [2] aaaba=aa with [3] baab=aaaab:

aaa ba baab

Critical pair: aaaaaaab=aaab.

Referenced by [5].

[5] aaaaaa=aa

Overlap of [4] aaaaaaab=aaab with [2] aaaba=aa:

aaaa aaab aaaba

Critical pair: aaaaaa=aaaba.

Reduce RHS:

[2]	(aaaba)
	⇒ aa

Defines rule #1.

Referenced by [6], [8].

[6] aaba=aaaaa

Overlap of [5] aaaaaa=aa with [2] aaaba=aa:

aaa aaa aaaba

Critical pair: aaaaa=aaba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

[7] baaaaa=aaa

Overlap of [3] baab=aaaab with [6] aaba=aaaaa:

b aab aaba

Critical pair: baaaaa=aaaaba.

Reduce RHS:

[2]	a(aaaba)
	⇒ aaa

Referenced by [8].

[8] baa=aaaa

Overlap of [7] baaaaa=aaa with [5] aaaaaa=aa:

b aaaaa aaaaaa

Critical pair: baa=aaaa.

Defines rule #2.