「元类型」

文言：记甲减乙之上界，合诸径以明其约；相矛盾者不授证。汉语：有限差分约束域，零号节点代表数学常量零。调用者保证其他节点对应整数值；这里不推断机器加法是否溢出，不证明数组长度。未知事实不等于零。最多三十二节点，所有内部加法均限制在安全范围。

「整数」

暂无说明。

化「整数」而（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化「整数」而化「整数」而「整数」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化「整数」而化「整数」而化「整数」而「有」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而「有」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而「爻」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化「整数」而化「整数」而化「整数」而「爻」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化「整数」而化「整数」而「爻」

文言：先证仿射之果纳于窄界，方许以数学加法论之。汉语：偏移仅接受正负 wasm32 上界以内；证明节点加偏移的数学值处于零至 UINT32_MAX，此时 i64 加法必不溢出。失败只表示未知，不允许删除原检查。

「元类型」

暂无说明。

化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化（「整数」合（「数组引用类」于「整数」）合（「引用类」于「爻」））而化（「列」于（「整数」合「整数」））而「爻」

文言：诸新参同取于旧域，不先改一参而证其余。汉语：对已闭合的入口约束和当前分支事实，同时代入全部参数表达式；表达式是节点加常量，且必须证明结果位于 wasm32 范围。零节点必须保持常量零。只适用于这些已建模的整数参数，不代表其他实参或副作用合法。