[STATEMENT]
lemma PO_m1_inv0_fin_trans [iff]:
  "{m1_inv0_fin} trans m1 {> m1_inv0_fin}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m1_inv0_fin} TS.trans m1 {> m1_inv0_fin}
[PROOF STEP]
by (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv0_finI)