Certificate for #16114 ⟨a, b | aab=aa, baaa=ab⟩

Completion settings:

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

[1] aab=aa

Axiom: aab=aa.

Referenced by [3].

[2] ab=baaa

Axiom: baaa=ab.

Flip LHS and RHS.

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

[3] baaaaaa=aa

Overlap of [1] aab=aa with [2] ab=baaa:

a ab ab

Critical pair: abaaa=aa.

Reduce LHS:

[2]	(ab)aaa
	⇒ baaaaaa

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

[4] aaaaa=aaa

Overlap of [2] ab=baaa with [3] baaaaaa=aa:

a b baaaaaa

Critical pair: aaa=baaaaaaaaa.

Reduce RHS:

[3]	(baaaaaa)aaa
	⇒ aaaaa

Flip LHS and RHS.

Referenced by [5].

[5] baaaa=aa

Overlap of [3] baaaaaa=aa with [2] ab=baaa:

baaaaa a ab

Critical pair: baaaaabaaa=aab.

Reduce LHS:

[4]	b(aaaaa)baaa
[2]	⇒ baa(ab)aaa
[3]	⇒ baa(baaaaaa)
	⇒ baaaa

Reduce RHS:

[2]	a(ab)
[2]	⇒ (ab)aaa
[3]	⇒ (baaaaaa)
	⇒ aa

Referenced by [6], [7].

[6] aaaa=aa

Overlap of [3] baaaaaa=aa with [5] baaaa=aa:

baaaaaa baaaa

Critical pair: aaaa=aa.

Defines rule #1.

Referenced by [7], [8].

[7] baaa=aaa

Overlap of [5] baaaa=aa with [6] aaaa=aa:

ba aaa aaaa

Critical pair: baaa=aaa.

Referenced by [8].

[8] baa=aa

Overlap of [7] baaa=aaa with [6] aaaa=aa:

b aaa aaaa

Critical pair: baa=aaaa.

Reduce RHS:

[6]	(aaaa)
	⇒ aa

Defines rule #2.

Referenced by [9].

[9] ab=aaa

Simplify [2] ab=baaa.

Reduce RHS:

[8]	(baa)a
	⇒ aaa

Defines rule #3.