Certificate for #19156 ⟨a, b | aba=a, bbabbb=a⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

Defines rule #2.

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

[2] bbabbb=a

Axiom: bbabbb=a.

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

[3] aabbb=bba

Overlap of [2] bbabbb=a with [2] bbabbb=a:

bbab bb bbabbb

Critical pair: bbaba=aabbb.

Reduce LHS:

[1]	bb(aba)
	⇒ bba

Flip LHS and RHS.

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

[4] bbbba=aa

Overlap of [3] aabbb=bba with [2] bbabbb=a:

aab bb bbabbb

Critical pair: aaba=bbaabbb.

Reduce LHS:

[1]	a(aba)
	⇒ aa

Reduce RHS:

[3]	bb(aabbb)
	⇒ bbbba

Flip LHS and RHS.

Referenced by [7].

[5] aabba=a

Overlap of [3] aabbb=bba with [2] bbabbb=a:

aabb b bbabbb

Critical pair: aabba=bbababbb.

Reduce RHS:

[1]	bb(aba)bbb
[2]	⇒ (bbabbb)
	⇒ a

Referenced by [6], [8].

[6] abbb=aaa

Overlap of [5] aabba=a with [2] bbabbb=a:

aa bba bbabbb

Critical pair: aaa=abbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[7] bba=aaaa

Overlap of [3] aabbb=bba with [4] bbbba=aa:

aa bbb bbbba

Critical pair: aaaa=bbaba.

Reduce RHS:

[1]	bb(aba)
	⇒ bba

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] aaaaaa=a

Overlap of [7] bba=aaaa with [6] abbb=aaa:

bb a abbb

Critical pair: bbaaa=aaaabbb.

Reduce LHS:

[7]	(bba)aa
	⇒ aaaaaa

Reduce RHS:

[3]	aa(aabbb)
[5]	⇒ (aabba)
	⇒ a

Defines rule #1.