| Back: | ⟨a, b | aa=1, ababba=bb⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #1.
Referenced by [3], [4], [6], [11], [12], [15].
Axiom: ababba=bb.
Referenced by [3], [4], [5], [7], [13].
Overlap of [1] aa=1 with [2] ababba=bb:
Critical pair: abb=babba.
Flip LHS and RHS.
Referenced by [5], [6], [7], [8], [9], [10], [14], [16], [17].
Overlap of [2] ababba=bb with [1] aa=1:
Critical pair: ababb=bba.
Overlap of [2] ababba=bb with [3] babba=abb:
Critical pair: abababb=bbbba.
Reduce LHS:
| [4] | ab(ababb) |
| ⇒ abbba |
Overlap of [3] babba=abb with [1] aa=1:
Critical pair: babb=abba.
Flip LHS and RHS.
Referenced by [9], [10], [11].
Overlap of [3] babba=abb with [2] ababba=bb:
Critical pair: babbbb=abbbabba.
Reduce RHS:
| [5] | (abbba)bba |
| [3] | ⇒ bbb(babba) |
| ⇒ bbbabb |
Overlap of [3] babba=abb with [3] babba=abb:
Critical pair: bababb=abbbba.
Reduce LHS:
| [4] | b(ababb) |
| ⇒ bbba |
Flip LHS and RHS.
Referenced by [9].
Overlap of [3] babba=abb with [6] abba=babb:
Critical pair: babbbabb=abbbba.
Reduce LHS:
| [5] | b(abbba)bb |
| ⇒ bbbbbabb |
Reduce RHS:
| [8] | (abbbba) |
| ⇒ bbba |
Referenced by [13].
Overlap of [6] abba=babb with [3] babba=abb:
Critical pair: ababb=babbbba.
Reduce LHS:
| [4] | (ababb) |
| ⇒ bba |
Reduce RHS:
| [7] | (babbbb)a |
| [3] | ⇒ bb(babba) |
| ⇒ bbabb |
Flip LHS and RHS.
Overlap of [6] abba=babb with [6] abba=babb:
Critical pair: abbbabb=babbbba.
Reduce LHS:
| [5] | (abbba)bb |
| [10] | ⇒ bb(bbabb) |
| ⇒ bbbba |
Reduce RHS:
| [7] | (babbbb)a |
| [10] | ⇒ b(bbabb)a |
| [1] | ⇒ bbb(aa) |
| ⇒ bbb |
Referenced by [12], [13], [14].
Overlap of [11] bbbba=bbb with [1] aa=1:
Critical pair: bbbb=bbba.
Flip LHS and RHS.
Referenced by [13], [14], [15], [16].
Overlap of [12] bbba=bbbb with [2] ababba=bb:
Critical pair: bbbbb=bbbbbabba.
Reduce RHS:
| [9] | (bbbbbabb)a |
| [12] | ⇒ (bbba)a |
| [11] | ⇒ (bbbba) |
| ⇒ bbb |
Referenced by [14].
Overlap of [12] bbba=bbbb with [3] babba=abb:
Critical pair: bbabb=bbbbbba.
Reduce LHS:
| [10] | (bbabb) |
| ⇒ bba |
Reduce RHS:
| [13] | (bbbbb)ba |
| [11] | ⇒ (bbbba) |
| ⇒ bbb |
Defines rule #2.
Referenced by [15], [16], [17].
Overlap of [14] bba=bbb with [1] aa=1:
Critical pair: bb=bbba.
Reduce RHS:
| [12] | (bbba) |
| ⇒ bbbb |
Flip LHS and RHS.
Defines rule #4.
Referenced by [16].
Overlap of [14] bba=bbb with [3] babba=abb:
Critical pair: babb=bbbbba.
Reduce RHS:
| [15] | (bbbb)ba |
| [12] | ⇒ (bbba) |
| [15] | ⇒ (bbbb) |
| ⇒ bb |
Referenced by [17].
Overlap of [3] babba=abb with [16] babb=bb:
Critical pair: bba=abb.
Reduce LHS:
| [14] | (bba) |
| ⇒ bbb |
Flip LHS and RHS.
Defines rule #3.