Certificate for #14357 ⟨a, b | aaaa=a, baaab=a⟩

Back:⟨a, b | aaaa=a, baaab=a⟩

Completion settings:

[1] aaaa=a

Axiom: aaaa=a.

Defines rule #3.

Referenced by [3], [4].

[2] baaab=a

Axiom: baaab=a.

Referenced by [3], [4].

[3] ba=ab

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

baaa b baaab

Critical pair: baaaa=aaaab.

Reduce LHS:

[1]b(aaaa)
⇒ ba

Reduce RHS:

[1](aaaa)b
⇒ ab

Defines rule #1.

Referenced by [4].

[4] abb=aa

Overlap of [2] baaab=a with [3] ba=ab:

baaa b ba

Critical pair: baaaab=aa.

Reduce LHS:

[3](ba)aaab
[3]⇒ a(ba)aab
[3]⇒ aa(ba)ab
[3]⇒ aaa(ba)b
[1]⇒ (aaaa)bb
⇒ abb

Defines rule #2.