| Back: | ⟨a, b | ababbaaabba=1⟩ |
|---|
Completion settings:
Axiom: ababbaaabba=1.
Referenced by [3].
Axiom: abbaa=c.
Defines rule #7.
Referenced by [3], [4], [5], [7], [8], [13], [14], [18], [24].
Overlap of [1] ababbaaabba=1 with [2] abbaa=c:
Critical pair: abcabba=1.
Overlap of [2] abbaa=c with [2] abbaa=c:
Critical pair: abbac=cbbaa.
Defines rule #4.
Referenced by [11], [20], [27].
Overlap of [2] abbaa=c with [3] abcabba=1:
Critical pair: abba=cbcabba.
Flip LHS and RHS.
Referenced by [7].
Overlap of [3] abcabba=1 with [3] abcabba=1:
Critical pair: abcabb=bcabba.
Referenced by [8], [11], [12], [14], [15], [16].
Overlap of [5] cbcabba=abba with [2] abbaa=c:
Critical pair: cbcabbc=abbabbaa.
Reduce RHS:
| [2] | abb(abbaa) |
| ⇒ abbc |
Referenced by [9].
Overlap of [3] abcabba=1 with [6] abcabb=bcabba:
Critical pair: bcabbaa=1.
Reduce LHS:
| [2] | bc(abbaa) |
| ⇒ bcc |
Referenced by [9], [10], [11], [15], [19], [21].
Overlap of [7] cbcabbc=abbc with [8] bcc=1:
Critical pair: cbcab=abbcc.
Reduce RHS:
| [8] | ab(bcc) |
| ⇒ ab |
Overlap of [9] cbcab=ab with [8] bcc=1:
Critical pair: cbca=abcc.
Reduce RHS:
| [8] | a(bcc) |
| ⇒ a |
Overlap of [6] abcabb=bcabba with [8] bcc=1:
Critical pair: abcab=bcabbacc.
Reduce RHS:
| [4] | bc(abbac)c |
| [8] | ⇒ (bcc)bbaac |
| ⇒ bbaac |
Flip LHS and RHS.
Overlap of [9] cbcab=ab with [6] abcabb=bcabba:
Critical pair: cbcbcabba=abcabb.
Reduce LHS:
| [10] | cb(cbca)bba |
| ⇒ cbabba |
Reduce RHS:
| [6] | (abcabb) |
| ⇒ bcabba |
Flip LHS and RHS.
Overlap of [2] abbaa=c with [11] bbaac=abcab:
Critical pair: aabcab=cc.
Overlap of [13] aabcab=cc with [6] abcabb=bcabba:
Critical pair: abcabba=ccb.
Reduce LHS:
| [6] | (abcabb)a |
| [12] | ⇒ (bcabba)a |
| [2] | ⇒ cb(abbaa) |
| ⇒ cbc |
Referenced by [15], [17], [18], [20], [21].
Overlap of [13] aabcab=cc with [6] abcabb=bcabba:
Critical pair: aabcbcabba=cccabb.
Reduce LHS:
| [14] | aab(cbc)abba |
| [8] | ⇒ aa(bcc)babba |
| ⇒ aababba |
Referenced by [24].
Simplify [6] abcabb=bcabba.
Reduce RHS:
| [12] | (bcabba) |
| ⇒ cbabba |
Overlap of [10] cbca=a with [14] cbc=ccb:
Critical pair: ccba=a.
Overlap of [17] ccba=a with [2] abbaa=c:
Critical pair: ccbc=abbaa.
Reduce LHS:
| [14] | c(cbc) |
| ⇒ cccb |
Reduce RHS:
| [2] | (abbaa) |
| ⇒ c |
Referenced by [19].
Overlap of [8] bcc=1 with [18] cccb=c:
Critical pair: bc=cb.
Defines rule #1.
Referenced by [20], [21], [22], [24], [25], [27].
Overlap of [16] abcabb=cbabba with [19] bc=cb:
Critical pair: abcabcb=cbabbac.
Reduce LHS:
| [19] | a(bc)abcb |
| [19] | ⇒ acba(bc)b |
| ⇒ acbacbb |
Reduce RHS:
| [4] | cb(abbac) |
| [14] | ⇒ (cbc)bbaa |
| ⇒ ccbbbaa |
Referenced by [26].
Overlap of [8] bcc=1 with [19] bc=cb:
Critical pair: cbc=1.
Reduce LHS:
| [14] | (cbc) |
| ⇒ ccb |
Defines rule #2.
Referenced by [22], [26], [28], [29].
Overlap of [21] ccb=1 with [11] bbaac=abcab:
Critical pair: ccabcab=baac.
Reduce LHS:
| [19] | cca(bc)ab |
| ⇒ ccacbab |
Flip LHS and RHS.
Referenced by [23].
Overlap of [17] ccba=a with [22] baac=ccacbab:
Critical pair: ccccacbab=aac.
Flip LHS and RHS.
Defines rule #3.
Overlap of [15] aababba=cccabb with [2] abbaa=c:
Critical pair: aababbc=cccabbbbaa.
Reduce LHS:
| [19] | aabab(bc) |
| [19] | ⇒ aaba(bc)b |
| ⇒ aabacbb |
Defines rule #9.
Overlap of [16] abcabb=cbabba with [19] bc=cb:
Critical pair: acbabb=cbabba.
Defines rule #5.
Referenced by [27].
Simplify [20] acbacbb=ccbbbaa.
Reduce RHS:
| [21] | (ccb)bbaa |
| ⇒ bbaa |
Defines rule #6.
Overlap of [4] abbac=cbbaa with [25] acbabb=cbabba:
Critical pair: abbcbabba=cbbaababb.
Reduce LHS:
| [19] | ab(bc)babba |
| [19] | ⇒ a(bc)bbabba |
| ⇒ acbbbabba |
Flip LHS and RHS.
Referenced by [28].
Overlap of [21] ccb=1 with [27] cbbaababb=acbbbabba:
Critical pair: cacbbbabba=baababb.
Flip LHS and RHS.
Referenced by [29].
Overlap of [21] ccb=1 with [28] baababb=cacbbbabba:
Critical pair: cccacbbbabba=aababb.
Flip LHS and RHS.
Defines rule #8.