---

{ [t:]. [voters,clients:Id List].
    (sc-program(t;voters;clients)  E#Program) }

{ Proof }

---

Definitions occuring in Statement :  sc-program: sc-program(t;voters;clients),  esharp-program: E#Program,  Id: Id,  nat: ,  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  esharp-program: E#Program,  sc-program: sc-program(t;voters;clients)
Lemmas :  sc-env_wf,  sc-rules_wf,  Id_wf,  nat_wf

---

\mforall{}[t:\mBbbN{}].  \mforall{}[voters,clients:Id  List].    (sc-program(t;voters;clients)  \mmember{}  E\#Program)


Date html generated: 2011_08_17-PM-06_34_01
Last ObjectModification: 2011_06_18-AM-11_57_53

Home Index