| Back: | ⟨a, b | aabbbaaaab=a⟩ |
|---|
Completion settings:
Axiom: aabbbaaaab=a.
Referenced by [3].
Axiom: aaaa=c.
Referenced by [3], [4], [5], [6], [8].
Overlap of [1] aabbbaaaab=a with [2] aaaa=c:
Critical pair: aabbbcb=a.
Referenced by [5], [6], [7], [10], [14].
Overlap of [2] aaaa=c with [2] aaaa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Referenced by [6], [7], [9], [15].
Overlap of [2] aaaa=c with [3] aabbbcb=a:
Critical pair: aaa=cbbbcb.
Referenced by [6], [8], [9], [10], [11], [16].
Overlap of [2] aaaa=c with [3] aabbbcb=a:
Critical pair: aaaa=cabbbcb.
Reduce LHS:
| [5] | (aaa)a |
| ⇒ cbbbcba |
Reduce RHS:
| [4] | (ca)bbbcb |
| ⇒ acbbbcb |
Overlap of [4] ca=ac with [3] aabbbcb=a:
Critical pair: ca=acabbbcb.
Reduce LHS:
| [4] | (ca) |
| ⇒ ac |
Reduce RHS:
| [4] | a(ca)bbbcb |
| ⇒ aacbbbcb |
Flip LHS and RHS.
Referenced by [12].
Overlap of [2] aaaa=c with [5] aaa=cbbbcb:
Critical pair: cbbbcba=c.
Reduce LHS:
| [6] | (cbbbcba) |
| ⇒ acbbbcb |
Referenced by [11], [13], [18].
Overlap of [4] ca=ac with [5] aaa=cbbbcb:
Critical pair: ccbbbcb=acaa.
Reduce RHS:
| [4] | a(ca)a |
| [4] | ⇒ aa(ca) |
| [5] | ⇒ (aaa)c |
| ⇒ cbbbcbc |
Defines rule #1.
Referenced by [15].
Overlap of [5] aaa=cbbbcb with [3] aabbbcb=a:
Critical pair: aa=cbbbcbbbbcb.
Referenced by [11], [12], [14], [15], [16].
Overlap of [5] aaa=cbbbcb with [8] acbbbcb=c:
Critical pair: aac=cbbbcbcbbbcb.
Reduce LHS:
| [10] | (aa)c |
| ⇒ cbbbcbbbbcbc |
Flip LHS and RHS.
Defines rule #5.
Simplify [7] aacbbbcb=ac.
Reduce LHS:
| [10] | (aa)cbbbcb |
| ⇒ cbbbcbbbbcbcbbbcb |
Flip LHS and RHS.
Overlap of [8] acbbbcb=c with [12] ac=cbbbcbbbbcbcbbbcb:
Critical pair: cbbbcbbbbcbcbbbcbbbbcb=c.
Referenced by [16].
Overlap of [3] aabbbcb=a with [10] aa=cbbbcbbbbcb:
Critical pair: cbbbcbbbbcbbbbcb=a.
Flip LHS and RHS.
Defines rule #14.
Referenced by [15], [16], [17], [18].
Overlap of [4] ca=ac with [10] aa=cbbbcbbbbcb:
Critical pair: ccbbbcbbbbcb=aca.
Reduce LHS:
| [9] | (ccbbbcb)bbbcb |
| [11] | ⇒ (cbbbcbcbbbcb) |
| ⇒ cbbbcbbbbcbc |
Reduce RHS:
| [14] | (a)ca |
| [4] | ⇒ cbbbcbbbbcbbbbcb(ca) |
| [14] | ⇒ cbbbcbbbbcbbbbcb(a)c |
| ⇒ cbbbcbbbbcbbbbcbcbbbcbbbbcbbbbcbc |
Flip LHS and RHS.
Referenced by [16].
Overlap of [5] aaa=cbbbcb with [10] aa=cbbbcbbbbcb:
Critical pair: aacbbbcbbbbcb=cbbbcba.
Reduce LHS:
| [14] | (a)acbbbcbbbbcb |
| [14] | ⇒ cbbbcbbbbcbbbbcb(a)cbbbcbbbbcb |
| [15] | ⇒ (cbbbcbbbbcbbbbcbcbbbcbbbbcbbbbcbc)bbbcbbbbcb |
| [13] | ⇒ (cbbbcbbbbcbcbbbcbbbbcb) |
| ⇒ c |
Reduce RHS:
| [6] | (cbbbcba) |
| [14] | ⇒ (a)cbbbcb |
| ⇒ cbbbcbbbbcbbbbcbcbbbcb |
Flip LHS and RHS.
Defines rule #13.
Referenced by [18], [19], [20], [21], [22], [23], [24], [25], [26].
Overlap of [12] ac=cbbbcbbbbcbcbbbcb with [14] a=cbbbcbbbbcbbbbcb:
Critical pair: cbbbcbbbbcbbbbcbc=cbbbcbbbbcbcbbbcb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [22].
Overlap of [8] acbbbcb=c with [16] cbbbcbbbbcbbbbcbcbbbcb=c:
Critical pair: acbbbc=cbbcbbbbcbbbbcbcbbbcb.
Reduce LHS:
| [14] | (a)cbbbc |
| ⇒ cbbbcbbbbcbbbbcbcbbbc |
Flip LHS and RHS.
Defines rule #12.
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [11] cbbbcbcbbbcb=cbbbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbbbcbbbbcbc=cbbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)bbcbbbbcbc |
| ⇒ cbbcbbbbcbc |
Flip LHS and RHS.
Defines rule #4.
Referenced by [20].
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [19] cbbcbcbbbcb=cbbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbbcbbbbcbc=cbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)bcbbbbcbc |
| ⇒ cbcbbbbcbc |
Flip LHS and RHS.
Defines rule #3.
Referenced by [21].
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [20] cbcbcbbbcb=cbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbcbbbbcbc=ccbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)cbbbbcbc |
| ⇒ ccbbbbcbc |
Flip LHS and RHS.
Defines rule #2.
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [17] cbbbcbbbbcbcbbbcb=cbbbcbbbbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbbbcbbbbcbbbbcbc=cbbcbbbbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)bbcbbbbcbbbbcbc |
| ⇒ cbbcbbbbcbbbbcbc |
Flip LHS and RHS.
Defines rule #8.
Referenced by [23].
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [22] cbbcbbbbcbcbbbcb=cbbcbbbbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbbcbbbbcbbbbcbc=cbcbbbbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)bcbbbbcbbbbcbc |
| ⇒ cbcbbbbcbbbbcbc |
Flip LHS and RHS.
Defines rule #7.
Referenced by [24].
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [23] cbcbbbbcbcbbbcb=cbcbbbbcbbbbcbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbcbbbbcbbbbcbc=ccbbbbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)cbbbbcbbbbcbc |
| ⇒ ccbbbbcbbbbcbc |
Flip LHS and RHS.
Defines rule #6.
Overlap of [16] cbbbcbbbbcbbbbcbcbbbcb=c with [18] cbbcbbbbcbbbbcbcbbbcb=cbbbcbbbbcbbbbcbcbbbc:
Critical pair: cbbbcbbbbcbbbbcbcbbbcbbbcbbbbcbbbbcbcbbbc=cbcbbbbcbbbbcbcbbbcb.
Reduce LHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)bbcbbbbcbbbbcbcbbbc |
| ⇒ cbbcbbbbcbbbbcbcbbbc |
Flip LHS and RHS.
Defines rule #11.
Overlap of [18] cbbcbbbbcbbbbcbcbbbcb=cbbbcbbbbcbbbbcbcbbbc with [18] cbbcbbbbcbbbbcbcbbbcb=cbbbcbbbbcbbbbcbcbbbc:
Critical pair: cbbcbbbbcbbbbcbcbbbcbbbcbbbbcbbbbcbcbbbc=cbbbcbbbbcbbbbcbcbbbcbcbbbbcbbbbcbcbbbcb.
Reduce LHS:
| [18] | (cbbcbbbbcbbbbcbcbbbcb)bbcbbbbcbbbbcbcbbbc |
| [16] | ⇒ (cbbbcbbbbcbbbbcbcbbbcb)bcbbbbcbbbbcbcbbbc |
| ⇒ cbcbbbbcbbbbcbcbbbc |
Reduce RHS:
| [16] | (cbbbcbbbbcbbbbcbcbbbcb)cbbbbcbbbbcbcbbbcb |
| ⇒ ccbbbbcbbbbcbcbbbcb |
Flip LHS and RHS.
Defines rule #10.