Certificate for #13244 ⟨a, b | bab=aaa, bba=aa⟩

Completion settings:

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

[1] bab=aaa

Axiom: bab=aaa.

Defines rule #6.

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

[2] bba=aa

Axiom: bba=aa.

Defines rule #5.

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

[3] aaaab=baaaa

Overlap of [1] bab=aaa with [1] bab=aaa:

ba b bab

Critical pair: baaaa=aaaab.

Flip LHS and RHS.

Referenced by [9].

[4] aaaba=baaa

Overlap of [1] bab=aaa with [2] bba=aa:

ba b bba

Critical pair: baaa=aaaba.

Flip LHS and RHS.

Referenced by [7].

[5] aab=baaa

Overlap of [2] bba=aa with [1] bab=aaa:

b ba bab

Critical pair: baaa=aab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7], [9], [10].

[6] abaaa=baaaa

Overlap of [2] bba=aa with [5] aab=baaa:

bb a aab

Critical pair: bbbaaa=aaab.

Reduce LHS:

[2]	b(bba)aa
	⇒ baaaa

Reduce RHS:

[5]	a(aab)
	⇒ abaaa

Flip LHS and RHS.

Referenced by [7], [10], [11].

[7] baaaaa=baaa

Simplify [4] aaaba=baaa.

Reduce LHS:

[5]	a(aab)a
[6]	⇒ (abaaa)a
	⇒ baaaaa

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

[8] aaaaaa=aaaa

Overlap of [2] bba=aa with [7] baaaaa=baaa:

b ba baaaaa

Critical pair: bbaaa=aaaaaa.

Reduce LHS:

[2]	(bba)aa
	⇒ aaaa

Flip LHS and RHS.

Referenced by [9].

[9] aaaaa=aaaa

Overlap of [7] baaaaa=baaa with [5] aab=baaa:

baaaa a aab

Critical pair: baaaabaaa=baaaab.

Reduce LHS:

[3]	b(aaaab)aaa
[2]	⇒ (bba)aaaaaa
[8]	⇒ (aaaaaa)aa
[8]	⇒ (aaaaaa)
	⇒ aaaa

Reduce RHS:

[3]	b(aaaab)
[2]	⇒ (bba)aaa
	⇒ aaaaa

Flip LHS and RHS.

Defines rule #1.

[10] baaaa=baaa

Overlap of [5] aab=baaa with [7] baaaaa=baaa:

aa b baaaaa

Critical pair: aabaaa=baaaaaaaa.

Reduce LHS:

[6]	a(abaaa)
[6]	⇒ (abaaa)a
[7]	⇒ (baaaaa)
	⇒ baaa

Reduce RHS:

[7]	(baaaaa)aaa
[7]	⇒ (baaaaa)a
	⇒ baaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

[11] abaaa=baaa

Simplify [6] abaaa=baaaa.

Reduce RHS:

[10]	(baaaa)
	⇒ baaa

Defines rule #3.