| Back: | ⟨a, b | aaaaabbbaba=1⟩ |
|---|
Completion settings:
Axiom: aaaaabbbaba=1.
Referenced by [4].
Axiom: aaaaaa=c.
Defines rule #5.
Referenced by [6], [7], [8], [11], [15], [17], [24], [26], [27], [30], [34], [38], [41], [43].
Axiom: bbbab=d.
Defines rule #20.
Overlap of [1] aaaaabbbaba=1 with [3] bbbab=d:
Critical pair: aaaaada=1.
Referenced by [7], [8], [9], [10], [11], [12].
Overlap of [3] bbbab=d with [3] bbbab=d:
Critical pair: bbbad=dbbab.
Flip LHS and RHS.
Referenced by [19].
Overlap of [2] aaaaaa=c with [2] aaaaaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [25], [33], [37], [40].
Overlap of [2] aaaaaa=c with [4] aaaaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Overlap of [2] aaaaaa=c with [4] aaaaada=1:
Critical pair: aa=cada.
Flip LHS and RHS.
Referenced by [11].
Overlap of [4] aaaaada=1 with [4] aaaaada=1:
Critical pair: aaaaad=aaaada.
Overlap of [7] cda=a with [4] aaaaada=1:
Critical pair: cd=aaaaada.
Reduce RHS:
| [9] | (aaaaad)a |
| ⇒ aaaadaa |
Flip LHS and RHS.
Overlap of [8] cada=aa with [4] aaaaada=1:
Critical pair: cad=aaaaaada.
Reduce RHS:
| [2] | (aaaaaa)da |
| [7] | ⇒ (cda) |
| ⇒ a |
Overlap of [4] aaaaada=1 with [9] aaaaad=aaaada:
Critical pair: aaaadaa=1.
Reduce LHS:
| [10] | (aaaadaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [13], [15], [17], [21], [27], [31], [36].
Simplify [10] aaaadaa=cd.
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Overlap of [13] aaaadaa=1 with [13] aaaadaa=1:
Critical pair: aaaad=aadaa.
Referenced by [15], [16], [17].
Overlap of [2] aaaaaa=c with [14] aaaad=aadaa:
Critical pair: aaaadaa=cd.
Reduce LHS:
| [14] | (aaaad)aa |
| ⇒ aadaaaa |
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Referenced by [16].
Overlap of [13] aaaadaa=1 with [14] aaaad=aadaa:
Critical pair: aaaadaadaa=aad.
Reduce LHS:
| [14] | (aaaad)aadaa |
| [15] | ⇒ (aadaaaa)daa |
| ⇒ daa |
Flip LHS and RHS.
Overlap of [2] aaaaaa=c with [16] aad=daa:
Critical pair: aaaadaa=cd.
Reduce LHS:
| [14] | (aaaad)aa |
| [16] | ⇒ (aad)aaaa |
| [2] | ⇒ d(aaaaaa) |
| ⇒ dc |
Reduce RHS:
| [12] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [18], [24], [26], [34], [38], [41], [42], [43].
Overlap of [17] dc=1 with [11] cad=a:
Critical pair: da=ad.
Flip LHS and RHS.
Defines rule #4.
Referenced by [19], [23], [35], [39].
Simplify [5] dbbab=bbbad.
Reduce RHS:
| [18] | bbb(ad) |
| ⇒ bbbda |
Defines rule #9.
Referenced by [20], [21], [22], [23].
Overlap of [11] cad=a with [19] dbbab=bbbda:
Critical pair: cabbbda=abbab.
Overlap of [12] cd=1 with [19] dbbab=bbbda:
Critical pair: cbbbda=bbab.
Referenced by [24].
Overlap of [16] aad=daa with [19] dbbab=bbbda:
Critical pair: aabbbda=daabbab.
Flip LHS and RHS.
Defines rule #13.
Referenced by [35].
Overlap of [18] ad=da with [19] dbbab=bbbda:
Critical pair: abbbda=dabbab.
Flip LHS and RHS.
Defines rule #11.
Overlap of [21] cbbbda=bbab with [2] aaaaaa=c:
Critical pair: cbbbdc=bbabaaaaa.
Reduce LHS:
| [17] | cbbb(dc) |
| ⇒ cbbb |
Defines rule #8.
Referenced by [27].
Overlap of [6] ac=ca with [20] cabbbda=abbab:
Critical pair: aabbab=caabbbda.
Flip LHS and RHS.
Overlap of [20] cabbbda=abbab with [2] aaaaaa=c:
Critical pair: cabbbdc=abbabaaaaa.
Reduce LHS:
| [17] | cabbb(dc) |
| ⇒ cabbb |
Defines rule #10.
Overlap of [24] cbbb=bbabaaaaa with [3] bbbab=d:
Critical pair: cd=bbabaaaaaab.
Reduce LHS:
| [12] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | bbab(aaaaaa)b |
| ⇒ bbabcb |
Flip LHS and RHS.
Overlap of [27] bbabcb=1 with [27] bbabcb=1:
Critical pair: bbabc=babcb.
Flip LHS and RHS.
Overlap of [27] bbabcb=1 with [28] babcb=bbabc:
Critical pair: bbabcbbabc=abcb.
Reduce LHS:
| [27] | (bbabcb)babc |
| ⇒ babc |
Flip LHS and RHS.
Defines rule #6.
Referenced by [30].
Overlap of [2] aaaaaa=c with [29] abcb=babc:
Critical pair: aaaaababc=cbcb.
Overlap of [30] aaaaababc=cbcb with [12] cd=1:
Critical pair: aaaaabab=cbcbd.
Defines rule #7.
Overlap of [30] aaaaababc=cbcb with [28] babcb=bbabc:
Critical pair: aaaaabbabc=cbcbb.
Referenced by [36].
Overlap of [6] ac=ca with [25] caabbbda=aabbab:
Critical pair: aaabbab=caaabbbda.
Flip LHS and RHS.
Overlap of [25] caabbbda=aabbab with [2] aaaaaa=c:
Critical pair: caabbbdc=aabbabaaaaa.
Reduce LHS:
| [17] | caabbb(dc) |
| ⇒ caabbb |
Defines rule #12.
Overlap of [18] ad=da with [22] daabbab=aabbbda:
Critical pair: aaabbbda=daaabbab.
Flip LHS and RHS.
Defines rule #15.
Referenced by [39].
Overlap of [32] aaaaabbabc=cbcbb with [12] cd=1:
Critical pair: aaaaabbab=cbcbbd.
Defines rule #19.
Referenced by [40].
Overlap of [6] ac=ca with [33] caaabbbda=aaabbab:
Critical pair: aaaabbab=caaaabbbda.
Flip LHS and RHS.
Overlap of [33] caaabbbda=aaabbab with [2] aaaaaa=c:
Critical pair: caaabbbdc=aaabbabaaaaa.
Reduce LHS:
| [17] | caaabbb(dc) |
| ⇒ caaabbb |
Defines rule #14.
Overlap of [18] ad=da with [35] daaabbab=aaabbbda:
Critical pair: aaaabbbda=daaaabbab.
Flip LHS and RHS.
Defines rule #17.
Overlap of [6] ac=ca with [37] caaaabbbda=aaaabbab:
Critical pair: aaaaabbab=caaaaabbbda.
Reduce LHS:
| [36] | (aaaaabbab) |
| ⇒ cbcbbd |
Flip LHS and RHS.
Referenced by [42].
Overlap of [37] caaaabbbda=aaaabbab with [2] aaaaaa=c:
Critical pair: caaaabbbdc=aaaabbabaaaaa.
Reduce LHS:
| [17] | caaaabbb(dc) |
| ⇒ caaaabbb |
Defines rule #16.
Overlap of [17] dc=1 with [40] caaaaabbbda=cbcbbd:
Critical pair: dcbcbbd=aaaaabbbda.
Reduce LHS:
| [17] | (dc)bcbbd |
| ⇒ bcbbd |
Flip LHS and RHS.
Referenced by [43].
Overlap of [42] aaaaabbbda=bcbbd with [2] aaaaaa=c:
Critical pair: aaaaabbbdc=bcbbdaaaaa.
Reduce LHS:
| [17] | aaaaabbb(dc) |
| ⇒ aaaaabbb |
Defines rule #18.