| Back: | ⟨a, b | aabbababaab=1⟩ |
|---|
Completion settings:
Axiom: aabbababaab=1.
Referenced by [4].
Axiom: ab=c.
Referenced by [4], [5], [10], [13].
Axiom: bbcca=d.
Overlap of [1] aabbababaab=1 with [2] ab=c:
Critical pair: acbababaab=1.
Reduce LHS:
| [2] | acb(ab)abaab |
| [2] | ⇒ acbc(ab)aab |
| [2] | ⇒ acbcca(ab) |
| ⇒ acbccac |
Referenced by [6].
Overlap of [2] ab=c with [3] bbcca=d:
Critical pair: ad=cbcca.
Flip LHS and RHS.
Simplify [4] acbccac=1.
Reduce LHS:
| [5] | a(cbcca)c |
| ⇒ aadc |
Referenced by [7], [8], [14], [15], [18], [24].
Overlap of [3] bbcca=d with [6] aadc=1:
Critical pair: bbcc=dadc.
Overlap of [6] aadc=1 with [5] cbcca=ad:
Critical pair: aadad=bcca.
Flip LHS and RHS.
Overlap of [3] bbcca=d with [7] bbcc=dadc:
Critical pair: dadca=d.
Referenced by [11], [12], [16], [17], [20].
Overlap of [2] ab=c with [8] bcca=aadad:
Critical pair: aaadad=ccca.
Overlap of [7] bbcc=dadc with [8] bcca=aadad:
Critical pair: baadad=dadca.
Reduce RHS:
| [9] | (dadca) |
| ⇒ d |
Referenced by [12].
Overlap of [11] baadad=d with [9] dadca=d:
Critical pair: baad=dca.
Overlap of [2] ab=c with [12] baad=dca:
Critical pair: adca=caad.
Flip LHS and RHS.
Overlap of [12] baad=dca with [6] aadc=1:
Critical pair: b=dcac.
Defines rule #6.
Overlap of [13] caad=adca with [6] aadc=1:
Critical pair: c=adcac.
Flip LHS and RHS.
Overlap of [9] dadca=d with [15] adcac=c:
Critical pair: dadcc=ddcac.
Referenced by [20].
Overlap of [10] aaadad=ccca with [9] dadca=d:
Critical pair: aaad=cccaca.
Referenced by [18], [22], [23].
Overlap of [17] aaad=cccaca with [6] aadc=1:
Critical pair: a=cccacac.
Flip LHS and RHS.
Defines rule #2.
Referenced by [19], [20], [21], [24], [31], [32].
Overlap of [15] adcac=c with [18] cccacac=a:
Critical pair: adcaa=cccacac.
Reduce RHS:
| [18] | (cccacac) |
| ⇒ a |
Overlap of [16] dadcc=ddcac with [18] cccacac=a:
Critical pair: dadca=ddcacccacac.
Reduce LHS:
| [9] | (dadca) |
| ⇒ d |
Reduce RHS:
| [18] | ddca(cccacac) |
| ⇒ ddcaa |
Flip LHS and RHS.
Referenced by [23].
Overlap of [18] cccacac=a with [18] cccacac=a:
Critical pair: cccacaa=accacac.
Defines rule #1.
Referenced by [23].
Overlap of [19] adcaa=a with [17] aaad=cccaca:
Critical pair: adccccaca=aad.
Flip LHS and RHS.
Overlap of [10] aaadad=ccca with [20] ddcaa=d:
Critical pair: aaadad=cccadcaa.
Reduce LHS:
| [17] | (aaad)ad |
| [21] | ⇒ (cccacaa)d |
| ⇒ accacacd |
Reduce RHS:
| [19] | ccc(adcaa) |
| ⇒ ccca |
Referenced by [31].
Overlap of [6] aadc=1 with [22] aad=adccccaca:
Critical pair: adccccacac=1.
Reduce LHS:
| [18] | adc(cccacac) |
| ⇒ adca |
Referenced by [25], [27], [28].
Simplify [13] caad=adca.
Reduce RHS:
| [24] | (adca) |
| ⇒ 1 |
Referenced by [26].
Overlap of [25] caad=1 with [22] aad=adccccaca:
Critical pair: cadccccaca=1.
Referenced by [29].
Overlap of [24] adca=1 with [24] adca=1:
Critical pair: adc=dca.
Referenced by [28], [29], [30].
Overlap of [24] adca=1 with [27] adc=dca:
Critical pair: dcaa=1.
Defines rule #3.
Simplify [26] cadccccaca=1.
Reduce LHS:
| [27] | c(adc)cccaca |
| ⇒ cdcacccaca |
Referenced by [30].
Overlap of [27] adc=dca with [29] cdcacccaca=1:
Critical pair: ad=dcadcacccaca.
Reduce RHS:
| [27] | dc(adc)acccaca |
| [28] | ⇒ dc(dcaa)cccaca |
| ⇒ dccccaca |
Defines rule #4.
Overlap of [18] cccacac=a with [23] accacacd=ccca:
Critical pair: cccacccca=acacacd.
Flip LHS and RHS.
Referenced by [32].
Overlap of [18] cccacac=a with [31] acacacd=cccacccca:
Critical pair: ccccccacccca=aacd.
Flip LHS and RHS.
Referenced by [33].
Overlap of [28] dcaa=1 with [32] aacd=ccccccacccca:
Critical pair: dcccccccacccca=cd.
Flip LHS and RHS.
Defines rule #5.