| Back: | ⟨a, b | aaa=1, bbbb=abba⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #13.
Axiom: bbbb=abba.
Flip LHS and RHS.
Referenced by [4].
Axiom: bba=c.
Defines rule #5.
Referenced by [4], [5], [7], [8], [11], [12], [13], [17], [20], [23].
Overlap of [2] abba=bbbb with [3] bba=c:
Critical pair: ac=bbbb.
Defines rule #11.
Referenced by [6], [7], [8], [9], [10], [13], [21].
Overlap of [3] bba=c with [1] aaa=1:
Critical pair: bb=caa.
Flip LHS and RHS.
Overlap of [1] aaa=1 with [4] ac=bbbb:
Critical pair: aabbbb=c.
Referenced by [11], [12], [13], [21], [22].
Overlap of [3] bba=c with [4] ac=bbbb:
Critical pair: bbbbbb=cc.
Flip LHS and RHS.
Defines rule #6.
Referenced by [13], [14], [17], [20].
Overlap of [4] ac=bbbb with [5] caa=bb:
Critical pair: abb=bbbbaa.
Reduce RHS:
| [3] | bb(bba)a |
| ⇒ bbca |
Flip LHS and RHS.
Referenced by [10], [13], [18].
Overlap of [5] caa=bb with [4] ac=bbbb:
Critical pair: cabbbb=bbc.
Referenced by [15].
Overlap of [8] bbca=abb with [4] ac=bbbb:
Critical pair: bbcbbbb=abbc.
Flip LHS and RHS.
Overlap of [6] aabbbb=c with [3] bba=c:
Critical pair: aabbc=ca.
Reduce LHS:
| [10] | a(abbc) |
| [10] | ⇒ (abbc)bbbb |
| ⇒ bbcbbbbbbbb |
Flip LHS and RHS.
Defines rule #9.
Referenced by [15], [17], [18], [20].
Overlap of [6] aabbbb=c with [3] bba=c:
Critical pair: aabbbc=cba.
Referenced by [16].
Overlap of [6] aabbbb=c with [8] bbca=abb:
Critical pair: aabbabb=cca.
Reduce LHS:
| [3] | aa(bba)bb |
| [4] | ⇒ a(ac)bb |
| ⇒ abbbbbb |
Reduce RHS:
| [7] | (cc)a |
| [3] | ⇒ bbbb(bba) |
| ⇒ bbbbc |
Referenced by [16].
Overlap of [7] cc=bbbbbb with [7] cc=bbbbbb:
Critical pair: cbbbbbb=bbbbbbc.
Flip LHS and RHS.
Defines rule #3.
Referenced by [17], [19], [20], [21], [22], [23].
Simplify [9] cabbbb=bbc.
Reduce LHS:
| [11] | (ca)bbbb |
| ⇒ bbcbbbbbbbbbbbb |
Referenced by [16], [21], [22].
Overlap of [12] aabbbc=cba with [15] bbcbbbbbbbbbbbb=bbc:
Critical pair: aabbbc=cbabbbbbbbbbbbb.
Reduce LHS:
| [12] | (aabbbc) |
| ⇒ cba |
Reduce RHS:
| [13] | cb(abbbbbb)bbbbbb |
| ⇒ cbbbbbcbbbbbb |
Defines rule #10.
Overlap of [5] caa=bb with [11] ca=bbcbbbbbbbb:
Critical pair: bbcbbbbbbbba=bb.
Reduce LHS:
| [3] | bbcbbbbbb(bba) |
| [14] | ⇒ bbc(bbbbbbc) |
| [7] | ⇒ bb(cc)bbbbbb |
| ⇒ bbbbbbbbbbbbbb |
Defines rule #1.
Overlap of [8] bbca=abb with [11] ca=bbcbbbbbbbb:
Critical pair: bbbbcbbbbbbbb=abb.
Flip LHS and RHS.
Defines rule #4.
Referenced by [19], [21], [22], [23].
Overlap of [10] abbc=bbcbbbb with [18] abb=bbbbcbbbbbbbb:
Critical pair: bbbbcbbbbbbbbc=bbcbbbb.
Reduce LHS:
| [14] | bbbbcbb(bbbbbbc) |
| ⇒ bbbbcbbcbbbbbb |
Referenced by [22].
Overlap of [11] ca=bbcbbbbbbbb with [1] aaa=1:
Critical pair: c=bbcbbbbbbbbaa.
Reduce RHS:
| [3] | bbcbbbbbb(bba)a |
| [14] | ⇒ bbc(bbbbbbc)a |
| [3] | ⇒ bbccbbbb(bba) |
| [7] | ⇒ bb(cc)bbbbc |
| [14] | ⇒ bbbbbb(bbbbbbc) |
| [14] | ⇒ (bbbbbbc)bbbbbb |
| ⇒ cbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [6] aabbbb=c with [14] bbbbbbc=cbbbbbb:
Critical pair: aacbbbbbb=cbbc.
Reduce LHS:
| [4] | a(ac)bbbbbb |
| [18] | ⇒ (abb)bbbbbbbb |
| [15] | ⇒ bb(bbcbbbbbbbbbbbb)bbbb |
| ⇒ bbbbcbbbb |
Flip LHS and RHS.
Defines rule #7.
Overlap of [6] aabbbb=c with [14] bbbbbbc=cbbbbbb:
Critical pair: aabbcbbbbbb=cbbbbc.
Reduce LHS:
| [18] | a(abb)cbbbbbb |
| [14] | ⇒ abbbbcbb(bbbbbbc)bbbbbb |
| [19] | ⇒ a(bbbbcbbcbbbbbb)bbbbbb |
| [18] | ⇒ (abb)cbbbbbbbbbb |
| [14] | ⇒ bbbbcbb(bbbbbbc)bbbbbbbbbb |
| [19] | ⇒ (bbbbcbbcbbbbbb)bbbbbbbbbb |
| [15] | ⇒ (bbcbbbbbbbbbbbb)bb |
| ⇒ bbcbb |
Flip LHS and RHS.
Defines rule #8.
Overlap of [18] abb=bbbbcbbbbbbbb with [3] bba=c:
Critical pair: abc=bbbbcbbbbbbbbba.
Reduce RHS:
| [3] | bbbbcbbbbbbb(bba) |
| [14] | ⇒ bbbbcb(bbbbbbc) |
| ⇒ bbbbcbcbbbbbb |
Defines rule #12.