| Back: | ⟨a, b | aabbaabb=ba⟩ |
|---|
Completion settings:
Axiom: aabbaabb=ba.
Referenced by [4].
Axiom: abb=c.
Defines rule #10.
Referenced by [4], [6], [7], [12].
Axiom: ac=d.
Defines rule #5.
Overlap of [1] aabbaabb=ba with [2] abb=c:
Critical pair: acaabb=ba.
Reduce LHS:
| [3] | (ac)aabb |
| [2] | ⇒ da(abb) |
| [3] | ⇒ d(ac) |
| ⇒ dd |
Flip LHS and RHS.
Defines rule #4.
Referenced by [5], [6], [7], [9].
Overlap of [4] ba=dd with [3] ac=d:
Critical pair: bd=ddc.
Defines rule #1.
Referenced by [6], [8], [9], [10], [13].
Overlap of [2] abb=c with [4] ba=dd:
Critical pair: abdd=ca.
Reduce LHS:
| [5] | a(bd)d |
| ⇒ addcd |
Defines rule #6.
Referenced by [11].
Overlap of [4] ba=dd with [2] abb=c:
Critical pair: bc=ddbb.
Flip LHS and RHS.
Defines rule #3.
Referenced by [8], [9], [10], [11], [13].
Overlap of [5] bd=ddc with [7] ddbb=bc:
Critical pair: bbc=ddcdbb.
Defines rule #9.
Referenced by [13].
Overlap of [7] ddbb=bc with [4] ba=dd:
Critical pair: ddbdd=bca.
Reduce LHS:
| [5] | dd(bd)d |
| ⇒ ddddcd |
Flip LHS and RHS.
Defines rule #8.
Referenced by [12].
Overlap of [7] ddbb=bc with [5] bd=ddc:
Critical pair: ddbddc=bcd.
Reduce LHS:
| [5] | dd(bd)dc |
| ⇒ ddddcdc |
Flip LHS and RHS.
Defines rule #2.
Overlap of [6] addcd=ca with [7] ddbb=bc:
Critical pair: addcbc=cadbb.
Defines rule #12.
Overlap of [9] bca=ddddcd with [2] abb=c:
Critical pair: bcc=ddddcdbb.
Defines rule #7.
Overlap of [7] ddbb=bc with [8] bbc=ddcdbb:
Critical pair: ddbddcdbb=bcbc.
Reduce LHS:
| [5] | dd(bd)dcdbb |
| ⇒ ddddcdcdbb |
Flip LHS and RHS.
Defines rule #11.