Certificate for #13207 ⟨a, b | abb=aba, baa=ab⟩

Completion settings:

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

[1] abb=aba

Axiom: abb=aba.

Referenced by [3].

[2] ab=baa

Axiom: baa=ab.

Flip LHS and RHS.

Defines rule #2.

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

[3] abb=baaa

Simplify [1] abb=aba.

Reduce RHS:

[2]	(ab)a
	⇒ baaa

Referenced by [4].

[4] bbaaaa=baaa

Overlap of [3] abb=baaa with [2] ab=baa:

abb ab

Critical pair: baab=baaa.

Reduce LHS:

[2]	ba(ab)
[2]	⇒ b(ab)aa
	⇒ bbaaaa

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

[5] baaaaaa=baaaaa

Overlap of [4] bbaaaa=baaa with [2] ab=baa:

bbaaa a ab

Critical pair: bbaaabaa=baaab.

Reduce LHS:

[2]	bbaa(ab)aa
[2]	⇒ bba(ab)aaaa
[2]	⇒ bb(ab)aaaaaa
[4]	⇒ b(bbaaaa)aaaa
[4]	⇒ (bbaaaa)aaa
	⇒ baaaaaa

Reduce RHS:

[2]	baa(ab)
[2]	⇒ ba(ab)aa
[2]	⇒ b(ab)aaaa
[4]	⇒ (bbaaaa)aa
	⇒ baaaaa

Referenced by [6].

[6] baaaaa=baaaa

Overlap of [4] bbaaaa=baaa with [5] baaaaaa=baaaaa:

b baaaa baaaaaa

Critical pair: bbaaaaa=baaaaa.

Reduce LHS:

[4]	(bbaaaa)a
	⇒ baaaa

Flip LHS and RHS.

Referenced by [7].

[7] baaaa=baaa

Overlap of [4] bbaaaa=baaa with [6] baaaaa=baaaa:

b baaaa baaaaa

Critical pair: bbaaaa=baaaa.

Reduce LHS:

[4]	(bbaaaa)
	⇒ baaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[8] bbaaa=baaa

Overlap of [4] bbaaaa=baaa with [7] baaaa=baaa:

b baaaa baaaa

Critical pair: bbaaa=baaa.

Defines rule #3.