| Back: | ⟨a, b | aababaa=aaab⟩ |
|---|
Completion settings:
Axiom: aababaa=aaab.
Defines rule #25.
Referenced by [4], [5], [6], [7], [8], [9], [10], [11], [12], [22], [27], [28], [29], [30], [35], [36], [46], [47], [48].
Axiom: bbabaa=c.
Defines rule #37.
Referenced by [4], [6], [7], [10], [11], [13], [15], [23], [34].
Axiom: caa=d.
Defines rule #5.
Referenced by [7], [8], [9], [14], [17], [19], [21], [25], [28], [31], [37], [40], [45].
Overlap of [1] aababaa=aaab with [1] aababaa=aaab:
Critical pair: aababaaab=aaabbabaa.
Reduce LHS:
| [1] | (aababaa)ab |
| ⇒ aaabab |
Reduce RHS:
| [2] | aaa(bbabaa) |
| ⇒ aaac |
Defines rule #26.
Referenced by [5], [27], [28].
Overlap of [1] aababaa=aaab with [1] aababaa=aaab:
Critical pair: aababaaaab=aaabababaa.
Reduce LHS:
| [1] | (aababaa)aab |
| ⇒ aaabaab |
Reduce RHS:
| [4] | (aaabab)abaa |
| ⇒ aaacabaa |
Overlap of [2] bbabaa=c with [1] aababaa=aaab:
Critical pair: bbabaaab=cbabaa.
Reduce LHS:
| [2] | (bbabaa)ab |
| ⇒ cab |
Flip LHS and RHS.
Defines rule #33.
Referenced by [11], [12], [13], [32], [33], [38], [39], [49].
Overlap of [2] bbabaa=c with [1] aababaa=aaab:
Critical pair: bbabaaaab=cababaa.
Reduce LHS:
| [2] | (bbabaa)aab |
| [3] | ⇒ (caa)b |
| ⇒ db |
Flip LHS and RHS.
Referenced by [14].
Overlap of [3] caa=d with [1] aababaa=aaab:
Critical pair: caaab=dbabaa.
Reduce LHS:
| [3] | (caa)ab |
| ⇒ dab |
Flip LHS and RHS.
Overlap of [3] caa=d with [1] aababaa=aaab:
Critical pair: caaaab=dababaa.
Reduce LHS:
| [3] | (caa)aab |
| ⇒ daab |
Flip LHS and RHS.
Referenced by [17].
Overlap of [8] dbabaa=dab with [1] aababaa=aaab:
Critical pair: dbabaaab=dabbabaa.
Reduce LHS:
| [8] | (dbabaa)ab |
| ⇒ dabab |
Reduce RHS:
| [2] | da(bbabaa) |
| ⇒ dac |
Overlap of [6] cbabaa=cab with [1] aababaa=aaab:
Critical pair: cbabaaab=cabbabaa.
Reduce LHS:
| [6] | (cbabaa)ab |
| ⇒ cabab |
Reduce RHS:
| [2] | ca(bbabaa) |
| ⇒ cac |
Defines rule #34.
Referenced by [12], [13], [14].
Overlap of [6] cbabaa=cab with [1] aababaa=aaab:
Critical pair: cbabaaaab=cabababaa.
Reduce LHS:
| [6] | (cbabaa)aab |
| ⇒ cabaab |
Reduce RHS:
| [11] | (cabab)abaa |
| ⇒ cacabaa |
Overlap of [11] cabab=cac with [2] bbabaa=c:
Critical pair: cabac=cacbabaa.
Reduce RHS:
| [6] | ca(cbabaa) |
| ⇒ cacab |
Defines rule #30.
Simplify [7] cababaa=db.
Reduce LHS:
| [11] | (cabab)aa |
| [3] | ⇒ ca(caa) |
| ⇒ cad |
Flip LHS and RHS.
Defines rule #12.
Referenced by [15], [16], [23], [34].
Overlap of [14] db=cad with [2] bbabaa=c:
Critical pair: dc=cadbabaa.
Reduce RHS:
| [14] | ca(db)abaa |
| ⇒ cacadabaa |
Flip LHS and RHS.
Referenced by [18].
Overlap of [8] dbabaa=dab with [14] db=cad:
Critical pair: cadabaa=dab.
Overlap of [9] dababaa=daab with [10] dabab=dac:
Critical pair: dacaa=daab.
Reduce LHS:
| [3] | da(caa) |
| ⇒ dad |
Flip LHS and RHS.
Defines rule #16.
Overlap of [15] cacadabaa=dc with [16] cadabaa=dab:
Critical pair: cadab=dc.
Overlap of [16] cadabaa=dab with [18] cadab=dc:
Critical pair: dcaa=dab.
Reduce LHS:
| [3] | d(caa) |
| ⇒ dd |
Flip LHS and RHS.
Defines rule #13.
Referenced by [20], [22], [23], [24], [34], [46].
Overlap of [10] dabab=dac with [19] dab=dd:
Critical pair: ddab=dac.
Reduce LHS:
| [19] | d(dab) |
| ⇒ ddd |
Flip LHS and RHS.
Defines rule #8.
Referenced by [21], [23], [26].
Overlap of [20] dac=ddd with [3] caa=d:
Critical pair: dad=dddaa.
Flip LHS and RHS.
Defines rule #1.
Overlap of [17] daab=dad with [1] aababaa=aaab:
Critical pair: daaab=dadabaa.
Reduce RHS:
| [19] | da(dab)aa |
| ⇒ daddaa |
Overlap of [17] daab=dad with [2] bbabaa=c:
Critical pair: daac=dadbabaa.
Reduce RHS:
| [14] | da(db)abaa |
| [20] | ⇒ (dac)adabaa |
| [19] | ⇒ ddda(dab)aa |
| ⇒ dddaddaa |
Referenced by [44].
Simplify [18] cadab=dc.
Reduce LHS:
| [19] | ca(dab) |
| ⇒ cadd |
Flip LHS and RHS.
Defines rule #7.
Referenced by [25].
Overlap of [24] dc=cadd with [3] caa=d:
Critical pair: dd=caddaa.
Flip LHS and RHS.
Defines rule #6.
Overlap of [20] dac=ddd with [25] caddaa=dd:
Critical pair: dadd=dddaddaa.
Flip LHS and RHS.
Referenced by [44].
Overlap of [1] aababaa=aaab with [4] aaabab=aaac:
Critical pair: aababaaac=aaababab.
Reduce LHS:
| [1] | (aababaa)ac |
| ⇒ aaabac |
Reduce RHS:
| [4] | (aaabab)ab |
| ⇒ aaacab |
Defines rule #22.
Overlap of [4] aaabab=aaac with [1] aababaa=aaab:
Critical pair: aaaab=aaacaa.
Reduce RHS:
| [3] | aaa(caa) |
| ⇒ aaad |
Defines rule #17.
Referenced by [29], [30], [31], [32], [33], [34].
Overlap of [1] aababaa=aaab with [28] aaaab=aaad:
Critical pair: aababaaad=aaabaab.
Reduce LHS:
| [1] | (aababaa)ad |
| ⇒ aaabad |
Reduce RHS:
| [5] | (aaabaab) |
| ⇒ aaacabaa |
Flip LHS and RHS.
Defines rule #21.
Referenced by [41].
Overlap of [1] aababaa=aaab with [28] aaaab=aaad:
Critical pair: aababaaaad=aaabaaab.
Reduce LHS:
| [1] | (aababaa)aad |
| ⇒ aaabaad |
Flip LHS and RHS.
Defines rule #28.
Overlap of [3] caa=d with [28] aaaab=aaad:
Critical pair: caaaad=daaab.
Reduce LHS:
| [3] | (caa)aad |
| ⇒ daad |
Reduce RHS:
| [22] | (daaab) |
| ⇒ daddaa |
Flip LHS and RHS.
Defines rule #2.
Referenced by [43].
Overlap of [6] cbabaa=cab with [28] aaaab=aaad:
Critical pair: cbabaaad=cabaab.
Reduce LHS:
| [6] | (cbabaa)ad |
| ⇒ cabad |
Reduce RHS:
| [12] | (cabaab) |
| ⇒ cacabaa |
Flip LHS and RHS.
Defines rule #29.
Referenced by [42].
Overlap of [6] cbabaa=cab with [28] aaaab=aaad:
Critical pair: cbabaaaad=cabaaab.
Reduce LHS:
| [6] | (cbabaa)aad |
| ⇒ cabaad |
Flip LHS and RHS.
Defines rule #36.
Referenced by [46].
Overlap of [28] aaaab=aaad with [2] bbabaa=c:
Critical pair: aaaac=aaadbabaa.
Reduce RHS:
| [14] | aaa(db)abaa |
| [19] | ⇒ aaaca(dab)aa |
| [25] | ⇒ aaa(caddaa) |
| ⇒ aaadd |
Defines rule #10.
Referenced by [35], [36], [37], [38], [39], [40].
Overlap of [1] aababaa=aaab with [34] aaaac=aaadd:
Critical pair: aababaaadd=aaabaac.
Reduce LHS:
| [1] | (aababaa)add |
| ⇒ aaabadd |
Flip LHS and RHS.
Defines rule #23.
Overlap of [1] aababaa=aaab with [34] aaaac=aaadd:
Critical pair: aababaaaadd=aaabaaac.
Reduce LHS:
| [1] | (aababaa)aadd |
| ⇒ aaabaadd |
Flip LHS and RHS.
Defines rule #24.
Overlap of [3] caa=d with [34] aaaac=aaadd:
Critical pair: caaaadd=daaac.
Reduce LHS:
| [3] | (caa)aadd |
| ⇒ daadd |
Flip LHS and RHS.
Defines rule #11.
Referenced by [45].
Overlap of [6] cbabaa=cab with [34] aaaac=aaadd:
Critical pair: cbabaaadd=cabaac.
Reduce LHS:
| [6] | (cbabaa)add |
| ⇒ cabadd |
Flip LHS and RHS.
Defines rule #31.
Overlap of [6] cbabaa=cab with [34] aaaac=aaadd:
Critical pair: cbabaaaadd=cabaaac.
Reduce LHS:
| [6] | (cbabaa)aadd |
| ⇒ cabaadd |
Flip LHS and RHS.
Defines rule #32.
Overlap of [34] aaaac=aaadd with [3] caa=d:
Critical pair: aaaad=aaaddaa.
Flip LHS and RHS.
Defines rule #3.
Referenced by [47], [48], [49].
Simplify [5] aaabaab=aaacabaa.
Reduce RHS:
| [29] | (aaacabaa) |
| ⇒ aaabad |
Defines rule #27.
Simplify [12] cabaab=cacabaa.
Reduce RHS:
| [32] | (cacabaa) |
| ⇒ cabad |
Defines rule #35.
Referenced by [46].
Simplify [22] daaab=daddaa.
Reduce RHS:
| [31] | (daddaa) |
| ⇒ daad |
Defines rule #18.
Simplify [23] daac=dddaddaa.
Reduce RHS:
| [26] | (dddaddaa) |
| ⇒ dadd |
Defines rule #9.
Overlap of [37] daaac=daadd with [3] caa=d:
Critical pair: daaad=daaddaa.
Flip LHS and RHS.
Defines rule #4.
Overlap of [42] cabaab=cabad with [1] aababaa=aaab:
Critical pair: cabaaab=cabadabaa.
Reduce LHS:
| [33] | (cabaaab) |
| ⇒ cabaad |
Reduce RHS:
| [19] | caba(dab)aa |
| ⇒ cabaddaa |
Flip LHS and RHS.
Defines rule #19.
Overlap of [1] aababaa=aaab with [40] aaaddaa=aaaad:
Critical pair: aababaaaad=aaabaddaa.
Reduce LHS:
| [1] | (aababaa)aad |
| ⇒ aaabaad |
Flip LHS and RHS.
Defines rule #14.
Overlap of [1] aababaa=aaab with [40] aaaddaa=aaaad:
Critical pair: aababaaaaad=aaabaaddaa.
Reduce LHS:
| [1] | (aababaa)aaad |
| ⇒ aaabaaad |
Flip LHS and RHS.
Defines rule #15.
Overlap of [6] cbabaa=cab with [40] aaaddaa=aaaad:
Critical pair: cbabaaaaad=cabaaddaa.
Reduce LHS:
| [6] | (cbabaa)aaad |
| ⇒ cabaaad |
Flip LHS and RHS.
Defines rule #20.