| Back: | ⟨a, b, c | aab=ba, abc=1⟩ |
|---|
Completion settings:
Axiom: aab=ba.
Flip LHS and RHS.
Referenced by [6], [7], [8], [13], [15].
Axiom: abc=1.
Referenced by [5].
Axiom: bc=d.
Referenced by [5], [9], [14], [17].
Axiom: aaaab=e.
Referenced by [7], [8], [9], [10], [13].
Overlap of [2] abc=1 with [3] bc=d:
Critical pair: ad=1.
Defines rule #1.
Referenced by [6], [9], [11], [14].
Overlap of [1] ba=aab with [5] ad=1:
Critical pair: b=aabd.
Flip LHS and RHS.
Overlap of [1] ba=aab with [4] aaaab=e:
Critical pair: be=aabaaab.
Reduce RHS:
| [1] | aa(ba)aab |
| [4] | ⇒ (aaaab)aab |
| ⇒ eaab |
Flip LHS and RHS.
Referenced by [18].
Overlap of [4] aaaab=e with [1] ba=aab:
Critical pair: aaaaaab=ea.
Reduce LHS:
| [4] | aa(aaaab) |
| ⇒ aae |
Flip LHS and RHS.
Defines rule #2.
Referenced by [11].
Overlap of [4] aaaab=e with [3] bc=d:
Critical pair: aaaad=ec.
Reduce LHS:
| [5] | aaa(ad) |
| ⇒ aaa |
Flip LHS and RHS.
Defines rule #3.
Overlap of [4] aaaab=e with [6] aabd=b:
Critical pair: aab=ed.
Referenced by [12], [13], [14], [15], [19].
Overlap of [8] ea=aae with [5] ad=1:
Critical pair: e=aaed.
Flip LHS and RHS.
Defines rule #4.
Overlap of [6] aabd=b with [10] aab=ed:
Critical pair: edd=b.
Flip LHS and RHS.
Defines rule #9.
Referenced by [16], [17], [18].
Overlap of [10] aab=ed with [1] ba=aab:
Critical pair: aaaab=eda.
Reduce LHS:
| [4] | (aaaab) |
| ⇒ e |
Flip LHS and RHS.
Defines rule #5.
Overlap of [10] aab=ed with [3] bc=d:
Critical pair: aad=edc.
Reduce LHS:
| [5] | a(ad) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #6.
Simplify [1] ba=aab.
Reduce RHS:
| [10] | (aab) |
| ⇒ ed |
Referenced by [16].
Overlap of [15] ba=ed with [12] b=edd:
Critical pair: edda=ed.
Defines rule #7.
Overlap of [3] bc=d with [12] b=edd:
Critical pair: eddc=d.
Defines rule #8.
Simplify [7] eaab=be.
Reduce RHS:
| [12] | (b)e |
| ⇒ edde |
Referenced by [19].
Overlap of [18] eaab=edde with [10] aab=ed:
Critical pair: eed=edde.
Defines rule #10.