| Back: | ⟨a, b | aaa=1, abbab=ba⟩ |
|---|
Completion settings:
Axiom: aaa=1.
Defines rule #1.
Referenced by [3], [6], [15], [16], [18], [19], [20], [21], [23], [24].
Axiom: abbab=ba.
Referenced by [3], [4], [5], [9], [10], [13], [14].
Overlap of [1] aaa=1 with [2] abbab=ba:
Critical pair: aaba=bbab.
Flip LHS and RHS.
Defines rule #2.
Referenced by [5], [7], [8], [11], [16], [18], [20].
Overlap of [2] abbab=ba with [2] abbab=ba:
Critical pair: abbba=babab.
Overlap of [3] bbab=aaba with [2] abbab=ba:
Critical pair: bbba=aababab.
Flip LHS and RHS.
Defines rule #9.
Referenced by [12], [20], [21].
Overlap of [4] abbba=babab with [1] aaa=1:
Critical pair: abbb=bababaa.
Defines rule #3.
Referenced by [8], [14], [20], [21].
Overlap of [4] abbba=babab with [3] bbab=aaba:
Critical pair: abaaba=bababb.
Flip LHS and RHS.
Defines rule #11.
Referenced by [9], [10], [11], [12], [13], [14].
Overlap of [3] bbab=aaba with [6] abbb=bababaa:
Critical pair: bbbababaa=aababb.
Reduce LHS:
| [3] | b(bbab)abaa |
| ⇒ baabaabaa |
Flip LHS and RHS.
Defines rule #8.
Referenced by [10].
Overlap of [2] abbab=ba with [7] bababb=abaaba:
Critical pair: ababaaba=baabb.
Referenced by [15].
Overlap of [2] abbab=ba with [7] bababb=abaaba:
Critical pair: abbaabaaba=baababb.
Reduce RHS:
| [8] | b(aababb) |
| ⇒ bbaabaabaa |
Referenced by [24].
Overlap of [3] bbab=aaba with [7] bababb=abaaba:
Critical pair: babaaba=aabaabb.
Flip LHS and RHS.
Defines rule #10.
Overlap of [5] aababab=bbba with [7] bababb=abaaba:
Critical pair: aabaabaaba=bbbaabb.
Flip LHS and RHS.
Referenced by [17].
Overlap of [7] bababb=abaaba with [2] abbab=ba:
Critical pair: babba=abaabaab.
Flip LHS and RHS.
Defines rule #6.
Referenced by [16], [17], [22].
Overlap of [7] bababb=abaaba with [6] abbb=bababaa:
Critical pair: babbababaa=abaabab.
Reduce LHS:
| [2] | b(abbab)abaa |
| ⇒ bbaabaa |
Flip LHS and RHS.
Defines rule #5.
Referenced by [18].
Overlap of [9] ababaaba=baabb with [1] aaa=1:
Critical pair: ababaab=baabbaa.
Defines rule #4.
Referenced by [20].
Overlap of [3] bbab=aaba with [13] abaabaab=babba:
Critical pair: bbbabba=aabaaabaab.
Reduce LHS:
| [3] | b(bbab)ba |
| ⇒ baababa |
Reduce RHS:
| [1] | aab(aaa)baab |
| ⇒ aabbaab |
Flip LHS and RHS.
Defines rule #7.
Referenced by [20], [21], [22].
Simplify [12] bbbaabb=aabaabaaba.
Reduce RHS:
| [13] | a(abaabaab)a |
| ⇒ ababbaa |
Defines rule #15.
Overlap of [3] bbab=aaba with [14] abaabab=bbaabaa:
Critical pair: bbbbaabaa=aabaaabab.
Reduce RHS:
| [1] | aab(aaa)bab |
| [3] | ⇒ aa(bbab) |
| [1] | ⇒ (aaa)aba |
| ⇒ aba |
Overlap of [18] bbbbaabaa=aba with [1] aaa=1:
Critical pair: bbbbaab=abaa.
Defines rule #14.
Overlap of [6] abbb=bababaa with [19] bbbbaab=abaa:
Critical pair: abbabaa=bababaabbbaab.
Reduce LHS:
| [3] | a(bbab)aa |
| [1] | ⇒ (aaa)baaa |
| [1] | ⇒ b(aaa) |
| ⇒ b |
Reduce RHS:
| [15] | b(ababaab)bbaab |
| [16] | ⇒ bb(aabbaab)baab |
| [5] | ⇒ bbb(aababab)aab |
| [1] | ⇒ bbbbbb(aaa)b |
| ⇒ bbbbbbb |
Flip LHS and RHS.
Defines rule #17.
Overlap of [16] aabbaab=baababa with [16] aabbaab=baababa:
Critical pair: aabbbaababa=baabababaab.
Reduce LHS:
| [6] | a(abbb)aababa |
| [1] | ⇒ ababab(aaa)ababa |
| ⇒ abababababa |
Reduce RHS:
| [5] | b(aababab)aab |
| [1] | ⇒ bbbb(aaa)b |
| ⇒ bbbbb |
Referenced by [23].
Overlap of [18] bbbbaabaa=aba with [16] aabbaab=baababa:
Critical pair: bbbbaabbaababa=ababbaab.
Reduce LHS:
| [19] | (bbbbaab)baababa |
| [13] | ⇒ (abaabaab)aba |
| ⇒ babbaaba |
Flip LHS and RHS.
Defines rule #13.
Overlap of [21] abababababa=bbbbb with [1] aaa=1:
Critical pair: ababababab=bbbbbaa.
Defines rule #16.
Overlap of [10] abbaabaaba=bbaabaabaa with [1] aaa=1:
Critical pair: abbaabaab=bbaabaabaaaa.
Reduce RHS:
| [1] | bbaabaab(aaa)a |
| ⇒ bbaabaaba |
Defines rule #12.