| Back: | ⟨a, b | aaaaabba=1⟩ |
|---|
Completion settings:
Axiom: aaaaabba=1.
Referenced by [4].
Axiom: aaaaaa=c.
Defines rule #8.
Axiom: bb=d.
Defines rule #1.
Overlap of [1] aaaaabba=1 with [3] bb=d:
Critical pair: aaaaada=1.
Referenced by [7], [8], [9], [11], [12], [13].
Overlap of [3] bb=d with [3] bb=d:
Critical pair: bd=db.
Flip LHS and RHS.
Defines rule #6.
Referenced by [10].
Overlap of [2] aaaaaa=c with [2] aaaaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #2.
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], [12], [13].
Overlap of [7] cda=a with [4] aaaaada=1:
Critical pair: cd=aaaaada.
Reduce RHS:
| [4] | (aaaaada) |
| ⇒ 1 |
Defines rule #4.
Overlap of [9] cd=1 with [5] db=bd:
Critical pair: cbd=b.
Referenced by [15].
Overlap of [4] aaaaada=1 with [8] aaaada=aaaaad:
Critical pair: aaaaadaaaaad=aaada.
Reduce LHS:
| [4] | (aaaaada)aaaad |
| ⇒ aaaad |
Flip LHS and RHS.
Referenced by [13].
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.
Referenced by [13].
Overlap of [12] aada=aaad with [8] aaaada=aaaaad:
Critical pair: aadaaaaad=aaadaaada.
Reduce LHS:
| [12] | (aada)aaaad |
| [11] | ⇒ (aaada)aaad |
| [8] | ⇒ (aaaada)aad |
| [4] | ⇒ (aaaaada)ad |
| ⇒ ad |
Reduce RHS:
| [11] | (aaada)aada |
| [8] | ⇒ (aaaada)ada |
| [4] | ⇒ (aaaaada)da |
| ⇒ da |
Flip LHS and RHS.
Defines rule #5.
Referenced by [14].
Overlap of [13] da=ad with [2] aaaaaa=c:
Critical pair: dc=adaaaaa.
Reduce RHS:
| [13] | a(da)aaaa |
| [13] | ⇒ aa(da)aaa |
| [13] | ⇒ aaa(da)aa |
| [13] | ⇒ aaaa(da)a |
| [13] | ⇒ aaaaa(da) |
| [2] | ⇒ (aaaaaa)d |
| [9] | ⇒ (cd) |
| ⇒ 1 |
Defines rule #7.
Referenced by [15].
Overlap of [10] cbd=b with [14] dc=1:
Critical pair: cb=bc.
Defines rule #3.