Certificate for #5410 ⟨a, b | aab=bb, bab=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.

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

[2] bab=aa

Axiom: bab=aa.

Defines rule #5.

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

[3] baa=aaaa

Overlap of [1] bb=aab with [2] bab=aa:

b b bab

Critical pair: baa=aabab.

Reduce RHS:

[2]	aa(bab)
	⇒ aaaa

Defines rule #2.

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

[4] aaaaab=aab

Overlap of [2] bab=aa with [1] bb=aab:

ba b bb

Critical pair: baaab=aab.

Reduce LHS:

[3]	(baa)ab
	⇒ aaaaab

Referenced by [7].

[5] aaab=aaaaa

Overlap of [2] bab=aa with [2] bab=aa:

ba b bab

Critical pair: baaa=aaab.

Reduce LHS:

[3]	(baa)a
	⇒ aaaaa

Flip LHS and RHS.

Referenced by [7].

[6] aaaaaaa=aaaa

Overlap of [2] bab=aa with [3] baa=aaaa:

ba b baa

Critical pair: baaaaa=aaaa.

Reduce LHS:

[3]	(baa)aaa
	⇒ aaaaaaa

Defines rule #1.

Referenced by [7].

[7] aab=aaaa

Overlap of [3] baa=aaaa with [5] aaab=aaaaa:

b aa aaab

Critical pair: baaaaa=aaaaab.

Reduce LHS:

[3]	(baa)aaa
[6]	⇒ (aaaaaaa)
	⇒ aaaa

Reduce RHS:

[4]	(aaaaab)
	⇒ aab

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] bb=aaaa

Simplify [1] bb=aab.

Reduce RHS:

[7]	(aab)
	⇒ aaaa

Defines rule #4.