| Back: | ⟨a, b | aabababa=aab⟩ |
|---|
Completion settings:
Axiom: aabababa=aab.
Referenced by [3], [4], [5], [6].
Axiom: aabb=c.
Referenced by [3], [4], [7], [9], [10], [20].
Overlap of [1] aabababa=aab with [1] aabababa=aab:
Critical pair: aabababaab=aababababa.
Reduce LHS:
| [1] | (aabababa)ab |
| ⇒ aabab |
Reduce RHS:
| [1] | (aabababa)ba |
| [2] | ⇒ (aabb)a |
| ⇒ ca |
Referenced by [4], [5], [6], [10], [18].
Overlap of [1] aabababa=aab with [2] aabb=c:
Critical pair: aabababc=aababb.
Reduce LHS:
| [3] | (aabab)abc |
| ⇒ caabc |
Reduce RHS:
| [3] | (aabab)b |
| ⇒ cab |
Overlap of [1] aabababa=aab with [3] aabab=ca:
Critical pair: caaba=aab.
Referenced by [8].
Overlap of [1] aabababa=aab with [3] aabab=ca:
Critical pair: aabababca=aababab.
Reduce LHS:
| [3] | (aabab)abca |
| [4] | ⇒ (caabc)a |
| ⇒ caba |
Reduce RHS:
| [3] | (aabab)ab |
| ⇒ caab |
Flip LHS and RHS.
Referenced by [7], [8], [14], [22].
Overlap of [6] caab=caba with [2] aabb=c:
Critical pair: cc=cabab.
Flip LHS and RHS.
Referenced by [12].
Simplify [5] caaba=aab.
Reduce LHS:
| [6] | (caab)a |
| ⇒ cabaa |
Referenced by [9], [10], [11].
Overlap of [8] cabaa=aab with [2] aabb=c:
Critical pair: cabc=aabbb.
Reduce RHS:
| [2] | (aabb)b |
| ⇒ cb |
Overlap of [8] cabaa=aab with [3] aabab=ca:
Critical pair: cabca=aabbab.
Reduce LHS:
| [9] | (cabc)a |
| ⇒ cba |
Reduce RHS:
| [2] | (aabb)ab |
| ⇒ cab |
Flip LHS and RHS.
Defines rule #6.
Referenced by [11], [12], [13], [16], [18], [21], [22], [26].
Overlap of [8] cabaa=aab with [10] cab=cba:
Critical pair: cbaaa=aab.
Flip LHS and RHS.
Defines rule #5.
Referenced by [12], [14], [18], [20].
Overlap of [7] cabab=cc with [10] cab=cba:
Critical pair: cbaab=cc.
Reduce LHS:
| [11] | cb(aab) |
| ⇒ cbcbaaa |
Simplify [9] cabc=cb.
Reduce LHS:
| [10] | (cab)c |
| ⇒ cbac |
Defines rule #2.
Referenced by [14], [15], [16], [20], [25], [27], [28].
Overlap of [13] cbac=cb with [6] caab=caba:
Critical pair: cbacaba=cbaab.
Reduce LHS:
| [13] | (cbac)aba |
| ⇒ cbaba |
Reduce RHS:
| [11] | cb(aab) |
| [12] | ⇒ (cbcbaaa) |
| ⇒ cc |
Referenced by [17].
Overlap of [13] cbac=cb with [13] cbac=cb:
Critical pair: cbacb=cbbac.
Reduce LHS:
| [13] | (cbac)b |
| ⇒ cbb |
Flip LHS and RHS.
Overlap of [13] cbac=cb with [10] cab=cba:
Critical pair: cbacba=cbab.
Reduce LHS:
| [13] | (cbac)ba |
| ⇒ cbba |
Flip LHS and RHS.
Simplify [14] cbaba=cc.
Reduce LHS:
| [16] | (cbab)a |
| ⇒ cbbaa |
Overlap of [17] cbbaa=cc with [3] aabab=ca:
Critical pair: cbbaca=ccabab.
Reduce LHS:
| [15] | (cbbac)a |
| ⇒ cbba |
Reduce RHS:
| [10] | c(cab)ab |
| [11] | ⇒ ccb(aab) |
| [12] | ⇒ c(cbcbaaa) |
| ⇒ ccc |
Referenced by [19], [20], [23].
Overlap of [17] cbbaa=cc with [18] cbba=ccc:
Critical pair: ccca=cc.
Overlap of [2] aabb=c with [11] aab=cbaaa:
Critical pair: cbaaab=c.
Reduce LHS:
| [11] | cba(aab) |
| [13] | ⇒ (cbac)baaa |
| [18] | ⇒ (cbba)aa |
| [19] | ⇒ (ccca)a |
| ⇒ cca |
Defines rule #1.
Simplify [4] caabc=cab.
Reduce RHS:
| [10] | (cab) |
| ⇒ cba |
Referenced by [22].
Overlap of [21] caabc=cba with [6] caab=caba:
Critical pair: cabac=cba.
Reduce LHS:
| [10] | (cab)ac |
| ⇒ cbaac |
Defines rule #4.
Overlap of [15] cbbac=cbb with [18] cbba=ccc:
Critical pair: cccc=cbb.
Flip LHS and RHS.
Defines rule #8.
Simplify [16] cbab=cbba.
Reduce RHS:
| [23] | (cbb)a |
| [19] | ⇒ c(ccca) |
| ⇒ ccc |
Defines rule #9.
Overlap of [13] cbac=cb with [20] cca=c:
Critical pair: cbac=cbca.
Reduce LHS:
| [13] | (cbac) |
| ⇒ cb |
Flip LHS and RHS.
Defines rule #3.
Overlap of [20] cca=c with [10] cab=cba:
Critical pair: ccba=cb.
Referenced by [27].
Overlap of [26] ccba=cb with [13] cbac=cb:
Critical pair: ccb=cbc.
Defines rule #7.
Referenced by [28].
Overlap of [13] cbac=cb with [27] ccb=cbc:
Critical pair: cbacbc=cbcb.
Reduce LHS:
| [13] | (cbac)bc |
| [23] | ⇒ (cbb)c |
| ⇒ ccccc |
Flip LHS and RHS.
Defines rule #10.