| Back: | ⟨a, b | abbaabaaaab=1⟩ |
|---|
Completion settings:
Axiom: abbaabaaaab=1.
Referenced by [4].
Axiom: bbaab=c.
Defines rule #9.
Referenced by [4], [5], [7], [10], [17], [20], [35].
Axiom: bacaa=d.
Overlap of [1] abbaabaaaab=1 with [2] bbaab=c:
Critical pair: acaaaab=1.
Referenced by [6], [8], [11], [13].
Overlap of [2] bbaab=c with [2] bbaab=c:
Critical pair: bbaac=cbaab.
Flip LHS and RHS.
Defines rule #13.
Overlap of [3] bacaa=d with [4] acaaaab=1:
Critical pair: b=daab.
Flip LHS and RHS.
Overlap of [6] daab=b with [2] bbaab=c:
Critical pair: daac=bbaab.
Reduce RHS:
| [2] | (bbaab) |
| ⇒ c |
Referenced by [8].
Overlap of [7] daac=c with [4] acaaaab=1:
Critical pair: da=caaaab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [9], [10], [13], [22], [36].
Overlap of [3] bacaa=d with [8] caaaab=da:
Critical pair: bada=daab.
Reduce RHS:
| [6] | (daab) |
| ⇒ b |
Referenced by [11].
Overlap of [8] caaaab=da with [2] bbaab=c:
Critical pair: caaaac=dabaab.
Defines rule #7.
Referenced by [22], [23], [28], [37].
Overlap of [4] acaaaab=1 with [9] bada=b:
Critical pair: acaaaab=ada.
Reduce LHS:
| [4] | (acaaaab) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [12], [13], [14].
Overlap of [3] bacaa=d with [11] ada=1:
Critical pair: baca=dda.
Overlap of [11] ada=1 with [4] acaaaab=1:
Critical pair: ad=caaaab.
Reduce RHS:
| [8] | (caaaab) |
| ⇒ da |
Defines rule #1.
Referenced by [14], [15], [17], [20], [22], [23], [24], [25], [26], [28], [33], [34], [38], [41].
Overlap of [11] ada=1 with [13] ad=da:
Critical pair: daa=1.
Defines rule #2.
Referenced by [16], [17], [19], [20], [22], [23], [24], [26], [27], [28], [30], [31], [32], [33], [34], [36], [38], [43], [44], [45], [46], [47], [48], [49].
Overlap of [12] baca=dda with [13] ad=da:
Critical pair: bacda=ddad.
Reduce RHS:
| [13] | dd(ad) |
| ⇒ ddda |
Referenced by [16].
Overlap of [15] bacda=ddda with [14] daa=1:
Critical pair: bac=dddaa.
Reduce RHS:
| [14] | dd(daa) |
| ⇒ dd |
Defines rule #3.
Referenced by [17], [21], [27].
Overlap of [2] bbaab=c with [16] bac=dd:
Critical pair: bbaadd=cac.
Reduce LHS:
| [13] | bba(ad)d |
| [13] | ⇒ bb(ad)ad |
| [14] | ⇒ bb(daa)d |
| ⇒ bbd |
Flip LHS and RHS.
Defines rule #5.
Referenced by [18], [29], [42].
Overlap of [12] baca=dda with [17] cac=bbd:
Critical pair: babbd=ddac.
Referenced by [19].
Overlap of [18] babbd=ddac with [14] daa=1:
Critical pair: babb=ddacaa.
Defines rule #10.
Overlap of [2] bbaab=c with [19] babb=ddacaa:
Critical pair: bbaaddacaa=cabb.
Reduce LHS:
| [13] | bba(ad)dacaa |
| [13] | ⇒ bb(ad)adacaa |
| [14] | ⇒ bb(daa)dacaa |
| ⇒ bbdacaa |
Flip LHS and RHS.
Defines rule #14.
Overlap of [19] babb=ddacaa with [16] bac=dd:
Critical pair: babdd=ddacaaac.
Flip LHS and RHS.
Referenced by [24].
Overlap of [10] caaaac=dabaab with [8] caaaab=da:
Critical pair: caaaada=dabaabaaaab.
Reduce LHS:
| [13] | caaa(ad)a |
| [13] | ⇒ caa(ad)aa |
| [13] | ⇒ ca(ad)aaa |
| [13] | ⇒ c(ad)aaaa |
| [14] | ⇒ c(daa)aaa |
| ⇒ caaa |
Flip LHS and RHS.
Overlap of [10] caaaac=dabaab with [10] caaaac=dabaab:
Critical pair: caaaadabaab=dabaabaaaac.
Reduce LHS:
| [13] | caaa(ad)abaab |
| [13] | ⇒ caa(ad)aabaab |
| [13] | ⇒ ca(ad)aaabaab |
| [13] | ⇒ c(ad)aaaabaab |
| [14] | ⇒ c(daa)aaabaab |
| ⇒ caaabaab |
Defines rule #18.
Overlap of [13] ad=da with [21] ddacaaac=babdd:
Critical pair: ababdd=dadacaaac.
Reduce RHS:
| [13] | d(ad)acaaac |
| [14] | ⇒ d(daa)caaac |
| ⇒ dcaaac |
Flip LHS and RHS.
Referenced by [25].
Overlap of [13] ad=da with [24] dcaaac=ababdd:
Critical pair: aababdd=dacaaac.
Flip LHS and RHS.
Referenced by [26].
Overlap of [13] ad=da with [25] dacaaac=aababdd:
Critical pair: aaababdd=daacaaac.
Reduce RHS:
| [14] | (daa)caaac |
| ⇒ caaac |
Flip LHS and RHS.
Defines rule #6.
Referenced by [27], [28], [29], [30], [39].
Overlap of [16] bac=dd with [26] caaac=aaababdd:
Critical pair: baaaababdd=ddaaac.
Reduce RHS:
| [14] | d(daa)ac |
| ⇒ dac |
Referenced by [31].
Overlap of [26] caaac=aaababdd with [10] caaaac=dabaab:
Critical pair: caaadabaab=aaababddaaaac.
Reduce LHS:
| [13] | caa(ad)abaab |
| [13] | ⇒ ca(ad)aabaab |
| [13] | ⇒ c(ad)aaabaab |
| [14] | ⇒ c(daa)aabaab |
| ⇒ caabaab |
Reduce RHS:
| [14] | aaababd(daa)aac |
| [14] | ⇒ aaabab(daa)c |
| ⇒ aaababc |
Defines rule #15.
Overlap of [26] caaac=aaababdd with [17] cac=bbd:
Critical pair: caaabbd=aaababddac.
Referenced by [43].
Overlap of [26] caaac=aaababdd with [26] caaac=aaababdd:
Critical pair: caaaaaababdd=aaababddaaac.
Reduce RHS:
| [14] | aaababd(daa)ac |
| ⇒ aaababdac |
Referenced by [46].
Overlap of [27] baaaababdd=dac with [14] daa=1:
Critical pair: baaaababd=dacaa.
Referenced by [32].
Overlap of [31] baaaababd=dacaa with [14] daa=1:
Critical pair: baaaabab=dacaaaa.
Defines rule #12.
Referenced by [34].
Overlap of [13] ad=da with [22] dabaabaaaab=caaa:
Critical pair: acaaa=daabaabaaaab.
Reduce RHS:
| [14] | (daa)baabaaaab |
| ⇒ baabaaaab |
Flip LHS and RHS.
Defines rule #11.
Overlap of [22] dabaabaaaab=caaa with [32] baaaabab=dacaaaa:
Critical pair: dabaabaaaadacaaaa=caaaaaaabab.
Reduce LHS:
| [13] | dabaabaaa(ad)acaaaa |
| [13] | ⇒ dabaabaa(ad)aacaaaa |
| [13] | ⇒ dabaaba(ad)aaacaaaa |
| [13] | ⇒ dabaab(ad)aaaacaaaa |
| [14] | ⇒ dabaab(daa)aaacaaaa |
| ⇒ dabaabaaacaaaa |
Flip LHS and RHS.
Defines rule #23.
Overlap of [2] bbaab=c with [33] baabaaaab=acaaa:
Critical pair: bbaaacaaa=caabaaaab.
Flip LHS and RHS.
Defines rule #16.
Overlap of [8] caaaab=da with [33] baabaaaab=acaaa:
Critical pair: caaaaacaaa=daaabaaaab.
Reduce RHS:
| [14] | (daa)abaaaab |
| ⇒ abaaaab |
Referenced by [37], [38], [39], [40].
Overlap of [10] caaaac=dabaab with [36] caaaaacaaa=abaaaab:
Critical pair: caaaaabaaaab=dabaabaaaaacaaa.
Defines rule #20.
Overlap of [36] caaaaacaaa=abaaaab with [13] ad=da:
Critical pair: caaaaacaada=abaaaabd.
Reduce LHS:
| [13] | caaaaaca(ad)a |
| [13] | ⇒ caaaaac(ad)aa |
| [14] | ⇒ caaaaac(daa)a |
| ⇒ caaaaaca |
Overlap of [36] caaaaacaaa=abaaaab with [26] caaac=aaababdd:
Critical pair: caaaaaaaababdd=abaaaabc.
Referenced by [48].
Overlap of [36] caaaaacaaa=abaaaab with [36] caaaaacaaa=abaaaab:
Critical pair: caaaaaabaaaab=abaaaabaacaaa.
Defines rule #22.
Overlap of [38] caaaaaca=abaaaabd with [13] ad=da:
Critical pair: caaaaacda=abaaaabdd.
Referenced by [44].
Overlap of [38] caaaaaca=abaaaabd with [17] cac=bbd:
Critical pair: caaaaabbd=abaaaabdc.
Referenced by [45].
Overlap of [29] caaabbd=aaababddac with [14] daa=1:
Critical pair: caaabb=aaababddacaa.
Defines rule #17.
Overlap of [41] caaaaacda=abaaaabdd with [14] daa=1:
Critical pair: caaaaac=abaaaabdda.
Defines rule #8.
Overlap of [42] caaaaabbd=abaaaabdc with [14] daa=1:
Critical pair: caaaaabb=abaaaabdcaa.
Defines rule #19.
Overlap of [30] caaaaaababdd=aaababdac with [14] daa=1:
Critical pair: caaaaaababd=aaababdacaa.
Referenced by [47].
Overlap of [46] caaaaaababd=aaababdacaa with [14] daa=1:
Critical pair: caaaaaabab=aaababdacaaaa.
Defines rule #21.
Overlap of [39] caaaaaaaababdd=abaaaabc with [14] daa=1:
Critical pair: caaaaaaaababd=abaaaabcaa.
Referenced by [49].
Overlap of [48] caaaaaaaababd=abaaaabcaa with [14] daa=1:
Critical pair: caaaaaaaabab=abaaaabcaaaa.
Defines rule #24.