寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
「进步已知」即「或可有」于（「整数」合「整数」）也。
「双步形证」即「整数」合「正则区域」合「正则原子」也。
「：文言：守界不等于必进；诸续皆进一且上界不移，乃可并步。汉语：此证明必须与已验证的循环范围守卫组合使用，前提为两个建模参数均是整数且0≤扫描≤上界≤UINT32_MAX。这里只证明循环体正常结束时恰好前进一步，异常仍在原位置发生。输入须先通过SSA编号与作用域验证。未知调用、提前正常返回与非尾调用均拒绝。：」
「验逐步续行」乃化「正则函数」而化「整数」而化「整数」而化「正则区域」而「爻」也。
「验逐步续行」者会「函」而会「上」而会「扫」而会「体」而
 虑「含」者（化「整数」而「爻」也会「号」而「存在吗」授以「整数」于（会「参」而「等于」于「参」于「号」）于（「函」中「二」））而
 若「或者」于（「大于」于（「函」中「四」）于「一二八」）于（「等于」于「上」于「扫」）则「阴」否则
 若「非」于（「且」于（「含」于「上」）于（「含」于「扫」））则「阴」否则
 虑「表」者「新数组引用」授以「进步已知」于「可无」于（「函」中「四」）而
 虑「无」者「写数组引用」授以「进步已知」于「表」于「上」于（「可有」于（「上」与「零」））而
 虑「无」者「写数组引用」授以「进步已知」于「表」于「扫」于（「可有」于（「扫」与「零」））而
 虑「取」者（化「正则原子」而「进步已知」也会「值」而鉴「值」而有（「正则局部」于「号」）则「读数组引用」授以「进步已知」于「表」于「号」或有「其他」则「可无」）而
 虑「移」者（化「正则原子」而化「整数」而「进步已知」也会「值」而会「数」而
  若「或者」于（「大于」于「数」于「一六」）于（「小于」于「数」于（「减」于「零」于「一六」））则「可无」否则
  鉴（「取」于「值」）而有（「可有」于「式」）则（
   虑「偏」者「加」于（「式」中「一」）于「数」而
   若「或者」于（「大于」于「偏」于「一六」）于（「小于」于「偏」于（「减」于「零」于「一六」））则「可无」否则「可有」于（（「式」中「零」）与「偏」））或有「可无」则「可无」）而
 虑「末同」者（化「整数」而化「正则结束」而「爻」也会「号」而会「终」而鉴「终」而
  有（「正则产出」于（「正则局部」于「返」））则「等于」于「号」于「返」或有「其他」则「阴」）而
 虑「守递」者（化（「列」于「正则原子」）而「爻」也会「实参」而
  若「非」于（「等于」于（「长度」授以「正则原子」于「实参」）于（「长度」授以「整数」于（「函」中「二」）））则「阴」否则
  递归虑「查」其化（「列」于「整数」）而化（「列」于「正则原子」）而「爻」者会「形」而会「实」而鉴「形」而
   有「罄」则「阳」或有（「缀」于「号」于「形余」）则（鉴「实」而有（「缀」于「值」于「实余」）则
    若「或者」于（「等于」于「号」于「上」）于（「等于」于「号」于「扫」）则（鉴（「取」于「值」）而有（「可有」于「式」）则
     「且」于（「且」于（「等于」于（「式」中「零」）于「号」）于（「等于」于（「式」中「一」）于（若「等于」于「号」于「扫」则「一」否则「零」）））于（「查」于「形余」于「实余」）
     或有「可无」则「阴」）否则「查」于「形余」于「实余」或有「罄」则「阴」）而
  「查」于（「函」中「二」）于「实参」）而
 递归虑「扫段」其化「正则区域」而「爻」者会「段」而鉴「段」而有（「正则段」于「令们」于「终」）则
  递归虑「扫列」其化（「列」于「正则指令」）而「爻」者会「列值」而鉴「列值」而
   有「罄」则「阴」
   或有（「缀」于「令」于「余」）则（
    虑「末」者鉴「余」而有「罄」则「阳」或有「其他」则「阴」而
    鉴「令」而
     有（「正则运算」于「号」于「类」于（「正则原语」于「名」）于「参」）则（
      虑「合」者鉴「名」而有『豫言_整数加』则「阳」或有『豫言_整数减』则「阳」或有『豫言_整数乘』则「阳」或有『豫言_整数除』则「阳」
       或有『豫言_整数相等』则「阳」或有『豫言_整数大于』则「阳」或有『豫言_读取引用数组』则「阳」或有『豫言_写入引用数组』则「阳」或有「其他」则「阴」而
      若「非」于「合」则「阴」否则
      虑「式」者若「串相等」于「名」于『豫言_整数加』则（鉴「参」而有（「列」【「值」，「正则整数」于「数」】）则「移」于「值」于「数」
       或有（「列」【「正则整数」于「数」，「值」】）则「移」于「值」于「数」或有「其他」则「可无」）否则
       若「串相等」于「名」于『豫言_整数减』则（鉴「参」而有（「列」【「值」，「正则整数」于「数」】）则
        若「或者」于（「大于」于「数」于「一六」）于（「小于」于「数」于（「减」于「零」于「一六」））则「可无」否则「移」于「值」于（「减」于「零」于「数」）或有「其他」则「可无」）否则「可无」而
      虑「无」者「写数组引用」授以「进步已知」于「表」于「号」于「式」而「扫列」于「余」）
     或有（「正则运算」于「号」于「类」于「正则调用」于（「缀」于（「正则函数引用」于「名」）于「实参」））则
      「且」于（「且」于「末」于（「末同」于「号」于「终」））于（「且」于（「串相等」于「名」于（「函」中「零」））于（「守递」于「实参」））
     或有（「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」）则
      「且」于（「且」于「末」于（「末同」于「号」于「终」））于（「且」于（「扫段」于「阳体」）于（「扫段」于「阴体」））
     或有「其他」则「阴」）而
  「扫列」于「令们」而
 「扫段」于「体」也。
「：文言：首唯等比，等则止，不等则续。汉语：首批要求根区域恰为比较与尾部条件两步，真分支为空且直接产出；描述符保留比较局部编号，生成器必须在单步中置假、退出时置真，不能丢失被其他表达式引用的原比较值。：」
「验双步形」乃化「正则函数」而化「整数」而化「整数」而（「或可有」于「双步形证」）也。
「验双步形」者会「函」而会「上」而会「扫」而鉴（「函」中「三」）而
 有（「正则段」于（「列」【
  「正则运算」于「比号」于「比类」于（「正则原语」于『豫言_整数相等』）于（「列」【「正则局部」于「甲」，「正则局部」于「乙」】），
  「正则如果」于「果号」于「果类」于（「正则局部」于「条件号」）于（「正则段」于「罄」于（「正则产出」于「果」））于「体」】）于（「正则产出」于（「正则局部」于「返号」）））则
 若「非」于（「且」于（「等于」于「比号」于「条件号」）于（「等于」于「果号」于「返号」））则「可无」否则
 若「非」于（「或者」于（「且」于（「等于」于「甲」于「上」）于（「等于」于「乙」于「扫」））于（「且」于（「等于」于「甲」于「扫」）于（「等于」于「乙」于「上」）））则「可无」否则
 若「验逐步续行」于「函」于「上」于「扫」于「体」则「可有」于（「比号」与「体」与「果」）否则「可无」
 或有「其他」则「可无」也。
