| Back: | ⟨a, b | ababbba=baba⟩ |
|---|
Completion settings:
Axiom: ababbba=baba.
Referenced by [5].
Axiom: bbbaba=c.
Referenced by [6].
Axiom: bb=d.
Defines rule #24.
Referenced by [5], [6], [7], [9], [11], [16], [19].
Axiom: badba=e.
Defines rule #26.
Referenced by [5], [11], [12], [13], [14], [16], [24].
Overlap of [1] ababbba=baba with [3] bb=d:
Critical pair: abadba=baba.
Reduce LHS:
| [4] | a(badba) |
| ⇒ ae |
Flip LHS and RHS.
Defines rule #25.
Referenced by [6], [9], [10], [13], [14], [19], [25].
Overlap of [2] bbbaba=c with [3] bb=d:
Critical pair: dbaba=c.
Reduce LHS:
| [5] | d(baba) |
| ⇒ dae |
Defines rule #7.
Referenced by [8], [13], [16], [17], [18], [19], [23], [25], [26], [27], [28], [29].
Overlap of [3] bb=d with [3] bb=d:
Critical pair: bd=db.
Defines rule #22.
Overlap of [7] bd=db with [6] dae=c:
Critical pair: bc=dbae.
Flip LHS and RHS.
Referenced by [17].
Overlap of [3] bb=d with [5] baba=ae:
Critical pair: bae=daba.
Overlap of [5] baba=ae with [5] baba=ae:
Critical pair: baae=aeba.
Defines rule #21.
Overlap of [3] bb=d with [4] badba=e:
Critical pair: be=dadba.
Defines rule #17.
Overlap of [4] badba=e with [4] badba=e:
Critical pair: bade=edba.
Defines rule #23.
Overlap of [4] badba=e with [5] baba=ae:
Critical pair: badae=eba.
Reduce LHS:
| [6] | ba(dae) |
| ⇒ bac |
Defines rule #20.
Overlap of [5] baba=ae with [4] badba=e:
Critical pair: bae=aedba.
Reduce LHS:
| [9] | (bae) |
| ⇒ daba |
Defines rule #15.
Referenced by [15].
Simplify [9] bae=daba.
Reduce RHS:
| [14] | (daba) |
| ⇒ aedba |
Defines rule #19.
Referenced by [16], [17], [19], [22].
Overlap of [3] bb=d with [15] bae=aedba:
Critical pair: baedba=dae.
Reduce LHS:
| [15] | (bae)dba |
| [4] | ⇒ aed(badba) |
| ⇒ aede |
Reduce RHS:
| [6] | (dae) |
| ⇒ c |
Defines rule #3.
Referenced by [18], [20], [21], [22], [30].
Overlap of [8] dbae=bc with [15] bae=aedba:
Critical pair: daedba=bc.
Reduce LHS:
| [6] | (dae)dba |
| ⇒ cdba |
Flip LHS and RHS.
Defines rule #18.
Overlap of [6] dae=c with [16] aede=c:
Critical pair: dc=cde.
Defines rule #6.
Overlap of [3] bb=d with [10] baae=aeba:
Critical pair: baeba=daae.
Reduce LHS:
| [15] | (bae)ba |
| [5] | ⇒ aed(baba) |
| [6] | ⇒ ae(dae) |
| ⇒ aec |
Flip LHS and RHS.
Defines rule #11.
Referenced by [21], [23], [27], [29].
Overlap of [10] baae=aeba with [16] aede=c:
Critical pair: bac=aebade.
Reduce LHS:
| [13] | (bac) |
| ⇒ eba |
Reduce RHS:
| [12] | ae(bade) |
| ⇒ aeedba |
Flip LHS and RHS.
Defines rule #13.
Referenced by [23], [24], [25].
Overlap of [19] daae=aec with [16] aede=c:
Critical pair: dac=aecde.
Defines rule #9.
Referenced by [22].
Overlap of [7] bd=db with [21] dac=aecde:
Critical pair: baecde=dbac.
Reduce LHS:
| [15] | (bae)cde |
| [13] | ⇒ aed(bac)de |
| [16] | ⇒ (aede)bade |
| [12] | ⇒ c(bade) |
| ⇒ cedba |
Reduce RHS:
| [13] | d(bac) |
| ⇒ deba |
Flip LHS and RHS.
Defines rule #16.
Overlap of [19] daae=aec with [20] aeedba=eba:
Critical pair: daeba=aecedba.
Reduce LHS:
| [6] | (dae)ba |
| ⇒ cba |
Flip LHS and RHS.
Defines rule #14.
Overlap of [20] aeedba=eba with [4] badba=e:
Critical pair: aeede=ebadba.
Reduce RHS:
| [4] | e(badba) |
| ⇒ ee |
Defines rule #4.
Overlap of [20] aeedba=eba with [5] baba=ae:
Critical pair: aeedae=ebaba.
Reduce LHS:
| [6] | aee(dae) |
| ⇒ aeec |
Reduce RHS:
| [5] | e(baba) |
| ⇒ eae |
Defines rule #1.
Overlap of [6] dae=c with [25] aeec=eae:
Critical pair: deae=cec.
Defines rule #12.
Referenced by [30].
Overlap of [19] daae=aec with [25] aeec=eae:
Critical pair: daeae=aecec.
Reduce LHS:
| [6] | (dae)ae |
| ⇒ cae |
Flip LHS and RHS.
Defines rule #2.
Overlap of [6] dae=c with [24] aeede=ee:
Critical pair: dee=cede.
Defines rule #8.
Overlap of [19] daae=aec with [24] aeede=ee:
Critical pair: daee=aecede.
Reduce LHS:
| [6] | (dae)e |
| ⇒ ce |
Flip LHS and RHS.
Defines rule #5.
Overlap of [26] deae=cec with [16] aede=c:
Critical pair: dec=cecde.
Defines rule #10.