| Back: | ⟨a, b | aabbabbaaab=1⟩ |
|---|
Completion settings:
Axiom: aabbabbaaab=1.
Referenced by [4].
Axiom: aabbab=c.
Referenced by [4], [6], [7], [11], [15].
Axiom: aaabc=d.
Defines rule #11.
Referenced by [5], [7], [17], [18], [19], [25], [30], [32], [33].
Overlap of [1] aabbabbaaab=1 with [2] aabbab=c:
Critical pair: cbaaab=1.
Referenced by [5], [6], [10], [12], [13], [14], [16].
Overlap of [4] cbaaab=1 with [3] aaabc=d:
Critical pair: cbd=c.
Referenced by [8].
Overlap of [4] cbaaab=1 with [2] aabbab=c:
Critical pair: cbac=bab.
Defines rule #4.
Referenced by [7], [8], [9], [22].
Overlap of [3] aaabc=d with [6] cbac=bab:
Critical pair: aaabbab=dbac.
Reduce LHS:
| [2] | a(aabbab) |
| ⇒ ac |
Flip LHS and RHS.
Referenced by [10].
Overlap of [6] cbac=bab with [5] cbd=c:
Critical pair: cbac=babbd.
Reduce LHS:
| [6] | (cbac) |
| ⇒ bab |
Flip LHS and RHS.
Referenced by [13].
Overlap of [6] cbac=bab with [6] cbac=bab:
Critical pair: cbabab=babbac.
Referenced by [24].
Overlap of [7] dbac=ac with [4] cbaaab=1:
Critical pair: dba=acbaaab.
Reduce RHS:
| [4] | a(cbaaab) |
| ⇒ a |
Referenced by [11].
Overlap of [10] dba=a with [2] aabbab=c:
Critical pair: dbc=aabbab.
Reduce RHS:
| [2] | (aabbab) |
| ⇒ c |
Referenced by [12].
Overlap of [11] dbc=c with [4] cbaaab=1:
Critical pair: db=cbaaab.
Reduce RHS:
| [4] | (cbaaab) |
| ⇒ 1 |
Defines rule #1.
Referenced by [21], [26], [32], [34], [35].
Overlap of [4] cbaaab=1 with [8] babbd=bab:
Critical pair: cbaaabab=abbd.
Reduce LHS:
| [4] | (cbaaab)ab |
| ⇒ ab |
Flip LHS and RHS.
Overlap of [4] cbaaab=1 with [13] abbd=ab:
Critical pair: cbaaab=bd.
Reduce LHS:
| [4] | (cbaaab) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [15], [16], [20], [23], [27], [30], [31], [39].
Overlap of [2] aabbab=c with [14] bd=1:
Critical pair: aabba=cd.
Referenced by [19].
Overlap of [4] cbaaab=1 with [14] bd=1:
Critical pair: cbaaa=d.
Defines rule #12.
Referenced by [17], [18], [28], [29], [37], [38].
Overlap of [16] cbaaa=d with [3] aaabc=d:
Critical pair: cbad=dabc.
Flip LHS and RHS.
Defines rule #6.
Overlap of [16] cbaaa=d with [3] aaabc=d:
Critical pair: cbaad=daabc.
Flip LHS and RHS.
Defines rule #9.
Referenced by [19].
Overlap of [15] aabba=cd with [3] aaabc=d:
Critical pair: aabbd=cdaabc.
Reduce LHS:
| [13] | a(abbd) |
| ⇒ aab |
Reduce RHS:
| [18] | c(daabc) |
| ⇒ ccbaad |
Flip LHS and RHS.
Referenced by [25], [26], [32].
Overlap of [14] bd=1 with [17] dabc=cbad:
Critical pair: bcbad=abc.
Referenced by [21].
Overlap of [20] bcbad=abc with [12] db=1:
Critical pair: bcba=abcb.
Defines rule #5.
Overlap of [21] bcba=abcb with [6] cbac=bab:
Critical pair: bbab=abcbc.
Referenced by [23].
Overlap of [22] bbab=abcbc with [14] bd=1:
Critical pair: bba=abcbcd.
Defines rule #3.
Simplify [9] cbabab=babbac.
Reduce RHS:
| [23] | ba(bba)c |
| ⇒ baabcbcdc |
Referenced by [39].
Overlap of [3] aaabc=d with [19] ccbaad=aab:
Critical pair: aaabaab=dcbaad.
Referenced by [27].
Overlap of [19] ccbaad=aab with [12] db=1:
Critical pair: ccbaa=aabb.
Defines rule #8.
Referenced by [32].
Overlap of [25] aaabaab=dcbaad with [14] bd=1:
Critical pair: aaabaa=dcbaadd.
Defines rule #18.
Referenced by [28], [29], [30].
Overlap of [16] cbaaa=d with [27] aaabaa=dcbaadd:
Critical pair: cbadcbaadd=dabaa.
Flip LHS and RHS.
Defines rule #14.
Overlap of [16] cbaaa=d with [27] aaabaa=dcbaadd:
Critical pair: cbaadcbaadd=daabaa.
Flip LHS and RHS.
Referenced by [36].
Overlap of [27] aaabaa=dcbaadd with [3] aaabc=d:
Critical pair: aaabd=dcbaaddabc.
Reduce LHS:
| [14] | aaa(bd) |
| ⇒ aaa |
Reduce RHS:
| [17] | dcbaad(dabc) |
| ⇒ dcbaadcbad |
Flip LHS and RHS.
Overlap of [14] bd=1 with [30] dcbaadcbad=aaa:
Critical pair: baaa=cbaadcbad.
Flip LHS and RHS.
Referenced by [34].
Overlap of [19] ccbaad=aab with [30] dcbaadcbad=aaa:
Critical pair: ccbaaaaa=aabcbaadcbad.
Reduce LHS:
| [26] | (ccbaa)aaa |
| [23] | ⇒ aa(bba)aa |
| [3] | ⇒ (aaabc)bcdaa |
| [12] | ⇒ (db)cdaa |
| ⇒ cdaa |
Reduce RHS:
| [21] | aa(bcba)adcbad |
| [3] | ⇒ (aaabc)badcbad |
| [12] | ⇒ (db)adcbad |
| ⇒ adcbad |
Defines rule #10.
Referenced by [33].
Overlap of [3] aaabc=d with [32] cdaa=adcbad:
Critical pair: aaabadcbad=ddaa.
Referenced by [35].
Overlap of [31] cbaadcbad=baaa with [12] db=1:
Critical pair: cbaadcba=baaab.
Defines rule #13.
Referenced by [36].
Overlap of [33] aaabadcbad=ddaa with [12] db=1:
Critical pair: aaabadcba=ddaab.
Defines rule #19.
Simplify [29] daabaa=cbaadcbaadd.
Reduce RHS:
| [34] | (cbaadcba)add |
| ⇒ baaabadd |
Defines rule #16.
Overlap of [16] cbaaa=d with [35] aaabadcba=ddaab:
Critical pair: cbaddaab=dabadcba.
Flip LHS and RHS.
Defines rule #15.
Overlap of [16] cbaaa=d with [35] aaabadcba=ddaab:
Critical pair: cbaaddaab=daabadcba.
Flip LHS and RHS.
Defines rule #17.
Overlap of [24] cbabab=baabcbcdc with [14] bd=1:
Critical pair: cbaba=baabcbcdcd.
Defines rule #7.