| Back: | ⟨a, b | bab=aaa, bbbb=b⟩ |
|---|
Completion settings:
Axiom: bab=aaa.
Defines rule #5.
Referenced by [3], [4], [5], [6], [7], [8], [13], [18].
Axiom: bbbb=b.
Defines rule #13.
Overlap of [1] bab=aaa with [1] bab=aaa:
Critical pair: baaaa=aaaab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [7], [8], [9], [10], [11], [13], [14].
Overlap of [1] bab=aaa with [2] bbbb=b:
Critical pair: bab=aaabbb.
Reduce LHS:
| [1] | (bab) |
| ⇒ aaa |
Flip LHS and RHS.
Defines rule #12.
Overlap of [2] bbbb=b with [1] bab=aaa:
Critical pair: bbbaaa=bab.
Reduce RHS:
| [1] | (bab) |
| ⇒ aaa |
Defines rule #10.
Overlap of [1] bab=aaa with [5] bbbaaa=aaa:
Critical pair: baaaa=aaabbaaa.
Flip LHS and RHS.
Defines rule #9.
Overlap of [5] bbbaaa=aaa with [3] aaaab=baaaa:
Critical pair: bbbabaaaa=aaaaab.
Reduce LHS:
| [1] | bb(bab)aaaa |
| ⇒ bbaaaaaaa |
Reduce RHS:
| [3] | a(aaaab) |
| ⇒ abaaaa |
Referenced by [10], [11], [14], [16].
Overlap of [6] aaabbaaa=baaaa with [3] aaaab=baaaa:
Critical pair: aaabbabaaaa=baaaaaab.
Reduce LHS:
| [1] | aaab(bab)aaaa |
| ⇒ aaabaaaaaaa |
Reduce RHS:
| [3] | baa(aaaab) |
| ⇒ baabaaaa |
Flip LHS and RHS.
Defines rule #6.
Overlap of [6] aaabbaaa=baaaa with [3] aaaab=baaaa:
Critical pair: aaabbaabaaaa=baaaaaaab.
Reduce LHS:
| [8] | aaab(baabaaaa) |
| ⇒ aaabaaabaaaaaaa |
Reduce RHS:
| [3] | baaa(aaaab) |
| ⇒ baaabaaaa |
Referenced by [12].
Overlap of [7] bbaaaaaaa=abaaaa with [3] aaaab=baaaa:
Critical pair: bbaaabaaaa=abaaaab.
Reduce RHS:
| [3] | ab(aaaab) |
| ⇒ abbaaaa |
Overlap of [7] bbaaaaaaa=abaaaa with [3] aaaab=baaaa:
Critical pair: bbaaaaaabaaaa=abaaaaaaab.
Reduce LHS:
| [3] | bbaa(aaaab)aaaa |
| [8] | ⇒ b(baabaaaa)aaaa |
| ⇒ baaabaaaaaaaaaaa |
Reduce RHS:
| [3] | abaaa(aaaab) |
| ⇒ abaaabaaaa |
Flip LHS and RHS.
Defines rule #8.
Referenced by [12].
Simplify [9] aaabaaabaaaaaaa=baaabaaaa.
Reduce LHS:
| [11] | aa(abaaabaaaa)aaa |
| [11] | ⇒ a(abaaabaaaa)aaaaaaaaaa |
| [11] | ⇒ (abaaabaaaa)aaaaaaaaaaaaaaaaa |
| ⇒ baaabaaaaaaaaaaaaaaaaaaaaaaaaaaaa |
Referenced by [13], [14], [15].
Overlap of [1] bab=aaa with [12] baaabaaaaaaaaaaaaaaaaaaaaaaaaaaaa=baaabaaaa:
Critical pair: babaaabaaaa=aaaaaabaaaaaaaaaaaaaaaaaaaaaaaaaaaa.
Reduce LHS:
| [1] | (bab)aaabaaaa |
| [3] | ⇒ aa(aaaab)aaaa |
| ⇒ aabaaaaaaaa |
Reduce RHS:
| [3] | aa(aaaab)aaaaaaaaaaaaaaaaaaaaaaaaaaaa |
| ⇒ aabaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa |
Flip LHS and RHS.
Referenced by [15].
Overlap of [12] baaabaaaaaaaaaaaaaaaaaaaaaaaaaaaa=baaabaaaa with [3] aaaab=baaaa:
Critical pair: baaabaaaaaaaaaaaaaaaaaaaaaaaabaaaa=baaabaaaab.
Reduce LHS:
| [3] | baaabaaaaaaaaaaaaaaaaaaaa(aaaab)aaaa |
| [3] | ⇒ baaabaaaaaaaaaaaaaaaa(aaaab)aaaaaaaa |
| [3] | ⇒ baaabaaaaaaaaaaaa(aaaab)aaaaaaaaaaaa |
| [3] | ⇒ baaabaaaaaaaa(aaaab)aaaaaaaaaaaaaaaa |
| [3] | ⇒ baaabaaaa(aaaab)aaaaaaaaaaaaaaaaaaaa |
| [3] | ⇒ baaab(aaaab)aaaaaaaaaaaaaaaaaaaaaaaa |
| [6] | ⇒ b(aaabbaaa)aaaaaaaaaaaaaaaaaaaaaaaaa |
| [7] | ⇒ (bbaaaaaaa)aaaaaaaaaaaaaaaaaaaaaa |
| ⇒ abaaaaaaaaaaaaaaaaaaaaaaaaaa |
Reduce RHS:
| [3] | baaab(aaaab) |
| [6] | ⇒ b(aaabbaaa)a |
| ⇒ bbaaaaa |
Flip LHS and RHS.
Defines rule #4.
Referenced by [15], [16], [18].
Overlap of [10] bbaaabaaaa=abbaaaa with [12] baaabaaaaaaaaaaaaaaaaaaaaaaaaaaaa=baaabaaaa:
Critical pair: bbaaabaaaa=abbaaaaaaaaaaaaaaaaaaaaaaaaaaaa.
Reduce LHS:
| [10] | (bbaaabaaaa) |
| ⇒ abbaaaa |
Reduce RHS:
| [14] | a(bbaaaaa)aaaaaaaaaaaaaaaaaaaaaaa |
| [13] | ⇒ (aabaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa)aaaaaaaaaaaaaaaaa |
| ⇒ aabaaaaaaaaaaaaaaaaaaaaaaaaa |
Defines rule #7.
Referenced by [17].
Overlap of [7] bbaaaaaaa=abaaaa with [14] bbaaaaa=abaaaaaaaaaaaaaaaaaaaaaaaaaa:
Critical pair: abaaaaaaaaaaaaaaaaaaaaaaaaaaaa=abaaaa.
Defines rule #2.
Simplify [10] bbaaabaaaa=abbaaaa.
Reduce RHS:
| [15] | (abbaaaa) |
| ⇒ aabaaaaaaaaaaaaaaaaaaaaaaaaa |
Defines rule #11.
Overlap of [5] bbbaaa=aaa with [14] bbaaaaa=abaaaaaaaaaaaaaaaaaaaaaaaaaa:
Critical pair: babaaaaaaaaaaaaaaaaaaaaaaaaaa=aaaaa.
Reduce LHS:
| [1] | (bab)aaaaaaaaaaaaaaaaaaaaaaaaaa |
| ⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaa |
Defines rule #1.