| Back: | ⟨a, b | abaababbaab=1⟩ |
|---|
Completion settings:
Axiom: abaababbaab=1.
Referenced by [3].
Axiom: baaba=c.
Referenced by [3], [4], [5], [6], [15], [17], [22].
Overlap of [1] abaababbaab=1 with [2] baaba=c:
Critical pair: acbbaab=1.
Referenced by [5], [7], [12], [14], [16], [19].
Overlap of [2] baaba=c with [2] baaba=c:
Critical pair: baac=caba.
Referenced by [7], [8], [13], [17], [23].
Overlap of [3] acbbaab=1 with [2] baaba=c:
Critical pair: acbc=a.
Referenced by [6], [8], [9], [10], [14], [17].
Overlap of [2] baaba=c with [5] acbc=a:
Critical pair: baaba=ccbc.
Reduce LHS:
| [2] | (baaba) |
| ⇒ c |
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] baac=caba with [3] acbbaab=1:
Critical pair: ba=cababbaab.
Flip LHS and RHS.
Overlap of [4] baac=caba with [5] acbc=a:
Critical pair: baa=cababc.
Flip LHS and RHS.
Overlap of [5] acbc=a with [8] cababc=baa:
Critical pair: acbbaa=aababc.
Flip LHS and RHS.
Referenced by [15], [19], [20].
Overlap of [5] acbc=a with [7] cababbaab=ba:
Critical pair: acbba=aababbaab.
Flip LHS and RHS.
Referenced by [26].
Overlap of [6] ccbc=c with [7] cababbaab=ba:
Critical pair: ccbba=cababbaab.
Reduce RHS:
| [7] | (cababbaab) |
| ⇒ ba |
Referenced by [12].
Overlap of [11] ccbba=ba with [3] acbbaab=1:
Critical pair: ccbb=bacbbaab.
Reduce RHS:
| [3] | b(acbbaab) |
| ⇒ b |
Referenced by [13].
Overlap of [4] baac=caba with [12] ccbb=b:
Critical pair: baab=cabacbb.
Flip LHS and RHS.
Referenced by [14].
Overlap of [5] acbc=a with [13] cabacbb=baab:
Critical pair: acbbaab=aabacbb.
Reduce LHS:
| [3] | (acbbaab) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [20].
Overlap of [2] baaba=c with [9] aababc=acbbaa:
Critical pair: bacbbaa=cbc.
Overlap of [15] bacbbaa=cbc with [3] acbbaab=1:
Critical pair: b=cbcb.
Flip LHS and RHS.
Overlap of [15] bacbbaa=cbc with [4] baac=caba:
Critical pair: bacbcaba=cbcc.
Reduce LHS:
| [5] | b(acbc)aba |
| [2] | ⇒ (baaba) |
| ⇒ c |
Flip LHS and RHS.
Overlap of [16] cbcb=b with [16] cbcb=b:
Critical pair: cbb=bcb.
Flip LHS and RHS.
Referenced by [20].
Overlap of [9] aababc=acbbaa with [17] cbcc=c:
Critical pair: aababc=acbbaabcc.
Reduce LHS:
| [9] | (aababc) |
| ⇒ acbbaa |
Reduce RHS:
| [3] | (acbbaab)cc |
| ⇒ cc |
Defines rule #7.
Referenced by [20], [27], [30], [36].
Overlap of [9] aababc=acbbaa with [18] bcb=cbb:
Critical pair: aabacbb=acbbaab.
Reduce LHS:
| [14] | (aabacbb) |
| ⇒ 1 |
Reduce RHS:
| [19] | (acbbaa)b |
| ⇒ ccb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [21], [22], [23], [26], [28], [29], [30], [31], [32], [34], [35], [36], [37], [38].
Overlap of [17] cbcc=c with [20] ccb=1:
Critical pair: cbc=ccb.
Reduce RHS:
| [20] | (ccb) |
| ⇒ 1 |
Overlap of [20] ccb=1 with [2] baaba=c:
Critical pair: ccc=aaba.
Flip LHS and RHS.
Referenced by [26].
Overlap of [20] ccb=1 with [4] baac=caba:
Critical pair: cccaba=aac.
Flip LHS and RHS.
Defines rule #4.
Referenced by [27], [29], [37].
Overlap of [16] cbcb=b with [21] cbc=1:
Critical pair: cb=bc.
Flip LHS and RHS.
Defines rule #1.
Referenced by [25], [29], [30], [31], [32], [33], [34], [37], [38].
Overlap of [21] cbc=1 with [8] cababc=baa:
Critical pair: cbbaa=ababc.
Reduce RHS:
| [24] | aba(bc) |
| ⇒ abacb |
Flip LHS and RHS.
Defines rule #6.
Referenced by [36].
Overlap of [10] aababbaab=acbba with [22] aaba=ccc:
Critical pair: cccbbaab=acbba.
Reduce LHS:
| [20] | c(ccb)baab |
| ⇒ cbaab |
Overlap of [23] aac=cccaba with [19] acbbaa=cc:
Critical pair: acc=cccababbaa.
Flip LHS and RHS.
Referenced by [32].
Overlap of [20] ccb=1 with [26] cbaab=acbba:
Critical pair: cacbba=aab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [36].
Overlap of [26] cbaab=acbba with [24] bc=cb:
Critical pair: cbaacb=acbbac.
Reduce LHS:
| [23] | cb(aac)b |
| [24] | ⇒ c(bc)ccabab |
| [20] | ⇒ (ccb)ccabab |
| ⇒ ccabab |
Flip LHS and RHS.
Defines rule #5.
Overlap of [29] acbbac=ccabab with [19] acbbaa=cc:
Critical pair: acbbcc=ccababbbaa.
Reduce LHS:
| [24] | acb(bc)c |
| [24] | ⇒ ac(bc)bc |
| [20] | ⇒ a(ccb)bc |
| [24] | ⇒ a(bc) |
| ⇒ acb |
Flip LHS and RHS.
Referenced by [34].
Overlap of [29] acbbac=ccabab with [29] acbbac=ccabab:
Critical pair: acbbccabab=ccababbbac.
Reduce LHS:
| [24] | acb(bc)cabab |
| [24] | ⇒ ac(bc)bcabab |
| [20] | ⇒ a(ccb)bcabab |
| [24] | ⇒ a(bc)abab |
| ⇒ acbabab |
Flip LHS and RHS.
Referenced by [38].
Overlap of [24] bc=cb with [27] cccababbaa=acc:
Critical pair: bacc=cbccababbaa.
Reduce RHS:
| [24] | c(bc)cababbaa |
| [20] | ⇒ (ccb)cababbaa |
| ⇒ cababbaa |
Flip LHS and RHS.
Referenced by [33].
Overlap of [24] bc=cb with [32] cababbaa=bacc:
Critical pair: bbacc=cbababbaa.
Flip LHS and RHS.
Overlap of [24] bc=cb with [30] ccababbbaa=acb:
Critical pair: bacb=cbcababbbaa.
Reduce RHS:
| [24] | c(bc)ababbbaa |
| [20] | ⇒ (ccb)ababbbaa |
| ⇒ ababbbaa |
Flip LHS and RHS.
Defines rule #11.
Overlap of [20] ccb=1 with [33] cbababbaa=bbacc:
Critical pair: cbbacc=ababbaa.
Flip LHS and RHS.
Defines rule #10.
Overlap of [25] abacb=cbbaa with [33] cbababbaa=bbacc:
Critical pair: ababbacc=cbbaaababbaa.
Reduce RHS:
| [28] | cbba(aab)abbaa |
| [19] | ⇒ cbbac(acbbaa)bbaa |
| [20] | ⇒ cbbac(ccb)baa |
| ⇒ cbbacbaa |
Referenced by [37].
Overlap of [36] ababbacc=cbbacbaa with [20] ccb=1:
Critical pair: ababbac=cbbacbaacb.
Reduce RHS:
| [23] | cbbacb(aac)b |
| [24] | ⇒ cbbac(bc)ccabab |
| [20] | ⇒ cbba(ccb)ccabab |
| ⇒ cbbaccabab |
Defines rule #8.
Overlap of [24] bc=cb with [31] ccababbbac=acbabab:
Critical pair: bacbabab=cbcababbbac.
Reduce RHS:
| [24] | c(bc)ababbbac |
| [20] | ⇒ (ccb)ababbbac |
| ⇒ ababbbac |
Flip LHS and RHS.
Defines rule #9.