Certificate for #5715 ⟨a, b | aaaa=1, ababb=b⟩

Back:⟨a, b | aaaa=1, ababb=b⟩

Completion settings:

[1] aaaa=1

Axiom: aaaa=1.

Defines rule #1.

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

[2] ababb=b

Axiom: ababb=b.

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

[3] babb=aaab

Overlap of [1] aaaa=1 with [2] ababb=b:

aaa a ababb

Critical pair: aaab=babb.

Flip LHS and RHS.

Defines rule #2.

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

[4] ababaaab=aaab

Overlap of [2] ababb=b with [3] babb=aaab:

abab b babb

Critical pair: ababaaab=babb.

Reduce RHS:

[3](babb)
⇒ aaab

Referenced by [6], [7].

[5] babaaab=aab

Overlap of [3] babb=aaab with [3] babb=aaab:

bab b babb

Critical pair: babaaab=aaababb.

Reduce RHS:

[2]aa(ababb)
⇒ aab

Defines rule #5.

Referenced by [6], [7].

[6] babaab=ab

Overlap of [3] babb=aaab with [5] babaaab=aab:

bab b babaaab

Critical pair: babaab=aaababaaab.

Reduce RHS:

[4]aa(ababaaab)
[1]⇒ (aaaa)ab
⇒ ab

Defines rule #4.

[7] babab=b

Overlap of [5] babaaab=aab with [5] babaaab=aab:

babaaa b babaaab

Critical pair: babaaaaab=aababaaab.

Reduce LHS:

[1]bab(aaaa)ab
⇒ babab

Reduce RHS:

[4]a(ababaaab)
[1]⇒ (aaaa)b
⇒ b

Defines rule #3.