| Back: | ⟨a, b | abbabbba=ab⟩ |
|---|
Completion settings:
Axiom: abbabbba=ab.
Referenced by [3], [4], [6], [19].
Axiom: abbbbb=c.
Overlap of [1] abbabbba=ab with [1] abbabbba=ab:
Critical pair: abbabbbab=abbbabbba.
Reduce LHS:
| [1] | (abbabbba)b |
| ⇒ abb |
Flip LHS and RHS.
Overlap of [1] abbabbba=ab with [2] abbbbb=c:
Critical pair: abbabbbc=abbbbbb.
Reduce RHS:
| [2] | (abbbbb)b |
| ⇒ cb |
Overlap of [3] abbbabbba=abb with [3] abbbabbba=abb:
Critical pair: abbbabb=abbbbba.
Reduce RHS:
| [2] | (abbbbb)a |
| ⇒ ca |
Referenced by [6], [7], [8], [9].
Overlap of [1] abbabbba=ab with [5] abbbabb=ca:
Critical pair: abbca=abbb.
Flip LHS and RHS.
Referenced by [11].
Overlap of [3] abbbabbba=abb with [5] abbbabb=ca:
Critical pair: caba=abb.
Flip LHS and RHS.
Referenced by [8], [9], [10], [11], [14], [18], [19].
Overlap of [3] abbbabbba=abb with [5] abbbabb=ca:
Critical pair: abbbca=abbbb.
Reduce LHS:
| [7] | (abb)bca |
| ⇒ cababca |
Reduce RHS:
| [7] | (abb)bb |
| [7] | ⇒ cab(abb) |
| ⇒ cabcaba |
Flip LHS and RHS.
Referenced by [10].
Overlap of [5] abbbabb=ca with [4] abbabbbc=cb:
Critical pair: abbbcb=caabbbc.
Reduce LHS:
| [7] | (abb)bcb |
| ⇒ cababcb |
Reduce RHS:
| [7] | ca(abb)bc |
| ⇒ cacababc |
Referenced by [22].
Overlap of [2] abbbbb=c with [7] abb=caba:
Critical pair: cababbb=c.
Reduce LHS:
| [7] | cab(abb)b |
| [8] | ⇒ (cabcaba)b |
| ⇒ cababcab |
Referenced by [12].
Simplify [6] abbb=abbca.
Reduce LHS:
| [7] | (abb)b |
| ⇒ cabab |
Reduce RHS:
| [7] | (abb)ca |
| ⇒ cabaca |
Referenced by [12], [13], [16].
Simplify [10] cababcab=c.
Reduce LHS:
| [11] | (cabab)cab |
| ⇒ cabacacab |
Referenced by [13], [14], [15], [17].
Overlap of [12] cabacacab=c with [11] cabab=cabaca:
Critical pair: cabacacabaca=cab.
Reduce LHS:
| [12] | (cabacacab)aca |
| ⇒ caca |
Flip LHS and RHS.
Referenced by [14], [15], [16], [17], [18], [19], [22], [23].
Overlap of [12] cabacacab=c with [7] abb=caba:
Critical pair: cabacaccaba=cb.
Reduce LHS:
| [13] | (cab)acaccaba |
| [13] | ⇒ cacaacac(cab)a |
| ⇒ cacaacaccacaa |
Flip LHS and RHS.
Referenced by [20], [23], [24].
Overlap of [12] cabacacab=c with [12] cabacacab=c:
Critical pair: cabacac=cacacab.
Reduce LHS:
| [13] | (cab)acac |
| ⇒ cacaacac |
Reduce RHS:
| [13] | caca(cab) |
| ⇒ cacacaca |
Flip LHS and RHS.
Defines rule #7.
Referenced by [23], [25], [26], [30].
Overlap of [11] cabab=cabaca with [13] cab=caca:
Critical pair: cacaab=cabaca.
Reduce RHS:
| [13] | (cab)aca |
| ⇒ cacaaca |
Referenced by [19], [21], [22], [23].
Overlap of [12] cabacacab=c with [13] cab=caca:
Critical pair: cacaacacab=c.
Reduce LHS:
| [13] | cacaaca(cab) |
| ⇒ cacaacacaca |
Defines rule #10.
Referenced by [20], [21], [23], [24], [25], [26], [27], [30].
Overlap of [13] cab=caca with [7] abb=caba:
Critical pair: ccaba=cacab.
Reduce LHS:
| [13] | c(cab)a |
| ⇒ ccacaa |
Reduce RHS:
| [13] | ca(cab) |
| ⇒ cacaca |
Referenced by [20], [23], [24], [25].
Overlap of [1] abbabbba=ab with [7] abb=caba:
Critical pair: cabaabbba=ab.
Reduce LHS:
| [13] | (cab)aabbba |
| [7] | ⇒ cacaa(abb)ba |
| [13] | ⇒ cacaa(cab)aba |
| [16] | ⇒ cacaa(cacaab)a |
| ⇒ cacaacacaacaa |
Flip LHS and RHS.
Defines rule #12.
Referenced by [21].
Simplify [4] abbabbbc=cb.
Reduce RHS:
| [14] | (cb) |
| [18] | ⇒ cacaaca(ccacaa) |
| [17] | ⇒ (cacaacacaca)ca |
| ⇒ cca |
Referenced by [21].
Overlap of [20] abbabbbc=cca with [19] ab=cacaacacaacaa:
Critical pair: cacaacacaacaababbbc=cca.
Reduce LHS:
| [19] | cacaacacaaca(ab)abbbc |
| [17] | ⇒ cacaa(cacaacacaca)acacaacaaabbbc |
| [17] | ⇒ (cacaacacaca)acaaabbbc |
| [19] | ⇒ cacaa(ab)bbc |
| [19] | ⇒ cacaacacaacacaaca(ab)bc |
| [17] | ⇒ cacaacacaa(cacaacacaca)acacaacaabc |
| [17] | ⇒ cacaa(cacaacacaca)acaabc |
| [16] | ⇒ cacaa(cacaab)c |
| ⇒ cacaacacaacac |
Defines rule #11.
Referenced by [27], [28], [29], [30], [31], [32].
Simplify [9] cababcb=cacababc.
Reduce RHS:
| [13] | ca(cab)abc |
| [16] | ⇒ ca(cacaab)c |
| ⇒ cacacaacac |
Referenced by [23].
Overlap of [22] cababcb=cacacaacac with [13] cab=caca:
Critical pair: cacaabcb=cacacaacac.
Reduce LHS:
| [16] | (cacaab)cb |
| [14] | ⇒ cacaaca(cb) |
| [17] | ⇒ (cacaacacaca)acaccacaa |
| [18] | ⇒ caca(ccacaa) |
| [15] | ⇒ (cacacaca)ca |
| ⇒ cacaacacca |
Flip LHS and RHS.
Defines rule #9.
Simplify [14] cb=cacaacaccacaa.
Reduce RHS:
| [18] | cacaaca(ccacaa) |
| [17] | ⇒ (cacaacacaca)ca |
| ⇒ cca |
Defines rule #13.
Overlap of [18] ccacaa=cacaca with [17] cacaacacaca=c:
Critical pair: cc=cacacacacaca.
Reduce RHS:
| [15] | (cacacaca)caca |
| ⇒ cacaacaccaca |
Flip LHS and RHS.
Referenced by [29].
Overlap of [15] cacacaca=cacaacac with [17] cacaacacaca=c:
Critical pair: cacac=cacaacacacacaca.
Reduce RHS:
| [17] | (cacaacacaca)caca |
| ⇒ ccaca |
Flip LHS and RHS.
Defines rule #2.
Referenced by [29], [30], [31].
Overlap of [21] cacaacacaacac=cca with [17] cacaacacaca=c:
Critical pair: cacaac=ccaaca.
Flip LHS and RHS.
Defines rule #3.
Overlap of [21] cacaacacaacac=cca with [21] cacaacacaacac=cca:
Critical pair: cacaacca=ccaaacac.
Flip LHS and RHS.
Defines rule #8.
Overlap of [21] cacaacacaacac=cca with [25] cacaacaccaca=cc:
Critical pair: cacaacc=ccacaca.
Reduce RHS:
| [26] | (ccaca)ca |
| ⇒ cacacca |
Flip LHS and RHS.
Defines rule #5.
Referenced by [31].
Overlap of [26] ccaca=cacac with [21] cacaacacaacac=cca:
Critical pair: ccca=cacacacacaacac.
Reduce RHS:
| [15] | (cacacaca)caacac |
| [27] | ⇒ cacaaca(ccaaca)c |
| [17] | ⇒ (cacaacacaca)acc |
| ⇒ cacc |
Defines rule #1.
Overlap of [26] ccaca=cacac with [21] cacaacacaacac=cca:
Critical pair: ccacca=cacaccaacacaacac.
Reduce RHS:
| [29] | (cacacca)acacaacac |
| [26] | ⇒ cacaa(ccaca)caacac |
| [29] | ⇒ cacaa(cacacca)acac |
| [26] | ⇒ cacaacacaa(ccaca)c |
| [21] | ⇒ (cacaacacaacac)acc |
| ⇒ ccaacc |
Defines rule #4.
Overlap of [27] ccaaca=cacaac with [21] cacaacacaacac=cca:
Critical pair: ccaacca=cacaaccaacacaacac.
Reduce RHS:
| [27] | cacaa(ccaaca)caacac |
| [27] | ⇒ cacaacacaa(ccaaca)c |
| [21] | ⇒ (cacaacacaacac)aacc |
| ⇒ ccaaacc |
Defines rule #6.