| Back: | ⟨a, b | aabababba=ab⟩ |
|---|
Completion settings:
Axiom: aabababba=ab.
Referenced by [3].
Axiom: bababba=c.
Overlap of [1] aabababba=ab with [2] bababba=c:
Critical pair: aac=ab.
Flip LHS and RHS.
Defines rule #11.
Overlap of [2] bababba=c with [3] ab=aac:
Critical pair: baacabba=c.
Reduce LHS:
| [3] | baac(ab)ba |
| ⇒ baacaacba |
Referenced by [5], [6], [7], [13].
Overlap of [3] ab=aac with [4] baacaacba=c:
Critical pair: ac=aacaacaacba.
Flip LHS and RHS.
Referenced by [8].
Overlap of [4] baacaacba=c with [3] ab=aac:
Critical pair: baacaacbaac=cb.
Reduce LHS:
| [4] | (baacaacba)ac |
| ⇒ cac |
Flip LHS and RHS.
Defines rule #10.
Referenced by [7], [8], [12], [13], [14].
Overlap of [4] baacaacba=c with [4] baacaacba=c:
Critical pair: baacaacc=cacaacba.
Reduce RHS:
| [6] | cacaa(cb)a |
| ⇒ cacaacaca |
Defines rule #7.
Referenced by [12].
Simplify [5] aacaacaacba=ac.
Reduce LHS:
| [6] | aacaacaa(cb)a |
| ⇒ aacaacaacaca |
Defines rule #6.
Referenced by [9], [10], [11].
Overlap of [8] aacaacaacaca=ac with [8] aacaacaacaca=ac:
Critical pair: aacaacaacacac=acacaacaacaca.
Reduce LHS:
| [8] | (aacaacaacaca)c |
| ⇒ acc |
Flip LHS and RHS.
Referenced by [10], [11], [15], [16].
Overlap of [8] aacaacaacaca=ac with [9] acacaacaacaca=acc:
Critical pair: aacaacaacc=acacaacaca.
Defines rule #2.
Overlap of [8] aacaacaacaca=ac with [9] acacaacaacaca=acc:
Critical pair: aacaacaacacc=accaacaacaca.
Defines rule #5.
Overlap of [6] cb=cac with [7] baacaacc=cacaacaca:
Critical pair: ccacaacaca=cacaacaacc.
Flip LHS and RHS.
Defines rule #1.
Overlap of [4] baacaacba=c with [6] cb=cac:
Critical pair: baacaacaca=c.
Defines rule #9.
Overlap of [6] cb=cac with [13] baacaacaca=c:
Critical pair: cc=cacaacaacaca.
Flip LHS and RHS.
Defines rule #4.
Referenced by [16].
Overlap of [13] baacaacaca=c with [9] acacaacaacaca=acc:
Critical pair: baacaacacc=ccaacaacaca.
Defines rule #8.
Overlap of [14] cacaacaacaca=cc with [9] acacaacaacaca=acc:
Critical pair: cacaacaacacc=cccaacaacaca.
Defines rule #3.