[STATEMENT]
lemma refine_basic:
  "\<lbrakk> init Tc \<subseteq> R``(init Ta); {R} (trans Ta), (trans Tc) {> R} \<rbrakk>
  \<Longrightarrow> PO_refines R Ta Tc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>init Tc \<subseteq> R `` init Ta; {R} TS.trans Ta, TS.trans Tc {> R}\<rbrakk> \<Longrightarrow> PO_refines R Ta Tc
[PROOF STEP]
by (simp add: PO_refines_def)