Level: Lib Thy Top: 1
Hypotheses:

  1. E :

  2. T :

  3. L :

  4. Ach : Signature(E;T;L)

  5. Tor : Signature(E;T;L)

  6. Run(E;T;L;Ach)

  7. Run(E;T;L;Tor)

  8. Ach Tor

  9. Ach.t1 Tor.t1

  10. IVP(Ach)

  11. TEP

  12. Ach || Tor

  13. t0 = t0

  14. Tor.t1 < Ach.t1

Conclusion:

False

Applied Tactic: Unfold `sign_t_ref_rel` 9 THEN Reduce 9 THEN Unfold `run` 6 THEN D 6 THEN D 7 THEN Thin 8 THEN Unfol d `ir_linorder` 7 THEN D 7 THEN Unfold `ir_order` 8 THEN D 8 THEN Unfold `irrefl` 8 THEN With Ach.t1 (D 8) THENA Auto THEN Unfold `trans` 8 THEN InstHyp [Ach.t1; Tor.t1; Ach.t1 ] 8 THEN Auto THEN D 11 THEN Auto THEN RWH (RevHypC 11) 16 THEN Auto
Generated subgoals:

None