| Back: | ⟨a, b | aaaa=a, baabb=a⟩ |
|---|
Completion settings:
Axiom: aaaa=a.
Referenced by [4], [5], [10], [11], [15], [16].
Axiom: baabb=a.
Referenced by [3], [4], [6], [7], [8], [13].
Overlap of [2] baabb=a with [2] baabb=a:
Critical pair: baaba=aaabb.
Referenced by [4], [9], [12], [14], [18].
Overlap of [3] baaba=aaabb with [3] baaba=aaabb:
Critical pair: baaaaabb=aaabbaba.
Reduce LHS:
| [1] | b(aaaa)abb |
| [2] | ⇒ (baabb) |
| ⇒ a |
Flip LHS and RHS.
Overlap of [1] aaaa=a with [4] aaabbaba=a:
Critical pair: aa=abbaba.
Flip LHS and RHS.
Referenced by [7], [8], [9], [17], [19].
Overlap of [4] aaabbaba=a with [2] baabb=a:
Critical pair: aaabbaa=aabb.
Referenced by [9].
Overlap of [2] baabb=a with [5] abbaba=aa:
Critical pair: baaa=aaba.
Overlap of [5] abbaba=aa with [2] baabb=a:
Critical pair: abbaa=aaabb.
Overlap of [5] abbaba=aa with [3] baaba=aaabb:
Critical pair: abbaaaabb=aaaba.
Reduce LHS:
| [8] | (abbaa)aabb |
| [6] | ⇒ (aaabbaa)bb |
| ⇒ aabbbb |
Flip LHS and RHS.
Referenced by [11].
Overlap of [7] baaa=aaba with [1] aaaa=a:
Critical pair: ba=aabaa.
Flip LHS and RHS.
Referenced by [11], [12], [13], [14].
Overlap of [1] aaaa=a with [10] aabaa=ba:
Critical pair: aaaba=aabaa.
Reduce LHS:
| [9] | (aaaba) |
| ⇒ aabbbb |
Reduce RHS:
| [10] | (aabaa) |
| ⇒ ba |
Referenced by [18], [23], [24], [25], [28].
Overlap of [3] baaba=aaabb with [10] aabaa=ba:
Critical pair: bba=aaabba.
Flip LHS and RHS.
Referenced by [20].
Overlap of [10] aabaa=ba with [2] baabb=a:
Critical pair: aaa=babb.
Referenced by [14], [15], [16], [17], [20], [22], [23].
Overlap of [10] aabaa=ba with [3] baaba=aaabb:
Critical pair: aaaaabb=baba.
Reduce LHS:
| [13] | (aaa)aabb |
| [8] | ⇒ b(abbaa)bb |
| [7] | ⇒ (baaa)bbbb |
| ⇒ aababbbb |
Referenced by [21].
Overlap of [1] aaaa=a with [13] aaa=babb:
Critical pair: babba=a.
Overlap of [1] aaaa=a with [13] aaa=babb:
Critical pair: aababb=aa.
Referenced by [21].
Overlap of [5] abbaba=aa with [13] aaa=babb:
Critical pair: abbabbabb=aaaa.
Reduce LHS:
| [15] | ab(babba)bb |
| ⇒ ababb |
Reduce RHS:
| [13] | (aaa)a |
| [15] | ⇒ (babba) |
| ⇒ a |
Referenced by [18], [19], [27].
Overlap of [3] baaba=aaabb with [17] ababb=a:
Critical pair: baa=aaabbbb.
Reduce RHS:
| [11] | a(aabbbb) |
| ⇒ aba |
Referenced by [22], [24], [29].
Overlap of [5] abbaba=aa with [17] ababb=a:
Critical pair: abba=aabb.
Referenced by [20].
Overlap of [12] aaabba=bba with [19] abba=aabb:
Critical pair: aaaabb=bba.
Reduce LHS:
| [13] | (aaa)abb |
| [15] | ⇒ (babba)bb |
| ⇒ abb |
Flip LHS and RHS.
Overlap of [14] aababbbb=baba with [16] aababb=aa:
Critical pair: aabb=baba.
Flip LHS and RHS.
Referenced by [24].
Overlap of [18] baa=aba with [13] aaa=babb:
Critical pair: bbabb=abaa.
Reduce LHS:
| [20] | (bba)bb |
| ⇒ abbbb |
Reduce RHS:
| [18] | a(baa) |
| ⇒ aaba |
Flip LHS and RHS.
Referenced by [24].
Overlap of [13] aaa=babb with [11] aabbbb=ba:
Critical pair: aba=babbbbbb.
Referenced by [26].
Overlap of [18] baa=aba with [11] aabbbb=ba:
Critical pair: baba=abaabbbb.
Reduce LHS:
| [21] | (baba) |
| ⇒ aabb |
Reduce RHS:
| [18] | a(baa)bbbb |
| [22] | ⇒ (aaba)bbbb |
| ⇒ abbbbbbbb |
Referenced by [25], [28], [29].
Overlap of [20] bba=abb with [11] aabbbb=ba:
Critical pair: bbba=abbabbbb.
Reduce LHS:
| [20] | b(bba) |
| ⇒ babb |
Reduce RHS:
| [20] | a(bba)bbbb |
| [24] | ⇒ (aabb)bbbb |
| ⇒ abbbbbbbbbbbb |
Referenced by [26].
Simplify [23] aba=babbbbbb.
Reduce RHS:
| [25] | (babb)bbbb |
| ⇒ abbbbbbbbbbbbbbbb |
Referenced by [27].
Overlap of [17] ababb=a with [26] aba=abbbbbbbbbbbbbbbb:
Critical pair: abbbbbbbbbbbbbbbbbb=a.
Defines rule #1.
Referenced by [29].
Overlap of [11] aabbbb=ba with [24] aabb=abbbbbbbb:
Critical pair: abbbbbbbbbb=ba.
Flip LHS and RHS.
Defines rule #2.
Referenced by [29].
Overlap of [18] baa=aba with [24] aabb=abbbbbbbb:
Critical pair: baabbbbbbbb=abaabb.
Reduce LHS:
| [24] | b(aabb)bbbbbb |
| [28] | ⇒ (ba)bbbbbbbbbbbbbb |
| [27] | ⇒ (abbbbbbbbbbbbbbbbbb)bbbbbb |
| ⇒ abbbbbb |
Reduce RHS:
| [24] | ab(aabb) |
| [28] | ⇒ a(ba)bbbbbbbb |
| [27] | ⇒ a(abbbbbbbbbbbbbbbbbb) |
| ⇒ aa |
Flip LHS and RHS.
Defines rule #3.