| Back: | ⟨a, b | abaabbaaab=1⟩ |
|---|
Completion settings:
Axiom: abaabbaaab=1.
Referenced by [4].
Axiom: baabb=c.
Axiom: aca=d.
Referenced by [4], [5], [8], [11], [12], [16], [20].
Overlap of [1] abaabbaaab=1 with [2] baabb=c:
Critical pair: acaaab=1.
Reduce LHS:
| [3] | (aca)aab |
| ⇒ daab |
Referenced by [7], [9], [13], [14], [15].
Overlap of [3] aca=d with [3] aca=d:
Critical pair: acd=dca.
Flip LHS and RHS.
Overlap of [2] baabb=c with [2] baabb=c:
Critical pair: baabc=caabb.
Referenced by [12].
Overlap of [4] daab=1 with [2] baabb=c:
Critical pair: daac=aabb.
Flip LHS and RHS.
Overlap of [3] aca=d with [7] aabb=daac:
Critical pair: acdaac=dabb.
Flip LHS and RHS.
Referenced by [10].
Overlap of [4] daab=1 with [7] aabb=daac:
Critical pair: ddaac=b.
Flip LHS and RHS.
Defines rule #7.
Referenced by [10], [12], [15].
Simplify [8] dabb=acdaac.
Reduce LHS:
| [9] | da(b)b |
| [9] | ⇒ daddaac(b) |
| ⇒ daddaacddaac |
Referenced by [11].
Overlap of [10] daddaacddaac=acdaac with [3] aca=d:
Critical pair: daddaacddad=acdaaca.
Reduce RHS:
| [3] | acda(aca) |
| ⇒ acdad |
Referenced by [13].
Simplify [6] baabc=caabb.
Reduce LHS:
| [9] | (b)aabc |
| [3] | ⇒ dda(aca)abc |
| [9] | ⇒ ddada(b)c |
| ⇒ ddadaddaacc |
Reduce RHS:
| [7] | c(aabb) |
| ⇒ cdaac |
Flip LHS and RHS.
Referenced by [22].
Overlap of [11] daddaacddad=acdad with [4] daab=1:
Critical pair: daddaacdda=acdadaab.
Reduce RHS:
| [4] | acda(daab) |
| ⇒ acda |
Referenced by [14].
Overlap of [13] daddaacdda=acda with [4] daab=1:
Critical pair: daddaacd=acdaab.
Reduce RHS:
| [4] | ac(daab) |
| ⇒ ac |
Referenced by [19].
Overlap of [4] daab=1 with [9] b=ddaac:
Critical pair: daaddaac=1.
Defines rule #3.
Referenced by [16], [17], [19], [23], [24].
Overlap of [15] daaddaac=1 with [3] aca=d:
Critical pair: daaddad=a.
Defines rule #1.
Referenced by [17], [18], [19], [21].
Overlap of [16] daaddad=a with [15] daaddaac=1:
Critical pair: daadda=aaaddaac.
Flip LHS and RHS.
Defines rule #4.
Referenced by [23].
Overlap of [16] daaddad=a with [16] daaddad=a:
Critical pair: daaddaa=aaaddad.
Flip LHS and RHS.
Defines rule #2.
Referenced by [21], [23], [24].
Overlap of [16] daaddad=a with [14] daddaacd=ac:
Critical pair: daaddaac=aaddaacd.
Reduce LHS:
| [15] | (daaddaac) |
| ⇒ 1 |
Flip LHS and RHS.
Overlap of [19] aaddaacd=1 with [5] dca=acd:
Critical pair: aaddaacacd=ca.
Reduce LHS:
| [3] | aadda(aca)cd |
| ⇒ aaddadcd |
Flip LHS and RHS.
Referenced by [21], [23], [24], [25].
Overlap of [20] ca=aaddadcd with [18] aaaddad=daaddaa:
Critical pair: cdaaddaa=aaddadcdaaddad.
Reduce RHS:
| [16] | aaddadc(daaddad) |
| [5] | ⇒ aadda(dca) |
| [19] | ⇒ (aaddaacd) |
| ⇒ 1 |
Referenced by [22].
Overlap of [12] cdaac=ddadaddaacc with [21] cdaaddaa=1:
Critical pair: cdaa=ddadaddaaccdaaddaa.
Reduce RHS:
| [21] | ddadaddaac(cdaaddaa) |
| ⇒ ddadaddaac |
Referenced by [23].
Overlap of [22] cdaa=ddadaddaac with [17] aaaddaac=daadda:
Critical pair: cddaadda=ddadaddaacaddaac.
Reduce RHS:
| [20] | ddadaddaa(ca)ddaac |
| [18] | ⇒ ddadadda(aaaddad)cdddaac |
| [15] | ⇒ ddadadda(daaddaac)dddaac |
| ⇒ ddadaddadddaac |
Referenced by [24].
Overlap of [23] cddaadda=ddadaddadddaac with [15] daaddaac=1:
Critical pair: cd=ddadaddadddaacac.
Reduce RHS:
| [20] | ddadaddadddaa(ca)c |
| [18] | ⇒ ddadaddaddda(aaaddad)cdc |
| [15] | ⇒ ddadaddaddda(daaddaac)dc |
| ⇒ ddadaddadddadc |
Defines rule #5.
Referenced by [25].
Simplify [20] ca=aaddadcd.
Reduce RHS:
| [24] | aaddad(cd) |
| ⇒ aaddadddadaddadddadc |
Defines rule #6.