| Back: | ⟨a, b | abab=1, aabbaa=b⟩ |
|---|
Completion settings:
Axiom: abab=1.
Referenced by [3], [4], [5], [6], [11], [17], [20].
Axiom: aabbaa=b.
Referenced by [3], [6], [7], [8], [10], [12], [15], [19].
Overlap of [2] aabbaa=b with [1] abab=1:
Critical pair: aabba=bbab.
Flip LHS and RHS.
Overlap of [1] abab=1 with [3] bbab=aabba:
Critical pair: abaaabba=bab.
Referenced by [6].
Overlap of [3] bbab=aabba with [3] bbab=aabba:
Critical pair: bbaaabba=aabbabab.
Reduce RHS:
| [1] | aabb(abab) |
| ⇒ aabb |
Referenced by [8].
Overlap of [4] abaaabba=bab with [2] aabbaa=b:
Critical pair: abab=baba.
Reduce LHS:
| [1] | (abab) |
| ⇒ 1 |
Flip LHS and RHS.
Overlap of [6] baba=1 with [2] aabbaa=b:
Critical pair: babb=abbaa.
Referenced by [8], [13], [14].
Overlap of [2] aabbaa=b with [5] bbaaabba=aabb:
Critical pair: aaaabb=babba.
Reduce RHS:
| [7] | (babb)a |
| ⇒ abbaaa |
Referenced by [9].
Overlap of [6] baba=1 with [8] aaaabb=abbaaa:
Critical pair: bababbaaa=aaabb.
Reduce LHS:
| [6] | (baba)bbaaa |
| ⇒ bbaaa |
Flip LHS and RHS.
Overlap of [9] aaabb=bbaaa with [2] aabbaa=b:
Critical pair: ab=bbaaaaa.
Flip LHS and RHS.
Referenced by [11], [12], [13], [14], [15], [16], [18].
Overlap of [1] abab=1 with [10] bbaaaaa=ab:
Critical pair: abaab=baaaaa.
Overlap of [2] aabbaa=b with [10] bbaaaaa=ab:
Critical pair: aaab=baaa.
Defines rule #2.
Overlap of [7] babb=abbaa with [10] bbaaaaa=ab:
Critical pair: baab=abbaaaaaaa.
Reduce RHS:
| [10] | a(bbaaaaa)aa |
| ⇒ aabaa |
Defines rule #5.
Referenced by [14], [16], [19].
Overlap of [7] babb=abbaa with [10] bbaaaaa=ab:
Critical pair: babab=abbaabaaaaa.
Reduce LHS:
| [6] | (baba)b |
| ⇒ b |
Reduce RHS:
| [13] | ab(baab)aaaaa |
| [11] | ⇒ (abaab)aaaaaaa |
| ⇒ baaaaaaaaaaaa |
Flip LHS and RHS.
Referenced by [20].
Overlap of [10] bbaaaaa=ab with [9] aaabb=bbaaa:
Critical pair: bbaabbaaa=abbb.
Reduce LHS:
| [2] | bb(aabbaa)a |
| ⇒ bbba |
Flip LHS and RHS.
Referenced by [17].
Overlap of [10] bbaaaaa=ab with [12] aaab=baaa:
Critical pair: bbaabaaa=abb.
Reduce LHS:
| [13] | b(baab)aaa |
| [13] | ⇒ (baab)aaaaa |
| ⇒ aabaaaaaaa |
Flip LHS and RHS.
Referenced by [17].
Simplify [15] abbb=bbba.
Reduce LHS:
| [16] | (abb)b |
| [12] | ⇒ aabaaaa(aaab) |
| [12] | ⇒ aaba(aaab)aaa |
| [1] | ⇒ a(abab)aaaaaa |
| ⇒ aaaaaaa |
Flip LHS and RHS.
Referenced by [18].
Overlap of [17] bbba=aaaaaaa with [10] bbaaaaa=ab:
Critical pair: bab=aaaaaaaaaaa.
Defines rule #4.
Overlap of [2] aabbaa=b with [13] baab=aabaa:
Critical pair: aabaabaa=bb.
Reduce LHS:
| [11] | a(abaab)aa |
| ⇒ abaaaaaaa |
Flip LHS and RHS.
Defines rule #3.
Overlap of [1] abab=1 with [14] baaaaaaaaaaaa=b:
Critical pair: abab=aaaaaaaaaaaa.
Reduce LHS:
| [1] | (abab) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.