| Back: | ⟨a, b | aabbbaab=baa⟩ |
|---|
Completion settings:
Axiom: aabbbaab=baa.
Referenced by [4].
Axiom: aa=c.
Defines rule #9.
Axiom: bbbc=d.
Simplify [1] aabbbaab=baa.
Reduce RHS:
| [2] | b(aa) |
| ⇒ bc |
Referenced by [5].
Overlap of [4] aabbbaab=bc with [2] aa=c:
Critical pair: cbbbaab=bc.
Reduce LHS:
| [2] | cbbb(aa)b |
| [3] | ⇒ c(bbbc)b |
| ⇒ cdb |
Flip LHS and RHS.
Defines rule #3.
Referenced by [6], [8], [9], [10], [11], [12], [15].
Overlap of [3] bbbc=d with [5] bc=cdb:
Critical pair: bbcdb=d.
Reduce LHS:
| [5] | b(bc)db |
| [5] | ⇒ (bc)dbdb |
| ⇒ cdbdbdb |
Defines rule #2.
Referenced by [10], [11], [13], [14], [15], [16].
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 [9].
Overlap of [5] bc=cdb with [8] cdba=bac:
Critical pair: bbac=cdbdba.
Flip LHS and RHS.
Defines rule #8.
Referenced by [15].
Overlap of [5] bc=cdb with [6] cdbdbdb=d:
Critical pair: bd=cdbdbdbdb.
Reduce RHS:
| [6] | (cdbdbdb)db |
| ⇒ ddb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [6] cdbdbdb=d with [5] bc=cdb:
Critical pair: cdbdbdcdb=dc.
Referenced by [16].
Overlap of [10] ddb=bd with [5] bc=cdb:
Critical pair: ddcdb=bdc.
Overlap of [12] ddcdb=bdc with [6] cdbdbdb=d:
Critical pair: ddd=bdcdbdb.
Flip LHS and RHS.
Referenced by [14].
Overlap of [6] cdbdbdb=d with [13] bdcdbdb=ddd:
Critical pair: cdbdbdddd=ddcdbdb.
Reduce RHS:
| [12] | (ddcdb)db |
| ⇒ bdcdb |
Flip LHS and RHS.
Referenced by [16].
Overlap of [5] bc=cdb with [9] cdbdba=bbac:
Critical pair: bbbac=cdbdbdba.
Reduce RHS:
| [6] | (cdbdbdb)a |
| ⇒ da |
Flip LHS and RHS.
Defines rule #5.
Overlap of [11] cdbdbdcdb=dc with [14] bdcdb=cdbdbdddd:
Critical pair: cdbdcdbdbdddd=dc.
Reduce LHS:
| [14] | cd(bdcdb)dbdddd |
| [10] | ⇒ cdcdbdbddd(ddb)dddd |
| [10] | ⇒ cdcdbdbd(ddb)ddddd |
| [6] | ⇒ cd(cdbdbdb)dddddd |
| ⇒ cdddddddd |
Flip LHS and RHS.
Defines rule #4.