| Back: | ⟨a, b | abaaaaabaab=1⟩ |
|---|
Completion settings:
Axiom: abaaaaabaab=1.
Referenced by [3].
Axiom: aba=c.
Referenced by [3], [4], [5], [8], [9], [11], [14], [16], [17], [18], [23].
Overlap of [1] abaaaaabaab=1 with [2] aba=c:
Critical pair: caaaabaab=1.
Reduce LHS:
| [2] | caaa(aba)ab |
| ⇒ caaacab |
Defines rule #3.
Referenced by [5], [6], [10], [12], [15], [19], [20], [21], [22].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Flip LHS and RHS.
Referenced by [9], [14], [18], [22].
Overlap of [3] caaacab=1 with [2] aba=c:
Critical pair: caaacc=a.
Defines rule #1.
Referenced by [6], [7], [8], [9], [15], [19], [20].
Overlap of [5] caaacc=a with [3] caaacab=1:
Critical pair: caaac=aaaacab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [15].
Overlap of [5] caaacc=a with [5] caaacc=a:
Critical pair: caaaca=aaaacc.
Flip LHS and RHS.
Defines rule #2.
Referenced by [8], [9], [20], [22].
Overlap of [2] aba=c with [7] aaaacc=caaaca:
Critical pair: abcaaaca=caaacc.
Reduce RHS:
| [5] | (caaacc) |
| ⇒ a |
Referenced by [11], [12], [13], [16].
Overlap of [4] cba=abc with [7] aaaacc=caaaca:
Critical pair: cbcaaaca=abcaaacc.
Reduce RHS:
| [5] | ab(caaacc) |
| [2] | ⇒ (aba) |
| ⇒ c |
Overlap of [9] cbcaaaca=c with [3] caaacab=1:
Critical pair: cbcaaa=caacab.
Referenced by [11], [17], [20].
Overlap of [2] aba=c with [8] abcaaaca=a:
Critical pair: aba=cbcaaaca.
Reduce LHS:
| [2] | (aba) |
| ⇒ c |
Reduce RHS:
| [10] | (cbcaaa)ca |
| ⇒ caacabca |
Flip LHS and RHS.
Overlap of [8] abcaaaca=a with [3] caaacab=1:
Critical pair: abcaaa=aaacab.
Referenced by [13], [15], [16].
Overlap of [8] abcaaaca=a with [11] caacabca=c:
Critical pair: abcaaac=aacabca.
Reduce LHS:
| [12] | (abcaaa)c |
| ⇒ aaacabc |
Flip LHS and RHS.
Referenced by [15].
Overlap of [11] caacabca=c with [2] aba=c:
Critical pair: caacabcc=cba.
Reduce RHS:
| [4] | (cba) |
| ⇒ abc |
Referenced by [15].
Overlap of [14] caacabcc=abc with [3] caaacab=1:
Critical pair: caacabc=abcaaacab.
Reduce RHS:
| [12] | (abcaaa)cab |
| [13] | ⇒ a(aacabca)b |
| [6] | ⇒ (aaaacab)cb |
| [5] | ⇒ (caaacc)b |
| ⇒ ab |
Referenced by [16], [17], [18].
Overlap of [8] abcaaaca=a with [15] caacabc=ab:
Critical pair: abcaaaab=aacabc.
Reduce LHS:
| [12] | (abcaaa)ab |
| [2] | ⇒ aaac(aba)b |
| ⇒ aaaccb |
Flip LHS and RHS.
Overlap of [9] cbcaaaca=c with [15] caacabc=ab:
Critical pair: cbcaaaab=cacabc.
Reduce LHS:
| [10] | (cbcaaa)ab |
| [2] | ⇒ caac(aba)b |
| ⇒ caaccb |
Flip LHS and RHS.
Referenced by [22].
Overlap of [15] caacabc=ab with [4] cba=abc:
Critical pair: caacababc=abba.
Reduce LHS:
| [2] | caac(aba)bc |
| ⇒ caaccbc |
Flip LHS and RHS.
Referenced by [19].
Overlap of [3] caaacab=1 with [18] abba=caaccbc:
Critical pair: caaaccaaccbc=ba.
Reduce LHS:
| [5] | (caaacc)aaccbc |
| ⇒ aaaccbc |
Flip LHS and RHS.
Overlap of [19] ba=aaaccbc with [7] aaaacc=caaaca:
Critical pair: bcaaaca=aaaccbcaaacc.
Reduce RHS:
| [10] | aaac(cbcaaa)cc |
| [16] | ⇒ aaacc(aacabc)c |
| [5] | ⇒ aaac(caaacc)bc |
| [16] | ⇒ a(aacabc) |
| [7] | ⇒ (aaaacc)b |
| [3] | ⇒ (caaacab) |
| ⇒ 1 |
Referenced by [21], [22], [23].
Overlap of [20] bcaaaca=1 with [3] caaacab=1:
Critical pair: bcaaa=aacab.
Overlap of [20] bcaaaca=1 with [17] cacabc=caaccb:
Critical pair: bcaaacaaccb=cabc.
Reduce LHS:
| [21] | (bcaaa)caaccb |
| [16] | ⇒ (aacabc)aaccb |
| [4] | ⇒ aaac(cba)accb |
| [16] | ⇒ a(aacabc)accb |
| [7] | ⇒ (aaaacc)baccb |
| [3] | ⇒ (caaacab)accb |
| ⇒ accb |
Flip LHS and RHS.
Referenced by [23].
Overlap of [20] bcaaaca=1 with [22] cabc=accb:
Critical pair: bcaaaaccb=bc.
Reduce LHS:
| [21] | (bcaaa)accb |
| [2] | ⇒ aac(aba)ccb |
| ⇒ aaccccb |
Flip LHS and RHS.
Defines rule #5.
Referenced by [24].
Simplify [19] ba=aaaccbc.
Reduce RHS:
| [23] | aaacc(bc) |
| ⇒ aaaccaaccccb |
Defines rule #6.