1258 value "sublists [a,b,cThe]"

  1259 

  1260 theorem bound_priority_inversion:

  1261   "card { s' @ s | s'. s' \<in> set t \<and>  th \<notin> running (s'@s) } \<le> 

  1262           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"

  1263    (is "?L \<le> ?R")

  1264 proof - 

  1265   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"

  1266   from occs_le[of ?Q t] 

  1267   have "?L \<le> (1 + length t) - occs ?Q t" by simp

  1268   also have "... \<le> ?R"

  1269   proof -

  1270     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))

  1271               \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")

  1272     proof -

  1273       have "?L1 = length (actions_of {th} t)" using actions_split by arith

  1274       also have "... \<le> ?R1" using actions_th_occs by simp

  1275       finally show ?thesis .

  1276     qed            

  1277     thus ?thesis by simp

  1278   qed

  1279   finally show ?thesis .

  1280 qed

  1281