Certificate for #12232 ⟨a, b | aaab=aa, babb=a⟩

Back:⟨a, b | aaab=aa, babb=a⟩

Completion settings:

[1] aaab=aa

Axiom: aaab=aa.

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

[2] babb=a

Axiom: babb=a.

Defines rule #5.

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

[3] aabb=baba

Overlap of [2] babb=a with [2] babb=a:

bab b babb

Critical pair: baba=aabb.

Flip LHS and RHS.

Referenced by [5].

[4] aab=aaaa

Overlap of [1] aaab=aa with [2] babb=a:

aaa b babb

Critical pair: aaaa=aaabb.

Reduce RHS:

[1](aaab)b
⇒ aab

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [7].

[5] baba=aaa

Simplify [3] aabb=baba.

Reduce LHS:

[4](aab)b
[1]⇒ a(aaab)
⇒ aaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] aaaaaa=aaa

Overlap of [1] aaab=aa with [5] baba=aaa:

aaa b baba

Critical pair: aaaaaa=aaaba.

Reduce RHS:

[1](aaab)a
⇒ aaa

Referenced by [8].

[7] baa=aaaa

Overlap of [5] baba=aaa with [2] babb=a:

ba ba babb

Critical pair: baa=aaabb.

Reduce RHS:

[1](aaab)b
[4]⇒ (aab)
⇒ aaaa

Defines rule #2.

Referenced by [8].

[8] aaaaa=aa

Overlap of [7] baa=aaaa with [1] aaab=aa:

ba a aaab

Critical pair: baaa=aaaaaab.

Reduce LHS:

[7](baa)a
⇒ aaaaa

Reduce RHS:

[6](aaaaaa)b
[1]⇒ (aaab)
⇒ aa

Defines rule #1.