| Back: | ⟨a, b, c | aab=1, abca=c⟩ |
|---|
Completion settings:
Axiom: aab=1.
Referenced by [5].
Axiom: abca=c.
Referenced by [6].
Axiom: cb=d.
Defines rule #11.
Referenced by [9], [13], [15].
Axiom: ab=e.
Defines rule #12.
Referenced by [5], [6], [9], [15].
Overlap of [1] aab=1 with [4] ab=e:
Critical pair: ae=1.
Defines rule #7.
Overlap of [2] abca=c with [4] ab=e:
Critical pair: eca=c.
Overlap of [5] ae=1 with [6] eca=c:
Critical pair: ac=ca.
Defines rule #5.
Overlap of [6] eca=c with [5] ae=1:
Critical pair: ec=ce.
Referenced by [11].
Overlap of [7] ac=ca with [3] cb=d:
Critical pair: ad=cab.
Reduce RHS:
| [4] | c(ab) |
| ⇒ ce |
Flip LHS and RHS.
Defines rule #4.
Referenced by [10], [11], [14].
Overlap of [7] ac=ca with [9] ce=ad:
Critical pair: aad=cae.
Reduce RHS:
| [5] | c(ae) |
| ⇒ c |
Defines rule #6.
Simplify [8] ec=ce.
Reduce RHS:
| [9] | (ce) |
| ⇒ ad |
Defines rule #8.
Referenced by [12], [13], [14], [16], [18].
Overlap of [6] eca=c with [11] ec=ad:
Critical pair: ada=c.
Referenced by [15], [16], [18].
Overlap of [11] ec=ad with [3] cb=d:
Critical pair: ed=adb.
Flip LHS and RHS.
Referenced by [20].
Overlap of [11] ec=ad with [9] ce=ad:
Critical pair: ead=ade.
Referenced by [17].
Overlap of [12] ada=c with [4] ab=e:
Critical pair: ade=cb.
Reduce RHS:
| [3] | (cb) |
| ⇒ d |
Referenced by [16], [17], [19].
Overlap of [15] ade=d with [11] ec=ad:
Critical pair: adad=dc.
Reduce LHS:
| [12] | (ada)d |
| ⇒ cd |
Flip LHS and RHS.
Defines rule #1.
Simplify [14] ead=ade.
Reduce RHS:
| [15] | (ade) |
| ⇒ d |
Defines rule #9.
Referenced by [18], [19], [20].
Overlap of [17] ead=d with [12] ada=c:
Critical pair: ec=da.
Reduce LHS:
| [11] | (ec) |
| ⇒ ad |
Flip LHS and RHS.
Defines rule #2.
Overlap of [17] ead=d with [15] ade=d:
Critical pair: ed=de.
Flip LHS and RHS.
Defines rule #3.
Overlap of [17] ead=d with [13] adb=ed:
Critical pair: eed=db.
Flip LHS and RHS.
Defines rule #10.