Certificate for #22807 ⟨a, b | aaa=1, abbab=bab⟩

Back:⟨a, b | aaa=1, abbab=bab⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3], [6].

[2] abbab=bab

Axiom: abbab=bab.

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

[3] bbab=aabab

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

aa a abbab

Critical pair: aabab=bbab.

Flip LHS and RHS.

Defines rule #2.

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

[4] abaabab=aabab

Overlap of [2] abbab=bab with [2] abbab=bab:

abb ab abbab

Critical pair: abbbab=babbab.

Reduce LHS:

[3]ab(bbab)
⇒ abaabab

Reduce RHS:

[2]b(abbab)
[3]⇒ (bbab)
⇒ aabab

Referenced by [6].

[5] baabab=abab

Overlap of [3] bbab=aabab with [2] abbab=bab:

bb ab abbab

Critical pair: bbbab=aababbab.

Reduce LHS:

[3]b(bbab)
⇒ baabab

Reduce RHS:

[2]aab(abbab)
[2]⇒ a(abbab)
⇒ abab

Defines rule #4.

Referenced by [6].

[6] babab=bab

Overlap of [3] bbab=aabab with [5] baabab=abab:

bba b baabab

Critical pair: bbaabab=aababaabab.

Reduce LHS:

[5]b(baabab)
⇒ babab

Reduce RHS:

[4]aab(abaabab)
[4]⇒ a(abaabab)
[1]⇒ (aaa)bab
⇒ bab

Defines rule #3.