寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则验证」之书。
寻观「编译器核心」之「编译步骤」之「代码生成」之「网页汇编纯调用证明」之书。
「：文言：不信类名，必察诸用；互递有污，传拒其上。汉语：直接构造并验证SSA，检查完整闭包而非暂定单函数结论；纯递归可能不终止，不执行该反例。：」
「造函」乃化「字符串」而化（「列」于「正则指令」）而化「正则原子」而「正则函数」也。
「造函」者会「名」而会「令」而会「果」而「名」与「阴」与（「列」【「零」】）与（「正则段」于「令」于（「正则产出」于「果」））与「八」也。
「甲」者「正则局部」于「零」也。
「乙」者「正则局部」于「一」也。
「调」乃化「字符串」而化（「列」于「正则原子」）而「正则指令」也。
「调」者会「名」而会「参」而「正则运算」于「一」于「正则整数值」于「正则调用」于（「缀」于（「正则函数引用」于「名」）于「参」）也。
「算」乃化「字符串」而化（「列」于「正则原子」）而「正则指令」也。
「算」者会「名」而会「参」而「正则运算」于「一」于「正则整数值」于（「正则原语」于「名」）于「参」也。
「验」乃化「正则模块」而化（「列」于「字符串」）而「有」也。
「验」者会「诸函」而会「期」而
 虑「无」者「态射」授以「正则函数」授以「有」于「诸函」于「验证正则函数」而
 虑「得」者「求纯整闭包」于「诸函」而
 若「且」于（「等于」于（「长度」授以「正则函数」于「得」）于（「长度」授以「字符串」于「期」））于
  （「全部符合」授以「字符串」于（会「名」而鉴（「纯整查函」于「名」于「得」）而有（「可有」于「函」）则「阳」或有「可无」则「阴」）于「期」）则「元」否则「发生事故」授以「有」于『纯调用闭包错误』也。
「单验」乃化「正则指令」而化「爻」而「有」也。
「单验」者会「令」而会「应」而「验」于（「列」【「造函」于『甲函』于（「列」【「令」】）于「乙」】）于（若「应」则（「列」【『甲函』】）否则「罄」）也。
「二参」者「列」【「甲」，「正则整数」于「一」】也。
「单验」于（「算」于『豫言_整数加』于「二参」）于「阳」。
「单验」于（「算」于『豫言_整数减』于「二参」）于「阳」。
「单验」于（「算」于『豫言_整数乘』于「二参」）于「阳」。
「单验」于（「算」于『豫言_整数除』于「二参」）于「阴」。
「单验」于（「算」于『豫言_整数加』于（「列」【「甲」】））于「阴」。
「单验」于（「算」于『豫言_整数加』于（「列」【「甲」，「正则字符串」于『伪整』】））于「阴」。
「单验」于（「算」于『豫言_读取引用数组』于「二参」）于「阴」。
「单验」于（「算」于『豫言_未知原语』于「二参」）于「阴」。
「单验」于（「正则运算」于「一」于「正则整数值」于「正则造元组」于「二参」）于「阴」。
「单验」于（「正则运算」于「一」于「正则整数值」于（「正则取字段」于「零」）于（「列」【「甲」】））于「阴」。
「单验」于（「正则运算」于「一」于「正则整数值」于（「正则读全局」于『路』于『名』于「零」）于「罄」）于「阴」。
「单验」于（「正则运算」于「一」于「正则整数值」于「正则调用」于（「列」【「甲」，「正则整数」于「一」】））于「阴」。
「单验」于（「调」于『未知』于（「列」【「甲」】））于「阴」。
「验」于（「列」【「造函」于『弃除』于（「列」【「算」于『豫言_整数除』于（「列」【「甲」，「正则整数」于「零」】）】）于「甲」】）于「罄」。
「验」于（「列」【「造函」于『恒等』于「罄」于「甲」】）于（「列」【『恒等』】）。
「验」于（「列」【「造函」于『自递』于（「列」【「调」于『自递』于（「列」【「甲」】）】）于「乙」】）于（「列」【『自递』】）。
「甲函」者「造函」于『互甲』于（「列」【「调」于『互乙』于（「列」【「甲」】）】）于「乙」也。
「乙函」者「造函」于『互乙』于（「列」【「调」于『互甲』于（「列」【「甲」】）】）于「乙」也。
「验」于（「列」【「甲函」，「乙函」】）于（「列」【『互甲』，『互乙』】）。
「验」于（「列」【「甲函」，「造函」于『互乙』于（「列」【「算」于『豫言_整数除』于「二参」】）于「乙」】）于「罄」。
「验」于（「列」【「造函」于『错参』于（「列」【「调」于『恒等』于「罄」】）于「乙」，「造函」于『恒等』于「罄」于「甲」】）于（「列」【『恒等』】）。
「分支函」乃化「正则原子」而化「正则原子」而「正则函数」也。
「分支函」者会「条件」而会「阴值」而「造函」于『分支』于（「列」【
 「正则如果」于「一」于「正则整数值」于「条件」于（「正则段」于「罄」于（「正则产出」于「甲」））于（「正则段」于「罄」于（「正则产出」于「阴值」））】）于「乙」也。
「验」于（「列」【「分支函」于（「正则爻」于「阳」）于（「正则整数」于「一」）】）于（「列」【『分支』】）。
「验」于（「列」【「分支函」于「甲」于（「正则整数」于「一」）】）于「罄」。
「验」于（「列」【「分支函」于（「正则爻」于「阳」）于（「正则字符串」于『未执行亦拒』）】）于「罄」。
「验」于（「列」【『超限』与「阴」与（「列」【「零」】）与（「正则段」于「罄」于（「正则产出」于「甲」））与「二五七」】）于「罄」。
「长链」者「态射」授以「整数」授以「正则函数」于（「整数范围」于「零」于「四零」）于（会「号」而「造函」于（「整数表示」于「号」）于（「列」【「调」于（「整数表示」于（「加」于「号」于「一」））于（「列」【「甲」】）】）于「乙」）也。
「验」于（「缀」于（「造函」于『独立纯函』于「罄」于「甲」）于「长链」）于「罄」。
「打印行」于『纯调用证明二十四项通过』。
