| Back: | ⟨a, b | aaaa=1, abbab=bb⟩ |
|---|
Completion settings:
Axiom: aaaa=1.
Defines rule #10.
Referenced by [3], [11], [17].
Axiom: abbab=bb.
Defines rule #4.
Referenced by [3], [4], [5], [9], [12], [15].
Overlap of [1] aaaa=1 with [2] abbab=bb:
Critical pair: aaabb=bbab.
Defines rule #7.
Referenced by [5].
Overlap of [2] abbab=bb with [2] abbab=bb:
Critical pair: abbbb=bbbab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [6], [7], [8], [9], [10], [12], [14].
Overlap of [3] aaabb=bbab with [2] abbab=bb:
Critical pair: aabb=bbabab.
Flip LHS and RHS.
Defines rule #6.
Overlap of [4] bbbab=abbbb with [5] bbabab=aabb:
Critical pair: baabb=abbbbab.
Reduce RHS:
| [4] | ab(bbbab) |
| ⇒ ababbbb |
Defines rule #5.
Referenced by [7], [8], [9], [10], [12].
Overlap of [5] bbabab=aabb with [4] bbbab=abbbb:
Critical pair: bbabaabbbb=aabbbbab.
Reduce LHS:
| [6] | bba(baabb)bb |
| ⇒ bbaababbbbbb |
Reduce RHS:
| [4] | aab(bbbab) |
| ⇒ aababbbb |
Referenced by [13].
Overlap of [4] bbbab=abbbb with [6] baabb=ababbbb:
Critical pair: bbbaababbbb=abbbbaabb.
Reduce RHS:
| [6] | abbb(baabb) |
| [4] | ⇒ a(bbbab)abbbb |
| [4] | ⇒ aab(bbbab)bbb |
| ⇒ aababbbbbbb |
Referenced by [16].
Overlap of [6] baabb=ababbbb with [2] abbab=bb:
Critical pair: babb=ababbbbab.
Reduce RHS:
| [4] | abab(bbbab) |
| ⇒ abababbbb |
Flip LHS and RHS.
Referenced by [11], [12], [14], [18].
Overlap of [6] baabb=ababbbb with [4] bbbab=abbbb:
Critical pair: baababbbb=ababbbbbbab.
Reduce RHS:
| [4] | ababbb(bbbab) |
| [4] | ⇒ aba(bbbab)bbb |
| [6] | ⇒ a(baabb)bbbbb |
| ⇒ aababbbbbbbbb |
Referenced by [12], [13], [16].
Overlap of [1] aaaa=1 with [9] abababbbb=babb:
Critical pair: aaababb=bababbbb.
Defines rule #11.
Referenced by [12].
Overlap of [9] abababbbb=babb with [6] baabb=ababbbb:
Critical pair: abababbbababbbb=babbaabb.
Reduce LHS:
| [4] | ababa(bbbab)abbbb |
| [4] | ⇒ ababaab(bbbab)bbb |
| [10] | ⇒ aba(baababbbb)bbb |
| [11] | ⇒ ab(aaababb)bbbbbbbbbb |
| [2] | ⇒ (abbab)abbbbbbbbbbbbbb |
| ⇒ bbabbbbbbbbbbbbbb |
Reduce RHS:
| [6] | bab(baabb) |
| [9] | ⇒ b(abababbbb) |
| ⇒ bbabb |
Referenced by [15].
Simplify [7] bbaababbbbbb=aababbbb.
Reduce LHS:
| [10] | b(baababbbb)bb |
| [10] | ⇒ (baababbbb)bbbbbbb |
| ⇒ aababbbbbbbbbbbbbbbb |
Referenced by [14].
Overlap of [13] aababbbbbbbbbbbbbbbb=aababbbb with [4] bbbab=abbbb:
Critical pair: aababbbbbbbbbbbbbabbbb=aababbbbab.
Reduce LHS:
| [4] | aababbbbbbbbbb(bbbab)bbb |
| [4] | ⇒ aababbbbbbb(bbbab)bbbbbb |
| [4] | ⇒ aababbbb(bbbab)bbbbbbbbb |
| [4] | ⇒ aabab(bbbab)bbbbbbbbbbbb |
| [9] | ⇒ a(abababbbb)bbbbbbbbbbbb |
| ⇒ ababbbbbbbbbbbbbb |
Reduce RHS:
| [4] | aabab(bbbab) |
| [9] | ⇒ a(abababbbb) |
| ⇒ ababb |
Referenced by [16], [17], [18].
Overlap of [2] abbab=bb with [12] bbabbbbbbbbbbbbbb=bbabb:
Critical pair: abbabb=bbbbbbbbbbbbbbb.
Reduce LHS:
| [2] | (abbab)b |
| ⇒ bbb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [8] bbbaababbbb=aababbbbbbb with [10] baababbbb=aababbbbbbbbb:
Critical pair: bbaababbbbbbbbb=aababbbbbbb.
Reduce LHS:
| [10] | b(baababbbb)bbbbb |
| [14] | ⇒ ba(ababbbbbbbbbbbbbb) |
| ⇒ baababb |
Defines rule #9.
Overlap of [1] aaaa=1 with [14] ababbbbbbbbbbbbbb=ababb:
Critical pair: aaaababb=babbbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aaaa)babb |
| ⇒ babb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [9] abababbbb=babb with [14] ababbbbbbbbbbbbbb=ababb:
Critical pair: abababb=babbbbbbbbbbbb.
Defines rule #8.