| Back: | ⟨a, b | aaabaabbba=1⟩ |
|---|
Completion settings:
Axiom: aaabaabbba=1.
Referenced by [4].
Axiom: bbb=c.
Defines rule #5.
Referenced by [4], [5], [13], [15], [18], [20], [29].
Axiom: aaaabaa=d.
Defines rule #17.
Referenced by [6], [7], [8], [9], [12], [14], [17], [20].
Overlap of [1] aaabaabbba=1 with [2] bbb=c:
Critical pair: aaabaaca=1.
Referenced by [8], [9], [10], [11].
Overlap of [2] bbb=c with [2] bbb=c:
Critical pair: bc=cb.
Defines rule #3.
Overlap of [3] aaaabaa=d with [3] aaaabaa=d:
Critical pair: aaaabd=daabaa.
Flip LHS and RHS.
Referenced by [23], [25], [31].
Overlap of [3] aaaabaa=d with [3] aaaabaa=d:
Critical pair: aaaabad=daaabaa.
Flip LHS and RHS.
Defines rule #14.
Referenced by [35].
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], [29].
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], [26], [33].
Overlap of [2] bbb=c with [12] baaca=abaac:
Critical pair: bbabaac=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] bbb=c with [14] baacd=baa:
Critical pair: bbbaa=caacd.
Reduce LHS:
| [2] | (bbb)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], [27].
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] bbb=c:
Critical pair: aacaaaac=bb.
Overlap of [18] aacaaaac=bb with [16] aacd=aa:
Critical pair: aacaaaa=bbd.
Overlap of [12] baaca=abaac with [19] aacaaaa=bbd:
Critical pair: bbbd=abaacaaa.
Reduce LHS:
| [2] | (bbb)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], [34], [36].
Overlap of [18] aacaaaac=bb with [19] aacaaaa=bbd:
Critical pair: aacaabbd=bbaaaa.
Flip LHS and RHS.
Referenced by [32].
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 [28].
Overlap of [11] dc=1 with [22] cbd=b:
Critical pair: db=bd.
Flip LHS and RHS.
Defines rule #4.
Referenced by [25], [28], [31], [32], [35].
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.
Overlap of [13] bbabaac=caaca with [12] baaca=abaac:
Critical pair: bbaabaac=caacaa.
Overlap of [13] bbabaac=caaca with [16] aacd=aa:
Critical pair: bbabaa=caacad.
Defines rule #7.
Simplify [23] caaaabd=aabaa.
Reduce LHS:
| [24] | caaaa(bd) |
| ⇒ caaaadb |
Referenced by [29].
Overlap of [28] caaaadb=aabaa with [2] bbb=c:
Critical pair: caaaadc=aabaabb.
Reduce LHS:
| [11] | caaaa(dc) |
| ⇒ caaaa |
Defines rule #8.
Referenced by [30].
Overlap of [5] bc=cb with [29] caaaa=aabaabb:
Critical pair: baabaabb=cbaaaa.
Flip LHS and RHS.
Defines rule #10.
Simplify [6] daabaa=aaaabd.
Reduce RHS:
| [24] | aaaa(bd) |
| ⇒ aaaadb |
Defines rule #9.
Simplify [21] bbaaaa=aacaabbd.
Reduce RHS:
| [24] | aacaab(bd) |
| [24] | ⇒ aacaa(bd)b |
| ⇒ aacaadbb |
Defines rule #12.
Overlap of [26] bbaabaac=caacaa with [12] baaca=abaac:
Critical pair: bbaaabaac=caacaaa.
Referenced by [36].
Overlap of [26] bbaabaac=caacaa with [20] cd=1:
Critical pair: bbaabaa=caacaad.
Defines rule #13.
Overlap of [24] bd=db with [7] daaabaa=aaaabad:
Critical pair: baaaabad=dbaaabaa.
Flip LHS and RHS.
Defines rule #15.
Overlap of [33] bbaaabaac=caacaaa with [20] cd=1:
Critical pair: bbaaabaa=caacaaad.
Defines rule #16.