| Back: | ⟨a, b | abaabababba=1⟩ |
|---|
Completion settings:
Axiom: abaabababba=1.
Referenced by [4].
Axiom: ba=c.
Axiom: accbb=d.
Overlap of [1] abaabababba=1 with [2] ba=c:
Critical pair: acabababba=1.
Reduce LHS:
| [2] | aca(ba)babba |
| [2] | ⇒ acac(ba)bba |
| [3] | ⇒ ac(accbb)a |
| ⇒ acda |
Referenced by [5], [6], [9], [11], [12], [13], [14].
Overlap of [2] ba=c with [4] acda=1:
Critical pair: b=ccda.
Referenced by [7].
Overlap of [4] acda=1 with [4] acda=1:
Critical pair: acd=cda.
Flip LHS and RHS.
Referenced by [7], [10], [13], [15], [16].
Simplify [5] b=ccda.
Reduce RHS:
| [6] | c(cda) |
| ⇒ cacd |
Defines rule #9.
Referenced by [8].
Simplify [3] accbb=d.
Reduce LHS:
| [7] | acc(b)b |
| [7] | ⇒ acccacd(b) |
| ⇒ acccacdcacd |
Overlap of [8] acccacdcacd=d with [4] acda=1:
Critical pair: acccacdc=da.
Referenced by [10], [12], [13].
Overlap of [8] acccacdcacd=d with [6] cda=acd:
Critical pair: acccacdcaacd=da.
Reduce LHS:
| [9] | (acccacdc)aacd |
| ⇒ daaacd |
Referenced by [11].
Overlap of [4] acda=1 with [10] daaacd=da:
Critical pair: acda=aacd.
Reduce LHS:
| [4] | (acda) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #5.
Referenced by [17], [18], [20], [23], [25].
Overlap of [4] acda=1 with [9] acccacdc=da:
Critical pair: acdda=cccacdc.
Referenced by [15].
Overlap of [9] acccacdc=da with [6] cda=acd:
Critical pair: acccacdacd=dada.
Reduce LHS:
| [4] | accc(acda)cd |
| ⇒ accccd |
Flip LHS and RHS.
Overlap of [4] acda=1 with [13] dada=accccd:
Critical pair: acaccccd=da.
Flip LHS and RHS.
Defines rule #7.
Referenced by [16], [17], [18], [23].
Overlap of [6] cda=acd with [13] dada=accccd:
Critical pair: caccccd=acdda.
Reduce RHS:
| [12] | (acdda) |
| ⇒ cccacdc |
Flip LHS and RHS.
Referenced by [23].
Overlap of [6] cda=acd with [14] da=acaccccd:
Critical pair: cacaccccd=acd.
Overlap of [16] cacaccccd=acd with [14] da=acaccccd:
Critical pair: cacaccccacaccccd=acda.
Reduce LHS:
| [16] | cacaccc(cacaccccd) |
| ⇒ cacacccacd |
Reduce RHS:
| [14] | ac(da) |
| [16] | ⇒ a(cacaccccd) |
| [11] | ⇒ (aacd) |
| ⇒ 1 |
Referenced by [18].
Overlap of [17] cacacccacd=1 with [14] da=acaccccd:
Critical pair: cacacccacacaccccd=a.
Reduce LHS:
| [16] | cacaccca(cacaccccd) |
| [11] | ⇒ cacaccc(aacd) |
| ⇒ cacaccc |
Defines rule #2.
Referenced by [19], [21], [23], [24].
Overlap of [18] cacaccc=a with [18] cacaccc=a:
Critical pair: cacacca=aacaccc.
Defines rule #1.
Referenced by [20], [21], [22].
Overlap of [19] cacacca=aacaccc with [11] aacd=1:
Critical pair: cacacc=aacacccacd.
Flip LHS and RHS.
Defines rule #6.
Overlap of [19] cacacca=aacaccc with [18] cacaccc=a:
Critical pair: cacaca=aacaccccaccc.
Flip LHS and RHS.
Defines rule #4.
Referenced by [23].
Overlap of [19] cacacca=aacaccc with [19] cacacca=aacaccc:
Critical pair: cacacaacaccc=aacaccccacca.
Flip LHS and RHS.
Defines rule #3.
Overlap of [14] da=acaccccd with [21] aacaccccaccc=cacaca:
Critical pair: dcacaca=acaccccdacaccccaccc.
Reduce RHS:
| [14] | acacccc(da)caccccaccc |
| [18] | ⇒ acaccc(cacaccc)cdcaccccaccc |
| [15] | ⇒ aca(cccacdc)accccaccc |
| [18] | ⇒ a(cacaccc)cdaccccaccc |
| [11] | ⇒ (aacd)accccaccc |
| ⇒ accccaccc |
Referenced by [24].
Overlap of [23] dcacaca=accccaccc with [18] cacaccc=a:
Critical pair: dcaa=accccacccccc.
Referenced by [25].
Overlap of [24] dcaa=accccacccccc with [11] aacd=1:
Critical pair: dc=accccacccccccd.
Defines rule #8.