| Back: | ⟨a, b | aabb=a, bbbab=a⟩ |
|---|
Completion settings:
Axiom: aabb=a.
Referenced by [3], [4], [6], [8], [12].
Axiom: bbbab=a.
Referenced by [3], [4], [5], [8], [10], [11], [14], [16], [17], [18].
Overlap of [1] aabb=a with [2] bbbab=a:
Critical pair: aaa=abab.
Referenced by [6], [7], [9], [13].
Overlap of [1] aabb=a with [2] bbbab=a:
Critical pair: aaba=abbab.
Referenced by [7].
Overlap of [2] bbbab=a with [2] bbbab=a:
Critical pair: bbbaa=abbab.
Flip LHS and RHS.
Referenced by [7], [9], [10], [11].
Overlap of [3] aaa=abab with [1] aabb=a:
Critical pair: aa=ababbb.
Flip LHS and RHS.
Referenced by [8], [9], [10], [11].
Overlap of [3] aaa=abab with [3] aaa=abab:
Critical pair: aabab=ababa.
Reduce LHS:
| [4] | (aaba)b |
| [5] | ⇒ (abbab)b |
| ⇒ bbbaab |
Flip LHS and RHS.
Referenced by [9].
Overlap of [2] bbbab=a with [6] ababbb=aa:
Critical pair: bbbaa=aabbb.
Reduce RHS:
| [1] | (aabb)b |
| ⇒ ab |
Referenced by [9], [10], [11].
Overlap of [3] aaa=abab with [6] ababbb=aa:
Critical pair: aaaa=ababbabbb.
Reduce LHS:
| [3] | (aaa)a |
| [7] | ⇒ (ababa) |
| [8] | ⇒ (bbbaa)b |
| ⇒ abb |
Reduce RHS:
| [5] | ab(abbab)bb |
| [8] | ⇒ ab(bbbaa)bb |
| [6] | ⇒ (ababbb) |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [10], [11], [12], [13], [16], [19].
Overlap of [6] ababbb=aa with [2] bbbab=a:
Critical pair: abaa=aaab.
Reduce LHS:
| [9] | ab(aa) |
| ⇒ ababb |
Reduce RHS:
| [9] | (aa)ab |
| [5] | ⇒ (abbab) |
| [8] | ⇒ (bbbaa) |
| ⇒ ab |
Referenced by [11].
Overlap of [6] ababbb=aa with [2] bbbab=a:
Critical pair: ababba=aabbab.
Reduce LHS:
| [10] | (ababb)a |
| ⇒ aba |
Reduce RHS:
| [5] | a(abbab) |
| [8] | ⇒ a(bbbaa) |
| [9] | ⇒ (aa)b |
| ⇒ abbb |
Referenced by [13], [14], [15].
Overlap of [1] aabb=a with [9] aa=abb:
Critical pair: abbbb=a.
Referenced by [13].
Overlap of [3] aaa=abab with [9] aa=abb:
Critical pair: abba=abab.
Reduce RHS:
| [11] | (aba)b |
| [12] | ⇒ (abbbb) |
| ⇒ a |
Referenced by [14].
Overlap of [2] bbbab=a with [13] abba=a:
Critical pair: bbba=aba.
Reduce RHS:
| [11] | (aba) |
| ⇒ abbb |
Flip LHS and RHS.
Referenced by [15].
Simplify [11] aba=abbb.
Reduce RHS:
| [14] | (abbb) |
| ⇒ bbba |
Referenced by [16].
Overlap of [2] bbbab=a with [15] aba=bbba:
Critical pair: bbbbbba=aa.
Reduce RHS:
| [9] | (aa) |
| ⇒ abb |
Flip LHS and RHS.
Referenced by [17].
Overlap of [2] bbbab=a with [16] abb=bbbbbba:
Critical pair: bbbbbbbbba=ab.
Flip LHS and RHS.
Defines rule #2.
Overlap of [2] bbbab=a with [17] ab=bbbbbbbbba:
Critical pair: bbbbbbbbbbbba=a.
Defines rule #1.
Referenced by [19].
Simplify [9] aa=abb.
Reduce RHS:
| [17] | (ab)b |
| [17] | ⇒ bbbbbbbbb(ab) |
| [18] | ⇒ bbbbbb(bbbbbbbbbbbba) |
| ⇒ bbbbbba |
Defines rule #3.