theory Noninterference

lemma confidentiality_part_not_PSched:
  "\<lbrakk>(s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) ();
    (t, t') \<in> Simulation.Step (big_step_ADT_A_if utf) ()\<rbrakk> \<Longrightarrow>
    (s, t) \<in> uwr PSched \<and> (s, t) \<in> uwr (part s) \<and> (s, t) \<in> uwr u \<and>
    system.reachable (big_step_ADT_A_if utf) s0 s \<and>
    system.reachable (big_step_ADT_A_if utf) s0 t \<and>
    (part s, u) \<in> policyFlows (pasPolicy initial_aag) \<and>
    part s \<noteq> PSched \<and> u \<noteq> PSched \<longrightarrow>
   (s', t') \<in> uwr u" apply (simp add: Step_big_step_ADT_A_if) apply (erule big_steps.induct)+ apply (intro impI | elim conjE)+ apply (subgoal_tac "asa = as") apply (drule_tac X="\<lambda>s t. (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 \<and>
    (part s, u) \<in> policyFlows (pasPolicy initial_aag) \<and>
    part s \<noteq> PSched" in relation_preserved_across_sub_big_steps) apply assumption apply (fastforce simp: small_step_reachable) apply assumption apply (simp del: split_paired_All) apply (thin_tac "(x,y) \<in> data_type.Step A b" for x y A b
         | thin_tac "big_step_R a b" for a b)+ apply (intro allI impI | elim conjE)+ apply (rename_tac x_s x_t x_s' x_t') apply (subgoal_tac "part x_s' = part x_s") apply (simp del: split_paired_All) apply (frule_tac u=u and s=x_s and t=x_t 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) apply (rule trans) apply (rule partitionIntegrity_part_unchanged[OF sub_big_steps_partitionIntegrity]) apply blast apply (erule big_step_R_rtranclp) apply (erule small_step_reachable) apply simp+ apply (rule sub_big_steps_not_PSched) apply blast apply (erule big_step_R_rtranclp) apply simp apply (rule sym) apply (rule partitionIntegrity_part_unchanged[OF sub_big_steps_partitionIntegrity]) apply blast apply (erule big_step_R_rtranclp) apply (erule small_step_reachable) apply (simp+)[3] apply (elim conjE) apply simp apply (drule_tac s=s' and t=s'a and u=u in small_Step_confidentiality_part_not_PSched) apply (simp+)[10] apply (fastforce dest: non_PSched_steps_run_in_lock_step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); (t, t') \<in> data_type.Step (big_step_ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> uwr2 s PSched t \<and> uwr2 s (part s) t \<and> uwr2 s u t \<and> reachable s \<and> reachable t \<and> policy2 (part s) u \<and> part s \<noteq> PSched \<and> u \<noteq> PSched \<longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); (t, t') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap ()\<rbrakk> \<Longrightarrow> uwr2 s PSched t \<and> uwr2 s (part s) t \<and> uwr2 s u t \<and> reachable s \<and> reachable t \<and> policy2 (part s) u \<and> part s \<noteq> PSched \<and> u \<noteq> PSched \<longrightarrow> uwr2 s' u t' proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa])\<rbrakk> \<Longrightarrow> uwr2 s PSched sa \<and> uwr2 s (part s) sa \<and> uwr2 s u sa \<and> reachable s \<and> reachable sa \<and> policy2 (part s) u \<and> part s \<noteq> PSched \<and> u \<noteq> PSched \<longrightarrow> uwr2 t u ta proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> uwr2 t u ta
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (6 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> (?t'27 s' as s t a s'a asa sa ta aa, ?as'27 s' as s t a s'a asa sa ta aa) \<in> sub_big_steps (ADT_A_if utf) big_step_R (?t27 s' as s t a s'a asa sa ta aa)
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> uwr2 s PSched (?t27 s' as s t a s'a asa sa ta aa) \<and> uwr2 s (part s) (?t27 s' as s t a s'a asa sa ta aa) \<and> uwr2 s u (?t27 s' as s t a s'a asa sa ta aa) \<and> system.reachable (ADT_A_if utf) s0 s \<and> system.reachable (ADT_A_if utf) s0 (?t27 s' as s t a s'a asa sa ta aa) \<and> policy2 (part s) u \<and> part s \<noteq> PSched
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> ?as'27 s' as s t a s'a asa sa ta aa = as
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa taa sa' ta'. (uwr2 saa PSched taa \<and> uwr2 saa (part saa) taa \<and> uwr2 saa u taa \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 taa \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched) \<and> (\<exists>bs. (saa, 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. (taa, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R (?t27 s' as s t a s'a asa sa ta aa) \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (taa, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched (?t'27 s' as s t a s'a asa sa ta aa) \<and> uwr2 s' (part s') (?t'27 s' as s t a s'a asa sa ta aa) \<and> uwr2 s' u (?t'27 s' as s t a s'a asa sa ta aa) \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 (?t'27 s' as s t a s'a asa sa ta aa) \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (5 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> uwr2 s PSched sa \<and> uwr2 s (part s) sa \<and> uwr2 s u sa \<and> system.reachable (ADT_A_if utf) s0 s \<and> system.reachable (ADT_A_if utf) s0 sa \<and> policy2 (part s) u \<and> part s \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> asa = as
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa ta sa' ta'. (uwr2 saa PSched ta \<and> uwr2 saa (part saa) ta \<and> uwr2 saa u ta \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched) \<and> (\<exists>bs. (saa, 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 sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> asa = as
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa ta sa' ta'. (uwr2 saa PSched ta \<and> uwr2 saa (part saa) ta \<and> uwr2 saa u ta \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched) \<and> (\<exists>bs. (saa, 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 sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa ta sa' ta'. (uwr2 saa PSched ta \<and> uwr2 saa (part saa) ta \<and> uwr2 saa u ta \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched) \<and> (\<exists>bs. (saa, 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 sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa ta sa' ta'. uwr2 saa PSched ta \<and> uwr2 saa (part saa) ta \<and> uwr2 saa u ta \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched \<and> (\<exists>bs. (saa, 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 sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as\<rbrakk> \<Longrightarrow> \<forall>saa ta sa' ta'. uwr2 saa PSched ta \<and> uwr2 saa (part saa) ta \<and> uwr2 saa u ta \<and> system.reachable (ADT_A_if utf) s0 saa \<and> system.reachable (ADT_A_if utf) s0 ta \<and> policy2 (part saa) u \<and> part saa \<noteq> PSched \<and> (\<exists>bs. (saa, 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 sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s) \<and> (saa, sa') \<in> data_type.Step (ADT_A_if utf) () \<and> (ta, ta') \<in> data_type.Step (ADT_A_if utf) () \<longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta saa taa sa' ta'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 saa PSched taa; uwr2 saa (part saa) taa; uwr2 saa u taa; system.reachable (ADT_A_if utf) s0 saa; system.reachable (ADT_A_if utf) s0 taa; policy2 (part saa) u; part saa \<noteq> PSched; \<exists>bs. (saa, 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. (taa, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (sa', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (saa, sa') \<in> data_type.Step (ADT_A_if utf) (); (taa, ta') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 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> policy2 (part sa') u \<and> part sa' \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> uwr2 x_s' PSched x_t' \<and> uwr2 x_s' (part x_s') x_t' \<and> uwr2 x_s' u x_t' \<and> system.reachable (ADT_A_if utf) s0 x_s' \<and> system.reachable (ADT_A_if utf) s0 x_t' \<and> policy2 (part x_s') u \<and> part x_s' \<noteq> PSched
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> uwr2 x_s' PSched x_t' \<and> uwr2 x_s' (part x_s') x_t' \<and> uwr2 x_s' u x_t' \<and> system.reachable (ADT_A_if utf) s0 x_s' \<and> system.reachable (ADT_A_if utf) s0 x_t' \<and> policy2 (part x_s') u \<and> part x_s' \<noteq> PSched
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part x_s' = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> uwr2 x_s' PSched x_t' \<and> uwr2 x_s' (part x_s) x_t' \<and> uwr2 x_s' u x_t' \<and> system.reachable (ADT_A_if utf) s0 x_s' \<and> system.reachable (ADT_A_if utf) s0 x_t'
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part x_s' = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (13 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> (x_t, ?t'74 as s s'a asa sa x_s x_t x_s' x_t') \<in> data_type.Step (ADT_A_if utf) ()
 2. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> uwr2 x_s PSched x_t
 3. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> uwr2 x_s (part x_s) x_t
 4. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> uwr2 x_s u x_t
 5. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 x_s
 6. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 x_t
 7. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> policy2 (part x_s) u
 8. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> part x_s \<noteq> PSched
 9. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s\<rbrakk> \<Longrightarrow> u \<noteq> PSched
 10. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s; uwr2 x_s' u (?t'74 as s s'a asa sa x_s x_t x_s' x_t') \<and> uwr2 x_s' PSched (?t'74 as s s'a asa sa x_s x_t x_s' x_t') \<and> uwr2 x_s' (part x_s) (?t'74 as s s'a asa sa x_s x_t x_s' x_t')\<rbrakk> \<Longrightarrow> uwr2 x_s' PSched x_t' \<and> uwr2 x_s' (part x_s) x_t' \<and> uwr2 x_s' u x_t' \<and> system.reachable (ADT_A_if utf) s0 x_s' \<and> system.reachable (ADT_A_if utf) s0 x_t'
A total of 13 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); part x_s' = part x_s; uwr2 x_s' u x_t' \<and> uwr2 x_s' PSched x_t' \<and> uwr2 x_s' (part x_s) x_t'\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 x_s' \<and> system.reachable (ADT_A_if utf) s0 x_t'
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part x_s' = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t'. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; \<exists>bs. (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; \<exists>cs. (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> part x_s' = part x_s
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' = part x_s
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' = ?s96 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> ?s96 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (9 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> (x_s', ?as100 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs)
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs)
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs)
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs) \<noteq> PSched
 5. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs) \<noteq> PSched
 6. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' \<noteq> PSched
 7. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part (?s99 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs) = part x_s
 8. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 9. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (8 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' \<noteq> PSched
 6. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 7. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 8. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (7 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' \<noteq> PSched
 5. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 7. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (6 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s' \<noteq> PSched
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (6 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> (x_s', ?blah152 as s s'a asa sa x_s x_t x_s' x_t' bs cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R (?s152 as s s'a asa sa x_s x_t x_s' x_t' bs cs)
 2. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 (?s152 as s s'a asa sa x_s x_t x_s' x_t' bs cs)
 3. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part (?s152 as s s'a asa sa x_s x_t x_s' x_t' bs cs) \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (5 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (4 subgoals):
 1. \<And>as s s'a asa sa x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s = part x_s
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s = part s
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 3. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (8 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> (x_s, ?as203 s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 6. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s \<noteq> PSched
 7. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 8. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (7 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 s
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 5. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s \<noteq> PSched
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 7. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (6 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 4. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s \<noteq> PSched
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 6. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (5 subgoals):
 1. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 2. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part s \<noteq> PSched
 3. \<And>s' as s t s'a asa sa ta x_s x_t x_s' x_t' bs cs. \<lbrakk>(s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 x_s PSched x_t; uwr2 x_s (part x_s) x_t; uwr2 x_s u x_t; system.reachable (ADT_A_if utf) s0 x_s; system.reachable (ADT_A_if utf) s0 x_t; policy2 (part x_s) u; part x_s \<noteq> PSched; (x_s, x_s') \<in> data_type.Step (ADT_A_if utf) (); (x_t, x_t') \<in> data_type.Step (ADT_A_if utf) (); (x_s, bs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s \<and> (x_s', bs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (x_t, cs) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa \<and> (x_s', cs @ [()]) \<in> sub_big_steps (ADT_A_if utf) big_step_R s\<rbrakk> \<Longrightarrow> part x_s \<noteq> PSched
 4. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 5. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a \<and> uwr2 s' (part s') s'a \<and> uwr2 s' u s'a \<and> system.reachable (ADT_A_if utf) s0 s' \<and> system.reachable (ADT_A_if utf) s0 s'a \<and> policy2 (part s') u \<and> part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (2 subgoals):
 1. \<And>s' as s t s'a asa sa ta. \<lbrakk>(s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 t u ta
 2. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (11 subgoals):
 1. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> (s'a, ?t'263 s' as s t s'a asa sa ta) \<in> data_type.Step (ADT_A_if utf) ()
 2. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' PSched s'a
 3. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' (part s') s'a
 4. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> uwr2 s' u s'a
 5. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s'
 6. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> system.reachable (ADT_A_if utf) s0 s'a
 7. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> policy2 (part s') u
 8. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> part s' \<noteq> PSched
 9. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched\<rbrakk> \<Longrightarrow> u \<noteq> PSched
 10. \<And>s' as s t s'a asa sa ta. \<lbrakk>big_step_R s t; (s'a, as) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched; asa = as; uwr2 s' PSched s'a; uwr2 s' (part s') s'a; uwr2 s' u s'a; system.reachable (ADT_A_if utf) s0 s'; system.reachable (ADT_A_if utf) s0 s'a; policy2 (part s') u; part s' \<noteq> PSched; uwr2 t u (?t'263 s' as s t s'a asa sa ta) \<and> uwr2 t PSched (?t'263 s' as s t s'a asa sa ta) \<and> uwr2 t (part s') (?t'263 s' as s t s'a asa sa ta)\<rbrakk> \<Longrightarrow> uwr2 t u ta
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a s'a asa sa ta aa. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a]); (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) aa; big_step_R sa ta; () = big_step_evmap (asa @ [aa]); uwr2 s PSched sa; uwr2 s (part s) sa; uwr2 s u sa; reachable s; reachable sa; policy2 (part s) u; part s \<noteq> PSched; u \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal:
No subgoals!