| Back: | ⟨a, b | aa=1, abbbab=bba⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #4.
Referenced by [3], [5], [7], [9], [11], [13], [17], [21], [24].
Axiom: abbbab=bba.
Referenced by [3], [4], [6], [7], [12], [14], [18], [19].
Overlap of [1] aa=1 with [2] abbbab=bba:
Critical pair: abba=bbbab.
Defines rule #6.
Referenced by [4], [5], [6], [8], [11], [15], [20].
Overlap of [2] abbbab=bba with [3] abba=bbbab:
Critical pair: abbbbbbab=bbaba.
Flip LHS and RHS.
Referenced by [5], [15], [20].
Overlap of [3] abba=bbbab with [1] aa=1:
Critical pair: abb=bbbaba.
Reduce RHS:
| [4] | b(bbaba) |
| ⇒ babbbbbbab |
Flip LHS and RHS.
Referenced by [7], [8], [9], [13], [15], [16].
Overlap of [3] abba=bbbab with [2] abbbab=bba:
Critical pair: abbbba=bbbabbbbab.
Flip LHS and RHS.
Referenced by [21].
Overlap of [2] abbbab=bba with [5] babbbbbbab=abb:
Critical pair: abbbaabb=bbaabbbbbbab.
Reduce LHS:
| [1] | abbb(aa)bb |
| ⇒ abbbbb |
Reduce RHS:
| [1] | bb(aa)bbbbbbab |
| ⇒ bbbbbbbbab |
Flip LHS and RHS.
Overlap of [5] babbbbbbab=abb with [3] abba=bbbab:
Critical pair: babbbbbbbbbab=abbba.
Reduce LHS:
| [7] | bab(bbbbbbbbab) |
| ⇒ bababbbbb |
Referenced by [10].
Overlap of [5] babbbbbbab=abb with [5] babbbbbbab=abb:
Critical pair: babbbbbbaabb=abbabbbbbbab.
Reduce LHS:
| [1] | babbbbbb(aa)bb |
| ⇒ babbbbbbbb |
Reduce RHS:
| [5] | ab(babbbbbbab) |
| ⇒ ababb |
Flip LHS and RHS.
Referenced by [10], [13], [16], [23].
Simplify [8] bababbbbb=abbba.
Reduce LHS:
| [9] | b(ababb)bbb |
| ⇒ bbabbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [11], [12], [14], [18], [19], [22].
Overlap of [1] aa=1 with [10] abbba=bbabbbbbbbbbbb:
Critical pair: abbabbbbbbbbbbb=bbba.
Reduce LHS:
| [3] | (abba)bbbbbbbbbbb |
| ⇒ bbbabbbbbbbbbbbb |
Referenced by [14].
Overlap of [2] abbbab=bba with [10] abbba=bbabbbbbbbbbbb:
Critical pair: bbabbbbbbbbbbbb=bba.
Referenced by [18].
Overlap of [9] ababb=babbbbbbbb with [5] babbbbbbab=abb:
Critical pair: aabb=babbbbbbbbbbbbab.
Reduce LHS:
| [1] | (aa)bb |
| ⇒ bb |
Reduce RHS:
| [7] | babbbb(bbbbbbbbab) |
| ⇒ babbbbabbbbb |
Flip LHS and RHS.
Referenced by [14], [15], [16].
Overlap of [2] abbbab=bba with [13] babbbbabbbbb=bb:
Critical pair: abbbb=bbabbbabbbbb.
Reduce RHS:
| [10] | bb(abbba)bbbbb |
| [11] | ⇒ b(bbbabbbbbbbbbbbb)bbbb |
| ⇒ bbbbabbbb |
Flip LHS and RHS.
Referenced by [15].
Overlap of [3] abba=bbbab with [13] babbbbabbbbb=bb:
Critical pair: abbb=bbbabbbbbabbbbb.
Reduce RHS:
| [14] | bbbab(bbbbabbbb)b |
| [4] | ⇒ b(bbaba)bbbbb |
| [5] | ⇒ (babbbbbbab)bbbbb |
| ⇒ abbbbbbb |
Flip LHS and RHS.
Referenced by [16].
Overlap of [9] ababb=babbbbbbbb with [13] babbbbabbbbb=bb:
Critical pair: abb=babbbbbbbbbbabbbbb.
Reduce RHS:
| [15] | b(abbbbbbb)bbbabbbbb |
| [5] | ⇒ (babbbbbbab)bbbb |
| ⇒ abbbbbb |
Flip LHS and RHS.
Referenced by [17], [18], [20], [23].
Overlap of [1] aa=1 with [16] abbbbbb=abb:
Critical pair: aabb=bbbbbb.
Reduce LHS:
| [1] | (aa)bb |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [2] abbbab=bba with [16] abbbbbb=abb:
Critical pair: abbbabb=bbabbbbb.
Reduce LHS:
| [10] | (abbba)bb |
| [12] | ⇒ (bbabbbbbbbbbbbb)b |
| ⇒ bbab |
Flip LHS and RHS.
Referenced by [19].
Overlap of [2] abbbab=bba with [10] abbba=bbabbbbbbbbbbb:
Critical pair: bbabbbbbbbbbbbb=bba.
Reduce LHS:
| [18] | (bbabbbbb)bbbbbbb |
| [18] | ⇒ (bbabbbbb)bbb |
| ⇒ bbabbbb |
Defines rule #2.
Simplify [4] bbaba=abbbbbbab.
Reduce RHS:
| [16] | (abbbbbb)ab |
| [3] | ⇒ (abba)b |
| ⇒ bbbabb |
Defines rule #8.
Overlap of [6] bbbabbbbab=abbbba with [19] bbabbbb=bba:
Critical pair: bbbaab=abbbba.
Reduce LHS:
| [1] | bbb(aa)b |
| ⇒ bbbb |
Flip LHS and RHS.
Referenced by [24].
Simplify [10] abbba=bbabbbbbbbbbbb.
Reduce RHS:
| [19] | (bbabbbb)bbbbbbb |
| [19] | ⇒ (bbabbbb)bbb |
| ⇒ bbabbb |
Defines rule #7.
Simplify [9] ababb=babbbbbbbb.
Reduce RHS:
| [16] | b(abbbbbb)bb |
| ⇒ babbbb |
Defines rule #5.
Overlap of [1] aa=1 with [21] abbbba=bbbb:
Critical pair: abbbb=bbbba.
Flip LHS and RHS.
Defines rule #3.