把执行步骤elaboration为proof[#86]

重放检查证书中的每条边能否被规则目录复现；Proof IR再把声明式规则实例、其定理依据和使用的前提引用连接起来。逐步elaboration会保留每一步的检查状态，即使部分算法步骤暂时没有可检查的定理：

Proof IR是等式推理的表示，节点包含前提引用、规则实例、反身、对称、传递，以及把等式提升到子表达式上下文中的congruence。elaboration把证书的规则边映射到这些节点，并检查规则规范和必要前提；只有所有步骤都有已检查的规则依据时，才会生成整条链的proof。因此重放通过描述证书边可被Grove的规则实现复现；Proof IR通过则进一步说明每条边都有已检查的数学依据。

elaboration: unsupportednchecked proof available: #fnstep evidence: ((0 differentiate-sum unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (1 differentiate-power unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (2 differentiate-product unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (3 differentiate-constant unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (4 differentiate-variable unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (5 differentiate-variable unsupported () unsupported ("the rule is outside the rational-polynomial checker")) (6 multiply-one semantically-checked () checked ()) (7 zero-multiply semantically-checked () checked ()) (8 zero-add semantically-checked () checked ()) (9 normalize-scalar unsupported () unsupported ("rule has no fixed RuleSpec to elaborate")))

本例的整体状态是unsupported：幂法则、乘积法则和求导规则目前还没有由标量代数检查器证明；归一化过程中的过程式规则也没有固定的RuleSpec。报告仍会标出已独立检查的代数步骤，例如multiply-one、zero-multiply和zero-add。每条已检查步骤的rule-instance都引用规则名，checker会重新检查其RuleSpec定理；步骤所需的前提则以proof premise节点引用derivation保存的假设。由于这条执行轨迹含有尚未证明的算法步骤，报告不会生成整条链的checked proof。