固有类（在本项目意义上的循环自嵌套结构）以终余代数 νF ≅ F(νF) 为数学家园。

在反基础公理（AFA）下，（平坦）方程组有唯一解（Aczel 解引理）；本原方程以此取代公理命题。

以互模拟为身份判据；有限情形可经 Paige–Tarjan 分划细化判定。

旋机矢列演算 RSC₀ 健全且完备。