| Back: | ⟨a, b | aabbabbaa=a⟩ |
|---|
Completion settings:
Axiom: aabbabbaa=a.
Referenced by [3].
Axiom: aa=c.
Defines rule #1.
Referenced by [3], [4], [6], [9], [10], [11], [12].
Overlap of [1] aabbabbaa=a with [2] aa=c:
Critical pair: cbbabbaa=a.
Reduce LHS:
| [2] | cbbabb(aa) |
| ⇒ cbbabbc |
Defines rule #8.
Referenced by [5], [6], [7], [9], [10].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #2.
Referenced by [6], [7], [10], [11].
Overlap of [3] cbbabbc=a with [3] cbbabbc=a:
Critical pair: cbbabba=abbabbc.
Defines rule #7.
Overlap of [3] cbbabbc=a with [4] ca=ac:
Critical pair: cbbabbac=aa.
Reduce LHS:
| [5] | (cbbabba)c |
| ⇒ abbabbcc |
Reduce RHS:
| [2] | (aa) |
| ⇒ c |
Referenced by [7].
Overlap of [6] abbabbcc=c with [3] cbbabbc=a:
Critical pair: abbabbca=cbbabbc.
Reduce LHS:
| [4] | abbabb(ca) |
| ⇒ abbabbac |
Reduce RHS:
| [3] | (cbbabbc) |
| ⇒ a |
Referenced by [8].
Overlap of [5] cbbabba=abbabbc with [7] abbabbac=a:
Critical pair: cbba=abbabbcbbac.
Flip LHS and RHS.
Overlap of [2] aa=c with [8] abbabbcbbac=cbba:
Critical pair: acbba=cbbabbcbbac.
Reduce RHS:
| [3] | (cbbabbc)bbac |
| ⇒ abbac |
Flip LHS and RHS.
Defines rule #3.
Referenced by [11].
Overlap of [4] ca=ac with [8] abbabbcbbac=cbba:
Critical pair: ccbba=acbbabbcbbac.
Reduce RHS:
| [3] | a(cbbabbc)bbac |
| [2] | ⇒ (aa)bbac |
| ⇒ cbbac |
Flip LHS and RHS.
Defines rule #5.
Overlap of [9] abbac=acbba with [4] ca=ac:
Critical pair: abbaac=acbbaa.
Reduce LHS:
| [2] | abb(aa)c |
| ⇒ abbcc |
Reduce RHS:
| [2] | acbb(aa) |
| ⇒ acbbc |
Defines rule #4.
Referenced by [12].
Overlap of [2] aa=c with [11] abbcc=acbbc:
Critical pair: aacbbc=cbbcc.
Reduce LHS:
| [2] | (aa)cbbc |
| ⇒ ccbbc |
Flip LHS and RHS.
Defines rule #6.