| Back: | ⟨a, b | aabbaab=baa⟩ |
|---|
Completion settings:
Axiom: aabbaab=baa.
Referenced by [4].
Axiom: aa=c.
Defines rule #8.
Axiom: bbc=d.
Simplify [1] aabbaab=baa.
Reduce RHS:
| [2] | b(aa) |
| ⇒ bc |
Referenced by [5].
Overlap of [4] aabbaab=bc with [2] aa=c:
Critical pair: cbbaab=bc.
Reduce LHS:
| [2] | cbb(aa)b |
| [3] | ⇒ c(bbc)b |
| ⇒ cdb |
Flip LHS and RHS.
Defines rule #3.
Referenced by [6], [8], [9], [10], [11], [12].
Overlap of [3] bbc=d with [5] bc=cdb:
Critical pair: bcdb=d.
Reduce LHS:
| [5] | (bc)db |
| ⇒ cdbdb |
Defines rule #2.
Referenced by [9], [10], [12], [13], [14], [15].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #6.
Referenced by [8].
Overlap of [5] bc=cdb with [7] ca=ac:
Critical pair: bac=cdba.
Flip LHS and RHS.
Defines rule #7.
Referenced by [12].
Overlap of [5] bc=cdb with [6] cdbdb=d:
Critical pair: bd=cdbdbdb.
Reduce RHS:
| [6] | (cdbdb)db |
| ⇒ ddb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [6] cdbdb=d with [5] bc=cdb:
Critical pair: cdbdcdb=dc.
Referenced by [15].
Overlap of [9] ddb=bd with [5] bc=cdb:
Critical pair: ddcdb=bdc.
Overlap of [5] bc=cdb with [8] cdba=bac:
Critical pair: bbac=cdbdba.
Reduce RHS:
| [6] | (cdbdb)a |
| ⇒ da |
Flip LHS and RHS.
Defines rule #5.
Overlap of [11] ddcdb=bdc with [6] cdbdb=d:
Critical pair: ddd=bdcdb.
Flip LHS and RHS.
Referenced by [14].
Overlap of [6] cdbdb=d with [13] bdcdb=ddd:
Critical pair: cdbdddd=ddcdb.
Reduce RHS:
| [11] | (ddcdb) |
| ⇒ bdc |
Flip LHS and RHS.
Referenced by [15].
Simplify [10] cdbdcdb=dc.
Reduce LHS:
| [14] | cd(bdc)db |
| [9] | ⇒ cdcdbddd(ddb) |
| [9] | ⇒ cdcdbd(ddb)d |
| [6] | ⇒ cd(cdbdb)dd |
| ⇒ cdddd |
Flip LHS and RHS.
Defines rule #4.