在Blog里写大段的证明可不是一个好的做法。尤其目前的Web大都用兼容LaTeX的库如KaTeX实现公式渲染，这对像我这样懒得背TeX语法的人来说，还是太过繁琐了。我个人更习惯用TeXmacs直接导出HTML页面，而对它们而言，CDN是个不错的归宿。下面是一个简要的目录，我尝试着在标题中把证明的内容简短地表达出来，但看上去这是一件相当困难的任务：
线性代数
形式语言与自动机
- Regex(扩展正规语言)与MFA(带缓冲区的有限状态自动机)的性质
- AFA(alternating finite automata)与DFA等价
- vsf-regex(variable-star-free regex)交的非空性判定算法
- 带Regex约束的straight line word equation至少是PS的
- 用2FT(双向有限状态转换机)编码带捕获与引用的replaceAll（半成品）
- 用NSST(非确定型字符流转换机nondeterministic streaming string transducer)编码带捕获与引用的replaceAll
- NFA在NSST作用下的原象的判定算法
- NSST约束总结（英文）