| Back: | ⟨a, b | aababaab=aba⟩ |
|---|
Completion settings:
Axiom: aababaab=aba.
Referenced by [3].
Axiom: ababa=c.
Overlap of [1] aababaab=aba with [2] ababa=c:
Critical pair: acab=aba.
Flip LHS and RHS.
Referenced by [4], [5], [6], [7], [8], [9], [16], [21].
Overlap of [2] ababa=c with [3] aba=acab:
Critical pair: acabba=c.
Referenced by [5], [6], [7], [9], [17], [22].
Overlap of [3] aba=acab with [3] aba=acab:
Critical pair: abacab=acabba.
Reduce LHS:
| [3] | (aba)cab |
| ⇒ acabcab |
Reduce RHS:
| [4] | (acabba) |
| ⇒ c |
Referenced by [6], [10], [11], [14].
Overlap of [3] aba=acab with [4] acabba=c:
Critical pair: abc=acabcabba.
Reduce RHS:
| [5] | (acabcab)ba |
| ⇒ cba |
Flip LHS and RHS.
Defines rule #4.
Referenced by [7], [13], [18], [19].
Overlap of [4] acabba=c with [3] aba=acab:
Critical pair: acabbacab=cba.
Reduce LHS:
| [4] | (acabba)cab |
| ⇒ ccab |
Reduce RHS:
| [6] | (cba) |
| ⇒ abc |
Referenced by [8], [11], [12].
Overlap of [7] ccab=abc with [3] aba=acab:
Critical pair: ccacab=abca.
Referenced by [9], [10], [11], [13].
Overlap of [8] ccacab=abca with [4] acabba=c:
Critical pair: ccc=abcaba.
Reduce RHS:
| [3] | abc(aba) |
| ⇒ abcacab |
Flip LHS and RHS.
Referenced by [10], [11], [15].
Overlap of [5] acabcab=c with [9] abcacab=ccc:
Critical pair: acabcccc=ccacab.
Reduce RHS:
| [8] | (ccacab) |
| ⇒ abca |
Flip LHS and RHS.
Referenced by [11], [13], [14], [15], [16], [18].
Overlap of [8] ccacab=abca with [9] abcacab=ccc:
Critical pair: ccacccc=abcacacab.
Reduce RHS:
| [10] | (abca)cacab |
| [8] | ⇒ acabccc(ccacab) |
| [7] | ⇒ acabc(ccab)ca |
| [5] | ⇒ (acabcab)cca |
| ⇒ ccca |
Flip LHS and RHS.
Referenced by [12], [13], [15], [18], [19].
Overlap of [11] ccca=ccacccc with [7] ccab=abc:
Critical pair: cabc=ccaccccb.
Flip LHS and RHS.
Referenced by [13].
Overlap of [12] ccaccccb=cabc with [6] cba=abc:
Critical pair: ccacccabc=cabca.
Reduce LHS:
| [11] | cca(ccca)bc |
| [12] | ⇒ cca(ccaccccb)c |
| [8] | ⇒ (ccacab)cc |
| [10] | ⇒ (abca)cc |
| ⇒ acabcccccc |
Reduce RHS:
| [10] | c(abca) |
| ⇒ cacabcccc |
Flip LHS and RHS.
Referenced by [14], [16], [17].
Overlap of [5] acabcab=c with [10] abca=acabcccc:
Critical pair: acacabccccb=c.
Reduce LHS:
| [13] | a(cacabcccc)b |
| ⇒ aacabccccccb |
Referenced by [16], [17], [18], [19], [23].
Overlap of [9] abcacab=ccc with [10] abca=acabcccc:
Critical pair: acabcccccab=ccc.
Reduce LHS:
| [11] | acabcc(ccca)b |
| [11] | ⇒ acabc(ccca)ccccb |
| [11] | ⇒ acab(ccca)ccccccccb |
| ⇒ acabccaccccccccccccb |
Overlap of [3] aba=acab with [14] aacabccccccb=c:
Critical pair: abc=acabacabccccccb.
Reduce RHS:
| [3] | ac(aba)cabccccccb |
| [10] | ⇒ acac(abca)bccccccb |
| [13] | ⇒ aca(cacabcccc)bccccccb |
| [14] | ⇒ ac(aacabccccccb)ccccccb |
| ⇒ accccccccb |
Flip LHS and RHS.
Defines rule #2.
Overlap of [4] acabba=c with [14] aacabccccccb=c:
Critical pair: acabbc=cacabccccccb.
Reduce RHS:
| [13] | (cacabcccc)ccb |
| ⇒ acabccccccccb |
Flip LHS and RHS.
Referenced by [20].
Overlap of [6] cba=abc with [14] aacabccccccb=c:
Critical pair: cbc=abcacabccccccb.
Reduce RHS:
| [10] | (abca)cabccccccb |
| [11] | ⇒ acabcc(ccca)bccccccb |
| [11] | ⇒ acabc(ccca)ccccbccccccb |
| [11] | ⇒ acab(ccca)ccccccccbccccccb |
| [15] | ⇒ (acabccaccccccccccccb)ccccccb |
| ⇒ cccccccccb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [14] aacabccccccb=c with [6] cba=abc:
Critical pair: aacabcccccabc=ca.
Reduce LHS:
| [11] | aacabcc(ccca)bc |
| [11] | ⇒ aacabc(ccca)ccccbc |
| [11] | ⇒ aacab(ccca)ccccccccbc |
| [15] | ⇒ a(acabccaccccccccccccb)c |
| ⇒ acccc |
Flip LHS and RHS.
Defines rule #3.
Referenced by [20], [21], [22], [23].
Simplify [17] acabccccccccb=acabbc.
Reduce LHS:
| [19] | a(ca)bccccccccb |
| ⇒ aaccccbccccccccb |
Reduce RHS:
| [19] | a(ca)bbc |
| ⇒ aaccccbbc |
Defines rule #5.
Simplify [3] aba=acab.
Reduce RHS:
| [19] | a(ca)b |
| ⇒ aaccccb |
Defines rule #6.
Overlap of [4] acabba=c with [19] ca=acccc:
Critical pair: aaccccbba=c.
Defines rule #8.
Overlap of [14] aacabccccccb=c with [19] ca=acccc:
Critical pair: aaaccccbccccccb=c.
Defines rule #7.