example. 搜索规则路径[#89]

有时作者知道想要的结论，却不想手工写所有步骤：

Search finished: 1 derivation found with these rules and assumptions.

命令从左侧源项搜索到目标项，并展示找到的证书。这个最小例子找到从形式导数到1的规则路径；上面的多项式则使用确定性的求导pass。通用搜索面对分支较多的项可能触及状态上限，搜索停止不等同于数学上的不可达证明。