Certificate for #12280 ⟨a, b | aaab=ba, abbb=a

Completion settings:

[1] ba=aaab

Axiom: aaab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] abbb=a

Axiom: abbb=a.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaaaaaaaaaaaaaa=aa

Overlap of [2] abbb=a with [1] ba=aaab:

abb b ba

Critical pair: abbaaab=aa.

Reduce LHS:

[1]ab(ba)aab
[1]a(ba)aabaab
[1]aaaa(ba)abaab
[1]aaaaaaa(ba)baab
[1]aaaaaaaaaab(ba)ab
[1]aaaaaaaaaa(ba)aabab
[1]aaaaaaaaaaaaa(ba)abab
[1]aaaaaaaaaaaaaaaa(ba)bab
[1]aaaaaaaaaaaaaaaaaaab(ba)b
[1]aaaaaaaaaaaaaaaaaaa(ba)aabb
[1]aaaaaaaaaaaaaaaaaaaaaa(ba)abb
[1]aaaaaaaaaaaaaaaaaaaaaaaaa(ba)bb
[2]aaaaaaaaaaaaaaaaaaaaaaaaaaa(abbb)
aaaaaaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.