Up

3.5.3.2 証明の例

---

πに ａ→ｂ が属するとき，記号列Φ： Ｌφａφ1Ｒ （Ｌは ＾ あるいは /，Ｒは ＾txt/ あるいは /──但し，/ はテクストの端を表わすメタ記号）に対して， Φ　→　Φφｂφ1 が推論規則になる。（ここで，ａ,ｂ,Φ,Ｌ,Ｒはメタ記号。） 　そこで例えば，記号列Ｘ,ｓ,ｔ,Ｙに対するテクストＸ＾ｓａｔ＾Ｙからは，変形： によって，テクストＸ＾ｓａｔ＾Ｙ＾ｓｂｔが演繹される。但し，　は， によって定義される代入枠 ｛(txt,Ｘ),(φ,ａ),(φ1,ｂ),(txt1,Ｙ)｝ の下の直接代入 ｛txt→Ｘ,φ→ｓ,φ1→ｔ,txt→Ｙ｝ である。