Certificate for #12441 ⟨a, b | aabb=aa, baab=b⟩

Back:⟨a, b | aabb=aa, baab=b⟩

Completion settings:

[1] aabb=aa

Axiom: aabb=aa.

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

[2] baab=b

Axiom: baab=b.

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

[3] aaaab=aa

Overlap of [1] aabb=aa with [2] baab=b:

aab b baab

Critical pair: aabb=aaaab.

Reduce LHS:

[1](aabb)
⇒ aa

Flip LHS and RHS.

Referenced by [6], [7], [8].

[4] bb=baa

Overlap of [2] baab=b with [1] aabb=aa:

b aab aabb

Critical pair: baa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] baaaa=b

Overlap of [4] bb=baa with [4] bb=baa:

b b bb

Critical pair: bbaa=baab.

Reduce LHS:

[4](bb)aa
⇒ baaaa

Reduce RHS:

[2](baab)
⇒ b

Defines rule #2.

Referenced by [7], [8].

[6] aab=aaaa

Overlap of [3] aaaab=aa with [1] aabb=aa:

aa aab aabb

Critical pair: aaaa=aab.

Flip LHS and RHS.

Defines rule #3.

[7] aaaaaa=aa

Overlap of [3] aaaab=aa with [5] baaaa=b:

aaaa b baaaa

Critical pair: aaaab=aaaaaa.

Reduce LHS:

[3](aaaab)
⇒ aa

Flip LHS and RHS.

Defines rule #1.

[8] bab=baaa

Overlap of [5] baaaa=b with [3] aaaab=aa:

ba aaa aaaab

Critical pair: baaa=bab.

Flip LHS and RHS.

Defines rule #5.