| Back: | ⟨a, b | abab=1, aaabbba=1⟩ |
|---|
Completion settings:
Axiom: abab=1.
Referenced by [3], [6], [7], [9], [10], [11], [13], [23].
Axiom: aaabbba=1.
Referenced by [3], [4], [5], [7], [12].
Overlap of [2] aaabbba=1 with [1] abab=1:
Critical pair: aaabbb=bab.
Overlap of [2] aaabbba=1 with [2] aaabbba=1:
Critical pair: aaabbb=aabbba.
Reduce LHS:
| [3] | (aaabbb) |
| ⇒ bab |
Flip LHS and RHS.
Referenced by [5], [6], [7], [10].
Overlap of [2] aaabbba=1 with [4] aabbba=bab:
Critical pair: aaabbbbab=abbba.
Reduce LHS:
| [3] | (aaabbb)bab |
| ⇒ babbab |
Referenced by [6].
Overlap of [4] aabbba=bab with [1] abab=1:
Critical pair: aabbb=babbab.
Reduce RHS:
| [5] | (babbab) |
| ⇒ abbba |
Overlap of [4] aabbba=bab with [2] aaabbba=1:
Critical pair: aabbb=babaabbba.
Reduce LHS:
| [6] | (aabbb) |
| ⇒ abbba |
Reduce RHS:
| [6] | bab(aabbb)a |
| [1] | ⇒ b(abab)bbaa |
| ⇒ bbbaa |
Referenced by [8].
Simplify [3] aaabbb=bab.
Reduce LHS:
| [6] | a(aabbb) |
| [6] | ⇒ (aabbb)a |
| [7] | ⇒ (abbba)a |
| ⇒ bbbaaa |
Overlap of [1] abab=1 with [8] bbbaaa=bab:
Critical pair: ababab=bbaaa.
Reduce LHS:
| [1] | (abab)ab |
| ⇒ ab |
Flip LHS and RHS.
Referenced by [13], [14], [15], [18], [20], [21], [24].
Overlap of [4] aabbba=bab with [8] bbbaaa=bab:
Critical pair: aabab=babaa.
Reduce LHS:
| [1] | a(abab) |
| ⇒ a |
Flip LHS and RHS.
Referenced by [11].
Overlap of [10] babaa=a with [1] abab=1:
Critical pair: baba=abab.
Reduce RHS:
| [1] | (abab) |
| ⇒ 1 |
Referenced by [12], [16], [22], [23], [25].
Overlap of [2] aaabbba=1 with [11] baba=1:
Critical pair: aaabb=ba.
Referenced by [14], [15], [16], [17], [20].
Overlap of [1] abab=1 with [9] bbaaa=ab:
Critical pair: abaab=baaa.
Overlap of [9] bbaaa=ab with [12] aaabb=ba:
Critical pair: bbba=abbb.
Flip LHS and RHS.
Referenced by [22].
Overlap of [12] aaabb=ba with [9] bbaaa=ab:
Critical pair: aaaab=baaaa.
Defines rule #2.
Overlap of [12] aaabb=ba with [11] baba=1:
Critical pair: aaab=baaba.
Flip LHS and RHS.
Overlap of [16] baaba=aaab with [12] aaabb=ba:
Critical pair: baabba=aaabaabb.
Reduce RHS:
| [13] | aa(abaab)b |
| ⇒ aabaaab |
Referenced by [19].
Overlap of [13] abaab=baaa with [9] bbaaa=ab:
Critical pair: abaaab=baaabaaa.
Defines rule #6.
Referenced by [19].
Simplify [17] baabba=aabaaab.
Reduce RHS:
| [18] | a(abaaab) |
| [18] | ⇒ (abaaab)aaa |
| ⇒ baaabaaaaaa |
Referenced by [20].
Overlap of [12] aaabb=ba with [19] baabba=baaabaaaaaa:
Critical pair: aaabbaaabaaaaaa=baaabba.
Reduce LHS:
| [12] | (aaabb)aaabaaaaaa |
| [15] | ⇒ b(aaaab)aaaaaa |
| [9] | ⇒ (bbaaa)aaaaaaa |
| ⇒ abaaaaaaa |
Reduce RHS:
| [12] | b(aaabb)a |
| ⇒ bbaa |
Flip LHS and RHS.
Referenced by [21], [22], [23].
Overlap of [9] bbaaa=ab with [20] bbaa=abaaaaaaa:
Critical pair: abaaaaaaaa=ab.
Referenced by [23].
Overlap of [14] abbb=bbba with [20] bbaa=abaaaaaaa:
Critical pair: abbabaaaaaaa=bbbabaa.
Reduce LHS:
| [11] | ab(baba)aaaaaa |
| ⇒ abaaaaaa |
Reduce RHS:
| [11] | bb(baba)a |
| ⇒ bba |
Flip LHS and RHS.
Referenced by [23].
Overlap of [20] bbaa=abaaaaaaa with [15] aaaab=baaaa:
Critical pair: bbbaaaa=abaaaaaaaaab.
Reduce LHS:
| [22] | b(bba)aaa |
| [11] | ⇒ (baba)aaaaaaaa |
| ⇒ aaaaaaaa |
Reduce RHS:
| [21] | (abaaaaaaaa)ab |
| [1] | ⇒ (abab) |
| ⇒ 1 |
Defines rule #1.
Referenced by [24], [25], [26].
Overlap of [9] bbaaa=ab with [23] aaaaaaaa=1:
Critical pair: bb=abaaaaa.
Defines rule #3.
Overlap of [11] baba=1 with [23] aaaaaaaa=1:
Critical pair: bab=aaaaaaa.
Defines rule #4.
Overlap of [16] baaba=aaab with [23] aaaaaaaa=1:
Critical pair: baab=aaabaaaaaaa.
Defines rule #5.