| Back: | ⟨a, b | aabaaaababa=1⟩ |
|---|
Completion settings:
Axiom: aabaaaababa=1.
Referenced by [4], [5], [6], [7], [10].
Axiom: abaaaba=c.
Referenced by [3], [5], [6], [8], [17].
Overlap of [2] abaaaba=c with [2] abaaaba=c:
Critical pair: abaac=caaba.
Flip LHS and RHS.
Referenced by [8].
Overlap of [1] aabaaaababa=1 with [1] aabaaaababa=1:
Critical pair: aabaaaabab=abaaaababa.
Overlap of [1] aabaaaababa=1 with [2] abaaaba=c:
Critical pair: aabaaaabc=aaba.
Overlap of [2] abaaaba=c with [1] aabaaaababa=1:
Critical pair: aba=caaababa.
Flip LHS and RHS.
Overlap of [6] caaababa=aba with [1] aabaaaababa=1:
Critical pair: caaabab=abaabaaaababa.
Reduce RHS:
| [4] | ab(aabaaaabab)a |
| ⇒ ababaaaababaa |
Flip LHS and RHS.
Referenced by [11].
Overlap of [5] aabaaaabc=aaba with [3] caaba=abaac:
Critical pair: aabaaaababaac=aabaaaba.
Reduce LHS:
| [4] | (aabaaaabab)aac |
| ⇒ abaaaababaaac |
Reduce RHS:
| [2] | a(abaaaba) |
| ⇒ ac |
Referenced by [9].
Overlap of [6] caaababa=aba with [8] abaaaababaaac=ac:
Critical pair: caaabac=abaaaababaaac.
Reduce RHS:
| [8] | (abaaaababaaac) |
| ⇒ ac |
Referenced by [12].
Overlap of [1] aabaaaababa=1 with [4] aabaaaabab=abaaaababa:
Critical pair: abaaaababaa=1.
Referenced by [11], [13], [14], [15], [16], [19], [20], [22].
Overlap of [7] ababaaaababaa=caaabab with [10] abaaaababaa=1:
Critical pair: ab=caaabab.
Flip LHS and RHS.
Overlap of [9] caaabac=ac with [11] caaabab=ab:
Critical pair: caaabaab=acaaabab.
Reduce RHS:
| [11] | a(caaabab) |
| ⇒ aab |
Referenced by [21].
Overlap of [6] caaababa=aba with [10] abaaaababaa=1:
Critical pair: caaab=abaaaababaa.
Reduce RHS:
| [10] | (abaaaababaa) |
| ⇒ 1 |
Referenced by [16], [17], [18], [19], [21], [23], [24], [27].
Overlap of [10] abaaaababaa=1 with [10] abaaaababaa=1:
Critical pair: abaaaab=aababaa.
Flip LHS and RHS.
Referenced by [15].
Overlap of [10] abaaaababaa=1 with [10] abaaaababaa=1:
Critical pair: abaaaababa=baaaababaa.
Reduce RHS:
| [14] | baa(aababaa) |
| ⇒ baaabaaaab |
Referenced by [16], [19], [20], [22].
Overlap of [11] caaabab=ab with [10] abaaaababaa=1:
Critical pair: caaab=abaaaababaa.
Reduce LHS:
| [13] | (caaab) |
| ⇒ 1 |
Reduce RHS:
| [15] | (abaaaababa)a |
| ⇒ baaabaaaaba |
Flip LHS and RHS.
Overlap of [13] caaab=1 with [2] abaaaba=c:
Critical pair: caac=aaaba.
Flip LHS and RHS.
Overlap of [13] caaab=1 with [5] aabaaaabc=aaba:
Critical pair: caaaba=aaaabc.
Reduce LHS:
| [13] | (caaab)a |
| ⇒ a |
Flip LHS and RHS.
Overlap of [10] abaaaababaa=1 with [18] aaaabc=a:
Critical pair: abaaaababa=aabc.
Reduce LHS:
| [15] | (abaaaababa) |
| [17] | ⇒ b(aaaba)aaab |
| [13] | ⇒ bcaa(caaab) |
| ⇒ bcaa |
Flip LHS and RHS.
Overlap of [10] abaaaababaa=1 with [18] aaaabc=a:
Critical pair: abaaaababaa=aaabc.
Reduce LHS:
| [15] | (abaaaababa)a |
| [16] | ⇒ (baaabaaaaba) |
| ⇒ 1 |
Reduce RHS:
| [19] | a(aabc) |
| ⇒ abcaa |
Flip LHS and RHS.
Referenced by [21].
Overlap of [12] caaabaab=aab with [20] abcaa=1:
Critical pair: caaaba=aabcaa.
Reduce LHS:
| [13] | (caaab)a |
| ⇒ a |
Reduce RHS:
| [19] | (aabc)aa |
| ⇒ bcaaaa |
Flip LHS and RHS.
Referenced by [22].
Overlap of [21] bcaaaa=a with [10] abaaaababaa=1:
Critical pair: bcaaa=abaaaababaa.
Reduce RHS:
| [15] | (abaaaababa)a |
| [16] | ⇒ (baaabaaaaba) |
| ⇒ 1 |
Defines rule #3.
Overlap of [13] caaab=1 with [17] aaaba=caac:
Critical pair: ccaac=a.
Defines rule #2.
Referenced by [24], [25], [28].
Overlap of [23] ccaac=a with [13] caaab=1:
Critical pair: ccaa=aaaab.
Flip LHS and RHS.
Referenced by [26].
Overlap of [23] ccaac=a with [23] ccaac=a:
Critical pair: ccaaa=acaac.
Defines rule #1.
Referenced by [27].
Overlap of [22] bcaaa=1 with [24] aaaab=ccaa:
Critical pair: bcccaa=ab.
Flip LHS and RHS.
Defines rule #4.
Overlap of [25] ccaaa=acaac with [13] caaab=1:
Critical pair: c=acaacb.
Flip LHS and RHS.
Referenced by [28].
Overlap of [23] ccaac=a with [27] acaacb=c:
Critical pair: ccac=aaacb.
Flip LHS and RHS.
Referenced by [29].
Overlap of [22] bcaaa=1 with [28] aaacb=ccac:
Critical pair: bcccac=cb.
Flip LHS and RHS.
Defines rule #5.