| Back: | ⟨a, b | aaa=a, bab=a⟩ |
|---|
Completion settings:
Axiom: aaa=a.
Defines rule #2.
Referenced by [4], [13], [15].
Axiom: bab=a.
Axiom: abb=c.
Referenced by [4], [5], [6], [7].
Overlap of [1] aaa=a with [3] abb=c:
Critical pair: aac=abb.
Reduce RHS:
| [3] | (abb) |
| ⇒ c |
Defines rule #3.
Referenced by [9].
Overlap of [2] bab=a with [3] abb=c:
Critical pair: bc=ab.
Flip LHS and RHS.
Defines rule #5.
Referenced by [6], [7], [8], [10].
Overlap of [3] abb=c with [2] bab=a:
Critical pair: aba=cab.
Reduce LHS:
| [5] | (ab)a |
| ⇒ bca |
Reduce RHS:
| [5] | c(ab) |
| ⇒ cbc |
Flip LHS and RHS.
Referenced by [10].
Overlap of [3] abb=c with [5] ab=bc:
Critical pair: bcb=c.
Overlap of [5] ab=bc with [2] bab=a:
Critical pair: aa=bcab.
Reduce RHS:
| [5] | bc(ab) |
| [7] | ⇒ (bcb)c |
| ⇒ cc |
Flip LHS and RHS.
Defines rule #1.
Referenced by [9], [12], [14].
Overlap of [8] cc=aa with [8] cc=aa:
Critical pair: caa=aac.
Reduce RHS:
| [4] | (aac) |
| ⇒ c |
Defines rule #4.
Referenced by [10], [12], [13].
Overlap of [9] caa=c with [5] ab=bc:
Critical pair: cabc=cb.
Reduce LHS:
| [5] | c(ab)c |
| [6] | ⇒ (cbc)c |
| ⇒ bcac |
Flip LHS and RHS.
Defines rule #6.
Referenced by [11].
Simplify [7] bcb=c.
Reduce LHS:
| [10] | b(cb) |
| ⇒ bbcac |
Referenced by [12].
Overlap of [11] bbcac=c with [8] cc=aa:
Critical pair: bbcaaa=cc.
Reduce LHS:
| [9] | bb(caa)a |
| ⇒ bbca |
Reduce RHS:
| [8] | (cc) |
| ⇒ aa |
Referenced by [13].
Overlap of [12] bbca=aa with [9] caa=c:
Critical pair: bbc=aaa.
Reduce RHS:
| [1] | (aaa) |
| ⇒ a |
Defines rule #8.
Referenced by [14].
Overlap of [13] bbc=a with [8] cc=aa:
Critical pair: bbaa=ac.
Referenced by [15].
Overlap of [14] bbaa=ac with [1] aaa=a:
Critical pair: bba=aca.
Defines rule #7.