| Back: | ⟨a, b | aba=bb, aaaaa=a⟩ |
|---|
Completion settings:
Axiom: aba=bb.
Defines rule #4.
Referenced by [3], [4], [5], [6], [7], [9], [10], [12], [15], [16].
Axiom: aaaaa=a.
Defines rule #15.
Overlap of [1] aba=bb with [1] aba=bb:
Critical pair: abbb=bbba.
Flip LHS and RHS.
Defines rule #3.
Referenced by [7], [8], [9], [11], [12], [16], [18].
Overlap of [1] aba=bb with [2] aaaaa=a:
Critical pair: aba=bbaaaa.
Reduce LHS:
| [1] | (aba) |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #14.
Overlap of [2] aaaaa=a with [1] aba=bb:
Critical pair: aaaabb=aba.
Reduce RHS:
| [1] | (aba) |
| ⇒ bb |
Defines rule #12.
Referenced by [6], [7], [14], [16].
Overlap of [1] aba=bb with [5] aaaabb=bb:
Critical pair: abbb=bbaaabb.
Flip LHS and RHS.
Defines rule #11.
Overlap of [5] aaaabb=bb with [3] bbba=abbb:
Critical pair: aaaababbb=bbbba.
Reduce LHS:
| [1] | aaa(aba)bbb |
| ⇒ aaabbbbb |
Reduce RHS:
| [3] | b(bbba) |
| ⇒ babbb |
Overlap of [7] aaabbbbb=babbb with [3] bbba=abbb:
Critical pair: aaabbabbb=babbba.
Reduce RHS:
| [3] | ba(bbba) |
| ⇒ baabbb |
Defines rule #13.
Referenced by [10], [11], [12], [19].
Overlap of [7] aaabbbbb=babbb with [3] bbba=abbb:
Critical pair: aaabbbbabbb=babbbbba.
Reduce LHS:
| [3] | aaab(bbba)bbb |
| [1] | ⇒ aa(aba)bbbbbb |
| ⇒ aabbbbbbbb |
Reduce RHS:
| [3] | babb(bbba) |
| ⇒ babbabbb |
Flip LHS and RHS.
Defines rule #6.
Referenced by [12].
Overlap of [1] aba=bb with [8] aaabbabbb=baabbb:
Critical pair: abbaabbb=bbaabbabbb.
Flip LHS and RHS.
Referenced by [13].
Overlap of [8] aaabbabbb=baabbb with [3] bbba=abbb:
Critical pair: aaabbaabbb=baabbba.
Reduce RHS:
| [3] | baa(bbba) |
| ⇒ baaabbb |
Referenced by [14].
Overlap of [8] aaabbabbb=baabbb with [3] bbba=abbb:
Critical pair: aaabbabbabbb=baabbbbba.
Reduce LHS:
| [9] | aaab(babbabbb) |
| [1] | ⇒ aa(aba)abbbbbbbb |
| ⇒ aabbabbbbbbbb |
Reduce RHS:
| [3] | baabb(bbba) |
| ⇒ baabbabbb |
Flip LHS and RHS.
Defines rule #10.
Referenced by [13].
Overlap of [10] bbaabbabbb=abbaabbb with [12] baabbabbb=aabbabbbbbbbb:
Critical pair: baabbabbbbbbbb=abbaabbb.
Reduce LHS:
| [12] | (baabbabbb)bbbbb |
| ⇒ aabbabbbbbbbbbbbbb |
Flip LHS and RHS.
Referenced by [14].
Overlap of [11] aaabbaabbb=baaabbb with [13] abbaabbb=aabbabbbbbbbbbbbbb:
Critical pair: aaaabbabbbbbbbbbbbbb=baaabbb.
Reduce LHS:
| [5] | (aaaabb)abbbbbbbbbbbbb |
| ⇒ bbabbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #9.
Overlap of [1] aba=bb with [14] baaabbb=bbabbbbbbbbbbbbb:
Critical pair: abbabbbbbbbbbbbbb=bbaabbb.
Flip LHS and RHS.
Defines rule #7.
Overlap of [14] baaabbb=bbabbbbbbbbbbbbb with [3] bbba=abbb:
Critical pair: baaaabbb=bbabbbbbbbbbbbbba.
Reduce LHS:
| [5] | b(aaaabb)b |
| ⇒ bbbb |
Reduce RHS:
| [3] | bbabbbbbbbbbb(bbba) |
| [3] | ⇒ bbabbbbbbb(bbba)bbb |
| [3] | ⇒ bbabbbb(bbba)bbbbbb |
| [3] | ⇒ bbab(bbba)bbbbbbbbb |
| [1] | ⇒ bb(aba)bbbbbbbbbbbb |
| ⇒ bbbbbbbbbbbbbbbb |
Flip LHS and RHS.
Defines rule #1.
Overlap of [7] aaabbbbb=babbb with [16] bbbbbbbbbbbbbbbb=bbbb:
Critical pair: aaabbbb=babbbbbbbbbbbbbb.
Defines rule #8.
Overlap of [16] bbbbbbbbbbbbbbbb=bbbb with [3] bbba=abbb:
Critical pair: bbbbbbbbbbbbbabbb=bbbba.
Reduce LHS:
| [3] | bbbbbbbbbb(bbba)bbb |
| [3] | ⇒ bbbbbbb(bbba)bbbbbb |
| [3] | ⇒ bbbb(bbba)bbbbbbbbb |
| [3] | ⇒ b(bbba)bbbbbbbbbbbb |
| ⇒ babbbbbbbbbbbbbbb |
Reduce RHS:
| [3] | b(bbba) |
| ⇒ babbb |
Defines rule #2.
Referenced by [19].
Overlap of [8] aaabbabbb=baabbb with [18] babbbbbbbbbbbbbbb=babbb:
Critical pair: aaabbabbb=baabbbbbbbbbbbbbbb.
Reduce LHS:
| [8] | (aaabbabbb) |
| ⇒ baabbb |
Flip LHS and RHS.
Defines rule #5.