| Back: | ⟨a, b | aababbaba=1⟩ |
|---|
Completion settings:
Axiom: aababbaba=1.
Referenced by [4].
Axiom: aaa=c.
Defines rule #5.
Referenced by [5], [6], [10], [20], [26], [27].
Axiom: babbab=d.
Referenced by [4], [11], [12], [17].
Overlap of [1] aababbaba=1 with [3] babbab=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.
Flip LHS and RHS.
Defines rule #1.
Referenced by [15], [16], [22], [23].
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.
Flip LHS and RHS.
Overlap of [6] cda=a with [4] aada=1:
Critical pair: cd=aada.
Reduce RHS:
| [4] | (aada) |
| ⇒ 1 |
Defines rule #2.
Referenced by [13], [15], [21], [22], [28].
Overlap of [4] aada=1 with [7] ada=aad:
Critical pair: aadaad=da.
Reduce LHS:
| [4] | (aada)ad |
| ⇒ ad |
Flip LHS and RHS.
Defines rule #3.
Referenced by [10], [12], [24], [25].
Overlap of [9] da=ad with [2] aaa=c:
Critical pair: dc=adaa.
Reduce RHS:
| [7] | (ada)a |
| [4] | ⇒ (aada) |
| ⇒ 1 |
Defines rule #4.
Referenced by [14], [17], [18], [19], [22].
Overlap of [3] babbab=d with [3] babbab=d:
Critical pair: babd=dbab.
Flip LHS and RHS.
Defines rule #7.
Referenced by [13], [22], [24], [25].
Overlap of [3] babbab=d with [3] babbab=d:
Critical pair: babbad=dabbab.
Reduce RHS:
| [9] | (da)bbab |
| ⇒ adbbab |
Flip LHS and RHS.
Defines rule #13.
Referenced by [15].
Overlap of [8] cd=1 with [11] dbab=babd:
Critical pair: cbabd=bab.
Referenced by [14].
Overlap of [13] cbabd=bab with [10] dc=1:
Critical pair: cbab=babc.
Defines rule #6.
Referenced by [15], [16], [17], [23].
Overlap of [5] ca=ac with [12] adbbab=babbad:
Critical pair: cbabbad=acdbbab.
Reduce LHS:
| [14] | (cbab)bad |
| ⇒ babcbad |
Reduce RHS:
| [8] | a(cd)bbab |
| ⇒ abbab |
Flip LHS and RHS.
Defines rule #8.
Overlap of [5] ca=ac with [15] abbab=babcbad:
Critical pair: cbabcbad=acbbab.
Reduce LHS:
| [14] | (cbab)cbad |
| ⇒ babccbad |
Flip LHS and RHS.
Defines rule #12.
Referenced by [26].
Overlap of [14] cbab=babc with [15] abbab=babcbad:
Critical pair: cbbabcbad=babcbab.
Reduce RHS:
| [14] | bab(cbab) |
| [3] | ⇒ (babbab)c |
| [10] | ⇒ (dc) |
| ⇒ 1 |
Referenced by [18].
Overlap of [10] dc=1 with [17] cbbabcbad=1:
Critical pair: d=bbabcbad.
Flip LHS and RHS.
Referenced by [19].
Overlap of [18] bbabcbad=d with [10] dc=1:
Critical pair: bbabcba=dc.
Reduce RHS:
| [10] | (dc) |
| ⇒ 1 |
Referenced by [20].
Overlap of [19] bbabcba=1 with [2] aaa=c:
Critical pair: bbabcbc=aa.
Referenced by [21].
Overlap of [20] bbabcbc=aa with [8] cd=1:
Critical pair: bbabcb=aad.
Defines rule #16.
Referenced by [22].
Overlap of [21] bbabcb=aad with [21] bbabcb=aad:
Critical pair: bbabcaad=aadbabcb.
Reduce LHS:
| [5] | bbab(ca)ad |
| [5] | ⇒ bbaba(ca)d |
| [8] | ⇒ bbabaa(cd) |
| ⇒ bbabaa |
Reduce RHS:
| [11] | aa(dbab)cb |
| [10] | ⇒ aabab(dc)b |
| ⇒ aababb |
Flip LHS and RHS.
Defines rule #9.
Overlap of [5] ca=ac with [22] aababb=bbabaa:
Critical pair: cbbabaa=acababb.
Reduce RHS:
| [5] | a(ca)babb |
| [14] | ⇒ aa(cbab)b |
| ⇒ aababcb |
Flip LHS and RHS.
Defines rule #10.
Overlap of [9] da=ad with [22] aababb=bbabaa:
Critical pair: dbbabaa=adababb.
Reduce RHS:
| [9] | a(da)babb |
| [11] | ⇒ aa(dbab)b |
| ⇒ aababdb |
Flip LHS and RHS.
Defines rule #11.
Referenced by [25].
Overlap of [9] da=ad with [24] aababdb=dbbabaa:
Critical pair: ddbbabaa=adababdb.
Reduce RHS:
| [9] | a(da)babdb |
| [11] | ⇒ aa(dbab)db |
| ⇒ aababddb |
Referenced by [27].
Overlap of [2] aaa=c with [16] acbbab=babccbad:
Critical pair: aababccbad=ccbbab.
Flip LHS and RHS.
Defines rule #14.
Overlap of [25] ddbbabaa=aababddb with [2] aaa=c:
Critical pair: ddbbabc=aababddba.
Referenced by [28].
Overlap of [27] ddbbabc=aababddba with [8] cd=1:
Critical pair: ddbbab=aababddbad.
Defines rule #15.