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