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 THEN Assert Ach Tor THENA Auto THEN Unfold `race` 12 THEN Auto THEN D 14
Generated subgoals:

1. False

2. False