| Back: | ⟨a, b, c | ba=ab, acca=1⟩ |
|---|
Completion settings:
Axiom: ba=ab.
Defines rule #3.
Referenced by [8].
Axiom: acca=1.
Referenced by [4].
Axiom: cc=d.
Defines rule #5.
Overlap of [2] acca=1 with [3] cc=d:
Critical pair: ada=1.
Overlap of [3] cc=d with [3] cc=d:
Critical pair: cd=dc.
Defines rule #4.
Referenced by [9].
Overlap of [4] ada=1 with [4] ada=1:
Critical pair: ad=da.
Defines rule #1.
Referenced by [7], [8], [10], [13].
Overlap of [4] ada=1 with [6] ad=da:
Critical pair: daa=1.
Defines rule #6.
Referenced by [9], [11], [12], [13].
Overlap of [1] ba=ab with [6] ad=da:
Critical pair: bda=abd.
Referenced by [11].
Overlap of [5] cd=dc with [7] daa=1:
Critical pair: c=dcaa.
Flip LHS and RHS.
Referenced by [10].
Overlap of [6] ad=da with [9] dcaa=c:
Critical pair: ac=dacaa.
Flip LHS and RHS.
Referenced by [13].
Overlap of [8] bda=abd with [7] daa=1:
Critical pair: b=abda.
Reduce RHS:
| [8] | a(bda) |
| ⇒ aabd |
Flip LHS and RHS.
Referenced by [12].
Overlap of [7] daa=1 with [11] aabd=b:
Critical pair: db=bd.
Flip LHS and RHS.
Defines rule #2.
Overlap of [6] ad=da with [10] dacaa=ac:
Critical pair: aac=daacaa.
Reduce RHS:
| [7] | (daa)caa |
| ⇒ caa |
Flip LHS and RHS.
Defines rule #7.