| Back: | ⟨a, b | aaa=a, babbbb=a⟩ |
|---|
Completion settings:
Axiom: aaa=a.
Defines rule #3.
Referenced by [4], [6], [9], [10], [13], [14], [16], [18], [22], [25], [26], [28].
Axiom: babbbb=a.
Referenced by [3], [5], [7], [8], [9], [12], [24], [25], [30], [31], [32], [33].
Overlap of [2] babbbb=a with [2] babbbb=a:
Critical pair: babbba=aabbbb.
Overlap of [3] babbba=aabbbb with [1] aaa=a:
Critical pair: babbba=aabbbbaa.
Reduce LHS:
| [3] | (babbba) |
| ⇒ aabbbb |
Flip LHS and RHS.
Referenced by [6].
Overlap of [3] babbba=aabbbb with [2] babbbb=a:
Critical pair: babba=aabbbbbbbb.
Referenced by [7].
Overlap of [1] aaa=a with [4] aabbbbaa=aabbbb:
Critical pair: aaabbbb=abbbbaa.
Reduce LHS:
| [1] | (aaa)bbbb |
| ⇒ abbbb |
Flip LHS and RHS.
Referenced by [11].
Overlap of [5] babba=aabbbbbbbb with [2] babbbb=a:
Critical pair: baba=aabbbbbbbbbbbb.
Overlap of [7] baba=aabbbbbbbbbbbb with [2] babbbb=a:
Critical pair: baa=aabbbbbbbbbbbbbbbb.
Referenced by [12], [13], [15], [17], [19], [20], [21], [23], [24], [25], [27].
Overlap of [7] baba=aabbbbbbbbbbbb with [3] babbba=aabbbb:
Critical pair: baaabbbb=aabbbbbbbbbbbbbbba.
Reduce LHS:
| [1] | b(aaa)bbbb |
| [2] | ⇒ (babbbb) |
| ⇒ a |
Flip LHS and RHS.
Overlap of [1] aaa=a with [9] aabbbbbbbbbbbbbbba=a:
Critical pair: aa=abbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [12].
Overlap of [6] abbbbaa=abbbb with [9] aabbbbbbbbbbbbbbba=a:
Critical pair: abbbba=abbbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [20].
Overlap of [2] babbbb=a with [10] abbbbbbbbbbbbbbba=aa:
Critical pair: baa=abbbbbbbbbbba.
Reduce LHS:
| [8] | (baa) |
| ⇒ aabbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [1] aaa=a:
Critical pair: ba=aabbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [14].
Overlap of [1] aaa=a with [13] aabbbbbbbbbbbbbbbba=ba:
Critical pair: aaba=aabbbbbbbbbbbbbbbba.
Reduce RHS:
| [13] | (aabbbbbbbbbbbbbbbba) |
| ⇒ ba |
Referenced by [15].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [14] aaba=ba:
Critical pair: bba=aabbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [16].
Overlap of [1] aaa=a with [15] aabbbbbbbbbbbbbbbbba=bba:
Critical pair: aabba=aabbbbbbbbbbbbbbbbba.
Reduce RHS:
| [15] | (aabbbbbbbbbbbbbbbbba) |
| ⇒ bba |
Referenced by [17].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [16] aabba=bba:
Critical pair: bbba=aabbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Overlap of [1] aaa=a with [17] aabbbbbbbbbbbbbbbbbba=bbba:
Critical pair: aabbba=aabbbbbbbbbbbbbbbbbba.
Reduce RHS:
| [17] | (aabbbbbbbbbbbbbbbbbba) |
| ⇒ bbba |
Referenced by [20].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [17] aabbbbbbbbbbbbbbbbbba=bbba:
Critical pair: bbbba=aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [29].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [18] aabbba=bbba:
Critical pair: bbbba=aabbbbbbbbbbbbbbbbbbba.
Reduce RHS:
| [11] | a(abbbbbbbbbbbbbbbbbbba) |
| ⇒ aabbbba |
Flip LHS and RHS.
Referenced by [21].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [20] aabbbba=bbbba:
Critical pair: bbbbba=aabbbbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [22].
Overlap of [1] aaa=a with [21] aabbbbbbbbbbbbbbbbbbbba=bbbbba:
Critical pair: aabbbbba=aabbbbbbbbbbbbbbbbbbbba.
Reduce RHS:
| [21] | (aabbbbbbbbbbbbbbbbbbbba) |
| ⇒ bbbbba |
Referenced by [23].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [22] aabbbbba=bbbbba:
Critical pair: bbbbbba=aabbbbbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [26].
Overlap of [2] babbbb=a with [12] abbbbbbbbbbba=aabbbbbbbbbbbbbbbb:
Critical pair: baabbbbbbbbbbbbbbbb=abbbbbbba.
Reduce LHS:
| [8] | (baa)bbbbbbbbbbbbbbbb |
| ⇒ aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [28].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [12] abbbbbbbbbbba=aabbbbbbbbbbbbbbbb:
Critical pair: baaabbbbbbbbbbbbbbbb=aabbbbbbbbbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [1] | b(aaa)bbbbbbbbbbbbbbbb |
| [2] | ⇒ (babbbb)bbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [29].
Overlap of [1] aaa=a with [23] aabbbbbbbbbbbbbbbbbbbbba=bbbbbba:
Critical pair: aabbbbbba=aabbbbbbbbbbbbbbbbbbbbba.
Reduce RHS:
| [23] | (aabbbbbbbbbbbbbbbbbbbbba) |
| ⇒ bbbbbba |
Referenced by [27].
Overlap of [8] baa=aabbbbbbbbbbbbbbbb with [26] aabbbbbba=bbbbbba:
Critical pair: bbbbbbba=aabbbbbbbbbbbbbbbbbbbbbba.
Flip LHS and RHS.
Referenced by [28].
Overlap of [1] aaa=a with [27] aabbbbbbbbbbbbbbbbbbbbbba=bbbbbbba:
Critical pair: aabbbbbbba=aabbbbbbbbbbbbbbbbbbbbbba.
Reduce LHS:
| [24] | a(abbbbbbba) |
| [1] | ⇒ (aaa)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
Reduce RHS:
| [27] | (aabbbbbbbbbbbbbbbbbbbbbba) |
| ⇒ bbbbbbba |
Flip LHS and RHS.
Referenced by [29].
Simplify [19] aabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbba=bbbba.
Reduce LHS:
| [28] | aabbbbbbbbbbbbbbbbbbbbbbbbbbb(bbbbbbba) |
| [25] | ⇒ (aabbbbbbbbbbbbbbbbbbbbbbbbbbba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [30].
Overlap of [29] bbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [31].
Overlap of [30] bbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [32].
Overlap of [31] bba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: ba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Defines rule #2.
Referenced by [33].
Overlap of [2] babbbb=a with [32] ba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:
Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a.
Defines rule #1.