theory Noninterference

lemma sub_big_steps_not_PSched_confidentiality_part:
  "\<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s;
    (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t;
     (s, t) \<in> uwr PSched; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;
     u \<noteq> PSched;     (part s, u) \<in> policyFlows (pasPolicy initial_aag);
     system.reachable (big_step_ADT_A_if utf) s0 s;
     system.reachable (big_step_ADT_A_if utf) s0 t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow>
  (s', t') \<in> uwr u \<and> (s', t') \<in> uwr PSched \<and> (s', t') \<in> uwr (part s) \<and>
   part s' = part s" apply (frule_tac s=s and t=t and X="\<lambda>s t. part s \<noteq> PSched \<and> ((s, t) \<in> uwr PSched \<and>
                                          (s, t) \<in> uwr (part s) \<and> (s, t) \<in> uwr u \<and>
                                          system.reachable (ADT_A_if utf) s0 s \<and>
                                          system.reachable (ADT_A_if utf) s0 t)"
               in relation_preserved_across_sub_big_steps) apply (simp add: small_step_reachable del: split_paired_All)+ apply (intro impI allI | elim conjE)+ apply (rename_tac sx tx sx' tx') apply (subgoal_tac "part sx = part s \<and> part sx' = part s") apply (frule_tac u=u and s=sx and t=tx in small_Step_confidentiality_part_not_PSched) apply (simp add: small_step_reachable)+ apply (fastforce intro: Step_system.reachable_Step[OF ADT_A_if_Step_system _ Step_ADT_A_if'',
                                                      rotated]) apply (elim exE conjE) apply (frule schedIncludesCurrentDom) apply (frule_tac s'=sx in partitionIntegrity_part_unchanged[OF sub_big_steps_partitionIntegrity]) apply (blast intro: big_step_R_rtranclp) apply (erule small_step_reachable) apply assumption apply assumption apply assumption apply (rule conjI, assumption) apply (rule partitionIntegrity_part_unchanged[OF sub_big_steps_partitionIntegrity]) apply assumption apply (blast intro: big_step_R_rtranclp) apply (erule small_step_reachable) apply assumption apply assumption apply (rule sub_big_steps_not_PSched) apply assumption apply (blast intro: big_step_R_rtranclp) apply assumption apply (frule_tac s'=s' in partitionIntegrity_part_unchanged[OF sub_big_steps_partitionIntegrity]) apply (blast intro: big_step_R_rtranclp) apply (erule small_step_reachable) apply assumption apply assumption apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> (?t', ?as') \<in> sub_big_steps (ADT_A_if utf) big_step_R t
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> part s \<noteq> PSched \<and> uwr2 s PSched t \<and> uwr2 s (part s) t \<and> uwr2 s u t \<and> system.reachable (ADT_A_if utf) s0 s \<and> system.reachable (ADT_A_if utf) s0 t
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> ?as' = as
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> \<forall>sa ta sa' ta'. (part sa \<noteq> PSched \<and> uwr2 sa PSched ta \<and> uwr2 sa (part sa) ta \<and> uwr2 sa u ta \<and> system.reachable (ADT_A_if utf) s0 sa \<and> system.reachable (ADT_A_if utf) s0 ta) \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sa', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (sa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> part sa' \<noteq> PSched \<and> uwr2 sa' PSched ta' \<and> uwr2 sa' (part sa') ta' \<and> uwr2 sa' u ta' \<and> system.reachable (ADT_A_if utf) s0 sa' \<and> system.reachable (ADT_A_if utf) s0 ta'
 5. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched ?t' \<and> uwr2 s' (part s') ?t' \<and> uwr2 s' u ?t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 ?t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> \<forall>sa ta sa' ta'. part sa \<noteq> PSched \<and> uwr2 sa PSched ta \<and> uwr2 sa (part sa) ta \<and> uwr2 sa u ta \<and> system.reachable (ADT_A_if utf) s0 sa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sa', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (sa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> part sa' \<noteq> PSched \<and> uwr2 sa' PSched ta' \<and> uwr2 sa' (part sa') ta' \<and> uwr2 sa' u ta' \<and> system.reachable (ADT_A_if utf) s0 sa' \<and> system.reachable (ADT_A_if utf) s0 ta'
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sa ta sa' ta'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sa \<noteq> PSched; uwr2 sa PSched ta; uwr2 sa (part sa) ta; uwr2 sa u ta; system.reachable (ADT_A_if utf) s0 sa; system.reachable (ADT_A_if utf) s0 ta; \<exists>bs. (sa, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sa', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (ta, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sa, sa') \<in> data_type.Step (ADT_A_if utf) (); (ta, ta') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part sa' \<noteq> PSched \<and> uwr2 sa' PSched ta' \<and> uwr2 sa' (part sa') ta' \<and> uwr2 sa' u ta' \<and> system.reachable (ADT_A_if utf) s0 sa' \<and> system.reachable (ADT_A_if utf) s0 ta'
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched \<and> uwr2 sx' PSched tx' \<and> uwr2 sx' (part sx') tx' \<and> uwr2 sx' u tx' \<and> system.reachable (ADT_A_if utf) s0 sx' \<and> system.reachable (ADT_A_if utf) s0 tx'
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (3 subgoals):
 1. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched \<and> uwr2 sx' PSched tx' \<and> uwr2 sx' (part sx') tx' \<and> uwr2 sx' u tx' \<and> system.reachable (ADT_A_if utf) s0 sx' \<and> system.reachable (ADT_A_if utf) s0 tx'
 2. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (12 subgoals):
 1. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> (tx, ?t'18 sx tx sx' tx') \<in> data_type.Step (ADT_A_if utf) ()
 2. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> uwr2 sx PSched tx
 3. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> uwr2 sx (part sx) tx
 4. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> uwr2 sx u tx
 5. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 sx
 6. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 tx
 7. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> policy2 (part sx) u
 8. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 9. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s\<rbrakk> \<Longrightarrow> u \<noteq> PSched
 10. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s; uwr2 sx' u (?t'18 sx tx sx' tx') \<and> uwr2 sx' PSched (?t'18 sx tx sx' tx') \<and> uwr2 sx' (part sx) (?t'18 sx tx sx' tx')\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched \<and> uwr2 sx' PSched tx' \<and> uwr2 sx' (part sx') tx' \<and> uwr2 sx' u tx' \<and> system.reachable (ADT_A_if utf) s0 sx' \<and> system.reachable (ADT_A_if utf) s0 tx'
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part s) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); part sx = part s \<and> part sx' = part s; uwr2 sx' u tx' \<and> uwr2 sx' PSched tx' \<and> uwr2 sx' (part s) tx'\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 sx' \<and> system.reachable (ADT_A_if utf) s0 tx'
 2. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx'. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; \<exists>bs. (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t \<and> (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (7 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 6. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 7. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (6 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 5. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 6. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (5 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 5. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (4 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (3 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t\<rbrakk> \<Longrightarrow> part sx \<noteq> PSched
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx = part s \<and> part sx' = part s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' = part s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (7 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> (sx', ?as58 sx tx sx' tx' bs cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 6. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 7. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (6 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 6. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (5 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 5. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (4 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (3 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part sx' \<noteq> PSched
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (4 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> (sx', ?blah72 sx tx sx' tx' bs cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R (?s72 sx tx sx' tx' bs cs)
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 (?s72 sx tx sx' tx' bs cs)
 3. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part (?s72 sx tx sx' tx' bs cs) \<noteq> PSched
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (3 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<And>sx tx sx' tx' bs cs. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part sx \<noteq> PSched; uwr2 sx PSched tx; uwr2 sx (part sx) tx; uwr2 sx u tx; system.reachable (ADT_A_if utf) s0 sx; system.reachable (ADT_A_if utf) s0 tx; (sx, sx') \<in> data_type.Step (ADT_A_if utf) (); (tx, tx') \<in> data_type.Step (ADT_A_if utf) (); (sx, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (sx', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (tx, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; (sx', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; part s = part t; part sx = part s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 6. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 5. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 4. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 3. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (t', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R t; uwr2 s PSched t; uwr2 s (part s) t; uwr2 s u t; u \<noteq> PSched; policy2 (part s) u; reachable s; reachable t; part s \<noteq> PSched; part s' \<noteq> PSched \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s') t' \<and> uwr2 s' u t' \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 t'; part s' = part s\<rbrakk> \<Longrightarrow> uwr2 s' u t' \<and> uwr2 s' PSched t' \<and> uwr2 s' (part s) t' \<and> part s' = part s proof (prove)
goal:
No subgoals!