Certificate for #20248 ⟨a, b | aba=b, aaaa=aaa

Completion settings:

[1] aba=b

Axiom: aba=b.

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

[2] aaaa=aaa

Axiom: aaaa=aaa.

Defines rule #3.

Referenced by [3].

[3] aaab=aab

Overlap of [2] aaaa=aaa with [1] aba=b:

aaa a aba

Critical pair: aaab=aaaba.

Reduce RHS:

[1]aa(aba)
aab

Referenced by [4].

[4] aab=ab

Overlap of [3] aaab=aab with [1] aba=b:

aa ab aba

Critical pair: aab=aaba.

Reduce RHS:

[1]a(aba)
ab

Referenced by [5].

[5] ab=b

Overlap of [4] aab=ab with [1] aba=b:

a ab aba

Critical pair: ab=aba.

Reduce RHS:

[1](aba)
b

Defines rule #1.

Referenced by [6].

[6] ba=b

Overlap of [1] aba=b with [5] ab=b:

aba ab

Critical pair: ba=b.

Defines rule #2.