寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
寻观「编译器核心」之「编译步骤」之「代码生成」之「网页汇编初始化证明」之书。
寻观「编译器核心」之「编译步骤」之「代码生成」之「网页汇编虚组消费」之书。

「：文言：私门其余诸参皆整，读果亦整，递参不可换类。汉语：只读证明之外，再证明所有非数组参数按整数入口进入后，各运算、分支结果与递归实参均能维持整数表示。数组参数仍单独处理，不能作为整数参与运算。这个证明不允许省略原条件的 i31 限制。：」
「虚组原子整」乃化（「数组引用类」于「爻」）而化「正则原子」而「爻」也。
「虚组原子整」者会「表」而会「值」而
  鉴「值」而
    有（「正则局部」于「号」）则
      「读数组引用」授以「爻」于「表」于「号」
    或有（「正则整数」于「数」）则「阳」
    或有（「正则爻」于「真」）则「阳」
    或有「其他」则「阴」
也。

「验虚组整数」乃化「正则函数」而化「整数」而「爻」也。
「验虚组整数」者会「函」而会「组号」而
  若「非」于（「验虚组只读」于「函」于「组号」）则
    「阴」
  否则
    虑「表」者「新数组引用」授以「爻」于「阴」于（「函」中「四」）
    而
    虑「可」者「新引用」授以「爻」于「阳」而
    虑「无」者
      「态射」授以「整数」授以「有」
      于（「函」中「二」）
      于（会「号」而「写数组引用」授以「爻」于「表」于「号」于（「非」于（「等于」于「号」于「组号」）））而
    递归虑「扫」其化「正则区域」而「爻」者会「段」而
      鉴「段」而
        有（「正则段」于「诸令」于「终」）则
          虑「无」者
            「态射」授以「正则指令」授以「有」
            于「诸令」
            于（会「令」而鉴「令」而
              有（「正则运算」于「号」于「类」于「术」于「参」）则（
                虑「合」者鉴「术」而
                  有（「正则原语」于『豫言_读取引用数组』）则
                    （鉴「参」而
                    有（「列」【「组」，「位」】）则「虚组原子整」于「表」于「位」
                    或有「其他」则「阴」）
                  或有（「正则原语」于「名」）则
                    「全部符合」授以「正则原子」
                    于（会「值」而「虚组原子整」于「表」于「值」）
                    于「参」
                  或有「正则调用」则（
                    鉴「参」而
                      有（「缀」于「头」于「余」）则
                        「全部符合」授以「整数」
                        于（会「位」
            而
            若「等于」
              于（「第N个」授以「整数」于「位」于（「函」中「二」））
              于「组号」则
                        「阳」
            否则
              「虚组原子整」
                于「表」
                于（「第N个」授以「正则原子」于「位」于「余」））
                于（「整数范围」于「零」于（「长度」授以「整数」于（「函」中「二」）））
                      或有「其他」则「阴」
                  ）
                  或有「其他」则
                    「阴」
                而
                虑「无」者
                  若「合」则「元」否则「写引用」于「可」于「阴」
                而
                「写数组引用」授以「爻」于「表」于「号」于「合」
              ）
              或有（「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」）则（
                虑「阳合」者「扫」于「阳体」
                而
                虑「阴合」者「扫」于「阴体」
                而
                虑「合」者
                  「且」
                    于（「虚组原子整」于「表」于「条件」）
                    于（「且」于「阳合」于「阴合」）
                而
                虑「无」者
                  若「合」则「元」否则「写引用」于「可」于「阴」
                而
                「写数组引用」授以「爻」于「表」于「号」于「合」
              ）
              或有「其他」则
                「写引用」于「可」于「阴」）
          而
          鉴「终」而
            有（「正则产出」于「值」）则
              「虚组原子整」于「表」于「值」
            或有「其他」则
              「阴」
    而
    虑「果」者「扫」于（「函」中「三」）而
    「且」于「果」于（「读引用」于「可」）
也。
