---

{ [t,x:Name]. [pre:pi_prefix()].  (prefix-replace(t;x;pre)  pi_prefix()) }

{ Proof }

---

Definitions occuring in Statement :  prefix-replace: prefix-replace(t;x;pre),  pi_prefix: pi_prefix(),  name: Name,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  prefix-replace: prefix-replace(t;x;pre),  let: let,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2]
Lemmas :  pi_prefix_ind_wf,  pisend_wf,  ifthenelse_wf,  name_eq_wf,  pi_prefix_wf,  name_wf

---

\mforall{}[t,x:Name].  \mforall{}[pre:pi\_prefix()].    (prefix-replace(t;x;pre)  \mmember{}  pi\_prefix())


Date html generated: 2011_08_17-PM-06_48_48
Last ObjectModification: 2011_06_18-PM-12_21_26

Home Index