| Back: | ⟨a, b | aaa=a, abaab=ba⟩ |
|---|
Completion settings:
Axiom: aaa=a.
Defines rule #5.
Axiom: abaab=ba.
Referenced by [3], [4], [5], [6], [9].
Overlap of [1] aaa=a with [2] abaab=ba:
Critical pair: aaba=abaab.
Reduce RHS:
| [2] | (abaab) |
| ⇒ ba |
Defines rule #6.
Referenced by [5], [6], [8], [10].
Overlap of [2] abaab=ba with [2] abaab=ba:
Critical pair: ababa=baaab.
Reduce RHS:
| [1] | b(aaa)b |
| ⇒ bab |
Referenced by [8].
Overlap of [2] abaab=ba with [3] aaba=ba:
Critical pair: abba=baa.
Flip LHS and RHS.
Referenced by [6], [7], [8], [9], [11].
Overlap of [3] aaba=ba with [2] abaab=ba:
Critical pair: aba=baab.
Reduce RHS:
| [5] | (baa)b |
| ⇒ abbab |
Flip LHS and RHS.
Overlap of [5] baa=abba with [1] aaa=a:
Critical pair: ba=abbaa.
Reduce RHS:
| [5] | ab(baa) |
| ⇒ ababba |
Flip LHS and RHS.
Referenced by [10].
Overlap of [5] baa=abba with [6] abbab=aba:
Critical pair: baaba=abbabbab.
Reduce LHS:
| [3] | b(aaba) |
| ⇒ bba |
Reduce RHS:
| [6] | (abbab)bab |
| [4] | ⇒ (ababa)b |
| ⇒ babb |
Defines rule #2.
Referenced by [9], [10], [11].
Overlap of [2] abaab=ba with [8] bba=babb:
Critical pair: abaababb=baba.
Reduce LHS:
| [2] | (abaab)abb |
| [5] | ⇒ (baa)bb |
| [6] | ⇒ (abbab)b |
| ⇒ abab |
Flip LHS and RHS.
Defines rule #4.
Referenced by [10].
Overlap of [9] baba=abab with [9] baba=abab:
Critical pair: baabab=ababba.
Reduce LHS:
| [3] | b(aaba)b |
| [8] | ⇒ (bba)b |
| ⇒ babbb |
Reduce RHS:
| [7] | (ababba) |
| ⇒ ba |
Defines rule #1.
Simplify [5] baa=abba.
Reduce RHS:
| [8] | a(bba) |
| ⇒ ababb |
Defines rule #3.