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

[2] aaaba=a

Axiom: abba=a.

Reduce LHS:

[1]	a(bb)a
	⇒ aaaba

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

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

[4] aaaaaaab=aab

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

aaa ba baab

Critical pair: aaaaaaab=aab.

Referenced by [5].

[5] aaba=aaaaa

Overlap of [4] aaaaaaab=aab with [2] aaaba=a:

aaaa aaab aaaba

Critical pair: aaaaa=aaba.

Flip LHS and RHS.

Referenced by [6].

[6] baaaaa=aa

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

b aab aaba

Critical pair: baaaaa=aaaaba.

Reduce RHS:

[2]	a(aaaba)
	⇒ aa

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

[7] baa=aaaa

Overlap of [1] bb=aab with [6] baaaaa=aa:

b b baaaaa

Critical pair: baa=aabaaaaa.

Reduce RHS:

[6]	aa(baaaaa)
	⇒ aaaa

Referenced by [8].

[8] aaaaaa=a

Overlap of [6] baaaaa=aa with [2] aaaba=a:

baaa aa aaaba

Critical pair: baaaa=aaaba.

Reduce LHS:

[7]	(baa)aa
	⇒ aaaaaa

Reduce RHS:

[2]	(aaaba)
	⇒ a

Defines rule #1.

Referenced by [9].

[9] ba=aaa

Overlap of [6] baaaaa=aa with [8] aaaaaa=a:

b aaaaa aaaaaa

Critical pair: ba=aaa.

Defines rule #2.