| Back: | ⟨a, b | abaaba=aabaa⟩ |
|---|
Completion settings:
Axiom: abaaba=aabaa.
Referenced by [3].
Axiom: aabaa=c.
Defines rule #13.
Referenced by [3], [4], [6], [7], [9].
Simplify [1] abaaba=aabaa.
Reduce RHS:
| [2] | (aabaa) |
| ⇒ c |
Defines rule #16.
Referenced by [5], [6], [7], [8], [10], [11], [13].
Overlap of [2] aabaa=c with [2] aabaa=c:
Critical pair: aabc=cbaa.
Flip LHS and RHS.
Referenced by [5].
Overlap of [3] abaaba=c with [3] abaaba=c:
Critical pair: abaabc=cbaaba.
Reduce RHS:
| [4] | (cbaa)ba |
| ⇒ aabcba |
Referenced by [16].
Overlap of [3] abaaba=c with [2] aabaa=c:
Critical pair: abc=ca.
Flip LHS and RHS.
Defines rule #5.
Referenced by [8], [9], [11], [14].
Overlap of [2] aabaa=c with [3] abaaba=c:
Critical pair: ac=cba.
Flip LHS and RHS.
Defines rule #6.
Referenced by [8], [9], [11], [16].
Overlap of [7] cba=ac with [3] abaaba=c:
Critical pair: cbc=acbaaba.
Reduce RHS:
| [7] | a(cba)aba |
| [6] | ⇒ aa(ca)ba |
| [7] | ⇒ aaab(cba) |
| ⇒ aaabac |
Flip LHS and RHS.
Defines rule #12.
Referenced by [9], [12], [15].
Overlap of [2] aabaa=c with [8] aaabac=cbc:
Critical pair: aabcbc=cabac.
Reduce RHS:
| [6] | (ca)bac |
| [7] | ⇒ ab(cba)c |
| ⇒ abacc |
Flip LHS and RHS.
Defines rule #7.
Referenced by [10], [11], [12].
Overlap of [3] abaaba=c with [9] abacc=aabcbc:
Critical pair: abaaabcbc=ccc.
Defines rule #15.
Referenced by [19].
Overlap of [3] abaaba=c with [9] abacc=aabcbc:
Critical pair: abaabaabcbc=cbacc.
Reduce LHS:
| [3] | (abaaba)abcbc |
| [6] | ⇒ (ca)bcbc |
| ⇒ abcbcbc |
Reduce RHS:
| [7] | (cba)cc |
| ⇒ accc |
Defines rule #4.
Referenced by [13], [14], [17], [18], [19].
Overlap of [8] aaabac=cbc with [9] abacc=aabcbc:
Critical pair: aaaabcbc=cbcc.
Defines rule #11.
Referenced by [18].
Overlap of [3] abaaba=c with [11] abcbcbc=accc:
Critical pair: abaabaccc=cbcbcbc.
Reduce LHS:
| [3] | (abaaba)ccc |
| ⇒ cccc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [15].
Overlap of [6] ca=abc with [11] abcbcbc=accc:
Critical pair: caccc=abcbcbcbc.
Reduce LHS:
| [6] | (ca)ccc |
| ⇒ abcccc |
Reduce RHS:
| [11] | (abcbcbc)bc |
| ⇒ acccbc |
Defines rule #3.
Overlap of [8] aaabac=cbc with [13] cbcbcbc=cccc:
Critical pair: aaabacccc=cbcbcbcbc.
Reduce LHS:
| [8] | (aaabac)ccc |
| ⇒ cbcccc |
Reduce RHS:
| [13] | (cbcbcbc)bc |
| ⇒ ccccbc |
Defines rule #1.
Simplify [5] abaabc=aabcba.
Reduce RHS:
| [7] | aab(cba) |
| ⇒ aabac |
Defines rule #8.
Referenced by [17].
Overlap of [16] abaabc=aabac with [11] abcbcbc=accc:
Critical pair: abaaccc=aabacbcbc.
Defines rule #9.
Overlap of [12] aaaabcbc=cbcc with [11] abcbcbc=accc:
Critical pair: aaaaccc=cbccbc.
Defines rule #10.
Overlap of [10] abaaabcbc=ccc with [11] abcbcbc=accc:
Critical pair: abaaaccc=cccbc.
Defines rule #14.