| Back: | ⟨a, b | abaaab=aabba⟩ |
|---|
Completion settings:
Axiom: abaaab=aabba.
Flip LHS and RHS.
Referenced by [3].
Axiom: aba=c.
Defines rule #1.
Referenced by [3], [4], [5], [6], [7], [8], [9], [10], [11], [12], [13], [15], [18].
Simplify [1] aabba=abaaab.
Reduce RHS:
| [2] | (aba)aab |
| ⇒ caab |
Defines rule #3.
Referenced by [5], [6], [7], [8].
Overlap of [2] aba=c with [2] aba=c:
Critical pair: abc=cba.
Flip LHS and RHS.
Defines rule #2.
Overlap of [3] aabba=caab with [3] aabba=caab:
Critical pair: aabbcaab=caababba.
Reduce RHS:
| [2] | ca(aba)bba |
| ⇒ cacbba |
Referenced by [10].
Overlap of [3] aabba=caab with [2] aba=c:
Critical pair: aabbc=caabba.
Reduce RHS:
| [3] | c(aabba) |
| ⇒ ccaab |
Defines rule #4.
Referenced by [8], [9], [10], [11], [12], [14], [15], [18], [19].
Overlap of [2] aba=c with [3] aabba=caab:
Critical pair: abcaab=cabba.
Flip LHS and RHS.
Defines rule #5.
Overlap of [3] aabba=caab with [6] aabbc=ccaab:
Critical pair: aabbccaab=caababbc.
Reduce LHS:
| [6] | (aabbc)caab |
| ⇒ ccaabcaab |
Reduce RHS:
| [2] | ca(aba)bbc |
| ⇒ cacbbc |
Defines rule #9.
Referenced by [13], [14], [15].
Overlap of [2] aba=c with [6] aabbc=ccaab:
Critical pair: abccaab=cabbc.
Flip LHS and RHS.
Defines rule #6.
Simplify [5] aabbcaab=cacbba.
Reduce LHS:
| [6] | (aabbc)aab |
| [2] | ⇒ cca(aba)ab |
| ⇒ ccacab |
Flip LHS and RHS.
Defines rule #7.
Referenced by [11], [12], [16].
Overlap of [10] cacbba=ccacab with [6] aabbc=ccaab:
Critical pair: cacbbccaab=ccacababbc.
Reduce RHS:
| [2] | ccac(aba)bbc |
| ⇒ ccaccbbc |
Defines rule #13.
Referenced by [17], [19], [20], [21].
Overlap of [6] aabbc=ccaab with [10] cacbba=ccacab:
Critical pair: aabbccacab=ccaabacbba.
Reduce LHS:
| [6] | (aabbc)cacab |
| ⇒ ccaabcacab |
Reduce RHS:
| [2] | cca(aba)cbba |
| ⇒ ccaccbba |
Flip LHS and RHS.
Defines rule #10.
Referenced by [18].
Overlap of [8] ccaabcaab=cacbbc with [2] aba=c:
Critical pair: ccaabcac=cacbbca.
Flip LHS and RHS.
Defines rule #8.
Referenced by [15], [16], [17], [20], [21].
Overlap of [8] ccaabcaab=cacbbc with [6] aabbc=ccaab:
Critical pair: ccaabcccaab=cacbbcbc.
Flip LHS and RHS.
Defines rule #12.
Referenced by [21].
Overlap of [6] aabbc=ccaab with [13] cacbbca=ccaabcac:
Critical pair: aabbccaabcac=ccaabacbbca.
Reduce LHS:
| [6] | (aabbc)caabcac |
| [8] | ⇒ (ccaabcaab)cac |
| ⇒ cacbbccac |
Reduce RHS:
| [2] | cca(aba)cbbca |
| ⇒ ccaccbbca |
Flip LHS and RHS.
Defines rule #11.
Overlap of [13] cacbbca=ccaabcac with [10] cacbba=ccacab:
Critical pair: cacbbccacab=ccaabcaccbba.
Flip LHS and RHS.
Defines rule #14.
Overlap of [13] cacbbca=ccaabcac with [13] cacbbca=ccaabcac:
Critical pair: cacbbccaabcac=ccaabcaccbbca.
Reduce LHS:
| [11] | (cacbbccaab)cac |
| ⇒ ccaccbbccac |
Flip LHS and RHS.
Defines rule #15.
Overlap of [12] ccaccbba=ccaabcacab with [6] aabbc=ccaab:
Critical pair: ccaccbbccaab=ccaabcacababbc.
Reduce RHS:
| [2] | ccaabcac(aba)bbc |
| ⇒ ccaabcaccbbc |
Defines rule #17.
Overlap of [11] cacbbccaab=ccaccbbc with [6] aabbc=ccaab:
Critical pair: cacbbccccaab=ccaccbbcbc.
Flip LHS and RHS.
Defines rule #16.
Overlap of [13] cacbbca=ccaabcac with [11] cacbbccaab=ccaccbbc:
Critical pair: cacbbccaccbbc=ccaabcaccbbccaab.
Flip LHS and RHS.
Defines rule #19.
Overlap of [13] cacbbca=ccaabcac with [14] cacbbcbc=ccaabcccaab:
Critical pair: cacbbccaabcccaab=ccaabcaccbbcbc.
Reduce LHS:
| [11] | (cacbbccaab)cccaab |
| ⇒ ccaccbbccccaab |
Flip LHS and RHS.
Defines rule #18.