| Back: | ⟨a, b | aab=ba, bbba=a⟩ |
|---|
Completion settings:
Axiom: aab=ba.
Referenced by [3], [5], [7], [9], [11].
Axiom: bbba=a.
Defines rule #3.
Referenced by [3], [4], [6], [8], [10].
Overlap of [1] aab=ba with [2] bbba=a:
Critical pair: aaa=babba.
Flip LHS and RHS.
Referenced by [4].
Overlap of [2] bbba=a with [3] babba=aaa:
Critical pair: bbaaa=abba.
Flip LHS and RHS.
Referenced by [5].
Overlap of [1] aab=ba with [4] abba=bbaaa:
Critical pair: abbaaa=baba.
Reduce LHS:
| [4] | (abba)aa |
| ⇒ bbaaaaa |
Flip LHS and RHS.
Referenced by [6].
Overlap of [2] bbba=a with [5] baba=bbaaaaa:
Critical pair: bbbbaaaaa=aba.
Reduce LHS:
| [2] | b(bbba)aaaa |
| ⇒ baaaaa |
Flip LHS and RHS.
Overlap of [1] aab=ba with [6] aba=baaaaa:
Critical pair: abaaaaa=baa.
Reduce LHS:
| [6] | (aba)aaaa |
| ⇒ baaaaaaaaa |
Referenced by [8].
Overlap of [2] bbba=a with [7] baaaaaaaaa=baa:
Critical pair: bbbaa=aaaaaaaaa.
Reduce LHS:
| [2] | (bbba)a |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [9].
Overlap of [8] aaaaaaaaa=aa with [1] aab=ba:
Critical pair: aaaaaaaba=aab.
Reduce LHS:
| [1] | aaaaa(aab)a |
| [1] | ⇒ aaa(aab)aa |
| [1] | ⇒ a(aab)aaa |
| [6] | ⇒ (aba)aaa |
| ⇒ baaaaaaaa |
Reduce RHS:
| [1] | (aab) |
| ⇒ ba |
Referenced by [10].
Overlap of [2] bbba=a with [9] baaaaaaaa=ba:
Critical pair: bbba=aaaaaaaa.
Reduce LHS:
| [2] | (bbba) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #1.
Referenced by [11].
Overlap of [10] aaaaaaaa=a with [1] aab=ba:
Critical pair: aaaaaaba=ab.
Reduce LHS:
| [1] | aaaa(aab)a |
| [1] | ⇒ aa(aab)aa |
| [1] | ⇒ (aab)aaa |
| ⇒ baaaa |
Flip LHS and RHS.
Defines rule #2.