| Back: | ⟨a, b | abab=1, aabaa=b⟩ |
|---|
Completion settings:
Axiom: abab=1.
Referenced by [4], [7], [12], [15].
Axiom: aabaa=b.
Referenced by [4], [5], [6], [8], [10].
Axiom: baaab=c.
Referenced by [6], [7], [8], [9].
Overlap of [2] aabaa=b with [2] aabaa=b:
Critical pair: aabab=babaa.
Reduce LHS:
| [1] | a(abab) |
| ⇒ a |
Flip LHS and RHS.
Overlap of [4] babaa=a with [2] aabaa=b:
Critical pair: babb=abaa.
Referenced by [16].
Overlap of [2] aabaa=b with [3] baaab=c:
Critical pair: aac=bab.
Flip LHS and RHS.
Defines rule #5.
Referenced by [8], [12], [13], [15], [16].
Overlap of [3] baaab=c with [1] abab=1:
Critical pair: baa=cab.
Flip LHS and RHS.
Referenced by [12].
Overlap of [3] baaab=c with [2] aabaa=b:
Critical pair: bab=caa.
Reduce LHS:
| [6] | (bab) |
| ⇒ aac |
Flip LHS and RHS.
Referenced by [10], [11], [12], [14].
Overlap of [4] babaa=a with [3] baaab=c:
Critical pair: bac=aab.
Flip LHS and RHS.
Defines rule #4.
Overlap of [8] caa=aac with [2] aabaa=b:
Critical pair: cb=aacbaa.
Flip LHS and RHS.
Referenced by [17].
Overlap of [8] caa=aac with [9] aab=bac:
Critical pair: cbac=aacb.
Flip LHS and RHS.
Overlap of [9] aab=bac with [1] abab=1:
Critical pair: a=bacab.
Reduce RHS:
| [7] | ba(cab) |
| [6] | ⇒ (bab)aa |
| [8] | ⇒ aa(caa) |
| ⇒ aaaac |
Flip LHS and RHS.
Overlap of [4] babaa=a with [12] aaaac=a:
Critical pair: baba=aaac.
Reduce LHS:
| [6] | (bab)a |
| ⇒ aaca |
Referenced by [14].
Overlap of [8] caa=aac with [12] aaaac=a:
Critical pair: ca=aacaac.
Reduce RHS:
| [13] | (aaca)ac |
| [13] | ⇒ a(aaca)c |
| [12] | ⇒ (aaaac)c |
| ⇒ ac |
Defines rule #1.
Overlap of [1] abab=1 with [6] bab=aac:
Critical pair: aaac=1.
Defines rule #2.
Overlap of [5] babb=abaa with [6] bab=aac:
Critical pair: aacb=abaa.
Reduce LHS:
| [11] | (aacb) |
| ⇒ cbac |
Referenced by [17].
Overlap of [10] aacbaa=cb with [11] aacb=cbac:
Critical pair: cbacaa=cb.
Reduce LHS:
| [16] | (cbac)aa |
| ⇒ abaaaa |
Flip LHS and RHS.
Defines rule #3.