None

Conclusion:

E,T,L:. Ach,Tor:Signature(E;T;L). u,w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 u u < w (w Ach.t1 w Tor.t1) (Ach.d u) < (Tor.d u) Def u Def w (v:T. u < v v < w Def v)

1. v:T. u < v v < w Def v