| Back: | ⟨a, b | abab=ba, baaa=b⟩ |
|---|
Completion settings:
Axiom: abab=ba.
Referenced by [3], [4], [8], [10], [12].
Axiom: baaa=b.
Defines rule #1.
Referenced by [4], [5], [6], [8], [11], [12], [13], [14].
Overlap of [1] abab=ba with [1] abab=ba:
Critical pair: abba=baab.
Referenced by [5], [6], [7], [10].
Overlap of [2] baaa=b with [1] abab=ba:
Critical pair: baaba=bbab.
Flip LHS and RHS.
Overlap of [2] baaa=b with [3] abba=baab:
Critical pair: baabaab=bbba.
Overlap of [3] abba=baab with [2] baaa=b:
Critical pair: abb=baabaa.
Defines rule #4.
Overlap of [3] abba=baab with [4] bbab=baaba:
Critical pair: abaaba=baabb.
Reduce RHS:
| [6] | ba(abb) |
| ⇒ babaabaa |
Flip LHS and RHS.
Referenced by [8].
Overlap of [5] baabaab=bbba with [5] baabaab=bbba:
Critical pair: baabbba=bbbaaab.
Reduce LHS:
| [6] | ba(abb)ba |
| [7] | ⇒ (babaabaa)ba |
| [1] | ⇒ aba(abab)a |
| [1] | ⇒ (abab)aa |
| [2] | ⇒ (baaa) |
| ⇒ b |
Reduce RHS:
| [2] | bb(baaa)b |
| ⇒ bbbb |
Flip LHS and RHS.
Defines rule #7.
Referenced by [9].
Overlap of [6] abb=baabaa with [8] bbbb=b:
Critical pair: ab=baabaabb.
Reduce RHS:
| [5] | (baabaab)b |
| [4] | ⇒ b(bbab) |
| ⇒ bbaaba |
Flip LHS and RHS.
Overlap of [3] abba=baab with [9] bbaaba=ab:
Critical pair: aab=baababa.
Reduce RHS:
| [1] | ba(abab)a |
| ⇒ babaa |
Flip LHS and RHS.
Overlap of [9] bbaaba=ab with [2] baaa=b:
Critical pair: bbaab=abaa.
Defines rule #6.
Overlap of [1] abab=ba with [10] babaa=aab:
Critical pair: aaab=baaa.
Reduce RHS:
| [2] | (baaa) |
| ⇒ b |
Defines rule #2.
Overlap of [10] babaa=aab with [2] baaa=b:
Critical pair: bab=aaba.
Defines rule #3.
Referenced by [14].
Overlap of [13] bab=aaba with [13] bab=aaba:
Critical pair: baaaba=aabaab.
Reduce LHS:
| [2] | (baaa)ba |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #5.