寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
寻观「编译器核心」之「编译步骤」之「代码生成」之「网页汇编栈表示证明」之书。
寻观「编译器核心」之「编译步骤」之「代码生成」之「网页汇编进步证明」之书。

「：文言：每步一写，索进一，余参不移，值为索之一次式，乃可并写。汉语：输入须通过 SSA、表示及封闭调用图验证。这里只证明单数组、单存储、无读取或其他调用的正向填充；退出必须为单元，扫描每步加一，其他参数保持原样。值表达式限加减乘且对扫描为常系数一次式，系数限制在-16..16，树大小不超过64。调用者仍须检查0≤扫描≤上界≤数组长度，不能据此省略根初始化。：」
「栈填表达」立「元类型」也。
  「栈填原子」立化「正则原子」而「栈填表达」也。
  「栈填二元」立化「字符串」而化「栈填表达」而化「栈填表达」而「栈填表达」也。

「栈填已知」即「或可有」于（「栈填表达」合「整数」合「整数」）也。

「栈填证」即
  「整数」
  合「整数」
  合「整数」
  合「栈填表达」
  合「整数」
也。

「取栈填式」乃
  化（「数组引用类」于「栈填已知」）而
  化「正则原子」而
  「栈填已知」
也。
「取栈填式」者会「表」而会「值」而
  鉴「值」而
    有（「正则局部」于「号」）则
      「读数组引用」授以「栈填已知」于「表」于「号」
    或有（「正则整数」于「数」）则
      「可有」于（（「栈填原子」于「值」）与「零」与「一」）
    或有「其他」则「可无」
也。

「栈填小常数」乃化「栈填表达」而「或可有」于「整数」也。
「栈填小常数」者会「式」而
  鉴「式」而
    有（「栈填原子」于（「正则整数」于「数」））则
      若「或者」于（「大于」于「数」于「一六」）于（「小于」于「数」于（「减」于「零」于「一六」））则
        「可无」
      否则
        「可有」于「数」
    或有「其他」则「可无」
也。

「合栈填式」乃化「字符串」而化「栈填已知」而化「栈填已知」而「栈填已知」也。
「合栈填式」者会「术名」而会「甲式」而会「乙式」而
  鉴「甲式」而
    有「可无」则「可无」
    或有（「可有」于「甲」）则（
      鉴「乙式」而
        有「可无」则「可无」
        或有（「可有」于「乙」）则（
          虑「费」者
            「加」于「一」于（「加」于（「甲」中「二」）于（「乙」中「二」））而
          若「大于」于「费」于「六四」则
            「可无」
          否则
            虑「率」者
              （「或可有」于「整数」也鉴「术名」而
                  有『豫言_整数加』则
                    「可有」于（「加」于（「甲」中「一」）于（「乙」中「一」））
                  或有『豫言_整数减』则
                    「可有」于（「减」于（「甲」中「一」）于（「乙」中「一」））
                  或有『豫言_整数乘』则（
                    若「且」
                      于（「等于」于（「甲」中「一」）于「零」）
                      于（「等于」于（「乙」中「一」）于「零」）则
                        「可有」于「零」
                    否则
                      鉴（「栈填小常数」于（「甲」中「零」））而
                        有（「可有」于「数」）则
                          「可有」
                            于（「乘」于「数」于（「乙」中「一」））
                        或有「可无」则（
                          鉴（「栈填小常数」于（「乙」中「零」））而
                            有（「可有」于「数」）则
                              「可有」
                                于（「乘」于「数」于（「甲」中「一」））
                            或有「可无」则「可无」
                        ）
                  ）
                  或有「其他」则「可无」）而
            鉴「率」而
              有「可无」则「可无」
              或有（「可有」于「数」）则
                若「或者」
                  于（「大于」于「数」于「一六」）
                  于（「小于」于「数」于（「减」于「零」于「一六」））则
                    「可无」
                否则
                  「可有」于（（「栈填二元」于「术名」于（「甲」中「零」）于（「乙」中「零」））与「数」与「费」）
        ）
    ）
也。

「验栈填方向」乃
  化「栈表示签」而
  化「正则函数」而
  化「整数」而
  化「整数」而
  化「整数」而
  「或可有」于「栈填证」
也。
「验栈填方向」者会「签」而会「函」而会「组」而会「上」而会「扫」而
  鉴（「验双步形」于「函」于「上」于「扫」）而
    有「可无」则「可无」
    或有（「可有」于「进」）则（
      若「非」于（鉴（「进」中「二」）而
      有「正则单元」则「阳」
      或有「其他」则「阴」）则
        「可无」
      否则
        虑「表」者
          「新数组引用」授以「栈填已知」于「可无」于（「函」中「四」）
        而
        虑「无」者
          「态射」授以「整数」授以「有」
          于（「函」中「二」）
          于（会「号」
  而
  若「等于」于「号」于「组」则
    「元」
  否则
    「写数组引用」授以「栈填已知」
    于「表」
    于「号」
    于（「可有」
      于（（「栈填原子」于（「正则局部」于「号」））与（
        若「等于」于「号」于「扫」则「一」否则「零」）与「一」）））
        而
        虑「所写」者「新引用」授以「栈填已知」于「可无」
        而
        虑「守参」者
          （化（「列」于「正则原子」）而「爻」也会「实」而
              若「非」于（「等于」于（「长度」授以「正则原子」于「实」）于（「长度」授以「整数」于（「函」中「二」）））
              则
                「阴」
              否则
                「全部符合」授以「整数」
                于（会「位」
                而
  虑「形」者「第N个」授以「整数」于「位」于（「函」中「二」）而
  若「等于」于「形」于「扫」则
    「阳」
  否则
    鉴（「第N个」授以「正则原子」于「位」于「实」）而
      有（「正则局部」于「实号」）则
        「等于」于「形」于「实号」
      或有「其他」则「阴」）
      于（「整数范围」于「零」于（「长度」授以「正则原子」于「实」））
          ）而
        递归虑「逐」其化（「列」于「正则指令」）而「爻」者会「诸令」而
          鉴「诸令」而
            有（「列」【「正则运算」于「号」于「类」于「正则调用」于（「缀」于（「正则函数引用」于「名」）于「实」）】）
            则
              「且」
                于（「串相等」于「名」于（「函」中「零」））
                于（「守参」于「实」）
            或有（「缀」于（「正则运算」于「号」于「类」于（「正则原语」于「术名」）于「实」）于「余」）则
              若「串相等」于「术名」于『豫言_写入引用数组』则（
                鉴「实」而
                  有（「列」【「值」，「正则局部」于「索号」，「正则局部」于「组号」】）则
                    若「非」于（「且」于（「等于」于「索号」于「扫」）于（「等于」于「组号」于「组」））则
                      「阴」
                    否则
                      鉴（「读引用」于「所写」）而
                        有（「可有」于「旧」）则「阴」
                        或有「可无」则（
                          鉴（「取栈填式」于「表」于「值」）而
                            有「可无」则「阴」
                            或有（「可有」于「式」）则
                              （虑「无」者「写引用」于「所写」于（「可有」于「式」）而「逐」于「余」）
                        ）
                        或有「其他」则「阴」
              ）否则（
                鉴「实」而
                  有（「列」【「甲」，「乙」】）则（
                    鉴（「合栈填式」于「术名」于（「取栈填式」于「表」于「甲」）于（「取栈填式」于「表」于「乙」））而
                      有「可无」则「阴」
                      或有（「可有」于「式」）则（
                        虑「无」者
                          「写数组引用」授以「栈填已知」
                          于「表」于「号」
                          于（「可有」于「式」）
                        而
                        「逐」于「余」
                      ）
                  ）
                  或有「其他」则「阴」
              ）
            或有「其他」则
              「阴」
        而
        虑「合」者鉴（「进」中「一」）而
          有（「正则段」于「诸令」于「终」）则
            「逐」于「诸令」
        而
        若「非」于「合」则
          「可无」
        否则
          鉴（「读引用」于「所写」）而
            有「可无」则「可无」
            或有（「可有」于「式」）则
              「可有」于（「组」与「上」与「扫」与（「式」中「零」）与（「式」中「一」））
    ）
也。

「验栈填充」乃化「栈表示签」而化「正则函数」而「或可有」于「栈填证」也。
「验栈填充」者会「签」而会「函」而
  若「非」于（「且」
    于（「等于」于（「签」中「一」）于「三」）
    于（「等于」于（「长度」授以「整数」于（「签」中「零」））于（「长度」授以「整数」于（「函」中「二」））））则
      「可无」
  否则
    若「非」于（「全部符合」授以「整数」
      于（会「类」而「或者」于（「等于」于「类」于「一」）于（「等于」于「类」于「四」））
      于（「签」中「零」））则
        「可无」
    否则
      虑「组位」者
        「滤」授以「整数」
        于（会「位」而「等于」于（「第N个」授以「整数」于「位」于（「签」中「零」））于「四」）
        于（「整数范围」于「零」于（「长度」授以「整数」于（「签」中「零」）））而
      鉴「组位」而
        有（「列」【「位」】）则（
          虑「组」者
            「第N个」授以「整数」于「位」于（「函」中「二」）而
          鉴（「函」中「三」）而
            有（「正则段」
              于（「缀」
                于（「正则运算」
                  于「号」
                  于「类」
                  于（「正则原语」于『豫言_整数相等』）
                  于（「列」【「正则局部」于「甲」，「正则局部」于「乙」】））
                  于「余」）于「终」）则（
              若「或者」
                于（「等于」于「甲」于「组」）
                于（「等于」于「乙」于「组」）则
                  「可无」
              否则
                鉴（「验栈填方向」于「签」于「函」于「组」于「甲」于「乙」）而
                  有（「可有」于「证」）则「可有」
                    于「证」
                  或有「可无」则
                    「验栈填方向」
                      于「签」于「函」于「组」于「乙」于「甲」
            ）
            或有「其他」则「可无」
        ）
        或有「其他」则「可无」
也。
