Certificate for #12582 ⟨a, b | abba=ab, bbba=a⟩

Back:⟨a, b | abba=ab, bbba=a⟩

Completion settings:

[1] abba=ab

Axiom: abba=ab.

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

[2] bbba=a

Axiom: bbba=a.

Defines rule #3.

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

[3] abb=aa

Overlap of [1] abba=ab with [1] abba=ab:

abb a abba

Critical pair: abbab=abbba.

Reduce LHS:

[1](abba)b
⇒ abb

Reduce RHS:

[2]a(bbba)
⇒ aa

Referenced by [4].

[4] ab=aaa

Overlap of [2] bbba=a with [1] abba=ab:

bbb a abba

Critical pair: bbbab=abba.

Reduce LHS:

[2](bbba)b
⇒ ab

Reduce RHS:

[3](abb)a
⇒ aaa

Defines rule #2.

Referenced by [5], [6].

[5] aaaaaa=aaa

Overlap of [1] abba=ab with [4] ab=aaa:

abba ab

Critical pair: aaaba=ab.

Reduce LHS:

[4]aa(ab)a
⇒ aaaaaa

Reduce RHS:

[4](ab)
⇒ aaa

Referenced by [6].

[6] aaaaa=aa

Overlap of [4] ab=aaa with [2] bbba=a:

a b bbba

Critical pair: aa=aaabba.

Reduce RHS:

[4]aa(ab)ba
[4]⇒ aaaa(ab)a
[5]⇒ (aaaaaa)aa
⇒ aaaaa

Flip LHS and RHS.

Defines rule #1.