| Back: | ⟨a, b | aa=1, abbabbba=b⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #4.
Referenced by [3], [4], [5], [9], [18], [21].
Axiom: abbabbba=b.
Overlap of [1] aa=1 with [2] abbabbba=b:
Critical pair: ab=bbabbba.
Flip LHS and RHS.
Referenced by [8], [9], [14], [15].
Overlap of [2] abbabbba=b with [1] aa=1:
Critical pair: abbabbb=ba.
Referenced by [5], [6], [9], [11], [12], [13], [17], [21].
Overlap of [1] aa=1 with [4] abbabbb=ba:
Critical pair: aba=bbabbb.
Defines rule #5.
Referenced by [6], [7], [8], [9], [19].
Overlap of [5] aba=bbabbb with [4] abbabbb=ba:
Critical pair: abba=bbabbbbbabbb.
Flip LHS and RHS.
Overlap of [5] aba=bbabbb with [5] aba=bbabbb:
Critical pair: abbbabbb=bbabbbba.
Flip LHS and RHS.
Referenced by [10].
Overlap of [3] bbabbba=ab with [3] bbabbba=ab:
Critical pair: bbabab=abbbba.
Reduce LHS:
| [5] | bb(aba)b |
| ⇒ bbbbabbbb |
Flip LHS and RHS.
Defines rule #8.
Referenced by [9], [10], [14], [19], [20].
Overlap of [4] abbabbb=ba with [3] bbabbba=ab:
Critical pair: abbabab=baabbba.
Reduce LHS:
| [5] | abb(aba)b |
| [8] | ⇒ (abbbba)bbbb |
| ⇒ bbbbabbbbbbbb |
Reduce RHS:
| [1] | b(aa)bbba |
| ⇒ bbbba |
Referenced by [11], [12], [13], [14].
Simplify [7] bbabbbba=abbbabbb.
Reduce LHS:
| [8] | bb(abbbba) |
| ⇒ bbbbbbabbbb |
Flip LHS and RHS.
Referenced by [12].
Overlap of [4] abbabbb=ba with [9] bbbbabbbbbbbb=bbbba:
Critical pair: abbabbbbba=babbabbbbbbbb.
Reduce LHS:
| [4] | (abbabbb)bba |
| ⇒ babba |
Reduce RHS:
| [4] | b(abbabbb)bbbbb |
| ⇒ bbabbbbb |
Referenced by [14].
Overlap of [4] abbabbb=ba with [9] bbbbabbbbbbbb=bbbba:
Critical pair: abbabbbbbba=babbbabbbbbbbb.
Reduce LHS:
| [4] | (abbabbb)bbba |
| ⇒ babbba |
Reduce RHS:
| [10] | b(abbbabbb)bbbbb |
| [9] | ⇒ bbb(bbbbabbbbbbbb)b |
| ⇒ bbbbbbbab |
Referenced by [15].
Overlap of [6] bbabbbbbabbb=abba with [9] bbbbabbbbbbbb=bbbba:
Critical pair: bbabbbbba=abbabbbbb.
Reduce RHS:
| [4] | (abbabbb)bb |
| ⇒ babb |
Referenced by [16].
Overlap of [3] bbabbba=ab with [11] babba=bbabbbbb:
Critical pair: bbabbbbabbbbb=abbba.
Reduce LHS:
| [8] | bb(abbbba)bbbbb |
| [9] | ⇒ bb(bbbbabbbbbbbb)b |
| ⇒ bbbbbbab |
Flip LHS and RHS.
Defines rule #7.
Overlap of [3] bbabbba=ab with [12] babbba=bbbbbbbab:
Critical pair: bbbbbbbbab=ab.
Overlap of [6] bbabbbbbabbb=abba with [13] bbabbbbba=babb:
Critical pair: babbbbb=abba.
Flip LHS and RHS.
Defines rule #6.
Referenced by [17], [18], [21].
Overlap of [4] abbabbb=ba with [16] abba=babbbbb:
Critical pair: babbbbbbbb=ba.
Defines rule #2.
Referenced by [19], [21], [22].
Overlap of [16] abba=babbbbb with [1] aa=1:
Critical pair: abb=babbbbba.
Flip LHS and RHS.
Referenced by [19], [20], [23].
Overlap of [18] babbbbba=abb with [8] abbbba=bbbbabbbb:
Critical pair: babbbbbbbbbabbbb=abbbbbba.
Reduce LHS:
| [17] | (babbbbbbbb)babbbb |
| [5] | ⇒ b(aba)bbbb |
| ⇒ bbbabbbbbbb |
Flip LHS and RHS.
Defines rule #10.
Overlap of [18] babbbbba=abb with [18] babbbbba=abb:
Critical pair: babbbbabb=abbbbbbba.
Reduce LHS:
| [8] | b(abbbba)bb |
| ⇒ bbbbbabbbbbb |
Flip LHS and RHS.
Defines rule #11.
Overlap of [4] abbabbb=ba with [17] babbbbbbbb=ba:
Critical pair: abbabbba=baabbbbbbbb.
Reduce LHS:
| [16] | (abba)bbba |
| [17] | ⇒ (babbbbbbbb)a |
| [1] | ⇒ b(aa) |
| ⇒ b |
Reduce RHS:
| [1] | b(aa)bbbbbbbb |
| ⇒ bbbbbbbbb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [15] bbbbbbbbab=ab with [17] babbbbbbbb=ba:
Critical pair: bbbbbbbba=abbbbbbbb.
Defines rule #3.
Overlap of [15] bbbbbbbbab=ab with [18] babbbbba=abb:
Critical pair: bbbbbbbabb=abbbbba.
Flip LHS and RHS.
Defines rule #9.