| Back: | ⟨a, b | aaababbba=ba⟩ |
|---|
Completion settings:
Axiom: aaababbba=ba.
Referenced by [3], [4], [5], [13].
Axiom: bbbba=c.
Overlap of [1] aaababbba=ba with [1] aaababbba=ba:
Critical pair: aaababbbba=baaababbba.
Reduce LHS:
| [2] | aaaba(bbbba) |
| ⇒ aaabac |
Reduce RHS:
| [1] | b(aaababbba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [6], [7], [8], [13], [14].
Overlap of [2] bbbba=c with [1] aaababbba=ba:
Critical pair: bbbbba=caababbba.
Reduce LHS:
| [2] | b(bbbba) |
| ⇒ bc |
Reduce RHS:
| [3] | caabab(bba) |
| ⇒ caababaaabac |
Flip LHS and RHS.
Defines rule #7.
Referenced by [5], [7], [8], [9], [10], [11].
Overlap of [3] bba=aaabac with [1] aaababbba=ba:
Critical pair: bbba=aaabacaababbba.
Reduce LHS:
| [3] | b(bba) |
| ⇒ baaabac |
Reduce RHS:
| [3] | aaabacaabab(bba) |
| [4] | ⇒ aaaba(caababaaabac) |
| ⇒ aaababc |
Flip LHS and RHS.
Defines rule #3.
Overlap of [3] bba=aaabac with [5] aaababc=baaabac:
Critical pair: bbbaaabac=aaabacaababc.
Reduce LHS:
| [3] | b(bba)aabac |
| ⇒ baaabacaabac |
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] caababaaabac=bc with [4] caababaaabac=bc:
Critical pair: caababaaababc=bcaababaaabac.
Reduce LHS:
| [5] | caabab(aaababc) |
| [3] | ⇒ caaba(bba)aabac |
| ⇒ caabaaaabacaabac |
Reduce RHS:
| [4] | b(caababaaabac) |
| ⇒ bbc |
Overlap of [5] aaababc=baaabac with [4] caababaaabac=bc:
Critical pair: aaababbc=baaabacaababaaabac.
Reduce RHS:
| [4] | baaaba(caababaaabac) |
| [5] | ⇒ b(aaababc) |
| [3] | ⇒ (bba)aabac |
| ⇒ aaabacaabac |
Referenced by [9], [10], [12].
Overlap of [8] aaababbc=aaabacaabac with [4] caababaaabac=bc:
Critical pair: aaababbbc=aaabacaabacaababaaabac.
Reduce RHS:
| [4] | aaabacaaba(caababaaabac) |
| [6] | ⇒ (aaabacaababc) |
| ⇒ baaabacaabac |
Referenced by [12].
Overlap of [4] caababaaabac=bc with [7] caabaaaabacaabac=bbc:
Critical pair: caababaaababbc=bcaabaaaabacaabac.
Reduce LHS:
| [8] | caabab(aaababbc) |
| [4] | ⇒ (caababaaabac)aabac |
| ⇒ bcaabac |
Reduce RHS:
| [7] | b(caabaaaabacaabac) |
| ⇒ bbbc |
Flip LHS and RHS.
Referenced by [11].
Overlap of [10] bbbc=bcaabac with [4] caababaaabac=bc:
Critical pair: bbbbc=bcaabacaababaaabac.
Reduce LHS:
| [10] | b(bbbc) |
| ⇒ bbcaabac |
Reduce RHS:
| [4] | bcaaba(caababaaabac) |
| ⇒ bcaababc |
Flip LHS and RHS.
Referenced by [12].
Overlap of [8] aaababbc=aaabacaabac with [11] bcaababc=bbcaabac:
Critical pair: aaababbbcaabac=aaabacaabacaababc.
Reduce LHS:
| [9] | (aaababbbc)aabac |
| ⇒ baaabacaabacaabac |
Flip LHS and RHS.
Referenced by [16].
Overlap of [1] aaababbba=ba with [3] bba=aaabac:
Critical pair: aaababaaabac=ba.
Defines rule #6.
Overlap of [2] bbbba=c with [3] bba=aaabac:
Critical pair: bbaaabac=c.
Reduce LHS:
| [3] | (bba)aabac |
| ⇒ aaabacaabac |
Defines rule #4.
Referenced by [15], [16], [17].
Overlap of [7] caabaaaabacaabac=bbc with [14] aaabacaabac=c:
Critical pair: caabac=bbc.
Flip LHS and RHS.
Defines rule #2.
Simplify [12] aaabacaabacaababc=baaabacaabacaabac.
Reduce RHS:
| [14] | b(aaabacaabac)aabac |
| ⇒ bcaabac |
Referenced by [17].
Overlap of [16] aaabacaabacaababc=bcaabac with [14] aaabacaabac=c:
Critical pair: caababc=bcaabac.
Defines rule #5.