2.2代数、基调和项 项的例子 -0,0+1∈Terw②N☑) -0+x∈Termsat(②N,),其中T={x:nat,…} 代数项中无约束变元 -[NWx]M就是简单地把M中x的每个出现都用N代替 记号 T,x:s'=TU{x:s 。引理2.1 若M∈Terms∑，T,x:s'且N∈Terms'2,),那么 [N/x]M∈Ters(,T 证明按Ters∑，)中项的结构进行归纳2.2 代数、基调和项 • 项的例子 – 0, 0 + 1 Termsnat (N , ) – 0 + x  Termsnat (N , )，其中 =  x : nat, … • 代数项中无约束变元 – NxM就是简单地把M中x的每个出现都用N代替 • 记号 , x : s =    x : s • 引理2.1 – 若MTermss (, , x : s)且NTermss (, )，那么 NxMTermss (, ) – 证明 按Termss (, )中项的结构进行归纳