| Back: | ⟨a, b | aaa=1, bbabbbb=a⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #3.
Referenced by [4], [5], [12], [13], [14].
Axiom: bbabbbb=a.
Referenced by [3], [6], [8], [9].
Overlap of [2] bbabbbb=a with [2] bbabbbb=a:
Critical pair: bbabba=aabbbb.
Flip LHS and RHS.
Referenced by [4], [10], [12].
Overlap of [1] aaa=1 with [3] aabbbb=bbabba:
Critical pair: abbabba=bbbb.
Overlap of [4] abbabba=bbbb with [1] aaa=1:
Critical pair: abbabb=bbbbaa.
Overlap of [4] abbabba=bbbb with [2] bbabbbb=a:
Critical pair: abbaa=bbbbbbbb.
Overlap of [4] abbabba=bbbb with [4] abbabba=bbbb:
Critical pair: abbbbbb=bbbbbba.
Referenced by [11].
Overlap of [5] abbabb=bbbbaa with [2] bbabbbb=a:
Critical pair: aa=bbbbaabb.
Flip LHS and RHS.
Referenced by [9], [10], [14].
Overlap of [2] bbabbbb=a with [8] bbbbaabb=aa:
Critical pair: bbabaa=abaabb.
Flip LHS and RHS.
Referenced by [11].
Overlap of [8] bbbbaabb=aa with [3] aabbbb=bbabba:
Critical pair: bbbbbbabba=aabb.
Flip LHS and RHS.
Simplify [9] abaabb=bbabaa.
Reduce LHS:
| [10] | ab(aabb) |
| [7] | ⇒ (abbbbbb)babba |
| ⇒ bbbbbbababba |
Referenced by [12].
Overlap of [3] aabbbb=bbabba with [11] bbbbbbababba=bbabaa:
Critical pair: aabbabaa=bbabbabbababba.
Reduce LHS:
| [10] | (aabb)abaa |
| [6] | ⇒ bbbbbb(abbaa)baa |
| ⇒ bbbbbbbbbbbbbbbaa |
Reduce RHS:
| [5] | bb(abbabb)ababba |
| [1] | ⇒ bbbbbb(aaa)babba |
| ⇒ bbbbbbbabba |
Flip LHS and RHS.
Referenced by [14].
Overlap of [6] abbaa=bbbbbbbb with [1] aaa=1:
Critical pair: abb=bbbbbbbba.
Defines rule #2.
Referenced by [14].
Overlap of [13] abb=bbbbbbbba with [8] bbbbaabb=aa:
Critical pair: aaa=bbbbbbbbabbaabb.
Reduce LHS:
| [1] | (aaa) |
| ⇒ 1 |
Reduce RHS:
| [12] | b(bbbbbbbabba)abb |
| [1] | ⇒ bbbbbbbbbbbbbbbb(aaa)bb |
| ⇒ bbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #1.