| Back: | ⟨a, b | ababa=b, abbaa=1⟩ |
|---|
Completion settings:
Axiom: ababa=b.
Axiom: abbaa=1.
Overlap of [1] ababa=b with [1] ababa=b:
Critical pair: abb=bba.
Flip LHS and RHS.
Defines rule #2.
Referenced by [4], [5], [6], [7], [8], [11].
Overlap of [1] ababa=b with [2] abbaa=1:
Critical pair: abab=bbbaa.
Reduce RHS:
| [3] | b(bba)a |
| [3] | ⇒ ba(bba) |
| ⇒ baabb |
Flip LHS and RHS.
Overlap of [2] abbaa=1 with [1] ababa=b:
Critical pair: abbab=baba.
Reduce LHS:
| [3] | a(bba)b |
| ⇒ aabbb |
Flip LHS and RHS.
Defines rule #4.
Referenced by [9], [11], [12].
Overlap of [2] abbaa=1 with [3] bba=abb:
Critical pair: aabba=1.
Reduce LHS:
| [3] | aa(bba) |
| ⇒ aaabb |
Referenced by [7], [9], [12], [14], [15].
Overlap of [6] aaabb=1 with [3] bba=abb:
Critical pair: aaababb=ba.
Overlap of [7] aaababb=ba with [3] bba=abb:
Critical pair: aaabaabb=baa.
Reduce LHS:
| [4] | aaa(baabb) |
| ⇒ aaaabab |
Overlap of [8] aaaabab=baa with [5] baba=aabbb:
Critical pair: aaaaaabbb=baaa.
Reduce LHS:
| [6] | aaa(aaabb)b |
| ⇒ aaab |
Flip LHS and RHS.
Referenced by [12].
Overlap of [8] aaaabab=baa with [7] aaababb=ba:
Critical pair: aba=baab.
Flip LHS and RHS.
Referenced by [11].
Overlap of [5] baba=aabbb with [10] baab=aba:
Critical pair: baaba=aabbbab.
Reduce LHS:
| [10] | (baab)a |
| ⇒ abaa |
Reduce RHS:
| [3] | aab(bba)b |
| ⇒ aababbb |
Referenced by [12].
Overlap of [9] baaa=aaab with [11] abaa=aababbb:
Critical pair: baaaababbb=aaabbaa.
Reduce LHS:
| [9] | (baaa)ababbb |
| [5] | ⇒ aaa(baba)bbb |
| [6] | ⇒ aa(aaabb)bbbb |
| ⇒ aabbbb |
Reduce RHS:
| [6] | (aaabb)aa |
| ⇒ aa |
Overlap of [4] baabb=abab with [12] aabbbb=aa:
Critical pair: baa=ababbb.
Defines rule #3.
Overlap of [6] aaabb=1 with [12] aabbbb=aa:
Critical pair: aaa=bb.
Defines rule #5.
Referenced by [15].
Overlap of [6] aaabb=1 with [14] aaa=bb:
Critical pair: bbbb=1.
Defines rule #1.