| Back: | ⟨a, b | aabbaaab=a⟩ |
|---|
Completion settings:
Axiom: aabbaaab=a.
Referenced by [3].
Axiom: aaa=c.
Referenced by [3], [4], [5], [6], [8].
Overlap of [1] aabbaaab=a with [2] aaa=c:
Critical pair: aabbcb=a.
Referenced by [5], [6], [7], [9].
Overlap of [2] aaa=c with [2] aaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Overlap of [2] aaa=c with [3] aabbcb=a:
Critical pair: aa=cbbcb.
Referenced by [6], [7], [8], [9].
Overlap of [2] aaa=c with [3] aabbcb=a:
Critical pair: aaa=cabbcb.
Reduce LHS:
| [5] | (aa)a |
| ⇒ cbbcba |
Reduce RHS:
| [4] | (ca)bbcb |
| ⇒ acbbcb |
Referenced by [8].
Overlap of [4] ca=ac with [3] aabbcb=a:
Critical pair: ca=acabbcb.
Reduce LHS:
| [4] | (ca) |
| ⇒ ac |
Reduce RHS:
| [4] | a(ca)bbcb |
| [5] | ⇒ (aa)cbbcb |
| ⇒ cbbcbcbbcb |
Overlap of [2] aaa=c with [5] aa=cbbcb:
Critical pair: cbbcba=c.
Reduce LHS:
| [6] | (cbbcba) |
| [7] | ⇒ (ac)bbcb |
| ⇒ cbbcbcbbcbbbcb |
Referenced by [11].
Overlap of [3] aabbcb=a with [5] aa=cbbcb:
Critical pair: cbbcbbbcb=a.
Flip LHS and RHS.
Defines rule #8.
Referenced by [10].
Simplify [7] ac=cbbcbcbbcb.
Reduce LHS:
| [9] | (a)c |
| ⇒ cbbcbbbcbc |
Flip LHS and RHS.
Defines rule #4.
Referenced by [11], [12], [13].
Simplify [8] cbbcbcbbcbbbcb=c.
Reduce LHS:
| [10] | (cbbcbcbbcb)bbcb |
| ⇒ cbbcbbbcbcbbcb |
Defines rule #7.
Referenced by [12], [13], [14], [15], [16].
Overlap of [10] cbbcbcbbcb=cbbcbbbcbc with [11] cbbcbbbcbcbbcb=c:
Critical pair: cbbcbc=cbbcbbbcbcbbcbcbbcb.
Reduce RHS:
| [11] | (cbbcbbbcbcbbcb)cbbcb |
| ⇒ ccbbcb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [11] cbbcbbbcbcbbcb=c with [10] cbbcbcbbcb=cbbcbbbcbc:
Critical pair: cbbcbbbcbcbbcbbcbbbcbc=cbcbcbbcb.
Reduce LHS:
| [11] | (cbbcbbbcbcbbcb)bcbbbcbc |
| ⇒ cbcbbbcbc |
Flip LHS and RHS.
Defines rule #3.
Referenced by [15].
Overlap of [11] cbbcbbbcbcbbcb=c with [11] cbbcbbbcbcbbcb=c:
Critical pair: cbbcbbbcbcbbc=cbcbbbcbcbbcb.
Flip LHS and RHS.
Defines rule #6.
Referenced by [16].
Overlap of [11] cbbcbbbcbcbbcb=c with [13] cbcbcbbcb=cbcbbbcbc:
Critical pair: cbbcbbbcbcbbcbcbbbcbc=ccbcbbcb.
Reduce LHS:
| [11] | (cbbcbbbcbcbbcb)cbbbcbc |
| ⇒ ccbbbcbc |
Flip LHS and RHS.
Defines rule #2.
Overlap of [11] cbbcbbbcbcbbcb=c with [14] cbcbbbcbcbbcb=cbbcbbbcbcbbc:
Critical pair: cbbcbbbcbcbbcbbcbbbcbcbbc=ccbbbcbcbbcb.
Reduce LHS:
| [11] | (cbbcbbbcbcbbcb)bcbbbcbcbbc |
| ⇒ cbcbbbcbcbbc |
Flip LHS and RHS.
Defines rule #5.