Theorem. 规则归纳法

设 $𝑃 (𝑡, 𝑡^{'})$ 是关于一对词项的性质．若对一步规约的每条规则实例，假定前提中的各个转移都满足 $𝑃$ 后，能够证明结论中的转移也满足 $𝑃$ ，则 $𝑃$ 对所有可推导的 $𝑡 ⟶ 𝑡^{'}$ 成立．

无前提的规则是基准情况，须直接验证其结论满足 $𝑃$ ；有前提的规则是归纳情况，可对前提的子推导使用归纳假设．这就是规则归纳法，也可理解为对有限推导树作结构归纳，其归纳对象是整条可推导的转移判断 $𝑡 ⟶ 𝑡^{'}$ ．

Proof.

令

𝑅 = {(𝑡, 𝑡^{'}) | 𝑡 ⟶ 𝑡^{'} 且 𝑃 (𝑡, 𝑡^{'})}

．假设恰好说明

𝑅

对十条规则封闭．

⟶

是对规则封闭的最小关系，所以

⟶ \subseteq 𝑅

．

∎

References