Certificate for #6633 ⟨a, b | aab=a, baaa=bb

Completion settings:

[1] aab=a

Axiom: aab=a.

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

[2] bb=baaa

Axiom: baaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] ab=aaaa

Overlap of [1] aab=a with [2] bb=baaa:

aa b bb

Critical pair: aabaaa=ab.

Reduce LHS:

[1](aab)aaa
aaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] aaaaaaa=aaa

Overlap of [3] ab=aaaa with [2] bb=baaa:

a b bb

Critical pair: abaaa=aaaab.

Reduce LHS:

[3](ab)aaa
aaaaaaa

Reduce RHS:

[1]aa(aab)
aaa

Referenced by [5].

[5] aaaaaa=aa

Overlap of [4] aaaaaaa=aaa with [1] aab=a:

aaaaa aa aab

Critical pair: aaaaaa=aaab.

Reduce RHS:

[1]a(aab)
aa

Referenced by [6].

[6] aaaaa=a

Overlap of [5] aaaaaa=aa with [1] aab=a:

aaaa aa aab

Critical pair: aaaaa=aab.

Reduce RHS:

[1](aab)
a

Defines rule #1.