| Back: | ⟨a, b | aaa=1, babbbb=a⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #3.
Referenced by [4], [6], [9], [10], [11], [15], [16], [19], [21], [22], [36].
Axiom: babbbb=a.
Referenced by [3], [5], [7], [8], [11], [18], [21], [23], [24], [25], [26], [27], [28], [29], [30], [31], [32], [33], [34], [35].
Overlap of [2] babbbb=a with [2] babbbb=a:
Critical pair: babbba=aabbbb.
Overlap of [3] babbba=aabbbb with [1] aaa=1:
Critical pair: babbb=aabbbbaa.
Flip LHS and RHS.
Referenced by [6].
Overlap of [3] babbba=aabbbb with [2] babbbb=a:
Critical pair: babba=aabbbbbbbb.
Overlap of [1] aaa=1 with [4] aabbbbaa=babbb:
Critical pair: ababbb=bbbbaa.
Flip LHS and RHS.
Overlap of [2] babbbb=a with [6] bbbbaa=ababbb:
Critical pair: babababbb=abaa.
Referenced by [8].
Overlap of [7] babababbb=abaa with [2] babbbb=a:
Critical pair: babaa=abaab.
Referenced by [9], [12], [14], [17].
Overlap of [8] babaa=abaab with [1] aaa=1:
Critical pair: bab=abaaba.
Flip LHS and RHS.
Referenced by [10], [11], [12], [13].
Overlap of [1] aaa=1 with [9] abaaba=bab:
Critical pair: aabab=baaba.
Flip LHS and RHS.
Referenced by [15].
Overlap of [6] bbbbaa=ababbb with [9] abaaba=bab:
Critical pair: bbbbabab=ababbbbaaba.
Reduce RHS:
| [2] | a(babbbb)aaba |
| [1] | ⇒ (aaa)aba |
| ⇒ aba |
Referenced by [21].
Overlap of [8] babaa=abaab with [9] abaaba=bab:
Critical pair: bbab=abaabba.
Flip LHS and RHS.
Referenced by [14].
Overlap of [9] abaaba=bab with [9] abaaba=bab:
Critical pair: ababab=bababa.
Flip LHS and RHS.
Referenced by [15].
Overlap of [8] babaa=abaab with [12] abaabba=bbab:
Critical pair: bbbab=abaabbba.
Flip LHS and RHS.
Overlap of [10] baaba=aabab with [13] bababa=ababab:
Critical pair: baaababab=aababbaba.
Reduce LHS:
| [1] | b(aaa)babab |
| ⇒ bbabab |
Reduce RHS:
| [5] | aa(babba)ba |
| [1] | ⇒ (aaa)abbbbbbbbba |
| ⇒ abbbbbbbbba |
Referenced by [20].
Overlap of [1] aaa=1 with [14] abaabbba=bbbab:
Critical pair: aabbbab=baabbba.
Flip LHS and RHS.
Referenced by [21].
Overlap of [8] babaa=abaab with [14] abaabbba=bbbab:
Critical pair: bbbbab=abaabbbba.
Flip LHS and RHS.
Referenced by [19].
Overlap of [5] babba=aabbbbbbbb with [2] babbbb=a:
Critical pair: baba=aabbbbbbbbbbbb.
Referenced by [20].
Overlap of [1] aaa=1 with [17] abaabbbba=bbbbab:
Critical pair: aabbbbab=baabbbba.
Flip LHS and RHS.
Referenced by [21].
Simplify [15] bbabab=abbbbbbbbba.
Reduce LHS:
| [18] | b(baba)b |
| ⇒ baabbbbbbbbbbbbb |
Referenced by [21].
Overlap of [20] baabbbbbbbbbbbbb=abbbbbbbbba with [16] baabbba=aabbbab:
Critical pair: baabbbbbbbbbbbbaabbbab=abbbbbbbbbaaabbba.
Reduce LHS:
| [16] | baabbbbbbbbbbb(baabbba)b |
| [16] | ⇒ baabbbbbbbbbb(baabbba)bb |
| [16] | ⇒ baabbbbbbbbb(baabbba)bbb |
| [16] | ⇒ baabbbbbbbb(baabbba)bbbb |
| [16] | ⇒ baabbbbbbb(baabbba)bbbbb |
| [16] | ⇒ baabbbbbb(baabbba)bbbbbb |
| [16] | ⇒ baabbbbb(baabbba)bbbbbbb |
| [16] | ⇒ baabbbb(baabbba)bbbbbbbb |
| [19] | ⇒ (baabbbba)abbbabbbbbbbbb |
| [11] | ⇒ aa(bbbbabab)bbabbbbbbbbb |
| [1] | ⇒ (aaa)babbabbbbbbbbb |
| [2] | ⇒ bab(babbbb)bbbbb |
| [2] | ⇒ ba(babbbb)b |
| ⇒ baab |
Reduce RHS:
| [1] | abbbbbbbbb(aaa)bbba |
| ⇒ abbbbbbbbbbbba |
Referenced by [22].
Overlap of [21] baab=abbbbbbbbbbbba with [21] baab=abbbbbbbbbbbba:
Critical pair: baaabbbbbbbbbbbba=abbbbbbbbbbbbaaab.
Reduce LHS:
| [1] | b(aaa)bbbbbbbbbbbba |
| ⇒ bbbbbbbbbbbbba |
Reduce RHS:
| [1] | abbbbbbbbbbbb(aaa)b |
| ⇒ abbbbbbbbbbbbb |
Referenced by [23].
Overlap of [22] bbbbbbbbbbbbba=abbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbbbbbbba=abbbbbbbbbbbbbbbbb.
Referenced by [24].
Overlap of [23] bbbbbbbbbbbba=abbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbbbbbba=abbbbbbbbbbbbbbbbbbbbb.
Referenced by [25].
Overlap of [24] bbbbbbbbbbba=abbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [26].
Overlap of [25] bbbbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [27].
Overlap of [26] bbbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [28].
Overlap of [27] bbbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [29].
Overlap of [28] bbbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [30].
Overlap of [29] bbbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [31].
Overlap of [30] bbbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [32].
Overlap of [31] bbbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [33].
Overlap of [32] bbba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: bba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Referenced by [34].
Overlap of [33] bba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb with [2] babbbb=a:
Critical pair: ba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Defines rule #2.
Referenced by [35].
Overlap of [2] babbbb=a with [34] ba=abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb:
Critical pair: abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a.
Referenced by [36].
Overlap of [1] aaa=1 with [35] abbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=a:
Critical pair: aaa=bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aaa) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #1.