| Back: | ⟨a, b | aaba=b, abbbb=a⟩ |
|---|
Completion settings:
Axiom: aaba=b.
Referenced by [3], [4], [6], [8], [9], [13], [14], [15], [17], [19], [21], [22], [23], [24].
Axiom: abbbb=a.
Referenced by [4], [5], [6], [10], [13], [15].
Overlap of [1] aaba=b with [1] aaba=b:
Critical pair: aabb=baba.
Referenced by [5], [14], [15].
Overlap of [1] aaba=b with [2] abbbb=a:
Critical pair: aaba=bbbbb.
Reduce LHS:
| [1] | (aaba) |
| ⇒ b |
Flip LHS and RHS.
Referenced by [7], [13], [18], [20].
Overlap of [3] aabb=baba with [2] abbbb=a:
Critical pair: aa=bababb.
Flip LHS and RHS.
Referenced by [6], [7], [8], [11], [14].
Overlap of [2] abbbb=a with [5] bababb=aa:
Critical pair: abbbaa=aababb.
Reduce RHS:
| [1] | (aaba)bb |
| ⇒ bbb |
Referenced by [12].
Overlap of [4] bbbbb=b with [5] bababb=aa:
Critical pair: bbbbaa=bababb.
Reduce RHS:
| [5] | (bababb) |
| ⇒ aa |
Overlap of [5] bababb=aa with [5] bababb=aa:
Critical pair: bababaa=aaababb.
Reduce RHS:
| [1] | a(aaba)bb |
| ⇒ abbb |
Flip LHS and RHS.
Overlap of [7] bbbbaa=aa with [1] aaba=b:
Critical pair: bbbbab=aaaba.
Reduce RHS:
| [1] | a(aaba) |
| ⇒ ab |
Overlap of [9] bbbbab=ab with [2] abbbb=a:
Critical pair: bbbba=abbbb.
Reduce RHS:
| [8] | (abbb)b |
| ⇒ bababaab |
Flip LHS and RHS.
Referenced by [16].
Overlap of [9] bbbbab=ab with [5] bababb=aa:
Critical pair: bbbaa=ababb.
Flip LHS and RHS.
Referenced by [14].
Simplify [6] abbbaa=bbb.
Reduce LHS:
| [8] | (abbb)aa |
| ⇒ bababaaaa |
Overlap of [2] abbbb=a with [12] bababaaaa=bbb:
Critical pair: abbbbbb=aababaaaa.
Reduce LHS:
| [4] | a(bbbbb)b |
| ⇒ abb |
Reduce RHS:
| [1] | (aaba)baaaa |
| ⇒ bbaaaa |
Referenced by [14], [15], [17], [19].
Overlap of [5] bababb=aa with [12] bababaaaa=bbb:
Critical pair: bababbbb=aaababaaaa.
Reduce LHS:
| [11] | b(ababb)bb |
| [7] | ⇒ (bbbbaa)bb |
| [3] | ⇒ (aabb) |
| ⇒ baba |
Reduce RHS:
| [1] | a(aaba)baaaa |
| [13] | ⇒ (abb)aaaa |
| ⇒ bbaaaaaaaa |
Overlap of [2] abbbb=a with [13] abb=bbaaaa:
Critical pair: bbaaaabb=a.
Reduce LHS:
| [3] | bbaa(aabb) |
| [1] | ⇒ bb(aaba)ba |
| ⇒ bbbba |
Referenced by [16], [17], [18], [20], [25].
Simplify [10] bababaab=bbbba.
Reduce RHS:
| [15] | (bbbba) |
| ⇒ a |
Referenced by [17].
Overlap of [16] bababaab=a with [14] baba=bbaaaaaaaa:
Critical pair: bbaaaaaaaabaab=a.
Reduce LHS:
| [1] | bbaaaaaa(aaba)ab |
| [1] | ⇒ bbaaaa(aaba)b |
| [13] | ⇒ bbaaa(abb) |
| [13] | ⇒ bbaa(abb)aaaa |
| [13] | ⇒ bba(abb)aaaaaaaa |
| [13] | ⇒ bb(abb)aaaaaaaaaaaa |
| [15] | ⇒ (bbbba)aaaaaaaaaaaaaaa |
| ⇒ aaaaaaaaaaaaaaaa |
Defines rule #1.
Referenced by [24].
Overlap of [15] bbbba=a with [14] baba=bbaaaaaaaa:
Critical pair: bbbbbaaaaaaaa=aba.
Reduce LHS:
| [4] | (bbbbb)aaaaaaaa |
| ⇒ baaaaaaaa |
Flip LHS and RHS.
Referenced by [19].
Overlap of [18] aba=baaaaaaaa with [1] aaba=b:
Critical pair: abb=baaaaaaaaaba.
Reduce LHS:
| [13] | (abb) |
| ⇒ bbaaaa |
Reduce RHS:
| [1] | baaaaaaa(aaba) |
| ⇒ baaaaaaab |
Flip LHS and RHS.
Referenced by [20].
Overlap of [15] bbbba=a with [19] baaaaaaab=bbaaaa:
Critical pair: bbbbbaaaa=aaaaaaab.
Reduce LHS:
| [4] | (bbbbb)aaaa |
| ⇒ baaaa |
Flip LHS and RHS.
Referenced by [21].
Overlap of [20] aaaaaaab=baaaa with [1] aaba=b:
Critical pair: aaaaab=baaaaa.
Referenced by [22].
Overlap of [21] aaaaab=baaaaa with [1] aaba=b:
Critical pair: aaab=baaaaaa.
Referenced by [23].
Overlap of [22] aaab=baaaaaa with [1] aaba=b:
Critical pair: ab=baaaaaaa.
Defines rule #3.
Overlap of [1] aaba=b with [17] aaaaaaaaaaaaaaaa=a:
Critical pair: aaba=baaaaaaaaaaaaaaa.
Reduce LHS:
| [1] | (aaba) |
| ⇒ b |
Flip LHS and RHS.
Defines rule #2.
Referenced by [25].
Overlap of [15] bbbba=a with [24] baaaaaaaaaaaaaaa=b:
Critical pair: bbbb=aaaaaaaaaaaaaaa.
Defines rule #4.