| Back: | ⟨a, b | aaaaabbba=1⟩ |
|---|
Completion settings:
Axiom: aaaaabbba=1.
Referenced by [4].
Axiom: aaaaaa=c.
Defines rule #8.
Referenced by [6], [7], [12], [14].
Axiom: bbb=d.
Defines rule #7.
Overlap of [1] aaaaabbba=1 with [3] bbb=d:
Critical pair: aaaaada=1.
Referenced by [7], [8], [9], [11].
Overlap of [3] bbb=d with [3] bbb=d:
Critical pair: bd=db.
Flip LHS and RHS.
Defines rule #5.
Referenced by [10].
Overlap of [2] aaaaaa=c with [2] aaaaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #1.
Referenced by [16].
Overlap of [2] aaaaaa=c with [4] aaaaada=1:
Critical pair: a=cda.
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] aaaaada=1 with [4] aaaaada=1:
Critical pair: aaaaad=aaaada.
Flip LHS and RHS.
Referenced by [11].
Overlap of [7] cda=a with [4] aaaaada=1:
Critical pair: cd=aaaaada.
Reduce RHS:
| [4] | (aaaaada) |
| ⇒ 1 |
Defines rule #3.
Referenced by [10], [12], [14], [17].
Overlap of [9] cd=1 with [5] db=bd:
Critical pair: cbd=b.
Referenced by [15].
Overlap of [8] aaaada=aaaaad with [8] aaaada=aaaaad:
Critical pair: aaaadaaaaad=aaaaadaaada.
Reduce LHS:
| [8] | (aaaada)aaaad |
| [4] | ⇒ (aaaaada)aaad |
| ⇒ aaad |
Reduce RHS:
| [4] | (aaaaada)aada |
| ⇒ aada |
Flip LHS and RHS.
Overlap of [11] aada=aaad with [2] aaaaaa=c:
Critical pair: aadc=aaadaaaaa.
Reduce RHS:
| [11] | a(aada)aaaa |
| [11] | ⇒ aa(aada)aaa |
| [11] | ⇒ aaa(aada)aa |
| [2] | ⇒ (aaaaaa)daa |
| [9] | ⇒ (cd)aa |
| ⇒ aa |
Referenced by [13].
Overlap of [11] aada=aaad with [12] aadc=aa:
Critical pair: aadaa=aaadadc.
Reduce LHS:
| [11] | (aada)a |
| [11] | ⇒ a(aada) |
| ⇒ aaaad |
Reduce RHS:
| [11] | a(aada)dc |
| ⇒ aaaaddc |
Flip LHS and RHS.
Referenced by [14].
Overlap of [2] aaaaaa=c with [13] aaaaddc=aaaad:
Critical pair: aaaaaad=cddc.
Reduce LHS:
| [2] | (aaaaaa)d |
| [9] | ⇒ (cd) |
| ⇒ 1 |
Reduce RHS:
| [9] | (cd)dc |
| ⇒ dc |
Flip LHS and RHS.
Defines rule #6.
Overlap of [10] cbd=b with [14] dc=1:
Critical pair: cb=bc.
Defines rule #2.
Overlap of [14] dc=1 with [6] ca=ac:
Critical pair: dac=a.
Referenced by [17].
Overlap of [16] dac=a with [9] cd=1:
Critical pair: da=ad.
Defines rule #4.