Certificate for #25210 ⟨a, b | aa=a, abbba=bab⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abbba=bab

Axiom: abbba=bab.

Defines rule #5.

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

[3] abab=bab

Overlap of [1] aa=a with [2] abbba=bab:

a a abbba

Critical pair: abab=abbba.

Reduce RHS:

[2]	(abbba)
	⇒ bab

Defines rule #2.

Referenced by [5], [6].

[4] baba=bab

Overlap of [2] abbba=bab with [1] aa=a:

abbb a aa

Critical pair: abbba=baba.

Reduce LHS:

[2]	(abbba)
	⇒ bab

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7].

[5] abbab=bbab

Overlap of [3] abab=bab with [2] abbba=bab:

ab ab abbba

Critical pair: abbab=babbba.

Reduce RHS:

[2]	b(abbba)
	⇒ bbab

Referenced by [6], [8].

[6] bbab=babb

Overlap of [3] abab=bab with [3] abab=bab:

ab ab abab

Critical pair: abbab=babab.

Reduce LHS:

[5]	(abbab)
	⇒ bbab

Reduce RHS:

[4]	(baba)b
	⇒ babb

Defines rule #4.

Referenced by [8].

[7] babba=babb

Overlap of [2] abbba=bab with [4] baba=bab:

abb ba baba

Critical pair: abbbab=babba.

Reduce LHS:

[2]	(abbba)b
	⇒ babb

Flip LHS and RHS.

Defines rule #6.

[8] babbb=babb

Overlap of [2] abbba=bab with [6] bbab=babb:

ab bba bbab

Critical pair: abbabb=babb.

Reduce LHS:

[5]	(abbab)b
[6]	⇒ (bbab)b
	⇒ babbb

Defines rule #7.