Certificate for #12983 ⟨a, b | abb=aaa, baab=b⟩

Back:⟨a, b | abb=aaa, baab=b⟩

Completion settings:

[1] abb=aaa

Axiom: abb=aaa.

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

[2] baab=b

Axiom: baab=b.

Defines rule #5.

Referenced by [3], [4].

[3] aaaaab=aaa

Overlap of [1] abb=aaa with [2] baab=b:

ab b baab

Critical pair: abb=aaaaab.

Reduce LHS:

[1](abb)
⇒ aaa

Flip LHS and RHS.

Referenced by [6].

[4] bb=baaaa

Overlap of [2] baab=b with [1] abb=aaa:

ba ab abb

Critical pair: baaaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [7].

[5] aaab=aaaaaaa

Overlap of [1] abb=aaa with [4] bb=baaaa:

ab b bb

Critical pair: abbaaaa=aaab.

Reduce LHS:

[1](abb)aaaa
⇒ aaaaaaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] aaaaaaaaa=aaa

Simplify [3] aaaaab=aaa.

Reduce LHS:

[5]aa(aaab)
⇒ aaaaaaaaa

Defines rule #1.

Referenced by [8].

[7] abaaaa=aaa

Overlap of [1] abb=aaa with [4] bb=baaaa:

a bb bb

Critical pair: abaaaa=aaa.

Referenced by [8].

[8] abaaa=aaaaaaaa

Overlap of [7] abaaaa=aaa with [6] aaaaaaaaa=aaa:

ab aaaa aaaaaaaaa

Critical pair: abaaa=aaaaaaaa.

Defines rule #2.