| Back: | ⟨a, b | aaabaabbbba=1⟩ |
|---|
Completion settings:
Axiom: aaabaabbbba=1.
Referenced by [4].
Axiom: bbbb=c.
Defines rule #5.
Referenced by [4], [5], [13], [15], [18], [20], [27].
Axiom: aaaabaa=d.
Defines rule #20.
Referenced by [6], [7], [8], [9], [12], [14], [17], [20].
Overlap of [1] aaabaabbbba=1 with [2] bbbb=c:
Critical pair: aaabaaca=1.
Referenced by [8], [9], [10], [11].
Overlap of [2] bbbb=c with [2] bbbb=c:
Critical pair: bc=cb.
Defines rule #3.
Referenced by [22], [30], [35].
Overlap of [3] aaaabaa=d with [3] aaaabaa=d:
Critical pair: aaaabd=daabaa.
Flip LHS and RHS.
Referenced by [23], [25], [32].
Overlap of [3] aaaabaa=d with [3] aaaabaa=d:
Critical pair: aaaabad=daaabaa.
Flip LHS and RHS.
Defines rule #16.
Referenced by [34].
Overlap of [3] aaaabaa=d with [4] aaabaaca=1:
Critical pair: a=dca.
Flip LHS and RHS.
Referenced by [11].
Overlap of [3] aaaabaa=d with [4] aaabaaca=1:
Critical pair: aaaab=dabaaca.
Flip LHS and RHS.
Referenced by [17].
Overlap of [4] aaabaaca=1 with [4] aaabaaca=1:
Critical pair: aaabaac=aabaaca.
Flip LHS and RHS.
Referenced by [12], [14], [17].
Overlap of [8] dca=a with [4] aaabaaca=1:
Critical pair: dc=aaabaaca.
Reduce RHS:
| [4] | (aaabaaca) |
| ⇒ 1 |
Defines rule #2.
Referenced by [12], [14], [16], [17], [20], [24], [27].
Overlap of [10] aabaaca=aaabaac with [10] aabaaca=aaabaac:
Critical pair: aabaacaaabaac=aaabaacabaaca.
Reduce LHS:
| [10] | (aabaaca)aabaac |
| [10] | ⇒ a(aabaaca)abaac |
| [3] | ⇒ (aaaabaa)cabaac |
| [11] | ⇒ (dc)abaac |
| ⇒ abaac |
Reduce RHS:
| [10] | a(aabaaca)baaca |
| [3] | ⇒ (aaaabaa)cbaaca |
| [11] | ⇒ (dc)baaca |
| ⇒ baaca |
Flip LHS and RHS.
Defines rule #6.
Referenced by [13], [14], [20], [28], [36].
Overlap of [2] bbbb=c with [12] baaca=abaac:
Critical pair: bbbabaac=caaca.
Overlap of [12] baaca=abaac with [3] aaaabaa=d:
Critical pair: baacd=abaacaaabaa.
Reduce RHS:
| [12] | a(baaca)aabaa |
| [10] | ⇒ (aabaaca)abaa |
| [10] | ⇒ a(aabaaca)baa |
| [3] | ⇒ (aaaabaa)cbaa |
| [11] | ⇒ (dc)baa |
| ⇒ baa |
Referenced by [15].
Overlap of [2] bbbb=c with [14] baacd=baa:
Critical pair: bbbbaa=caacd.
Reduce LHS:
| [2] | (bbbb)aa |
| ⇒ caa |
Flip LHS and RHS.
Referenced by [16].
Overlap of [11] dc=1 with [15] caacd=caa:
Critical pair: dcaa=aacd.
Reduce LHS:
| [11] | (dc)aa |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [17], [19], [29].
Overlap of [16] aacd=aa with [9] dabaaca=aaaab:
Critical pair: aacaaaab=aaabaaca.
Reduce RHS:
| [10] | a(aabaaca) |
| [3] | ⇒ (aaaabaa)c |
| [11] | ⇒ (dc) |
| ⇒ 1 |
Referenced by [18].
Overlap of [17] aacaaaab=1 with [2] bbbb=c:
Critical pair: aacaaaac=bbb.
Overlap of [18] aacaaaac=bbb with [16] aacd=aa:
Critical pair: aacaaaa=bbbd.
Overlap of [12] baaca=abaac with [19] aacaaaa=bbbd:
Critical pair: bbbbd=abaacaaa.
Reduce LHS:
| [2] | (bbbb)d |
| ⇒ cd |
Reduce RHS:
| [12] | a(baaca)aa |
| [12] | ⇒ aa(baaca)a |
| [12] | ⇒ aaa(baaca) |
| [3] | ⇒ (aaaabaa)c |
| [11] | ⇒ (dc) |
| ⇒ 1 |
Defines rule #1.
Referenced by [22], [23], [37], [39].
Overlap of [18] aacaaaac=bbb with [19] aacaaaa=bbbd:
Critical pair: aacaabbbd=bbbaaaa.
Flip LHS and RHS.
Referenced by [33].
Overlap of [5] bc=cb with [20] cd=1:
Critical pair: b=cbd.
Flip LHS and RHS.
Referenced by [24].
Overlap of [20] cd=1 with [6] daabaa=aaaabd:
Critical pair: caaaabd=aabaa.
Referenced by [26].
Overlap of [11] dc=1 with [22] cbd=b:
Critical pair: db=bd.
Flip LHS and RHS.
Defines rule #4.
Referenced by [25], [26], [31], [32], [33], [34], [38].
Overlap of [24] bd=db with [6] daabaa=aaaabd:
Critical pair: baaaabd=dbaabaa.
Reduce LHS:
| [24] | baaaa(bd) |
| ⇒ baaaadb |
Flip LHS and RHS.
Defines rule #11.
Referenced by [31].
Simplify [23] caaaabd=aabaa.
Reduce LHS:
| [24] | caaaa(bd) |
| ⇒ caaaadb |
Referenced by [27].
Overlap of [26] caaaadb=aabaa with [2] bbbb=c:
Critical pair: caaaadc=aabaabbb.
Reduce LHS:
| [11] | caaaa(dc) |
| ⇒ caaaa |
Defines rule #8.
Referenced by [30].
Overlap of [13] bbbabaac=caaca with [12] baaca=abaac:
Critical pair: bbbaabaac=caacaa.
Overlap of [13] bbbabaac=caaca with [16] aacd=aa:
Critical pair: bbbabaa=caacad.
Defines rule #7.
Overlap of [5] bc=cb with [27] caaaa=aabaabbb:
Critical pair: baabaabbb=cbaaaa.
Flip LHS and RHS.
Defines rule #10.
Referenced by [35].
Overlap of [24] bd=db with [25] dbaabaa=baaaadb:
Critical pair: bbaaaadb=dbbaabaa.
Flip LHS and RHS.
Defines rule #13.
Simplify [6] daabaa=aaaabd.
Reduce RHS:
| [24] | aaaa(bd) |
| ⇒ aaaadb |
Defines rule #9.
Simplify [21] bbbaaaa=aacaabbbd.
Reduce RHS:
| [24] | aacaabb(bd) |
| [24] | ⇒ aacaab(bd)b |
| [24] | ⇒ aacaa(bd)bb |
| ⇒ aacaadbbb |
Defines rule #14.
Overlap of [24] bd=db with [7] daaabaa=aaaabad:
Critical pair: baaaabad=dbaaabaa.
Flip LHS and RHS.
Defines rule #17.
Referenced by [38].
Overlap of [5] bc=cb with [30] cbaaaa=baabaabbb:
Critical pair: bbaabaabbb=cbbaaaa.
Flip LHS and RHS.
Defines rule #12.
Overlap of [28] bbbaabaac=caacaa with [12] baaca=abaac:
Critical pair: bbbaaabaac=caacaaa.
Referenced by [39].
Overlap of [28] bbbaabaac=caacaa with [20] cd=1:
Critical pair: bbbaabaa=caacaad.
Defines rule #15.
Overlap of [24] bd=db with [34] dbaaabaa=baaaabad:
Critical pair: bbaaaabad=dbbaaabaa.
Flip LHS and RHS.
Defines rule #18.
Overlap of [36] bbbaaabaac=caacaaa with [20] cd=1:
Critical pair: bbbaaabaa=caacaaad.
Defines rule #19.