| Back: | ⟨a, b | aababaaabba=1⟩ |
|---|
Completion settings:
Axiom: aababaaabba=1.
Referenced by [3].
Axiom: baaab=c.
Referenced by [3], [4], [5], [6].
Overlap of [1] aababaaabba=1 with [2] baaab=c:
Critical pair: aabacba=1.
Referenced by [5], [6], [7], [8], [9], [11], [16].
Overlap of [2] baaab=c with [2] baaab=c:
Critical pair: baaac=caaab.
Flip LHS and RHS.
Referenced by [13].
Overlap of [2] baaab=c with [3] aabacba=1:
Critical pair: ba=cacba.
Flip LHS and RHS.
Referenced by [12].
Overlap of [3] aabacba=1 with [2] baaab=c:
Critical pair: aabacc=aab.
Referenced by [17].
Overlap of [3] aabacba=1 with [3] aabacba=1:
Critical pair: aabacb=abacba.
Overlap of [3] aabacba=1 with [7] aabacb=abacba:
Critical pair: abacbaa=1.
Overlap of [3] aabacba=1 with [7] aabacb=abacba:
Critical pair: aabacbabacba=abacb.
Reduce LHS:
| [7] | (aabacb)abacba |
| [8] | ⇒ (abacbaa)bacba |
| ⇒ bacba |
Flip LHS and RHS.
Referenced by [10], [18], [20].
Simplify [8] abacbaa=1.
Reduce LHS:
| [9] | (abacb)aa |
| ⇒ bacbaaa |
Referenced by [11], [12], [15].
Overlap of [3] aabacba=1 with [10] bacbaaa=1:
Critical pair: aabac=cbaaa.
Overlap of [5] cacba=ba with [10] bacbaaa=1:
Critical pair: cac=bacbaaa.
Reduce RHS:
| [10] | (bacbaaa) |
| ⇒ 1 |
Referenced by [13], [14], [19].
Overlap of [12] cac=1 with [4] caaab=baaac:
Critical pair: cabaaac=aaab.
Flip LHS and RHS.
Overlap of [12] cac=1 with [12] cac=1:
Critical pair: ca=ac.
Flip LHS and RHS.
Defines rule #1.
Referenced by [15], [16], [17], [18], [19], [20], [21], [22], [24], [25].
Overlap of [10] bacbaaa=1 with [14] ac=ca:
Critical pair: bacbaaca=c.
Reduce LHS:
| [14] | b(ac)baaca |
| [14] | ⇒ bcaba(ac)a |
| [14] | ⇒ bcab(ac)aa |
| ⇒ bcabcaaa |
Overlap of [3] aabacba=1 with [11] aabac=cbaaa:
Critical pair: cbaaaba=1.
Reduce LHS:
| [13] | cb(aaab)a |
| [14] | ⇒ cbcabaa(ac)a |
| [14] | ⇒ cbcaba(ac)aa |
| [14] | ⇒ cbcab(ac)aaa |
| [15] | ⇒ c(bcabcaaa)a |
| ⇒ cca |
Defines rule #2.
Referenced by [23], [24], [25], [27], [28].
Overlap of [6] aabacc=aab with [11] aabac=cbaaa:
Critical pair: cbaaac=aab.
Reduce LHS:
| [14] | cbaa(ac) |
| [14] | ⇒ cba(ac)a |
| [14] | ⇒ cb(ac)aa |
| ⇒ cbcaaa |
Flip LHS and RHS.
Defines rule #3.
Referenced by [19], [23], [25].
Simplify [7] aabacb=abacba.
Reduce RHS:
| [9] | (abacb)a |
| [14] | ⇒ b(ac)baa |
| ⇒ bcabaa |
Referenced by [19].
Overlap of [18] aabacb=bcabaa with [17] aab=cbcaaa:
Critical pair: cbcaaaacb=bcabaa.
Reduce LHS:
| [14] | cbcaaa(ac)b |
| [14] | ⇒ cbcaa(ac)ab |
| [14] | ⇒ cbca(ac)aab |
| [12] | ⇒ cb(cac)aaab |
| [13] | ⇒ cb(aaab) |
| [14] | ⇒ cbcabaa(ac) |
| [14] | ⇒ cbcaba(ac)a |
| [14] | ⇒ cbcab(ac)aa |
| [15] | ⇒ c(bcabcaaa) |
| ⇒ cc |
Flip LHS and RHS.
Referenced by [22].
Simplify [9] abacb=bacba.
Reduce RHS:
| [14] | b(ac)ba |
| ⇒ bcaba |
Referenced by [21].
Overlap of [20] abacb=bcaba with [14] ac=ca:
Critical pair: abcab=bcaba.
Overlap of [19] bcabaa=cc with [14] ac=ca:
Critical pair: bcabaca=ccc.
Reduce LHS:
| [14] | bcab(ac)a |
| ⇒ bcabcaa |
Referenced by [25].
Overlap of [16] cca=1 with [17] aab=cbcaaa:
Critical pair: cccbcaaa=ab.
Referenced by [24].
Overlap of [23] cccbcaaa=ab with [14] ac=ca:
Critical pair: cccbcaaca=abc.
Reduce LHS:
| [14] | cccbca(ac)a |
| [14] | ⇒ cccbc(ac)aa |
| [16] | ⇒ cccb(cca)aa |
| ⇒ cccbaa |
Referenced by [25].
Overlap of [24] cccbaa=abc with [17] aab=cbcaaa:
Critical pair: cccbacbcaaa=abcab.
Reduce LHS:
| [14] | cccb(ac)bcaaa |
| [22] | ⇒ ccc(bcabcaa)a |
| [16] | ⇒ cccc(cca) |
| ⇒ cccc |
Reduce RHS:
| [21] | (abcab) |
| ⇒ bcaba |
Flip LHS and RHS.
Referenced by [26].
Simplify [21] abcab=bcaba.
Reduce RHS:
| [25] | (bcaba) |
| ⇒ cccc |
Overlap of [16] cca=1 with [26] abcab=cccc:
Critical pair: cccccc=bcab.
Flip LHS and RHS.
Defines rule #5.
Overlap of [26] abcab=cccc with [26] abcab=cccc:
Critical pair: abccccc=cccccab.
Reduce RHS:
| [16] | ccc(cca)b |
| ⇒ cccb |
Flip LHS and RHS.
Defines rule #4.