| Back: | ⟨a, b | aabaaab=aba⟩ |
|---|
Completion settings:
Axiom: aabaaab=aba.
Referenced by [3].
Axiom: aaba=c.
Defines rule #37.
Referenced by [3], [4], [5], [6], [7], [8], [9], [14], [20], [24], [25].
Overlap of [1] aabaaab=aba with [2] aaba=c:
Critical pair: caab=aba.
Overlap of [2] aaba=c with [2] aaba=c:
Critical pair: aabc=caba.
Referenced by [7].
Overlap of [3] caab=aba with [2] aaba=c:
Critical pair: cc=abaa.
Flip LHS and RHS.
Defines rule #35.
Referenced by [6], [7], [8], [9], [11], [21], [22], [27], [32], [56].
Overlap of [2] aaba=c with [5] abaa=cc:
Critical pair: acc=ca.
Flip LHS and RHS.
Defines rule #2.
Referenced by [7], [9], [10], [11], [12], [13], [16], [18], [20], [22], [46].
Overlap of [2] aaba=c with [5] abaa=cc:
Critical pair: aabcc=cbaa.
Reduce LHS:
| [4] | (aabc)c |
| [6] | ⇒ (ca)bac |
| ⇒ accbac |
Defines rule #18.
Referenced by [14], [15], [17], [18], [19], [28], [33], [57].
Overlap of [5] abaa=cc with [2] aaba=c:
Critical pair: abc=ccba.
Defines rule #5.
Referenced by [12], [13], [14], [15], [29], [37], [38], [39], [54], [58].
Overlap of [5] abaa=cc with [2] aaba=c:
Critical pair: abac=ccaba.
Reduce RHS:
| [6] | c(ca)ba |
| [6] | ⇒ (ca)ccba |
| ⇒ accccba |
Flip LHS and RHS.
Defines rule #19.
Overlap of [3] caab=aba with [6] ca=acc:
Critical pair: accab=aba.
Reduce LHS:
| [6] | ac(ca)b |
| [6] | ⇒ a(ca)ccb |
| ⇒ aaccccb |
Defines rule #20.
Referenced by [20], [21], [22], [23], [25].
Overlap of [6] ca=acc with [5] abaa=cc:
Critical pair: ccc=accbaa.
Flip LHS and RHS.
Defines rule #36.
Referenced by [14], [15], [17], [18], [23].
Overlap of [6] ca=acc with [8] abc=ccba:
Critical pair: cccba=accbc.
Flip LHS and RHS.
Defines rule #6.
Referenced by [16], [17], [19], [26], [30], [33], [35], [48], [59].
Overlap of [8] abc=ccba with [6] ca=acc:
Critical pair: abacc=ccbaa.
Defines rule #17.
Overlap of [2] aaba=c with [11] accbaa=ccc:
Critical pair: aabccc=cccbaa.
Reduce LHS:
| [8] | a(abc)cc |
| [7] | ⇒ (accbac)c |
| ⇒ cbaac |
Flip LHS and RHS.
Defines rule #16.
Overlap of [11] accbaa=ccc with [8] abc=ccba:
Critical pair: accbaccba=cccbc.
Reduce LHS:
| [7] | (accbac)cba |
| ⇒ cbaacba |
Defines rule #46.
Overlap of [6] ca=acc with [12] accbc=cccba:
Critical pair: ccccba=accccbc.
Flip LHS and RHS.
Defines rule #7.
Referenced by [37], [41], [49], [61].
Overlap of [11] accbaa=ccc with [12] accbc=cccba:
Critical pair: accbacccba=cccccbc.
Reduce LHS:
| [7] | (accbac)ccba |
| ⇒ cbaaccba |
Defines rule #47.
Overlap of [7] accbac=cbaa with [6] ca=acc:
Critical pair: accbaacc=cbaaa.
Reduce LHS:
| [11] | (accbaa)cc |
| ⇒ ccccc |
Flip LHS and RHS.
Defines rule #33.
Referenced by [24], [25], [26].
Overlap of [7] accbac=cbaa with [12] accbc=cccba:
Critical pair: accbcccba=cbaacbc.
Reduce LHS:
| [12] | (accbc)ccba |
| ⇒ cccbaccba |
Flip LHS and RHS.
Defines rule #29.
Overlap of [2] aaba=c with [10] aaccccb=aba:
Critical pair: aababa=caccccb.
Reduce LHS:
| [2] | (aaba)ba |
| ⇒ cba |
Reduce RHS:
| [6] | (ca)ccccb |
| ⇒ accccccb |
Flip LHS and RHS.
Defines rule #8.
Referenced by [32], [33], [34], [36], [42], [50], [55], [62].
Overlap of [5] abaa=cc with [10] aaccccb=aba:
Critical pair: ababa=ccccccb.
Defines rule #49.
Referenced by [38], [39], [40], [63].
Overlap of [5] abaa=cc with [10] aaccccb=aba:
Critical pair: abaaba=ccaccccb.
Reduce LHS:
| [5] | (abaa)ba |
| ⇒ ccba |
Reduce RHS:
| [6] | c(ca)ccccb |
| [6] | ⇒ (ca)ccccccb |
| ⇒ accccccccb |
Flip LHS and RHS.
Defines rule #9.
Referenced by [51].
Overlap of [11] accbaa=ccc with [10] aaccccb=aba:
Critical pair: accbaba=cccccccb.
Defines rule #51.
Overlap of [18] cbaaa=ccccc with [2] aaba=c:
Critical pair: cbac=cccccba.
Flip LHS and RHS.
Defines rule #4.
Referenced by [27], [28], [29], [30], [31], [34], [40], [41], [43], [45].
Overlap of [18] cbaaa=ccccc with [10] aaccccb=aba:
Critical pair: cbaaba=cccccccccb.
Reduce LHS:
| [2] | cb(aaba) |
| ⇒ cbc |
Flip LHS and RHS.
Defines rule #1.
Referenced by [55].
Overlap of [18] cbaaa=ccccc with [12] accbc=cccba:
Critical pair: cbaacccba=cccccccbc.
Defines rule #48.
Overlap of [24] cccccba=cbac with [5] abaa=cc:
Critical pair: cccccbcc=cbacbaa.
Flip LHS and RHS.
Defines rule #45.
Overlap of [24] cccccba=cbac with [7] accbac=cbaa:
Critical pair: cccccbcbaa=cbacccbac.
Flip LHS and RHS.
Defines rule #27.
Overlap of [24] cccccba=cbac with [8] abc=ccba:
Critical pair: cccccbccba=cbacbc.
Flip LHS and RHS.
Defines rule #11.
Referenced by [48], [49], [50], [51].
Overlap of [24] cccccba=cbac with [12] accbc=cccba:
Critical pair: cccccbcccba=cbacccbc.
Flip LHS and RHS.
Defines rule #12.
Overlap of [24] cccccba=cbac with [13] abacc=ccbaa:
Critical pair: cccccbccbaa=cbacbacc.
Flip LHS and RHS.
Defines rule #26.
Referenced by [52].
Overlap of [5] abaa=cc with [20] accccccb=cba:
Critical pair: abacba=ccccccccb.
Defines rule #50.
Referenced by [65].
Overlap of [7] accbac=cbaa with [20] accccccb=cba:
Critical pair: accbcba=cbaacccccb.
Reduce LHS:
| [12] | (accbc)ba |
| ⇒ cccbaba |
Flip LHS and RHS.
Defines rule #31.
Overlap of [24] cccccba=cbac with [20] accccccb=cba:
Critical pair: cccccbcba=cbacccccccb.
Flip LHS and RHS.
Defines rule #14.
Overlap of [14] cccbaa=cbaac with [12] accbc=cccba:
Critical pair: cccbacccba=cbaacccbc.
Flip LHS and RHS.
Defines rule #30.
Overlap of [14] cccbaa=cbaac with [20] accccccb=cba:
Critical pair: cccbacba=cbaacccccccb.
Flip LHS and RHS.
Defines rule #32.
Overlap of [9] accccba=abac with [8] abc=ccba:
Critical pair: accccbccba=abacbc.
Reduce LHS:
| [16] | (accccbc)cba |
| ⇒ ccccbacba |
Flip LHS and RHS.
Defines rule #34.
Overlap of [21] ababa=ccccccb with [8] abc=ccba:
Critical pair: ababccba=ccccccbbc.
Reduce LHS:
| [8] | ab(abc)cba |
| [8] | ⇒ (abc)cbacba |
| ⇒ ccbacbacba |
Referenced by [44].
Overlap of [21] ababa=ccccccb with [21] ababa=ccccccb:
Critical pair: abccccccb=ccccccbba.
Reduce LHS:
| [8] | (abc)cccccb |
| ⇒ ccbacccccb |
Defines rule #15.
Overlap of [24] cccccba=cbac with [21] ababa=ccccccb:
Critical pair: cccccbccccccb=cbacbaba.
Flip LHS and RHS.
Defines rule #56.
Referenced by [47].
Overlap of [24] cccccba=cbac with [16] accccbc=ccccba:
Critical pair: cccccbccccba=cbacccccbc.
Flip LHS and RHS.
Defines rule #13.
Referenced by [53].
Overlap of [27] cbacbaa=cccccbcc with [20] accccccb=cba:
Critical pair: cbacbacba=cccccbccccccccb.
Defines rule #57.
Referenced by [44].
Overlap of [24] cccccba=cbac with [23] accbaba=cccccccb:
Critical pair: cccccbcccccccb=cbacccbaba.
Flip LHS and RHS.
Defines rule #58.
Overlap of [38] ccbacbacba=ccccccbbc with [42] cbacbacba=cccccbccccccccb:
Critical pair: ccccccbccccccccb=ccccccbbc.
Defines rule #3.
Overlap of [39] ccbacccccb=ccccccbba with [24] cccccba=cbac:
Critical pair: ccbacbac=ccccccbbaa.
Defines rule #28.
Referenced by [46], [47], [48], [49], [50], [51], [52].
Overlap of [45] ccbacbac=ccccccbbaa with [6] ca=acc:
Critical pair: ccbacbaacc=ccccccbbaaa.
Reduce LHS:
| [27] | c(cbacbaa)cc |
| ⇒ ccccccbcccc |
Flip LHS and RHS.
Defines rule #44.
Overlap of [45] ccbacbac=ccccccbbaa with [9] accccba=abac:
Critical pair: ccbacbabac=ccccccbbaacccba.
Reduce LHS:
| [40] | c(cbacbaba)c |
| ⇒ ccccccbccccccbc |
Flip LHS and RHS.
Defines rule #55.
Overlap of [45] ccbacbac=ccccccbbaa with [12] accbc=cccba:
Critical pair: ccbacbcccba=ccccccbbaacbc.
Reduce LHS:
| [29] | c(cbacbc)ccba |
| ⇒ ccccccbccbaccba |
Flip LHS and RHS.
Defines rule #40.
Overlap of [45] ccbacbac=ccccccbbaa with [16] accccbc=ccccba:
Critical pair: ccbacbccccba=ccccccbbaacccbc.
Reduce LHS:
| [29] | c(cbacbc)cccba |
| ⇒ ccccccbccbacccba |
Flip LHS and RHS.
Defines rule #41.
Overlap of [45] ccbacbac=ccccccbbaa with [20] accccccb=cba:
Critical pair: ccbacbcba=ccccccbbaacccccb.
Reduce LHS:
| [29] | c(cbacbc)ba |
| ⇒ ccccccbccbaba |
Flip LHS and RHS.
Defines rule #42.
Overlap of [45] ccbacbac=ccccccbbaa with [22] accccccccb=ccba:
Critical pair: ccbacbccba=ccccccbbaacccccccb.
Reduce LHS:
| [29] | c(cbacbc)cba |
| ⇒ ccccccbccbacba |
Flip LHS and RHS.
Defines rule #43.
Overlap of [45] ccbacbac=ccccccbbaa with [31] cbacbacc=cccccbccbaa:
Critical pair: ccccccbccbaa=ccccccbbaac.
Defines rule #25.
Overlap of [39] ccbacccccb=ccccccbba with [41] cbacccccbc=cccccbccccba:
Critical pair: ccccccbccccba=ccccccbbac.
Defines rule #10.
Referenced by [56], [57], [58], [59], [60], [61], [62], [63], [64], [65].
Overlap of [46] ccccccbbaaa=ccccccbcccc with [8] abc=ccba:
Critical pair: ccccccbbaaccba=ccccccbccccbc.
Defines rule #54.
Overlap of [46] ccccccbbaaa=ccccccbcccc with [20] accccccb=cba:
Critical pair: ccccccbbaacba=ccccccbccccccccccb.
Reduce RHS:
| [25] | ccccccbc(cccccccccb) |
| ⇒ ccccccbccbc |
Defines rule #53.
Overlap of [53] ccccccbccccba=ccccccbbac with [5] abaa=cc:
Critical pair: ccccccbccccbcc=ccccccbbacbaa.
Flip LHS and RHS.
Defines rule #52.
Overlap of [53] ccccccbccccba=ccccccbbac with [7] accbac=cbaa:
Critical pair: ccccccbccccbcbaa=ccccccbbacccbac.
Flip LHS and RHS.
Defines rule #39.
Overlap of [53] ccccccbccccba=ccccccbbac with [8] abc=ccba:
Critical pair: ccccccbccccbccba=ccccccbbacbc.
Flip LHS and RHS.
Defines rule #21.
Overlap of [53] ccccccbccccba=ccccccbbac with [12] accbc=cccba:
Critical pair: ccccccbccccbcccba=ccccccbbacccbc.
Flip LHS and RHS.
Defines rule #22.
Overlap of [53] ccccccbccccba=ccccccbbac with [13] abacc=ccbaa:
Critical pair: ccccccbccccbccbaa=ccccccbbacbacc.
Flip LHS and RHS.
Defines rule #38.
Overlap of [53] ccccccbccccba=ccccccbbac with [16] accccbc=ccccba:
Critical pair: ccccccbccccbccccba=ccccccbbacccccbc.
Flip LHS and RHS.
Defines rule #23.
Overlap of [53] ccccccbccccba=ccccccbbac with [20] accccccb=cba:
Critical pair: ccccccbccccbcba=ccccccbbacccccccb.
Flip LHS and RHS.
Defines rule #24.
Overlap of [53] ccccccbccccba=ccccccbbac with [21] ababa=ccccccb:
Critical pair: ccccccbccccbccccccb=ccccccbbacbaba.
Flip LHS and RHS.
Defines rule #59.
Overlap of [53] ccccccbccccba=ccccccbbac with [23] accbaba=cccccccb:
Critical pair: ccccccbccccbcccccccb=ccccccbbacccbaba.
Flip LHS and RHS.
Defines rule #61.
Overlap of [53] ccccccbccccba=ccccccbbac with [32] abacba=ccccccccb:
Critical pair: ccccccbccccbccccccccb=ccccccbbacbacba.
Flip LHS and RHS.
Defines rule #60.