| Back: | ⟨a, b | aaa=a, baabbb=a⟩ |
|---|
Completion settings:
Axiom: aaa=a.
Referenced by [3], [4], [5], [11], [12], [13], [14], [17].
Axiom: baabbb=a.
Referenced by [3], [4], [6], [8], [11], [14], [15], [19], [22].
Overlap of [2] baabbb=a with [2] baabbb=a:
Critical pair: baabba=aaabbb.
Reduce RHS:
| [1] | (aaa)bbb |
| ⇒ abbb |
Referenced by [4], [5], [6], [7], [16], [26].
Overlap of [2] baabbb=a with [3] baabba=abbb:
Critical pair: baabbabbb=aaabba.
Reduce LHS:
| [3] | (baabba)bbb |
| ⇒ abbbbbb |
Reduce RHS:
| [1] | (aaa)bba |
| ⇒ abba |
Flip LHS and RHS.
Referenced by [7], [8], [9], [10], [18], [26].
Overlap of [3] baabba=abbb with [1] aaa=a:
Critical pair: baabba=abbbaa.
Reduce LHS:
| [3] | (baabba) |
| ⇒ abbb |
Flip LHS and RHS.
Overlap of [3] baabba=abbb with [2] baabbb=a:
Critical pair: baaba=abbbabbb.
Referenced by [9], [10], [11], [12], [16], [17], [20], [23].
Overlap of [5] abbbaa=abbb with [3] baabba=abbb:
Critical pair: abbabbb=abbbbba.
Reduce LHS:
| [4] | (abba)bbb |
| ⇒ abbbbbbbbb |
Flip LHS and RHS.
Referenced by [25].
Overlap of [4] abba=abbbbbb with [2] baabbb=a:
Critical pair: aba=abbbbbbabbb.
Flip LHS and RHS.
Referenced by [14], [21], [24].
Overlap of [4] abba=abbbbbb with [6] baaba=abbbabbb:
Critical pair: ababbbabbb=abbbbbbaba.
Flip LHS and RHS.
Referenced by [27].
Overlap of [5] abbbaa=abbb with [6] baaba=abbbabbb:
Critical pair: abbabbbabbb=abbbba.
Reduce LHS:
| [4] | (abba)bbbabbb |
| ⇒ abbbbbbbbbabbb |
Referenced by [29].
Overlap of [6] baaba=abbbabbb with [2] baabbb=a:
Critical pair: baaa=abbbabbbabbb.
Reduce LHS:
| [1] | b(aaa) |
| ⇒ ba |
Flip LHS and RHS.
Referenced by [13], [14], [15], [18], [25].
Overlap of [6] baaba=abbbabbb with [6] baaba=abbbabbb:
Critical pair: baaabbbabbb=abbbabbbaba.
Reduce LHS:
| [1] | b(aaa)bbbabbb |
| ⇒ babbbabbb |
Flip LHS and RHS.
Referenced by [16].
Overlap of [1] aaa=a with [11] abbbabbbabbb=ba:
Critical pair: aaba=abbbabbbabbb.
Reduce RHS:
| [11] | (abbbabbbabbb) |
| ⇒ ba |
Referenced by [16], [17], [18], [23].
Overlap of [8] abbbbbbabbb=aba with [11] abbbabbbabbb=ba:
Critical pair: abbbbbbba=abaabbbabbb.
Reduce RHS:
| [2] | a(baabbb)abbb |
| [1] | ⇒ (aaa)bbb |
| ⇒ abbb |
Referenced by [30].
Overlap of [11] abbbabbbabbb=ba with [11] abbbabbbabbb=ba:
Critical pair: abbbba=baabbb.
Reduce RHS:
| [2] | (baabbb) |
| ⇒ a |
Referenced by [19], [20], [21], [22], [23], [24], [25], [29].
Overlap of [6] baaba=abbbabbb with [13] aaba=ba:
Critical pair: baabba=abbbabbbaba.
Reduce LHS:
| [3] | (baabba) |
| ⇒ abbb |
Reduce RHS:
| [12] | (abbbabbbaba) |
| ⇒ babbbabbb |
Flip LHS and RHS.
Referenced by [18].
Overlap of [13] aaba=ba with [6] baaba=abbbabbb:
Critical pair: aaabbbabbb=baaba.
Reduce LHS:
| [1] | (aaa)bbbabbb |
| ⇒ abbbabbb |
Reduce RHS:
| [13] | b(aaba) |
| ⇒ bba |
Overlap of [13] aaba=ba with [11] abbbabbbabbb=ba:
Critical pair: aabba=babbbabbbabbb.
Reduce LHS:
| [4] | a(abba) |
| ⇒ aabbbbbb |
Reduce RHS:
| [16] | (babbbabbb)abbb |
| [17] | ⇒ (abbbabbb) |
| ⇒ bba |
Referenced by [23], [25], [26], [27].
Overlap of [2] baabbb=a with [15] abbbba=a:
Critical pair: baa=aba.
Referenced by [20], [23], [25].
Overlap of [6] baaba=abbbabbb with [15] abbbba=a:
Critical pair: baaba=abbbabbbbbbba.
Reduce LHS:
| [19] | (baa)ba |
| ⇒ ababa |
Reduce RHS:
| [17] | (abbbabbb)bbbba |
| [15] | ⇒ bb(abbbba) |
| ⇒ bba |
Referenced by [21].
Overlap of [8] abbbbbbabbb=aba with [15] abbbba=a:
Critical pair: abbbbbba=ababa.
Reduce RHS:
| [20] | (ababa) |
| ⇒ bba |
Overlap of [15] abbbba=a with [2] baabbb=a:
Critical pair: abbba=aabbb.
Referenced by [23], [25], [27].
Overlap of [15] abbbba=a with [6] baaba=abbbabbb:
Critical pair: abbbabbbabbb=aaba.
Reduce LHS:
| [22] | (abbba)bbbabbb |
| [18] | ⇒ (aabbbbbb)abbb |
| [19] | ⇒ b(baa)bbb |
| ⇒ bababbb |
Reduce RHS:
| [13] | (aaba) |
| ⇒ ba |
Referenced by [25].
Overlap of [15] abbbba=a with [8] abbbbbbabbb=aba:
Critical pair: abbbbaba=abbbbbbabbb.
Reduce LHS:
| [15] | (abbbba)ba |
| ⇒ aba |
Reduce RHS:
| [21] | (abbbbbba)bbb |
| ⇒ bbabbb |
Referenced by [28].
Overlap of [15] abbbba=a with [11] abbbabbbabbb=ba:
Critical pair: abbbbba=abbbabbbabbb.
Reduce LHS:
| [7] | (abbbbba) |
| ⇒ abbbbbbbbb |
Reduce RHS:
| [22] | (abbba)bbbabbb |
| [18] | ⇒ (aabbbbbb)abbb |
| [19] | ⇒ b(baa)bbb |
| [23] | ⇒ (bababbb) |
| ⇒ ba |
Flip LHS and RHS.
Defines rule #2.
Referenced by [26], [28], [30].
Overlap of [3] baabba=abbb with [4] abba=abbbbbb:
Critical pair: baabbbbbb=abbb.
Reduce LHS:
| [18] | b(aabbbbbb) |
| [25] | ⇒ bb(ba) |
| [25] | ⇒ b(ba)bbbbbbbbb |
| [25] | ⇒ (ba)bbbbbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbbbbbbbbbbbbbbb |
Referenced by [28].
Simplify [9] abbbbbbaba=ababbbabbb.
Reduce RHS:
| [22] | ab(abbba)bbb |
| [18] | ⇒ ab(aabbbbbb) |
| [22] | ⇒ (abbba) |
| ⇒ aabbb |
Referenced by [28].
Overlap of [27] abbbbbbaba=aabbb with [21] abbbbbba=bba:
Critical pair: bbaba=aabbb.
Reduce LHS:
| [24] | bb(aba) |
| [25] | ⇒ bbb(ba)bbb |
| [25] | ⇒ bb(ba)bbbbbbbbbbbb |
| [25] | ⇒ b(ba)bbbbbbbbbbbbbbbbbbbbb |
| [26] | ⇒ b(abbbbbbbbbbbbbbbbbbbbbbbbbbb)bbb |
| [25] | ⇒ (ba)bbbbbb |
| ⇒ abbbbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [31].
Simplify [10] abbbbbbbbbabbb=abbbba.
Reduce RHS:
| [15] | (abbbba) |
| ⇒ a |
Referenced by [30].
Overlap of [29] abbbbbbbbbabbb=a with [25] ba=abbbbbbbbb:
Critical pair: abbbbbbbbabbbbbbbbbbbb=a.
Reduce LHS:
| [25] | abbbbbbb(ba)bbbbbbbbbbbb |
| [14] | ⇒ (abbbbbbba)bbbbbbbbbbbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbbbbbbbbbbbbbb |
Defines rule #1.
Referenced by [31].
Overlap of [28] aabbb=abbbbbbbbbbbbbbb with [30] abbbbbbbbbbbbbbbbbbbbbbbb=a:
Critical pair: aa=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Reduce RHS:
| [30] | (abbbbbbbbbbbbbbbbbbbbbbbb)bbbbbbbbbbbb |
| ⇒ abbbbbbbbbbbb |
Defines rule #3.