| Back: | ⟨a, b | aababbababa=1⟩ |
|---|
Completion settings:
Axiom: aababbababa=1.
Referenced by [4].
Axiom: aaa=c.
Defines rule #5.
Referenced by [5], [6], [11], [15], [17], [20], [24], [27].
Axiom: babbabab=d.
Referenced by [4], [12], [17], [18].
Overlap of [1] aababbababa=1 with [3] babbabab=d:
Critical pair: aada=1.
Referenced by [6], [7], [8], [9], [10].
Overlap of [2] aaa=c with [2] aaa=c:
Critical pair: ac=ca.
Defines rule #3.
Referenced by [16].
Overlap of [2] aaa=c with [4] aada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [8].
Overlap of [4] aada=1 with [4] aada=1:
Critical pair: aad=ada.
Referenced by [8], [9], [10], [11].
Overlap of [6] cda=a with [4] aada=1:
Critical pair: cd=aada.
Reduce RHS:
| [7] | (aad)a |
| ⇒ adaa |
Flip LHS and RHS.
Overlap of [4] aada=1 with [7] aad=ada:
Critical pair: adaa=1.
Reduce LHS:
| [8] | (adaa) |
| ⇒ cd |
Defines rule #1.
Referenced by [10], [11], [13], [17], [23], [28].
Overlap of [4] aada=1 with [7] aad=ada:
Critical pair: aadada=ad.
Reduce LHS:
| [7] | (aad)ada |
| [8] | ⇒ (adaa)da |
| [9] | ⇒ (cd)da |
| ⇒ da |
Flip LHS and RHS.
Defines rule #4.
Referenced by [11], [12], [14], [18], [22].
Overlap of [2] aaa=c with [10] ad=da:
Critical pair: aada=cd.
Reduce LHS:
| [7] | (aad)a |
| [10] | ⇒ (ad)aa |
| [2] | ⇒ d(aaa) |
| ⇒ dc |
Reduce RHS:
| [9] | (cd) |
| ⇒ 1 |
Defines rule #2.
Referenced by [15], [25], [26], [27].
Overlap of [3] babbabab=d with [3] babbabab=d:
Critical pair: babbad=dbabab.
Reduce LHS:
| [10] | babb(ad) |
| ⇒ babbda |
Flip LHS and RHS.
Defines rule #7.
Overlap of [9] cd=1 with [12] dbabab=babbda:
Critical pair: cbabbda=babab.
Referenced by [15].
Overlap of [10] ad=da with [12] dbabab=babbda:
Critical pair: ababbda=dababab.
Flip LHS and RHS.
Defines rule #10.
Referenced by [22].
Overlap of [13] cbabbda=babab with [2] aaa=c:
Critical pair: cbabbdc=bababaa.
Reduce LHS:
| [11] | cbabb(dc) |
| ⇒ cbabb |
Defines rule #6.
Referenced by [16], [17], [24].
Overlap of [5] ac=ca with [15] cbabb=bababaa:
Critical pair: abababaa=cababb.
Flip LHS and RHS.
Defines rule #9.
Overlap of [15] cbabb=bababaa with [3] babbabab=d:
Critical pair: cd=bababaaabab.
Reduce LHS:
| [9] | (cd) |
| ⇒ 1 |
Reduce RHS:
| [2] | babab(aaa)bab |
| ⇒ bababcbab |
Flip LHS and RHS.
Referenced by [18], [19], [24].
Overlap of [17] bababcbab=1 with [3] babbabab=d:
Critical pair: bababcbad=abbabab.
Reduce LHS:
| [10] | bababcb(ad) |
| ⇒ bababcbda |
Flip LHS and RHS.
Defines rule #13.
Overlap of [17] bababcbab=1 with [17] bababcbab=1:
Critical pair: bababc=abcbab.
Flip LHS and RHS.
Defines rule #8.
Overlap of [2] aaa=c with [19] abcbab=bababc:
Critical pair: aabababc=cbcbab.
Overlap of [19] abcbab=bababc with [19] abcbab=bababc:
Critical pair: abcbbababc=bababccbab.
Referenced by [28].
Overlap of [10] ad=da with [14] dababab=ababbda:
Critical pair: aababbda=daababab.
Flip LHS and RHS.
Referenced by [26].
Overlap of [20] aabababc=cbcbab with [9] cd=1:
Critical pair: aababab=cbcbabd.
Defines rule #12.
Referenced by [26].
Overlap of [20] aabababc=cbcbab with [17] bababcbab=1:
Critical pair: aa=cbcbabbab.
Reduce RHS:
| [15] | cb(cbabb)ab |
| [2] | ⇒ cbbabab(aaa)b |
| ⇒ cbbababcb |
Flip LHS and RHS.
Referenced by [25].
Overlap of [11] dc=1 with [24] cbbababcb=aa:
Critical pair: daa=bbababcb.
Flip LHS and RHS.
Defines rule #14.
Overlap of [22] daababab=aababbda with [23] aababab=cbcbabd:
Critical pair: dcbcbabd=aababbda.
Reduce LHS:
| [11] | (dc)bcbabd |
| ⇒ bcbabd |
Flip LHS and RHS.
Referenced by [27].
Overlap of [26] aababbda=bcbabd with [2] aaa=c:
Critical pair: aababbdc=bcbabdaa.
Reduce LHS:
| [11] | aababb(dc) |
| ⇒ aababb |
Defines rule #11.
Overlap of [21] abcbbababc=bababccbab with [9] cd=1:
Critical pair: abcbbabab=bababccbabd.
Defines rule #15.