| Back: | ⟨a, b | baa=abb, aaaa=a⟩ |
|---|
Completion settings:
Axiom: baa=abb.
Flip LHS and RHS.
Defines rule #1.
Referenced by [3], [5], [6], [8], [9], [11].
Axiom: aaaa=a.
Defines rule #2.
Referenced by [3], [4], [5], [6], [7], [9], [10], [11].
Overlap of [2] aaaa=a with [1] abb=baa:
Critical pair: aaabaa=abb.
Reduce RHS:
| [1] | (abb) |
| ⇒ baa |
Overlap of [3] aaabaa=baa with [2] aaaa=a:
Critical pair: aaaba=baaaa.
Reduce RHS:
| [2] | b(aaaa) |
| ⇒ ba |
Referenced by [5].
Overlap of [3] aaabaa=baa with [3] aaabaa=baa:
Critical pair: aaabbaa=baaabaa.
Reduce LHS:
| [1] | aa(abb)aa |
| [2] | ⇒ aab(aaaa) |
| ⇒ aaba |
Reduce RHS:
| [4] | b(aaaba)a |
| ⇒ bbaa |
Defines rule #3.
Overlap of [5] aaba=bbaa with [1] abb=baa:
Critical pair: aabbaa=bbaabb.
Reduce LHS:
| [1] | a(abb)aa |
| [2] | ⇒ ab(aaaa) |
| ⇒ aba |
Reduce RHS:
| [1] | bba(abb) |
| ⇒ bbabaa |
Flip LHS and RHS.
Referenced by [7].
Overlap of [6] bbabaa=aba with [2] aaaa=a:
Critical pair: bbaba=abaaa.
Defines rule #4.
Referenced by [8].
Overlap of [1] abb=baa with [7] bbaba=abaaa:
Critical pair: ababaaa=baababa.
Reduce RHS:
| [5] | b(aaba)ba |
| [5] | ⇒ bbb(aaba) |
| ⇒ bbbbbaa |
Flip LHS and RHS.
Referenced by [9], [10], [11].
Overlap of [1] abb=baa with [8] bbbbbaa=ababaaa:
Critical pair: abababaaa=baabbbbaa.
Reduce RHS:
| [1] | ba(abb)bbaa |
| [1] | ⇒ baba(abb)aa |
| [2] | ⇒ babab(aaaa) |
| ⇒ bababa |
Referenced by [11].
Overlap of [8] bbbbbaa=ababaaa with [2] aaaa=a:
Critical pair: bbbbba=ababaaaaa.
Reduce RHS:
| [2] | abab(aaaa)a |
| ⇒ ababaa |
Defines rule #5.
Referenced by [11].
Overlap of [8] bbbbbaa=ababaaa with [5] aaba=bbaa:
Critical pair: bbbbbabbaa=ababaaaaba.
Reduce LHS:
| [10] | (bbbbba)bbaa |
| [1] | ⇒ ababa(abb)aa |
| [9] | ⇒ (abababaaa)a |
| ⇒ bababaa |
Reduce RHS:
| [2] | abab(aaaa)ba |
| ⇒ abababa |
Flip LHS and RHS.
Defines rule #6.