| Back: | ⟨a, b | abaabbabaab=1⟩ |
|---|
Completion settings:
Axiom: abaabbabaab=1.
Referenced by [3].
Axiom: babaa=c.
Referenced by [3], [4], [5], [6], [18].
Overlap of [1] abaabbabaab=1 with [2] babaa=c:
Critical pair: abaabcb=1.
Referenced by [4], [5], [7], [9].
Overlap of [2] babaa=c with [3] abaabcb=1:
Critical pair: b=cbcb.
Flip LHS and RHS.
Overlap of [3] abaabcb=1 with [2] babaa=c:
Critical pair: abaabcc=abaa.
Referenced by [10].
Overlap of [4] cbcb=b with [2] babaa=c:
Critical pair: cbcc=babaa.
Reduce RHS:
| [2] | (babaa) |
| ⇒ c |
Overlap of [3] abaabcb=1 with [6] cbcc=c:
Critical pair: abaabc=cc.
Overlap of [4] cbcb=b with [6] cbcc=c:
Critical pair: cbc=bcc.
Flip LHS and RHS.
Overlap of [3] abaabcb=1 with [7] abaabc=cc:
Critical pair: ccb=1.
Defines rule #2.
Referenced by [11], [12], [13], [14], [15], [16], [19], [21], [25], [26], [27], [28], [29], [31].
Overlap of [5] abaabcc=abaa with [7] abaabc=cc:
Critical pair: ccc=abaa.
Flip LHS and RHS.
Defines rule #7.
Referenced by [12], [16], [27].
Overlap of [8] bcc=cbc with [9] ccb=1:
Critical pair: bc=cbccb.
Reduce RHS:
| [8] | c(bcc)b |
| [9] | ⇒ (ccb)cb |
| ⇒ cb |
Defines rule #1.
Referenced by [14], [15], [16], [22], [23], [24], [25], [27], [30].
Overlap of [10] abaa=ccc with [10] abaa=ccc:
Critical pair: abaccc=cccbaa.
Reduce RHS:
| [9] | c(ccb)aa |
| ⇒ caa |
Referenced by [13].
Overlap of [12] abaccc=caa with [9] ccb=1:
Critical pair: abac=caab.
Defines rule #4.
Referenced by [14], [17], [24].
Overlap of [13] abac=caab with [9] ccb=1:
Critical pair: aba=caabcb.
Reduce RHS:
| [11] | caa(bc)b |
| ⇒ caacbb |
Flip LHS and RHS.
Referenced by [15].
Overlap of [8] bcc=cbc with [14] caacbb=aba:
Critical pair: bcaba=cbcaacbb.
Reduce LHS:
| [11] | (bc)aba |
| ⇒ cbaba |
Reduce RHS:
| [11] | c(bc)aacbb |
| [9] | ⇒ (ccb)aacbb |
| ⇒ aacbb |
Flip LHS and RHS.
Overlap of [10] abaa=ccc with [15] aacbb=cbaba:
Critical pair: abcbaba=ccccbb.
Reduce LHS:
| [11] | a(bc)baba |
| ⇒ acbbaba |
Reduce RHS:
| [9] | cc(ccb)b |
| [9] | ⇒ (ccb) |
| ⇒ 1 |
Overlap of [13] abac=caab with [16] acbbaba=1:
Critical pair: ab=caabbbaba.
Flip LHS and RHS.
Referenced by [23].
Overlap of [16] acbbaba=1 with [2] babaa=c:
Critical pair: acbbac=baa.
Defines rule #5.
Referenced by [19], [20], [25].
Overlap of [18] acbbac=baa with [9] ccb=1:
Critical pair: acbba=baacb.
Flip LHS and RHS.
Overlap of [18] acbbac=baa with [18] acbbac=baa:
Critical pair: acbbbaa=baabbac.
Flip LHS and RHS.
Referenced by [29].
Overlap of [9] ccb=1 with [19] baacb=acbba:
Critical pair: ccacbba=aacb.
Flip LHS and RHS.
Defines rule #6.
Overlap of [19] baacb=acbba with [15] aacbb=cbaba:
Critical pair: bcbaba=acbbab.
Reduce LHS:
| [11] | (bc)baba |
| ⇒ cbbaba |
Flip LHS and RHS.
Defines rule #3.
Overlap of [11] bc=cb with [17] caabbbaba=ab:
Critical pair: bab=cbaabbbaba.
Flip LHS and RHS.
Referenced by [26].
Overlap of [13] abac=caab with [22] acbbab=cbbaba:
Critical pair: abcbbaba=caabbbab.
Reduce LHS:
| [11] | a(bc)bbaba |
| ⇒ acbbbaba |
Flip LHS and RHS.
Referenced by [30].
Overlap of [18] acbbac=baa with [22] acbbab=cbbaba:
Critical pair: acbbcbbaba=baabbab.
Reduce LHS:
| [11] | acb(bc)bbaba |
| [11] | ⇒ ac(bc)bbbaba |
| [9] | ⇒ a(ccb)bbbaba |
| ⇒ abbbaba |
Flip LHS and RHS.
Referenced by [28].
Overlap of [9] ccb=1 with [23] cbaabbbaba=bab:
Critical pair: cbab=aabbbaba.
Flip LHS and RHS.
Referenced by [27].
Overlap of [26] aabbbaba=cbab with [10] abaa=ccc:
Critical pair: aabbbabccc=cbabbaa.
Reduce LHS:
| [11] | aabbba(bc)cc |
| [11] | ⇒ aabbbac(bc)c |
| [9] | ⇒ aabbba(ccb)c |
| ⇒ aabbbac |
Defines rule #11.
Overlap of [9] ccb=1 with [25] baabbab=abbbaba:
Critical pair: ccabbbaba=aabbab.
Flip LHS and RHS.
Defines rule #8.
Overlap of [9] ccb=1 with [20] baabbac=acbbbaa:
Critical pair: ccacbbbaa=aabbac.
Flip LHS and RHS.
Defines rule #10.
Overlap of [11] bc=cb with [24] caabbbab=acbbbaba:
Critical pair: bacbbbaba=cbaabbbab.
Flip LHS and RHS.
Referenced by [31].
Overlap of [9] ccb=1 with [30] cbaabbbab=bacbbbaba:
Critical pair: cbacbbbaba=aabbbab.
Flip LHS and RHS.
Defines rule #9.