| Back: | ⟨a, b | aabaabbba=ba⟩ |
|---|
Completion settings:
Axiom: aabaabbba=ba.
Referenced by [3], [4], [5], [13].
Axiom: bbbba=c.
Overlap of [1] aabaabbba=ba with [1] aabaabbba=ba:
Critical pair: aabaabbbba=baabaabbba.
Reduce LHS:
| [2] | aabaa(bbbba) |
| ⇒ aabaac |
Reduce RHS:
| [1] | b(aabaabbba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [6], [7], [8], [13], [14].
Overlap of [2] bbbba=c with [1] aabaabbba=ba:
Critical pair: bbbbba=cabaabbba.
Reduce LHS:
| [2] | b(bbbba) |
| ⇒ bc |
Reduce RHS:
| [3] | cabaab(bba) |
| ⇒ cabaabaabaac |
Flip LHS and RHS.
Defines rule #7.
Referenced by [5], [7], [8], [9], [10], [11].
Overlap of [3] bba=aabaac with [1] aabaabbba=ba:
Critical pair: bbba=aabaacabaabbba.
Reduce LHS:
| [3] | b(bba) |
| ⇒ baabaac |
Reduce RHS:
| [3] | aabaacabaab(bba) |
| [4] | ⇒ aabaa(cabaabaabaac) |
| ⇒ aabaabc |
Flip LHS and RHS.
Defines rule #3.
Overlap of [3] bba=aabaac with [5] aabaabc=baabaac:
Critical pair: bbbaabaac=aabaacabaabc.
Reduce LHS:
| [3] | b(bba)abaac |
| ⇒ baabaacabaac |
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] cabaabaabaac=bc with [4] cabaabaabaac=bc:
Critical pair: cabaabaabaabc=bcabaabaabaac.
Reduce LHS:
| [5] | cabaab(aabaabc) |
| [3] | ⇒ cabaa(bba)abaac |
| ⇒ cabaaaabaacabaac |
Reduce RHS:
| [4] | b(cabaabaabaac) |
| ⇒ bbc |
Overlap of [5] aabaabc=baabaac with [4] cabaabaabaac=bc:
Critical pair: aabaabbc=baabaacabaabaabaac.
Reduce RHS:
| [4] | baabaa(cabaabaabaac) |
| [5] | ⇒ b(aabaabc) |
| [3] | ⇒ (bba)abaac |
| ⇒ aabaacabaac |
Referenced by [9], [10], [12].
Overlap of [8] aabaabbc=aabaacabaac with [4] cabaabaabaac=bc:
Critical pair: aabaabbbc=aabaacabaacabaabaabaac.
Reduce RHS:
| [4] | aabaacabaa(cabaabaabaac) |
| [6] | ⇒ (aabaacabaabc) |
| ⇒ baabaacabaac |
Referenced by [12].
Overlap of [4] cabaabaabaac=bc with [7] cabaaaabaacabaac=bbc:
Critical pair: cabaabaabaabbc=bcabaaaabaacabaac.
Reduce LHS:
| [8] | cabaab(aabaabbc) |
| [4] | ⇒ (cabaabaabaac)abaac |
| ⇒ bcabaac |
Reduce RHS:
| [7] | b(cabaaaabaacabaac) |
| ⇒ bbbc |
Flip LHS and RHS.
Referenced by [11].
Overlap of [10] bbbc=bcabaac with [4] cabaabaabaac=bc:
Critical pair: bbbbc=bcabaacabaabaabaac.
Reduce LHS:
| [10] | b(bbbc) |
| ⇒ bbcabaac |
Reduce RHS:
| [4] | bcabaa(cabaabaabaac) |
| ⇒ bcabaabc |
Flip LHS and RHS.
Referenced by [12].
Overlap of [8] aabaabbc=aabaacabaac with [11] bcabaabc=bbcabaac:
Critical pair: aabaabbbcabaac=aabaacabaacabaabc.
Reduce LHS:
| [9] | (aabaabbbc)abaac |
| ⇒ baabaacabaacabaac |
Flip LHS and RHS.
Referenced by [16].
Overlap of [1] aabaabbba=ba with [3] bba=aabaac:
Critical pair: aabaabaabaac=ba.
Defines rule #6.
Overlap of [2] bbbba=c with [3] bba=aabaac:
Critical pair: bbaabaac=c.
Reduce LHS:
| [3] | (bba)abaac |
| ⇒ aabaacabaac |
Defines rule #4.
Referenced by [15], [16], [17].
Overlap of [7] cabaaaabaacabaac=bbc with [14] aabaacabaac=c:
Critical pair: cabaac=bbc.
Flip LHS and RHS.
Defines rule #2.
Simplify [12] aabaacabaacabaabc=baabaacabaacabaac.
Reduce RHS:
| [14] | b(aabaacabaac)abaac |
| ⇒ bcabaac |
Referenced by [17].
Overlap of [16] aabaacabaacabaabc=bcabaac with [14] aabaacabaac=c:
Critical pair: cabaabc=bcabaac.
Defines rule #5.