化「字符串」而化（「列」于（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」））而（「或可有」于（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」））

文言：整参入而整数出，无外效方可复用；无外效非必终。汉语：输入须为已验证SSA，且调用处另外证明所有实参都是整数。本分析独立重建整数与布尔种类，不信任结果类型标签；拒绝分配、内存访问、除法与未知操作。结论是条件性的无外部副作用和整数返回，不保证终止，不允许将调用提前到原本不执行的路径。

化（「列」于（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」））而化（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」）而「爻」

暂无说明。

化（「列」于（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」））而（「列」于（「字符串」合「爻」合（「列」于「整数」）合「正则区域」合「整数」））

文言：候选自全而削，互递同验，未定则尽拒。汉语：求封闭的整数函数集合，删除含未知操作的函数及所有依赖者；支持互递归。达到迭代预算仍未收敛则返回空集，不发布暂定证明。调用者不得单独把一次验纯整函数的假设检查当作最终证明。