| Back: | ⟨a, b | aabbbaaab=ba⟩ |
|---|
Completion settings:
Axiom: aabbbaaab=ba.
Referenced by [4].
Axiom: abbba=c.
Axiom: aab=d.
Defines rule #7.
Referenced by [4], [5], [7], [9].
Overlap of [1] aabbbaaab=ba with [3] aab=d:
Critical pair: dbbaaab=ba.
Reduce LHS:
| [3] | dbba(aab) |
| ⇒ dbbad |
Referenced by [6].
Overlap of [3] aab=d with [2] abbba=c:
Critical pair: ac=dbba.
Flip LHS and RHS.
Referenced by [6], [8], [10], [12].
Simplify [4] dbbad=ba.
Reduce LHS:
| [5] | (dbba)d |
| ⇒ acd |
Flip LHS and RHS.
Defines rule #10.
Referenced by [7], [8], [9], [10], [11], [12].
Overlap of [3] aab=d with [6] ba=acd:
Critical pair: aaacd=da.
Defines rule #2.
Referenced by [10].
Overlap of [6] ba=acd with [2] abbba=c:
Critical pair: bc=acdbbba.
Reduce RHS:
| [6] | acdbb(ba) |
| [5] | ⇒ ac(dbba)cd |
| ⇒ acaccd |
Defines rule #9.
Overlap of [6] ba=acd with [3] aab=d:
Critical pair: bd=acdab.
Defines rule #8.
Overlap of [7] aaacd=da with [5] dbba=ac:
Critical pair: aaacac=dabba.
Reduce RHS:
| [6] | dab(ba) |
| [6] | ⇒ da(ba)cd |
| ⇒ daacdcd |
Defines rule #5.
Overlap of [2] abbba=c with [6] ba=acd:
Critical pair: abbacd=c.
Reduce LHS:
| [6] | ab(ba)cd |
| [6] | ⇒ a(ba)cdcd |
| ⇒ aacdcdcd |
Defines rule #3.
Referenced by [14].
Overlap of [5] dbba=ac with [6] ba=acd:
Critical pair: dbacd=ac.
Reduce LHS:
| [6] | d(ba)cd |
| ⇒ dacdcd |
Defines rule #1.
Overlap of [12] dacdcd=ac with [12] dacdcd=ac:
Critical pair: dacdcac=acacdcd.
Defines rule #4.
Overlap of [11] aacdcdcd=c with [12] dacdcd=ac:
Critical pair: aacdcdcac=cacdcd.
Defines rule #6.