| Back: | ⟨a, b | abababaab=ba⟩ |
|---|
Completion settings:
Axiom: abababaab=ba.
Referenced by [4], [5], [6], [8], [18].
Axiom: abaabab=c.
Referenced by [3], [4], [5], [6], [7], [9], [10], [11], [14], [19].
Overlap of [2] abaabab=c with [2] abaabab=c:
Critical pair: abaabc=caabab.
Overlap of [1] abababaab=ba with [2] abaabab=c:
Critical pair: ababc=baab.
Referenced by [7], [8], [9], [15], [18].
Overlap of [2] abaabab=c with [1] abababaab=ba:
Critical pair: ababa=cabaab.
Referenced by [6].
Overlap of [2] abaabab=c with [1] abababaab=ba:
Critical pair: abaabba=cababaab.
Reduce RHS:
| [5] | c(ababa)ab |
| [2] | ⇒ cc(abaabab) |
| ⇒ ccc |
Referenced by [7], [8], [12], [16].
Overlap of [2] abaabab=c with [4] ababc=baab:
Critical pair: abaabbaab=cabc.
Reduce LHS:
| [6] | (abaabba)ab |
| ⇒ cccab |
Flip LHS and RHS.
Referenced by [13], [20], [22].
Overlap of [1] abababaab=ba with [6] abaabba=ccc:
Critical pair: ababccc=baba.
Reduce LHS:
| [4] | (ababc)cc |
| ⇒ baabcc |
Flip LHS and RHS.
Referenced by [9], [10], [18].
Overlap of [2] abaabab=c with [8] baba=baabcc:
Critical pair: abaabaabcc=ca.
Reduce LHS:
| [3] | aba(abaabc)c |
| [4] | ⇒ abaca(ababc) |
| ⇒ abacabaab |
Referenced by [11], [12], [20].
Overlap of [8] baba=baabcc with [2] abaabab=c:
Critical pair: bc=baabccabab.
Flip LHS and RHS.
Referenced by [21].
Overlap of [9] abacabaab=ca with [2] abaabab=c:
Critical pair: abacc=caab.
Overlap of [9] abacabaab=ca with [6] abaabba=ccc:
Critical pair: abacccc=caba.
Reduce LHS:
| [11] | (abacc)cc |
| ⇒ caabcc |
Flip LHS and RHS.
Referenced by [13], [14], [15], [16], [17], [18], [19], [20], [21].
Overlap of [7] cabc=cccab with [12] caba=caabcc:
Critical pair: cabcaabcc=cccababa.
Reduce LHS:
| [7] | (cabc)aabcc |
| [12] | ⇒ cc(caba)abcc |
| [7] | ⇒ cccaabc(cabc)c |
| [7] | ⇒ cccaabccc(cabc) |
| ⇒ cccaabccccccab |
Reduce RHS:
| [12] | cc(caba)ba |
| ⇒ cccaabccba |
Flip LHS and RHS.
Referenced by [19], [20], [21].
Overlap of [12] caba=caabcc with [2] abaabab=c:
Critical pair: cc=caabccabab.
Reduce RHS:
| [12] | caabc(caba)b |
| ⇒ caabccaabccb |
Flip LHS and RHS.
Referenced by [20].
Overlap of [12] caba=caabcc with [4] ababc=baab:
Critical pair: cbaab=caabccbc.
Flip LHS and RHS.
Referenced by [21].
Overlap of [12] caba=caabcc with [6] abaabba=ccc:
Critical pair: cccc=caabccabba.
Flip LHS and RHS.
Overlap of [12] caba=caabcc with [11] abacc=caab:
Critical pair: ccaab=caabcccc.
Flip LHS and RHS.
Referenced by [19], [20], [21].
Overlap of [1] abababaab=ba with [8] baba=baabcc:
Critical pair: abaabccbaab=ba.
Reduce LHS:
| [3] | (abaabc)cbaab |
| [4] | ⇒ ca(ababc)baab |
| [12] | ⇒ (caba)abbaab |
| [16] | ⇒ (caabccabba)ab |
| ⇒ ccccab |
Flip LHS and RHS.
Defines rule #3.
Referenced by [19], [20], [21], [22].
Overlap of [2] abaabab=c with [18] ba=ccccab:
Critical pair: accccababab=c.
Reduce LHS:
| [12] | accc(caba)bab |
| [13] | ⇒ ac(cccaabccba)b |
| [17] | ⇒ accc(caabcccc)ccabb |
| ⇒ acccccaabccabb |
Referenced by [22].
Overlap of [9] abacabaab=ca with [18] ba=ccccab:
Critical pair: accccabcabaab=ca.
Reduce LHS:
| [7] | accc(cabc)abaab |
| [12] | ⇒ accccc(caba)baab |
| [13] | ⇒ accc(cccaabccba)ab |
| [17] | ⇒ accccc(caabcccc)ccabab |
| [12] | ⇒ acccccccaabc(caba)b |
| [14] | ⇒ acccccc(caabccaabccb) |
| ⇒ acccccccc |
Defines rule #1.
Referenced by [22].
Overlap of [10] baabccabab=bc with [18] ba=ccccab:
Critical pair: ccccababccabab=bc.
Reduce LHS:
| [12] | ccc(caba)bccabab |
| [15] | ⇒ ccc(caabccbc)cabab |
| [18] | ⇒ cccc(ba)abcabab |
| [12] | ⇒ ccccccc(caba)bcabab |
| [15] | ⇒ ccccccc(caabccbc)abab |
| [18] | ⇒ cccccccc(ba)ababab |
| [12] | ⇒ ccccccccccc(caba)babab |
| [13] | ⇒ ccccccccc(cccaabccba)bab |
| [17] | ⇒ ccccccccccc(caabcccc)ccabbab |
| [16] | ⇒ cccccccccccc(caabccabba)b |
| ⇒ ccccccccccccccccb |
Flip LHS and RHS.
Defines rule #2.
Referenced by [22].
Simplify [19] acccccaabccabb=c.
Reduce LHS:
| [21] | acccccaa(bc)cabb |
| [20] | ⇒ accccca(acccccccc)ccccccccbcabb |
| [20] | ⇒ acccccac(acccccccc)bcabb |
| [7] | ⇒ acccccac(cabc)abb |
| [18] | ⇒ acccccacccca(ba)bb |
| ⇒ acccccaccccaccccabbb |
Defines rule #4.