| Back: | ⟨a, b | abaaabab=aab⟩ |
|---|
Completion settings:
Axiom: abaaabab=aab.
Referenced by [3].
Axiom: abaaaba=c.
Overlap of [1] abaaabab=aab with [2] abaaaba=c:
Critical pair: cb=aab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [4], [5], [6], [8].
Overlap of [2] abaaaba=c with [3] aab=cb:
Critical pair: abacba=c.
Defines rule #7.
Referenced by [5], [6], [7], [9], [10], [11], [13].
Overlap of [3] aab=cb with [4] abacba=c:
Critical pair: ac=cbacba.
Flip LHS and RHS.
Defines rule #9.
Referenced by [7], [11], [12].
Overlap of [4] abacba=c with [3] aab=cb:
Critical pair: abacbcb=cab.
Referenced by [14].
Overlap of [4] abacba=c with [4] abacba=c:
Critical pair: abacbc=cbacba.
Reduce RHS:
| [5] | (cbacba) |
| ⇒ ac |
Defines rule #8.
Referenced by [8], [9], [10], [14].
Overlap of [3] aab=cb with [7] abacbc=ac:
Critical pair: aac=cbacbc.
Flip LHS and RHS.
Overlap of [4] abacba=c with [7] abacbc=ac:
Critical pair: abacbac=cbacbc.
Reduce LHS:
| [4] | (abacba)c |
| ⇒ cc |
Reduce RHS:
| [8] | (cbacbc) |
| ⇒ aac |
Flip LHS and RHS.
Defines rule #1.
Referenced by [10], [11], [12], [15].
Overlap of [4] abacba=c with [9] aac=cc:
Critical pair: abacbcc=cac.
Reduce LHS:
| [7] | (abacbc)c |
| ⇒ acc |
Flip LHS and RHS.
Defines rule #2.
Overlap of [4] abacba=c with [5] cbacba=ac:
Critical pair: abaac=ccba.
Reduce LHS:
| [9] | ab(aac) |
| ⇒ abcc |
Flip LHS and RHS.
Defines rule #5.
Overlap of [9] aac=cc with [5] cbacba=ac:
Critical pair: aaac=ccbacba.
Reduce LHS:
| [9] | a(aac) |
| ⇒ acc |
Reduce RHS:
| [11] | (ccba)cba |
| [11] | ⇒ abc(ccba) |
| ⇒ abcabcc |
Flip LHS and RHS.
Referenced by [13].
Overlap of [11] ccba=abcc with [4] abacba=c:
Critical pair: ccbc=abccbacba.
Reduce RHS:
| [11] | ab(ccba)cba |
| [11] | ⇒ ababc(ccba) |
| [12] | ⇒ ab(abcabcc) |
| ⇒ abacc |
Defines rule #6.
Overlap of [6] abacbcb=cab with [7] abacbc=ac:
Critical pair: acb=cab.
Flip LHS and RHS.
Defines rule #4.
Simplify [8] cbacbc=aac.
Reduce RHS:
| [9] | (aac) |
| ⇒ cc |
Defines rule #10.