| Back: | ⟨a, b | aaaaaababba=1⟩ |
|---|
Completion settings:
Axiom: aaaaaababba=1.
Referenced by [4].
Axiom: aaaaaaa=c.
Defines rule #5.
Referenced by [6], [7], [17], [19], [21], [24], [26], [27], [30], [34], [37], [40].
Axiom: babb=d.
Defines rule #21.
Overlap of [1] aaaaaababba=1 with [3] babb=d:
Critical pair: aaaaaada=1.
Referenced by [7], [8], [9], [10], [11], [12], [13], [14].
Overlap of [3] babb=d with [3] babb=d:
Critical pair: babd=dabb.
Referenced by [15].
Overlap of [2] aaaaaaa=c with [2] aaaaaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #3.
Referenced by [20], [22], [28], [31], [35], [38].
Overlap of [2] aaaaaaa=c with [4] aaaaaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] aaaaaada=1 with [4] aaaaaada=1:
Critical pair: aaaaaad=aaaaada.
Flip LHS and RHS.
Referenced by [10], [11], [12], [13], [14].
Overlap of [7] cda=a with [4] aaaaaada=1:
Critical pair: cd=aaaaaada.
Reduce RHS:
| [4] | (aaaaaada) |
| ⇒ 1 |
Defines rule #2.
Referenced by [17], [19], [21], [27], [30], [34], [37], [39], [40].
Overlap of [4] aaaaaada=1 with [8] aaaaada=aaaaaad:
Critical pair: aaaaaadaaaaaad=aaaada.
Reduce LHS:
| [4] | (aaaaaada)aaaaad |
| ⇒ aaaaad |
Flip LHS and RHS.
Referenced by [12], [13], [14].
Overlap of [8] aaaaada=aaaaaad with [8] aaaaada=aaaaaad:
Critical pair: aaaaadaaaaaad=aaaaaadaaaada.
Reduce LHS:
| [8] | (aaaaada)aaaaad |
| [4] | ⇒ (aaaaaada)aaaad |
| ⇒ aaaad |
Reduce RHS:
| [4] | (aaaaaada)aaada |
| ⇒ aaada |
Flip LHS and RHS.
Referenced by [12], [13], [14].
Overlap of [11] aaada=aaaad with [4] aaaaaada=1:
Critical pair: aaad=aaaadaaaaada.
Reduce RHS:
| [10] | (aaaada)aaaada |
| [8] | ⇒ (aaaaada)aaada |
| [4] | ⇒ (aaaaaada)aada |
| ⇒ aada |
Flip LHS and RHS.
Referenced by [14].
Overlap of [11] aaada=aaaad with [8] aaaaada=aaaaaad:
Critical pair: aaadaaaaaad=aaaadaaaada.
Reduce LHS:
| [11] | (aaada)aaaaad |
| [10] | ⇒ (aaaada)aaaad |
| [8] | ⇒ (aaaaada)aaad |
| [4] | ⇒ (aaaaaada)aad |
| ⇒ aad |
Reduce RHS:
| [10] | (aaaada)aaada |
| [8] | ⇒ (aaaaada)aada |
| [4] | ⇒ (aaaaaada)ada |
| ⇒ ada |
Flip LHS and RHS.
Referenced by [14].
Overlap of [13] ada=aad with [4] aaaaaada=1:
Critical pair: ad=aadaaaaada.
Reduce RHS:
| [12] | (aada)aaaada |
| [11] | ⇒ (aaada)aaada |
| [10] | ⇒ (aaaada)aada |
| [8] | ⇒ (aaaaada)ada |
| [4] | ⇒ (aaaaaada)da |
| ⇒ da |
Flip LHS and RHS.
Defines rule #4.
Referenced by [15], [16], [17], [23], [29], [32], [36].
Simplify [5] babd=dabb.
Reduce RHS:
| [14] | (da)bb |
| ⇒ adbb |
Defines rule #7.
Overlap of [15] babd=adbb with [14] da=ad:
Critical pair: babad=adbba.
Defines rule #10.
Referenced by [23].
Overlap of [14] da=ad with [2] aaaaaaa=c:
Critical pair: dc=adaaaaaa.
Reduce RHS:
| [14] | a(da)aaaaa |
| [14] | ⇒ aa(da)aaaa |
| [14] | ⇒ aaa(da)aaa |
| [14] | ⇒ aaaa(da)aa |
| [14] | ⇒ aaaaa(da)a |
| [14] | ⇒ aaaaaa(da) |
| [2] | ⇒ (aaaaaaa)d |
| [9] | ⇒ (cd) |
| ⇒ 1 |
Defines rule #1.
Referenced by [18], [24], [33].
Overlap of [15] babd=adbb with [17] dc=1:
Critical pair: bab=adbbc.
Flip LHS and RHS.
Overlap of [2] aaaaaaa=c with [18] adbbc=bab:
Critical pair: aaaaaabab=cdbbc.
Reduce RHS:
| [9] | (cd)bbc |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #6.
Referenced by [24].
Overlap of [18] adbbc=bab with [6] ca=ac:
Critical pair: adbbac=baba.
Overlap of [2] aaaaaaa=c with [20] adbbac=baba:
Critical pair: aaaaaababa=cdbbac.
Reduce RHS:
| [9] | (cd)bbac |
| ⇒ bbac |
Flip LHS and RHS.
Defines rule #9.
Overlap of [20] adbbac=baba with [6] ca=ac:
Critical pair: adbbaac=babaa.
Overlap of [16] babad=adbba with [14] da=ad:
Critical pair: babaad=adbbaa.
Defines rule #12.
Referenced by [29].
Overlap of [3] babb=d with [19] bbc=aaaaaabab:
Critical pair: baaaaaaabab=dc.
Reduce LHS:
| [2] | b(aaaaaaa)bab |
| ⇒ bcbab |
Reduce RHS:
| [17] | (dc) |
| ⇒ 1 |
Referenced by [25].
Overlap of [24] bcbab=1 with [24] bcbab=1:
Critical pair: bcba=cbab.
Defines rule #8.
Referenced by [26].
Overlap of [25] bcba=cbab with [2] aaaaaaa=c:
Critical pair: bcbc=cbabaaaaaa.
Flip LHS and RHS.
Referenced by [33].
Overlap of [2] aaaaaaa=c with [22] adbbaac=babaa:
Critical pair: aaaaaababaa=cdbbaac.
Reduce RHS:
| [9] | (cd)bbaac |
| ⇒ bbaac |
Flip LHS and RHS.
Defines rule #11.
Overlap of [22] adbbaac=babaa with [6] ca=ac:
Critical pair: adbbaaac=babaaa.
Overlap of [23] babaad=adbbaa with [14] da=ad:
Critical pair: babaaad=adbbaaa.
Defines rule #14.
Referenced by [32].
Overlap of [2] aaaaaaa=c with [28] adbbaaac=babaaa:
Critical pair: aaaaaababaaa=cdbbaaac.
Reduce RHS:
| [9] | (cd)bbaaac |
| ⇒ bbaaac |
Flip LHS and RHS.
Defines rule #13.
Overlap of [28] adbbaaac=babaaa with [6] ca=ac:
Critical pair: adbbaaaac=babaaaa.
Overlap of [29] babaaad=adbbaaa with [14] da=ad:
Critical pair: babaaaad=adbbaaaa.
Defines rule #16.
Referenced by [36].
Overlap of [17] dc=1 with [26] cbabaaaaaa=bcbc:
Critical pair: dbcbc=babaaaaaa.
Flip LHS and RHS.
Defines rule #20.
Referenced by [38].
Overlap of [2] aaaaaaa=c with [31] adbbaaaac=babaaaa:
Critical pair: aaaaaababaaaa=cdbbaaaac.
Reduce RHS:
| [9] | (cd)bbaaaac |
| ⇒ bbaaaac |
Flip LHS and RHS.
Defines rule #15.
Overlap of [31] adbbaaaac=babaaaa with [6] ca=ac:
Critical pair: adbbaaaaac=babaaaaa.
Overlap of [32] babaaaad=adbbaaaa with [14] da=ad:
Critical pair: babaaaaad=adbbaaaaa.
Defines rule #18.
Overlap of [2] aaaaaaa=c with [35] adbbaaaaac=babaaaaa:
Critical pair: aaaaaababaaaaa=cdbbaaaaac.
Reduce RHS:
| [9] | (cd)bbaaaaac |
| ⇒ bbaaaaac |
Flip LHS and RHS.
Defines rule #17.
Overlap of [35] adbbaaaaac=babaaaaa with [6] ca=ac:
Critical pair: adbbaaaaaac=babaaaaaa.
Reduce RHS:
| [33] | (babaaaaaa) |
| ⇒ dbcbc |
Referenced by [39].
Overlap of [38] adbbaaaaaac=dbcbc with [9] cd=1:
Critical pair: adbbaaaaaa=dbcbcd.
Reduce RHS:
| [9] | dbcb(cd) |
| ⇒ dbcb |
Referenced by [40].
Overlap of [2] aaaaaaa=c with [39] adbbaaaaaa=dbcb:
Critical pair: aaaaaadbcb=cdbbaaaaaa.
Reduce RHS:
| [9] | (cd)bbaaaaaa |
| ⇒ bbaaaaaa |
Flip LHS and RHS.
Defines rule #19.