Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

E,T,L:. Ach,Tor:Signature(E;T;L). (Run(E;T;L;Ach) Run(E;T;L;Tor)) Ach Tor Ach.t1 Tor.t1 IVP(Ach) TEP

Applied Tactic: Auto THEN D 0 THENW Auto
Generated subgoals:

1. False