diff --git a/thys/Factored_Transition_System_Bounding/AcycSspace.thy b/thys/Factored_Transition_System_Bounding/AcycSspace.thy
--- a/thys/Factored_Transition_System_Bounding/AcycSspace.thy
+++ b/thys/Factored_Transition_System_Bounding/AcycSspace.thy
@@ -1,906 +1,900 @@
 theory AcycSspace
   imports
     FactoredSystem
     ActionSeqProcess
     SystemAbstraction
     Acyclicity
     FmapUtils
 begin
 
 
 section "Acyclic State Spaces"
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 \<comment> \<open>NOTE type for `max` had to be fixed to natural number maximum (due to problem with loose
 typing).\<close>
 value "(state_successors (prob_proj PROB vs))"
 definition S
   where "S vs lss PROB s \<equiv> wlp
     (\<lambda>x y. y \<in> (state_successors (prob_proj PROB vs) x))
     (\<lambda>s. problem_plan_bound (snapshot PROB s))
     (max :: nat \<Rightarrow> nat \<Rightarrow> nat) (\<lambda>x y. x + y + 1) s lss
   "
 
 \<comment> \<open>NOTE name shortened.\<close>
 \<comment> \<open>NOTE using `fun` because of multiple defining equations.\<close>
 fun vars_change where
   "vars_change [] vs s = []"
 | "vars_change (a # as) vs s = (if fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s
     then state_succ s a # vars_change as vs (state_succ s a)
     else vars_change as vs (state_succ s a)
   )"
 
 
 lemma vars_change_cat:
   fixes s
   shows "
     vars_change (as1 @ as2) vs s
     = (vars_change as1 vs s @ vars_change as2 vs (exec_plan s as1))
   "
   by (induction as1 arbitrary: s as2 vs) auto
 
 
 lemma empty_change_no_change:
   fixes s
   assumes "(vars_change as vs s = [])"
   shows "(fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs s)"
   using assms
 proof (induction as arbitrary: s vs)
   case (Cons a as)
   then show ?case
   proof (cases "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s")
     case True
       \<comment> \<open>NOTE This case violates the induction premise @{term "vars_change (a # as) vs s = []"} since the
         empty list is impossible.\<close>
     then have "state_succ s a # vars_change as vs (state_succ s a) = []"
       using Cons.prems True
       by simp
     then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
       by blast
   next
     case False
     then have "vars_change as vs (state_succ s a) = []"
       using Cons.prems False
       by force
     then have
       "fmrestrict_set vs (exec_plan (state_succ s a) as) = fmrestrict_set vs (state_succ s a)"
       using Cons.IH[of vs "(state_succ s a)"]
       by blast
     then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
       using False
       by simp
   qed
 qed auto
 
 
 \<comment> \<open>NOTE renamed variable `a` to `b` to not conflict with naming for list head in induction step.\<close>
 lemma zero_change_imp_all_effects_submap:
   fixes s s'
   assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
     "(fmrestrict_set vs s = fmrestrict_set vs s')"
   shows "(fmrestrict_set vs (snd b) \<subseteq>\<^sub>f fmrestrict_set vs s')"
   using assms
 proof (induction as arbitrary: s s' vs b)
   case (Cons a as)
     \<comment> \<open>NOTE Having either @{term "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s"} or
     @{term "\<not>ListMem b as"} leads to simpler propositions so we split here.\<close>
   then show "(fmrestrict_set vs (snd b) \<subseteq>\<^sub>f fmrestrict_set vs s')"
     using Cons.prems(1)
   proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s \<and> ListMem b as")
     case True
     let ?s="state_succ s a"
     have "vars_change as vs ?s = []"
       using True Cons.prems(1)
       by auto
     moreover have "sat_precond_as ?s as"
       using Cons.prems(2) sat_precond_as.simps(2)
       by blast
     ultimately show ?thesis
       using True Cons.prems(4) Cons.IH
       by auto
   next
     case False
     then consider
       (i) "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s"
       | (ii) "\<not>ListMem b as"
       by blast
     then show ?thesis
       using Cons.prems(1)
     proof (cases)
       case ii
       then have "a = b"
         using Cons.prems(3) ListMem_iff set_ConsD
         by metis
           \<comment> \<open>NOTE Mysteriously sledgehammer finds a proof here while the premises of
             `no\_change\_vs\_eff\_submap` cannot be proven individually.\<close>
       then show ?thesis
         using Cons.prems(1, 2, 4) no_change_vs_eff_submap
         by (metis list.distinct(1) sat_precond_as.simps(2) vars_change.simps(2))
     qed simp
   qed
 qed (simp add: ListMem_iff)
 
 
 lemma zero_change_imp_all_preconds_submap:
   fixes s s'
   assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
     "(fmrestrict_set vs s = fmrestrict_set vs s')"
   shows "(fmrestrict_set vs (fst b) \<subseteq>\<^sub>f fmrestrict_set vs s')"
   using assms
 proof (induction as arbitrary: vs s s')
   case (Cons a as)
     \<comment> \<open>NOTE Having either @{term "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s"} or
     @{term "\<not>ListMem b as"} leads to simpler propositions so we split here.\<close>
   then show "(fmrestrict_set vs (fst b) \<subseteq>\<^sub>f fmrestrict_set vs s')"
     using Cons.prems(1)
   proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s \<and> ListMem b as")
     case True
     let ?s="state_succ s a"
     have "vars_change as vs ?s = []"
       using True Cons.prems(1)
       by auto
     moreover have "sat_precond_as ?s as"
       using Cons.prems(2) sat_precond_as.simps(2)
       by blast
     ultimately show ?thesis
       using True Cons.prems(4) Cons.IH
       by auto
   next
     case False
     then consider
       (i) "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s"
       | (ii) "\<not>ListMem b as"
       by blast
     then show ?thesis
       using Cons.prems(1)
     proof (cases)
       case ii
       then have "a = b"
         using Cons.prems(3) ListMem_iff set_ConsD
         by metis
       then show ?thesis
         using Cons.prems(2, 4) fmsubset_restrict_set_mono
         by (metis sat_precond_as.simps(2))
     qed simp
   qed
 qed (simp add: ListMem_iff)
 
 
 lemma no_vs_change_valid_in_snapshot:
   assumes "(as \<in> valid_plans PROB)" "(sat_precond_as s as)" "(vars_change as vs s = [])"
   shows "(as \<in> valid_plans (snapshot PROB (fmrestrict_set vs s)))"
 proof -
   {
     fix a
     assume P: "ListMem a as"
     then have "agree (fst a) (fmrestrict_set vs s)"
       by (metis agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
           restricted_agree_imp_agree zero_change_imp_all_preconds_submap)
     moreover have "agree (snd a) (fmrestrict_set vs s)"
       by (metis (no_types) P agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
           restricted_agree_imp_agree zero_change_imp_all_effects_submap)
     ultimately have "agree (fst a) (fmrestrict_set vs s)" "agree (snd a) (fmrestrict_set vs s)"
       by simp+
   }
   then show ?thesis
     using assms(1) as_mem_agree_valid_in_snapshot
     by blast
 qed
 
 
 \<comment> \<open>NOTE type of `PROB` had to be fixed for `problem\_plan\_bound\_works`.\<close>
 lemma no_vs_change_obtain_snapshot_bound_1st_step:
   fixes PROB :: "'a problem"
   assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
     "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
     (
       exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
       = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
     )
     \<and> (subseq as' as)
     \<and> (length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
   )"
 proof -
   let ?s="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
   let ?PROB="(snapshot PROB (fmrestrict_set vs s))"
   {
     have "finite (snapshot PROB (fmrestrict_set vs s))"
       using assms(1) FINITE_snapshot
       by blast
   }
   moreover {
     have "
       fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s
       \<in> valid_states (snapshot PROB (fmrestrict_set vs s))"
       using assms(4) graph_plan_not_eq_last_diff_paths valid_states_snapshot
       by blast
   }
   moreover {
     have "as \<in> valid_plans (snapshot PROB (fmrestrict_set vs s))"
       using assms(2, 3, 5) no_vs_change_valid_in_snapshot
       by blast
   }
   ultimately show ?thesis
     using problem_plan_bound_works[of ?PROB ?s as]
     by blast
 qed
 
 
 \<comment> \<open>NOTE type of `PROB` had to be fixed for `no\_vs\_change\_obtain\_snapshot\_bound\_1st\_step`.\<close>
 lemma no_vs_change_obtain_snapshot_bound_2nd_step:
   fixes PROB :: "'a problem"
   assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
     "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
     (
       exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s)))  s) as
       = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
     )
     \<and> (subseq as' as)
     \<and> (sat_precond_as s as')
     \<and> (length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
   )"
 proof -
   obtain as'' where 1:
     "
       exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
       = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as''"
     "subseq as'' as" "length as'' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
     using assms no_vs_change_obtain_snapshot_bound_1st_step
     by blast
   let ?s'="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
   let ?as'="rem_condless_act ?s' [] as''"
   have "exec_plan ?s' as = exec_plan ?s' as''"
     using 1(1) rem_condless_valid_1
     by blast
   moreover have "subseq ?as' as"
     using 1(2) rem_condless_valid_8 sublist_trans
     by blast
   moreover have "sat_precond_as s ?as'"
     using sat_precond_drest_sat_precond rem_condless_valid_2
     by fast
   moreover have "(length ?as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))"
     using 1 rem_condless_valid_3 le_trans
     by blast
   ultimately show ?thesis
     using 1 rem_condless_valid_1
     by auto
 qed
 
 
 lemma no_vs_change_obtain_snapshot_bound_3rd_step:
   assumes "finite (PROB :: 'a problem)" "(vars_change as vs s = [])" "(no_effectless_act as)"
     "(sat_precond_as s as)" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
     (
       fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as)
       = fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')
     )
     \<and> (subseq as' as)
     \<and> (length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
   )"
 proof -
   obtain as' :: "(('a, bool) fmap \<times> ('a, bool) fmap) list" where
     "(
       exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
       = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
     )" "subseq as' as" "sat_precond_as s as'"
     "length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
     using assms(1, 2, 4, 5, 6) no_vs_change_obtain_snapshot_bound_2nd_step
     by blast
   moreover have
     "exec_plan (fmrestrict_set vs s) (as_proj as vs) = fmrestrict_set vs (exec_plan s as)"
     using assms(4) sat_precond_exec_as_proj_eq_proj_exec
     by blast
   moreover have "as_proj as (prob_dom (snapshot PROB (fmrestrict_set vs s))) = as"
     using assms(2, 3, 4, 6) as_proj_eq_as no_vs_change_valid_in_snapshot
     by blast
   ultimately show ?thesis
     using sublist_as_proj_eq_as proj_exec_proj_eq_exec_proj'
     by metis
 qed
 
 \<comment> \<open>NOTE added lemma.\<close>
 \<comment> \<open>TODO remove unused assumptions.\<close>
 lemma no_vs_change_snapshot_s_vs_is_valid_bound_i:
   fixes PROB :: "'a problem"
   assumes  "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
     "(sat_precond_as s as)" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
     "fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
         fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
     "subseq as' as" "length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
   shows
     "fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         (exec_plan s as)
       = fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         s
     \<and> fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         (exec_plan s as')
       = fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         s"
 proof -
   let ?vs="(prob_dom (snapshot PROB (fmrestrict_set vs s)))"
   let ?vs'="(fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
   let ?vs''="(fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
   let ?s="(exec_plan s as)"
   let ?s'="(exec_plan s as')"
   have 1: "as \<in> valid_plans (snapshot PROB (fmrestrict_set vs s))"
     using assms(2, 4, 6) no_vs_change_valid_in_snapshot
     by blast
   {
     {
       fix a
       assume "ListMem a as"
       then have "fmdom' (snd a) \<subseteq> prob_dom (snapshot PROB (fmrestrict_set vs s))"
         using 1 FDOM_eff_subset_prob_dom_pair valid_plan_mems
         by metis
       then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as)
           - prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
         = {}"
         using subset_inter_diff_empty[of "fmdom' (snd a)"
             "prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
         by metis
     }
     then have
       "fmrestrict_set ?vs' (exec_plan s as) = fmrestrict_set ?vs' s"
       using disjoint_effects_no_effects[of as ?vs' s]
       by blast
   }
   moreover {
     {
       fix a
       assume P: "ListMem a as'"
       moreover have \<alpha>: "as' \<in> valid_plans (snapshot PROB (fmrestrict_set vs s))"
         using assms(8) 1 sublist_valid_plan
         by blast
       moreover have "a \<in> PROB"
         using P \<alpha> snapshot_subset subsetCE valid_plan_mems
         by fast
       ultimately have "fmdom' (snd a) \<subseteq> prob_dom (snapshot PROB (fmrestrict_set vs s))"
         using FDOM_eff_subset_prob_dom_pair valid_plan_mems
         by metis
       then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as')
           - prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
         = {}"
         using subset_inter_diff_empty[of "fmdom' (snd a)"
             "prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
         by metis
     }
     then have
       "fmrestrict_set ?vs'' (exec_plan s as') = fmrestrict_set ?vs'' s"
       using disjoint_effects_no_effects[of as' ?vs'' s]
       by blast
   }
   ultimately show ?thesis
     by blast
 qed
 
 \<comment> \<open>NOTE type for `PROB` had to be fixed.\<close>
 lemma no_vs_change_snapshot_s_vs_is_valid_bound:
   fixes PROB :: "'a problem"
   assumes "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
     "(sat_precond_as s as)" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
     (exec_plan s as = exec_plan s as')
     \<and> (subseq as' as)
     \<and> (length as' <= problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
   )"
 proof -
   obtain as' where 1:
     "fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
       fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
     "subseq as' as" "length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
     using assms no_vs_change_obtain_snapshot_bound_3rd_step
     by blast
   {
 
     have a: "fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         (exec_plan s as)
       = fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         s "
       "fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         (exec_plan s as')
       = fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
         s"
       using assms 1 no_vs_change_snapshot_s_vs_is_valid_bound_i
       by blast+
     moreover have "as' \<in> valid_plans (snapshot PROB (fmrestrict_set vs s))"
       using "1"(2) assms(2) assms(4) assms(6) no_vs_change_valid_in_snapshot sublist_valid_plan
       by blast
     moreover have "(exec_plan s as) \<in> valid_states PROB"
       using assms(5, 6) valid_as_valid_exec
       by blast
     moreover have "(exec_plan s as') \<in> valid_states PROB"
       using assms(5, 6) 1 valid_as_valid_exec sublist_valid_plan
       by blast
     ultimately have "exec_plan s as = exec_plan s as'"
       using assms
       unfolding valid_states_def
       using graph_plan_lemma_5[where vs="prob_dom (snapshot PROB (fmrestrict_set vs s))", OF _ 1(1)]
       by force
   }
   then show ?thesis
     using 1
     by blast
 qed
 
 
 \<comment> \<open>TODO showcase (problems with stronger typing: Isabelle requires strict typing for `max`; whereas
 in HOL4 this is not required, possible because 'MAX' is natural number specific.\<close>
 lemma snapshot_bound_leq_S:
   shows "
     problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
     \<le> S vs lss PROB (fmrestrict_set vs s)
   "
 proof -
   have "geq_arg (max :: nat \<Rightarrow> nat \<Rightarrow> nat)"
     unfolding geq_arg_def
     using max.cobounded1
     by simp
   then show ?thesis
     unfolding S_def
     using individual_weight_less_eq_lp[where
         g="max :: nat \<Rightarrow> nat \<Rightarrow> nat"
         and x="(fmrestrict_set vs s)" and R="(\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x)"
         and w="(\<lambda>s. problem_plan_bound (snapshot PROB s))" and f="(\<lambda>x y. x + y + 1)" and l=lss]
     by blast
 qed
 
 
 \<comment> \<open>NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.\<close>
 \<comment> \<open>NOTE the type of `1` had to be restricted to `nat` to ensure the proofs for `geq\_arg` work.\<close>
 lemma S_geq_S_succ_plus_ell:
   assumes "(s \<in> valid_states PROB)"
     "(top_sorted_abs (\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x) lss)"
     "(s' \<in> state_successors (prob_proj PROB vs) s)" "(set lss = valid_states (prob_proj PROB vs))"
   shows "(
     problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
       + S vs lss PROB (fmrestrict_set vs s')
       + (1 :: nat)
     \<le> S vs lss PROB (fmrestrict_set vs s)
   )"
 proof -
   let ?f="\<lambda>x y. x + y + (1 :: nat)"
   let ?R="(\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x)"
   let ?w="(\<lambda>s. problem_plan_bound (snapshot PROB s))"
   let ?g="max :: nat \<Rightarrow> nat \<Rightarrow> nat"
   let ?vtx1="(fmrestrict_set vs s')"
   let ?G="lss"
   let ?vtx2="(fmrestrict_set vs s)"
   have "geq_arg ?f"
     unfolding geq_arg_def
     by simp
   moreover have "geq_arg ?g"
     unfolding geq_arg_def
     by simp
   moreover have "\<forall>x. ListMem x lss \<longrightarrow> \<not>?R x x"
     unfolding state_successors_def
     by blast
   moreover have "?R ?vtx2 ?vtx1"
     unfolding state_successors_def
     using assms(3) state_in_successor_proj_in_state_in_successor state_successors_def
     by blast
   moreover have
     "ListMem ?vtx1 ?G"
     using assms(1, 3, 4)
     by (metis ListMem_iff contra_subsetD graph_plan_not_eq_last_diff_paths proj_successors_of_valid_are_valid)
   moreover have "top_sorted_abs ?R ?G"
     using assms(2)
     by simp
   ultimately show ?thesis
     unfolding S_def
     using lp_geq_lp_from_successor[of ?f ?g ?G ?R ?vtx2 ?vtx1 ?w]
     by blast
 qed
 
 
 lemma vars_change_cons:
   fixes s s'
   assumes "(vars_change as vs s = (s' # ss))"
   shows "(\<exists>as1 act as2.
     (as = as1 @ (act # as2))
     \<and> (vars_change as1 vs s = [])
     \<and> (state_succ (exec_plan s as1) act = s')
     \<and> (vars_change as2 vs (state_succ (exec_plan s as1) act) = ss)
   )"
   using assms
 proof (induction as arbitrary: s s' vs ss)
   case (Cons a as)
   then show ?case
   proof (cases "fmrestrict_set vs (state_succ s a) \<noteq> fmrestrict_set vs s")
     case True
     then have "state_succ s a = s'" "vars_change as vs (state_succ s a) = ss"
       using Cons.prems
       by simp+
     then show ?thesis
       by fastforce
   next
     case False
     then have "vars_change as vs (state_succ s a) = s' # ss"
       using Cons.prems
       by simp
     then obtain as1 act as2 where
       "as = as1 @ act # as2" "vars_change as1 vs (state_succ s a) = []"
       "state_succ (exec_plan (state_succ s a) as1) act = s'"
       "vars_change as2 vs (state_succ (exec_plan (state_succ s a) as1) act) = ss"
       using Cons.IH
       by blast
     then show ?thesis
       by (metis False append_Cons exec_plan.simps(2) vars_change.simps(2))
   qed
 qed simp
 
 
 lemma vars_change_cons_2:
   fixes s s'
   assumes "(vars_change as vs s = (s' # ss))"
   shows "(fmrestrict_set vs s' \<noteq> fmrestrict_set vs s)"
   using assms
   apply(induction as arbitrary: s s' vs ss)
   apply(auto)
   by (metis list.inject)
 
 
 \<comment> \<open>NOTE first argument of `top\_sorted\_abs had to be wrapped into lambda.\<close>
 lemma problem_plan_bound_S_bound_1st_step:
   fixes PROB :: "'a problem"
   assumes "finite PROB" "(top_sorted_abs (\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x) lss)"
     "(set lss = valid_states (prob_proj PROB vs))" "(s \<in> valid_states PROB)"
     "(as \<in> valid_plans PROB)" "(no_effectless_act as)" "(sat_precond_as s as)"
   shows "(\<exists>as'.
       (exec_plan s as' = exec_plan s as)
       \<and> (subseq as' as)
       \<and> (length as' <= S vs lss PROB (fmrestrict_set vs s))
     )"
   using assms
 proof (induction "vars_change as vs s" arbitrary: PROB as vs s lss)
   case Nil
   then obtain as' where
     "exec_plan s as = exec_plan s as'" "subseq as' as"
     "length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
     using Nil(1) Nil.prems(1,4,5,6,7) no_vs_change_snapshot_s_vs_is_valid_bound
     by metis
   moreover have "
       problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
       \<le> S vs lss PROB (fmrestrict_set vs s)
     "
     using snapshot_bound_leq_S le_trans
     by fast
   ultimately show ?case
     using le_trans
     by fastforce
 next
   case (Cons s' ss)
   then obtain as1 act as2 where 1:
     "as = as1 @ act # as2" "vars_change as1 vs s = []" "state_succ (exec_plan s as1) act = s'"
     "vars_change as2 vs (state_succ (exec_plan s as1) act) = ss"
     using vars_change_cons
     by smt
   text\<open> Obtain conclusion of induction hypothesis for 'as2' and
       '(state\_succ (exec\_plan s as1) act)'. \<close>
   {
     {
       have "as1 \<in> valid_plans PROB"
         using Cons.prems(5) 1(1) valid_append_valid_pref
         by blast
       moreover have "act \<in> PROB"
         using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
         by fast
       ultimately have "state_succ (exec_plan s as1) act \<in> valid_states PROB"
         using Cons.prems(4) valid_as_valid_exec lemma_1_i
         by blast
     }
     moreover have "as2 \<in> valid_plans PROB"
       using Cons.prems(5) 1(1) valid_append_valid_suff valid_plan_valid_tail
       by fast
     moreover have "no_effectless_act as2"
       using Cons.prems(6) 1(1) rem_effectless_works_13 sublist_append_back
       by blast
     moreover have "sat_precond_as (state_succ (exec_plan s as1) act) as2"
       using Cons.prems(7) 1(1) graph_plan_lemma_17 sat_precond_as.simps(2)
       by blast
     ultimately have "\<exists>as'.
           exec_plan (state_succ (exec_plan s as1) act) as'
           = exec_plan (state_succ (exec_plan s as1) act) as2
         \<and> subseq as' as2
         \<and> length as' \<le> S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
       using Cons.prems(1, 2, 3) 1(4)
         Cons(1)[where as="as2" and s="(state_succ (exec_plan s as1) act)"]
       by blast
   }
   note a=this
   {
     have "no_effectless_act as1"
       using Cons.prems(6) 1(1) rem_effectless_works_12
       by blast
     moreover have "sat_precond_as s as1"
       using Cons.prems(7) 1(1) sat_precond_as_pfx
       by blast
     moreover have "as1 \<in> valid_plans PROB"
       using Cons.prems(5) 1(1) valid_append_valid_pref
       by blast
     ultimately have "\<exists>as'. exec_plan s as1 = exec_plan s as' \<and>
         subseq as' as1 \<and> length as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
       using no_vs_change_snapshot_s_vs_is_valid_bound[of _ as1]
       using Cons.prems(1, 4) 1(2)
       by blast
   }
   then obtain as'' where b:
     "exec_plan s as1 = exec_plan s as''" "subseq as'' as1"
     "length as'' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
     by blast
   {
     obtain as' where i:
       "exec_plan (state_succ (exec_plan s as1) act) as'
           = exec_plan (state_succ (exec_plan s as1) act) as2"
       "subseq as' as2"
       "length as' \<le> S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
       using a
       by blast
     let ?as'="as'' @ act # as'"
     have "exec_plan s ?as' = exec_plan s as"
       using 1(1) b(1) i(1) exec_plan_Append exec_plan.simps(2)
       by metis
     moreover have "subseq ?as' as"
       using 1(1) b(2) i(2) subseq_append_iff
       by blast
     moreover
     {
       {
         \<comment> \<open>NOTE this is proved earlier in the original proof script. Moved here to improve
             transparency.\<close>
         have "sat_precond_as (exec_plan s as1) (act # as2)"
           using empty_replace_proj_dual7
           using 1(1) Cons.prems(7)
           by blast
         then have "fst act \<subseteq>\<^sub>f (exec_plan s as1)"
           by simp
       }
       note A = this
       {
         have
           "fmrestrict_set vs (state_succ (exec_plan s as1) act)
               = (state_succ (fmrestrict_set vs (exec_plan s as'')) (action_proj act vs))"
           using b(1) A drest_succ_proj_eq_drest_succ[where s="exec_plan s as1", symmetric]
           by simp
         also have "\<dots> = (state_succ (fmrestrict_set vs s) (action_proj act vs))"
           using 1(2) b(1) empty_change_no_change
           by fastforce
         finally have "\<dots> = fmrestrict_set  vs (state_succ s (action_proj act vs))"
           using  succ_drest_eq_drest_succ
           by blast
       }
       note B = this
       have C: "fmrestrict_set vs (exec_plan s as'') = fmrestrict_set vs s"
         using 1(2) b(1) empty_change_no_change
         by fastforce
       {
         have "act \<in> PROB"
           using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
           by fast
         then have \<aleph>: "action_proj act vs \<in> prob_proj PROB vs"
           using action_proj_in_prob_proj
           by blast
         then have "(state_succ s (action_proj act vs)) \<in> (state_successors (prob_proj PROB vs) s)"
         proof (cases "fst (action_proj act vs) \<subseteq>\<^sub>f s")
           case True
           then show ?thesis
             unfolding state_successors_def
             using Cons.hyps(2) 1(3) b(1) A B C \<aleph> DiffI imageI singletonD vars_change_cons_2
               drest_succ_proj_eq_drest_succ
             by metis
         next
           case False
           then show ?thesis
             unfolding state_successors_def
             using Cons.hyps(2) 1(3) b(1) A B C \<aleph> DiffI imageI singletonD
               drest_succ_proj_eq_drest_succ vars_change_cons_2
             by metis
         qed
       }
       then have D:
         "problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
                 + S vs lss PROB (fmrestrict_set vs (state_succ s (action_proj act vs)))
                 + 1
               \<le> S vs lss PROB (fmrestrict_set vs s)"
         using Cons.prems(2, 3, 4) S_geq_S_succ_plus_ell[where s'="state_succ s (action_proj act vs)"]
         by blast
       {
         have
           "length ?as' \<le> problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
                 + 1 + S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
           using b i
           by fastforce
         then have "length ?as' \<le> S vs lss PROB (fmrestrict_set vs s)"
           using b(1) A B C D drest_succ_proj_eq_drest_succ
           by (smt Suc_eq_plus1 add_Suc dual_order.trans)
       }
     }
     ultimately have ?case
       by blast
   }
   then show ?case
     by blast
 qed
 
 
 \<comment> \<open>NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.\<close>
 lemma problem_plan_bound_S_bound_2nd_step:
   assumes "finite (PROB :: 'a problem)"
     "(top_sorted_abs (\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x) lss)"
     "(set lss = valid_states (prob_proj PROB vs))" "(s \<in> valid_states PROB)"
     "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
     (exec_plan s as' = exec_plan s as)
     \<and> (subseq as' as)
     \<and> (length as' \<le> S vs lss PROB (fmrestrict_set vs s))
   )"
 proof -
   \<comment> \<open>NOTE Proof premises and obtain conclusion of `problem\_plan\_bound\_S\_bound\_1st\_step`.\<close>
   {
     have a: "rem_condless_act s [] (rem_effectless_act as) \<in> valid_plans PROB"
       using assms(5) rem_effectless_works_4' rem_condless_valid_10
       by blast
     then have b: "no_effectless_act (rem_condless_act s [] (rem_effectless_act as))"
       using assms rem_effectless_works_6 rem_condless_valid_9
       by fast
     then have "sat_precond_as s (rem_condless_act s [] (rem_effectless_act as))"
       using assms rem_condless_valid_2
       by blast
     then have "\<exists>as'.
       exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))
       \<and> subseq as' (rem_condless_act s [] (rem_effectless_act as))
       \<and> length as' \<le> S vs lss PROB (fmrestrict_set vs s)
     "
       using assms a b problem_plan_bound_S_bound_1st_step
       by blast
   }
   then obtain as' where 1:
     "exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))"
     "subseq as' (rem_condless_act s [] (rem_effectless_act as))"
     "length as' \<le> S vs lss PROB (fmrestrict_set vs s)"
     by blast
   then have 2: "exec_plan s as' = exec_plan s as"
     using rem_condless_valid_1 rem_effectless_works_14
     by metis
   then have "subseq as' as"
     using 1(2) rem_condless_valid_8 rem_effectless_works_9 sublist_trans
     by metis
   then show ?thesis
     using 1(3) 2
     by blast
 qed
 
 
 \<comment> \<open>NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.\<close>
 lemma S_in_MPLS_leq_2_pow_n:
   assumes "finite (PROB :: 'a problem)"
     "(top_sorted_abs (\<lambda> x y. y \<in> state_successors (prob_proj PROB vs) x) lss)"
     "(set lss = valid_states (prob_proj PROB vs))" "(s \<in> valid_states PROB)"
     "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.
       (exec_plan s as' = exec_plan s as)
       \<and> (subseq as' as)
       \<and> (length as' \<le> Sup {S vs lss PROB s' | s'. s' \<in> valid_states (prob_proj PROB  vs)})
     )"
 proof -
   obtain as' where
     "exec_plan s as' = exec_plan s as" "subseq as' as"
     "length as' \<le> S vs lss PROB (fmrestrict_set vs s)"
     using assms problem_plan_bound_S_bound_2nd_step
     by blast
   moreover {
     \<comment> \<open>NOTE Derive sufficient conditions for inferring that `S vs lss PROB` is smaller or equal to
     the supremum of the set @{term "{S vs lss PROB s' | s'. s' \<in> valid_states (prob_proj PROB vs)}"}: i.e.
     being contained and that the supremum is contained as well.\<close>
     let ?S="{S vs lss PROB s' | s'. s' \<in> valid_states (prob_proj PROB vs)}"
     {
       have "fmrestrict_set vs s \<in> valid_states (prob_proj PROB vs)"
         using assms(4) graph_plan_not_eq_last_diff_paths
         by blast
       then have "S vs lss PROB (fmrestrict_set vs s) \<in> ?S"
         using calculation(1)
         by blast
     }
-    note 1 = this
+    moreover
     {
       have "finite (prob_proj PROB vs)"
-        unfolding prob_proj_def valid_states_def
-        using assms(1)
-        by simp
+        by (simp add: assms(1) prob_proj_def)
       then have "finite ?S"
         using Setcompr_eq_image assms(3)
         by (metis List.finite_set finite_imageI)
     }
-    then have "S vs lss PROB (fmrestrict_set vs s) \<le> Max ?S"
-      using 1 Max.coboundedI
-      by blast
-    then have "S vs lss PROB (fmrestrict_set vs s) \<le> Sup ?S"
-      using Sup_nat_def
-      by presburger
+    ultimately have "S vs lss PROB (fmrestrict_set vs s) \<le> Sup ?S"
+      using le_cSup_finite by blast
   }
   ultimately show ?thesis
     using le_trans
     by blast
 qed
 
 
 \<comment> \<open>NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.\<close>
 lemma problem_plan_bound_S_bound:
   fixes PROB :: "'a problem"
   assumes "finite PROB" "(top_sorted_abs (\<lambda>x y. y \<in> state_successors (prob_proj PROB vs) x) lss)"
     "(set lss = valid_states (prob_proj PROB vs))"
   shows "
     problem_plan_bound PROB
     \<le> Sup {S vs lss PROB (s' :: 'a state) | s'. s' \<in> valid_states (prob_proj PROB vs)}
   "
 proof -
   let ?f="\<lambda>PROB.
     Sup {S vs lss PROB (s' :: 'a state) | s'. s' \<in> valid_states (prob_proj PROB vs)} + 1"
   {
     fix as and s :: "'a state"
     assume "s \<in> valid_states PROB" "as \<in> valid_plans PROB"
     then obtain as' where a:
       "exec_plan s as' = exec_plan s as" "subseq as' as"
       "length as' \<le> Sup {S vs lss PROB s' |s'. s' \<in> valid_states (prob_proj PROB vs)}"
       using assms S_in_MPLS_leq_2_pow_n
       by blast
     then have "length as' < ?f PROB"
       by linarith
     moreover have "exec_plan s as = exec_plan s as'"
       using a(1)
       by simp
     ultimately have
       "\<exists>as'. exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' < ?f PROB"
       using a(2)
       by blast
   }
   then show ?thesis
     using assms(1) problem_plan_bound_UBound[where f="?f"]
     by fastforce
 qed
 
 subsection "State Space Acyclicity"
 
 text \<open> State space acyclicity is again formalized using graphs to model the state space. However
 the relation inducing the graph is the successor relation on states. [Abdulaziz et al.,
 Definition 15, HOL4 Definition 15, p.27]
 
 With this, the acyclic system compositional bound `S` can be shown to be an upper bound on the
 sublist diameter (lemma `problem\_plan\_bound\_S\_bound\_thesis`). [Abdulaziz et al., p.29] \<close>
 
 \<comment> \<open>NOTE name shortened.\<close>
 \<comment> \<open>NOTE first argument of 'top\_sorted\_abs' had to be wrapped into lambda.\<close>
 definition sspace_DAG where
   "sspace_DAG PROB lss \<equiv> (
     (set lss = valid_states PROB)
     \<and> (top_sorted_abs (\<lambda>x y. y \<in> state_successors PROB x) lss)
   )"
 
 
 lemma problem_plan_bound_S_bound_2nd_step_thesis:
   assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
     "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'.   (exec_plan s as' = exec_plan s as)
     \<and> (subseq as' as)
     \<and> (length as' \<le> S vs lss PROB (fmrestrict_set vs s))
   )"
   using assms problem_plan_bound_S_bound_2nd_step sspace_DAG_def
   by fast
 
 
 text \<open>And finally, this is the main lemma about the upper bounding algorithm.\<close>
 
 theorem problem_plan_bound_S_bound_thesis:
   assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
   shows "(
     problem_plan_bound PROB
     \<le> Sup {S vs lss PROB s' | s'. s' \<in> valid_states (prob_proj PROB vs)}
   )"
   using assms problem_plan_bound_S_bound sspace_DAG_def
   by fast
 
 
 end
\ No newline at end of file
diff --git a/thys/Factored_Transition_System_Bounding/TopologicalProps.thy b/thys/Factored_Transition_System_Bounding/TopologicalProps.thy
--- a/thys/Factored_Transition_System_Bounding/TopologicalProps.thy
+++ b/thys/Factored_Transition_System_Bounding/TopologicalProps.thy
@@ -1,2352 +1,2352 @@
 theory TopologicalProps
   imports Main FactoredSystem ActionSeqProcess SetUtils
 begin 
 
 
 section "Topological Properties"
 subsection "Basic Definitions and Properties"
 
 definition PLS_charles where
   "PLS_charles s as PROB \<equiv> {length as' | as'. 
     (as' \<in> valid_plans PROB) \<and> (exec_plan s as' = exec_plan s as)}"
 
 
 definition MPLS_charles where
   "MPLS_charles PROB \<equiv> {Inf (PLS_charles (fst p) (snd p) PROB) | p. 
     ((fst p) \<in> valid_states PROB) 
     \<and> ((snd p) \<in> valid_plans PROB)
   }"
 
 
 \<comment> \<open>NOTE name shortened to 'problem\_plan\_bound\_charles'.\<close>
 definition problem_plan_bound_charles where
   "problem_plan_bound_charles PROB \<equiv> Sup (MPLS_charles PROB)"
 
 
 \<comment> \<open>NOTE name shortened to 'PLS\_state'.\<close>  
 definition PLS_state_1 where
   "PLS_state_1 s as \<equiv> length ` {as'. (exec_plan s as' = exec_plan s as)}"
 
 
 \<comment> \<open>NOTE name shortened to 'MPLS\_stage\_1'.\<close>
 definition MPLS_stage_1 where
   "MPLS_stage_1 PROB \<equiv> 
     (\<lambda> (s, as). Inf (PLS_state_1 s as)) 
     ` {(s, as). (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)}
   "
 
 
 \<comment> \<open>NOTE name shortened to 'problem\_plan\_bound\_stage\_1'.\<close>
 definition problem_plan_bound_stage_1 where
   "problem_plan_bound_stage_1 PROB \<equiv> Sup (MPLS_stage_1 PROB)"
 for PROB :: "'a problem"
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition PLS where
   "PLS s as \<equiv> length ` {as'. (exec_plan s as' = exec_plan s as) \<and> (subseq as' as)}"
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 \<comment> \<open>NOTE proof finite PLS for use in 'proof in\_MPLS\_leq\_2\_pow\_n\_i'\<close> 
 lemma finite_PLS: "finite (PLS s as)"
 proof -
   let ?S = "{as'. (exec_plan s as' = exec_plan s as) \<and> (subseq as' as)}"
   let ?S1 = "length ` {as'. (exec_plan s as' = exec_plan s as) }" 
   let ?S2 = "length ` {as'. (subseq as' as)}"
   let ?n = "length as + 1"
   have "finite ?S2"
     using bounded_nat_set_is_finite[where n = ?n and N = ?S2]
     by fastforce
   moreover have "length ` ?S \<subseteq> (?S1 \<inter> ?S2)"
     by blast
   ultimately have "finite (length ` ?S)"
     using infinite_super 
     by auto 
   then show ?thesis 
     unfolding PLS_def 
     by blast
 qed
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition MPLS where
   "MPLS PROB \<equiv>
     (\<lambda> (s, as). Inf (PLS s as)) 
     ` {(s, as). (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)}
   "
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition problem_plan_bound where
   "problem_plan_bound PROB \<equiv> Sup (MPLS PROB)"
 
 
 lemma expanded_problem_plan_bound_thm_1: 
   fixes PROB
   shows " 
     (problem_plan_bound PROB) = Sup (
       (\<lambda>(s,as). Inf (PLS s as)) `
       {(s, as). (s \<in> (valid_states PROB)) \<and> (as \<in> valid_plans PROB)}
     )  
   "
   unfolding problem_plan_bound_def MPLS_def 
   by blast
 
 lemma expanded_problem_plan_bound_thm: 
   fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set"
   shows "
     problem_plan_bound PROB = Sup ({Inf (PLS s as) | s as. 
       (s \<in> valid_states PROB) 
       \<and> (as \<in> valid_plans PROB)
     })
   "
 proof -
   {
     have "(
         {Inf (PLS s as) | s as. (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)}
       ) = ((\<lambda>(s, as). Inf (PLS s as)) ` {(s, as).
         (s \<in> valid_states PROB) 
         \<and> (as \<in> valid_plans PROB)
       })
     "
       by fast
     also have "\<dots> = 
       (\<lambda>(s, as). Inf (PLS s as)) ` 
       ({s. fmdom' s = prob_dom PROB} \<times> {as. set as \<subseteq> PROB})
     "
       unfolding valid_states_def valid_plans_def
       by simp
     finally have "
       Sup ({Inf (PLS s as) | s as. (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)})
       = Sup (
         (\<lambda>(s, as). Inf (PLS s as)) ` 
         ({s. fmdom' s = prob_dom PROB} \<times> {as. set as \<subseteq> PROB})
       )
     "
       by argo
   }
   moreover have "
     problem_plan_bound PROB 
     = 
       Sup ((\<lambda>(s, as). Inf (PLS s as)) ` 
       ({s. fmdom' s = prob_dom PROB} \<times> {as. set as \<subseteq> PROB}))
     " 
     unfolding problem_plan_bound_def MPLS_def valid_states_def valid_plans_def
     by fastforce
   ultimately show "
     problem_plan_bound PROB 
     = Sup ({Inf (PLS s as) | s as. 
       (s \<in> valid_states PROB) 
       \<and> (as \<in> valid_plans PROB)
     })
   "
     by argo 
 qed
 
 
 subsection "Recurrence Diameter" 
 
 text \<open> The recurrence diameter---defined as the longest simple path in the digraph modelling the
 state space---provides a loose upper bound on the system diameter. [Abdulaziz et al., Definition 9, 
 p.15] \<close>
 
 \<comment> \<open>NOTE name shortened.\<close>
 \<comment> \<open>NOTE 'fun' because of multiple defining equations, pattern matches.\<close>
 fun valid_path where
   "valid_path Pi [] = True"
 | "valid_path Pi [s] = (s \<in> valid_states Pi)"
 | "valid_path Pi (s1 # s2 # rest) = (
   (s1 \<in> valid_states Pi) 
   \<and> (\<exists>a. (a \<in> Pi) \<and> (exec_plan s1 [a] = s2))
   \<and> (valid_path Pi (s2 # rest))
 )"
 
 
 lemma valid_path_ITP2015: "
   (valid_path Pi [] \<longleftrightarrow> True)
   \<and> (valid_path Pi [s] \<longleftrightarrow> (s \<in> valid_states Pi))
   \<and> (valid_path Pi (s1 # s2 # rest) \<longleftrightarrow>
       (s1 \<in> valid_states Pi) 
       \<and> (\<exists>a. 
         (a \<in> Pi)
         \<and> (exec_plan s1 [a] = s2)
       ) 
       \<and> (valid_path Pi (s2 # rest))
   )
 "
   using valid_states_def
   by simp
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 \<comment> \<open>NOTE second declaration skipped (declared twice in source).\<close>
 definition RD where
   "RD Pi \<equiv> (Sup {length p - 1 | p. valid_path Pi p \<and> distinct p})"
 for Pi :: "'a problem"
 
 
 lemma in_PLS_leq_2_pow_n: 
   fixes PROB :: "'a problem" and s :: "'a state" and as
   assumes "finite PROB" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)" 
   shows "(\<exists>x. 
     (x \<in> PLS s as) 
     \<and> (x \<le> (2 ^ card (prob_dom PROB)) - 1)
   )"
 proof -
   obtain as' where 1:
     "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' \<le> 2 ^ card (prob_dom PROB) - 1" 
     using assms main_lemma 
     by blast
   let ?x="length as'"
   have "?x \<in> PLS s as" 
     unfolding PLS_def
     using 1
     by simp
   moreover have "?x \<le> 2 ^ card (prob_dom PROB) - 1"
     using 1(3)
     by blast
   ultimately show "(\<exists>x. 
     (x \<in> PLS s as) 
     \<and> (x \<le> (2 ^ card (prob_dom PROB)) - 1)
   )" 
     unfolding PLS_def
     by blast
 qed
 
 
 lemma in_MPLS_leq_2_pow_n: 
   fixes PROB :: "'a problem" and x
   assumes "finite PROB" "(x \<in> MPLS PROB)"
   shows "(x \<le> 2 ^ card (prob_dom PROB) - 1)" 
 proof -
   let ?mpls = "MPLS PROB"
     \<comment> \<open>NOTE obtain p = (s, as) where 'x = Inf (PLS s as)' from premise.\<close>
   have "?mpls = 
     (\<lambda> (s, as). Inf (PLS s as)) ` 
     {(s, as).  (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)}
   "
     using MPLS_def 
     by blast
   then obtain s :: "('a, bool) fmap" and as :: "(('a, bool) fmap \<times> ('a, bool) fmap) list" 
     where obtain_s_as: "x \<in> 
       ((\<lambda> (s, as). Inf (PLS s as)) ` 
       {(s, as). (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB)})
     "
     using assms(2) 
     by blast
   then have 
     "x \<in> {Inf (PLS (fst p) (snd p)) | p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)}" 
     using assms(1) obtain_s_as 
     by auto
   then have 
     "\<exists> p. x = Inf (PLS (fst p) (snd p)) \<and> (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)" 
     by blast
   then obtain p :: "('a, bool) fmap \<times> (('a, bool) fmap \<times> ('a, bool) fmap) list" where obtain_p:
     "x = Inf (PLS (fst p) (snd p))" "(fst p \<in> valid_states PROB)" "(snd p \<in> valid_plans PROB)" 
     by blast 
   then have "fst p \<in> valid_states PROB" "snd p \<in> valid_plans PROB"
     using obtain_p 
     by blast+    
   then obtain x' :: nat where obtain_x':
     "x' \<in> PLS (fst p) (snd p) \<and> x' \<le> 2 ^ card (prob_dom PROB) - 1" 
     using assms(1) in_PLS_leq_2_pow_n[where s = "fst p" and as = "snd p"]
     by blast
   then have 1: "x' \<le> 2 ^ card (prob_dom PROB) - 1" "x' \<in> PLS (fst p) (snd p)" 
     "x = Inf (PLS (fst p) (snd p))" "finite (PLS (fst p) (snd p))"
     using obtain_x' obtain_p finite_PLS 
     by blast+
   moreover have "x \<le> x'" 
     using 1(2, 4) obtain_p(1) cInf_le_finite
     by blast
   ultimately show "(x \<le> 2 ^ card (prob_dom PROB) - 1)"
     by linarith
 qed
 
 
 lemma FINITE_MPLS: 
   assumes "finite (Pi :: 'a problem)"
   shows "finite (MPLS Pi)"
 proof -
   have "\<forall>x \<in> MPLS Pi. x \<le> 2 ^ card (prob_dom Pi) - 1"
     using assms in_MPLS_leq_2_pow_n
     by blast
   then show "finite (MPLS Pi)" 
     using mems_le_finite[of "MPLS Pi" "2 ^ card (prob_dom Pi) - 1"]
     by blast
 qed
 
 
 \<comment> \<open>NOTE 'fun' because of multiple defining equations.\<close>
 fun statelist' where
   "statelist' s [] = [s]"
 | "statelist' s (a # as) = (s # statelist' (state_succ s a) as)"
 
 
 lemma LENGTH_statelist': 
   fixes as s
   shows "length (statelist' s as) = (length as + 1)"
   by (induction as arbitrary: s) auto
 
 
 lemma valid_path_statelist': 
   fixes as and s :: "('a, 'b) fmap"
   assumes "(as \<in> valid_plans Pi)" "(s \<in> valid_states Pi)"
   shows "(valid_path Pi (statelist' s as))"
   using assms 
 proof (induction as arbitrary: s Pi)
   case cons: (Cons a as)
   then have 1: "a \<in> Pi" "as \<in> valid_plans Pi"
     using valid_plan_valid_head valid_plan_valid_tail 
     by metis+
   then show ?case     
   proof (cases as)
     case Nil
     {
       have "state_succ s a \<in> valid_states Pi"
         using 1 cons.prems(2) valid_action_valid_succ
         by blast
       then have "valid_path Pi [state_succ s a]"
         using 1 cons.prems(2) cons.IH
         by force
       moreover have "(\<exists>aa. aa \<in> Pi \<and> exec_plan s [aa] = state_succ s a)"
         using 1(1) 
         by fastforce
       ultimately have "valid_path Pi (statelist' s [a])" 
         using cons.prems(2)
         by simp
     }
     then show ?thesis 
       using Nil
       by blast
   next
     case (Cons b list)
     {
       have "s \<in> valid_states Pi" 
         using cons.prems(2)
         by simp
           \<comment> \<open>TODO this step is inefficient (~5s).\<close>
       then have 
         "valid_path Pi (state_succ s a # statelist' (state_succ (state_succ s a) b) list)"
         using 1 cons.IH cons.prems(2) Cons lemma_1_i
         by fastforce
       moreover have 
         "(\<exists>aa b. (aa, b) \<in> Pi \<and> state_succ s (aa, b) = state_succ s a)"
         using 1(1) surjective_pairing
         by metis
       ultimately have "valid_path Pi (statelist' s (a # b # list))" 
         using cons.prems(2)
         by auto
     }
     then show ?thesis 
       using Cons
       by blast
   qed
 qed simp
 
 
 \<comment> \<open>TODO explicit proof.\<close>
 lemma statelist'_exec_plan: 
   fixes a s p
   assumes "(statelist' s as = p)"
   shows "(exec_plan s as = last p)"
   using assms 
   apply(induction as arbitrary: s p)
    apply(auto)
   apply(cases "as")
   by 
     (metis LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3))
     (metis (no_types) LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3))
 
 
 lemma statelist'_EQ_NIL: "statelist' s as \<noteq> []"
   by (cases as) auto
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 lemma statelist'_TAKE_i:
   assumes "Suc m \<le> length (a # as)"
   shows "m \<le> length as"
   using assms 
   by (induction as arbitrary: a m) auto
 
 lemma statelist'_TAKE: 
   fixes as s p
   assumes "(statelist' s as = p)"
   shows "(\<forall>n. n \<le> length as \<longrightarrow> (exec_plan s (take n as)) = (p ! n))" 
   using assms
 proof (induction as arbitrary: s p)
   case Nil
   {
     fix n
     assume P1: "n \<le> length []"
     then have "exec_plan s (take n []) = s" 
       by simp
     moreover have "p ! 0 = s" 
       using Nil.prems 
       by force
     ultimately have "exec_plan s (take n []) = p ! n" 
       using P1
       by simp
   }
   then show ?case by blast
 next
   case (Cons a as)
   {
     fix n
     assume P2: "n \<le> length (a # as)"
     then have "exec_plan s (take n (a # as)) = p ! n" 
       using Cons.prems 
     proof (cases "n = 0")
       case False
       then obtain m where a: "n = Suc m"
         using not0_implies_Suc
         by presburger
       moreover have b: "statelist' s (a # as) ! n = statelist' (state_succ s a) as ! m"
         using a nth_Cons_Suc
         by simp
       moreover have c: "exec_plan s (take n (a # as)) = exec_plan (state_succ s a) (take m as)"
         using a
         by force
       moreover have "m \<le> length as" 
         using a P2 statelist'_TAKE_i
         by simp
       moreover have 
         "exec_plan (state_succ s a) (take m as) = statelist' (state_succ s a) as ! m"
         using calculation(2, 3, 4) Cons.IH
         by blast
       ultimately show ?thesis 
         using Cons.prems
         by argo
     qed fastforce
   }
   then show ?case by blast
 qed
 
 
 lemma MPLS_nempty: 
   fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set" 
   assumes "finite PROB"
   shows "MPLS PROB \<noteq> {}"
 proof -
   let ?S="{(s, as). s \<in> valid_states PROB \<and> as \<in> valid_plans PROB}"
     \<comment> \<open>NOTE type of 's' had to be fixed for 'valid\_states\_nempty'.\<close>
   obtain s :: "('a, 'b) fmap"  where "s \<in> valid_states PROB"
     using assms valid_states_nempty
     by blast
   moreover have "[] \<in> valid_plans PROB"
     using empty_plan_is_valid
     by auto
   ultimately have "(s, []) \<in> ?S" 
     by blast
   then show ?thesis 
     unfolding MPLS_def
     by blast
 qed
 
 
 theorem bound_main_lemma: 
   fixes PROB :: "'a problem" 
   assumes "finite PROB"
   shows "(problem_plan_bound PROB \<le> (2 ^ (card (prob_dom PROB))) - 1)"
 proof -
   have "MPLS PROB \<noteq> {}"
     using assms MPLS_nempty
     by auto
   moreover have "(\<forall>x. x \<in> MPLS PROB \<longrightarrow> x \<le> 2 ^ card (prob_dom PROB) - 1)"
     using assms in_MPLS_leq_2_pow_n
     by blast
   ultimately show ?thesis
     unfolding problem_plan_bound_def
     using cSup_least 
     by blast
 qed
 
 
 \<comment> \<open>NOTE types in premise had to be fixed to be able to match `valid\_as\_valid\_exec`.\<close>
 lemma bound_child_parent_card_state_set_cons: 
   fixes P f
   assumes "(\<forall>(PROB :: 'a problem) as (s :: 'a state). 
     (P PROB) 
     \<and> (as \<in> valid_plans PROB) 
     \<and> (s \<in> valid_states PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as) 
       \<and> (length as' < f PROB)
     )
   )"
   shows "(\<forall>PROB s as. 
     (P PROB)
     \<and> (as \<in> valid_plans PROB)
     \<and> (s \<in> (valid_states PROB))
     \<longrightarrow> (\<exists>x. 
       (x \<in> PLS s as) 
       \<and> (x < f PROB)
     )
   )"
 proof -
   {
     fix PROB :: "'a problem" and as and s :: "'a state"
     assume P1: "(P PROB)" 
       "(as \<in> valid_plans PROB)"
       "(s \<in> valid_states PROB)" 
       "(\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> (subseq as' as) 
         \<and> (length as' < f PROB)
       )"
     have "(exec_plan s as \<in> valid_states PROB)"
       using assms P1 valid_as_valid_exec
       by blast
     then have "(P PROB)
       \<and> (as \<in> valid_plans PROB)
       \<and> (s \<in> (valid_states PROB))
       \<longrightarrow> (\<exists>x. 
         (x \<in> PLS s as) 
         \<and> (x < f PROB)
       )
     "
       unfolding PLS_def 
       using P1 
       by force
   }
   then show "(\<forall>PROB s as. 
     (P PROB)
     \<and> (as \<in> valid_plans PROB)
     \<and> (s \<in> (valid_states PROB))
     \<longrightarrow> (\<exists>x. 
       (x \<in> PLS s as) 
       \<and> (x < f PROB)
     )
   )"
     using assms
     by simp
 qed
 
 
 \<comment> \<open>NOTE types of premise had to be fixed to be able to use lemma `bound\_child\_parent\_card\_state\_set\_cons`.\<close>
 lemma bound_on_all_plans_bounds_MPLS: 
   fixes P f
   assumes "(\<forall>(PROB :: 'a problem) as (s :: 'a state).
     (P PROB) 
     \<and> (s \<in> valid_states PROB) 
     \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as) 
       \<and> (length as' < f PROB)
     )
   )"
   shows "(\<forall>PROB x. P PROB
     \<longrightarrow> (x \<in> MPLS(PROB)) 
     \<longrightarrow> (x < f PROB)
   )"
 proof -
   {
     fix PROB :: "'a problem" and as and s :: "'a state"
     assume "(P PROB)"
       "(s \<in> valid_states PROB)"
       "(as \<in> valid_plans PROB)"
       "(\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> (subseq as' as) 
         \<and> (length as' < f PROB)
       )"
     then have "(\<exists>x. x \<in> PLS s as \<and> x < f PROB)"
       using assms(1) bound_child_parent_card_state_set_cons[where P = P and f = f]
       by presburger
   }
   note 1 = this
   {
     fix PROB x
     assume P1: "P PROB" "x \<in> MPLS PROB"
       \<comment> \<open>TODO refactor 'x\_in\_MPLS\_if' and use here.\<close>
     then obtain s as where a:
       "x = Inf (PLS s as)" "s \<in> valid_states PROB" "as \<in> valid_plans PROB"
       unfolding MPLS_def
       by auto
     moreover have "(\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as) 
       \<and> (length as' < f PROB)
     )"
       using P1(1) assms calculation(2, 3) 
       by blast
     ultimately obtain x' where "x' \<in> PLS s as" "x' < f PROB"
       using P1 1
       by blast
     then have "x < f PROB"
       using a(1) mem_lt_imp_MIN_lt
       by fastforce
   }
   then show ?thesis
     by blast
 qed
 
 
 lemma bound_child_parent_card_state_set_cons_finite: 
   fixes P f
   assumes "(\<forall>PROB as s.
     P PROB \<and> finite PROB \<and> as \<in> (valid_plans PROB) \<and> s \<in> (valid_states PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> subseq as' as 
       \<and> length as' < f(PROB)
     )
   )"
   shows "(\<forall>PROB s as. 
     P PROB \<and> finite PROB \<and> as \<in> (valid_plans PROB) \<and> (s \<in> (valid_states PROB))
     \<longrightarrow> (\<exists>x. (x \<in> PLS s as) \<and> x < f PROB)
   )"
 proof -
   {
     fix PROB s as
     assume "P PROB" "finite PROB" "as \<in> (valid_plans PROB)" "s \<in> (valid_states PROB)"
       " (\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> subseq as' as 
         \<and> length as' < f PROB
       )"
       (* NOTE[1]
         moreover have "exec_plan s as \<in> valid_states PROB" 
           using calculation valid_as_valid_exec by blast
     *)
     then obtain as' where 
       "(exec_plan s as = exec_plan s as')" "subseq as' as" "length as' < f PROB"
       by blast
     moreover have "length as' \<in> PLS s as" 
       unfolding PLS_def
       using calculation
       by fastforce
     ultimately have "(\<exists>x. (x \<in> PLS s as) \<and> x < f PROB)"
       by blast
   }
   then show "(\<forall>PROB s as. 
     P PROB  
     \<and> finite PROB
     \<and> as \<in> (valid_plans PROB)
     \<and> (s \<in> (valid_states PROB))
     \<longrightarrow> (\<exists>x. (x \<in> PLS s as) \<and> x < f PROB)
   )" 
     using assms
     by auto
 qed
 
 
 lemma bound_on_all_plans_bounds_MPLS_finite: 
   fixes P f
   assumes "(\<forall>PROB as s. 
     P PROB \<and> finite PROB \<and> s \<in> (valid_states PROB) \<and> as \<in> (valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> subseq as' as 
       \<and> length as' < f(PROB)
     )
   )"
   shows "(\<forall>PROB x. 
     P PROB \<and> finite PROB 
     \<longrightarrow> (x \<in> MPLS PROB)
     \<longrightarrow> x < f PROB
   )"
 proof -
   {
     fix PROB x
     assume P1: "P PROB" "finite PROB" "x \<in> MPLS PROB"
       \<comment> \<open>TODO refactor 'x\_in\_MPLS\_if' and use here.\<close>
     then obtain s as where a:
       "x = Inf (PLS s as)" "s \<in> valid_states PROB" "as \<in> valid_plans PROB"
       unfolding MPLS_def
       by auto
     moreover have "(\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as) 
       \<and> (length as' < f PROB)
     )"
       using P1(1, 2) assms calculation(2, 3)
       by blast
     moreover obtain x' where "x' \<in> PLS s as" "x' < f PROB"
       using PLS_def calculation(4)
       by fastforce 
     then have "x < f PROB" 
       using a(1) mem_lt_imp_MIN_lt 
       by fastforce
   }
   then show ?thesis
     using assms
     by blast
 qed
 
 
 lemma bound_on_all_plans_bounds_problem_plan_bound: 
   fixes P f
   assumes "(\<forall>PROB as s. 
     (P PROB) 
     \<and> finite PROB
     \<and> (s \<in> valid_states PROB) 
     \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as')
       \<and> (subseq as' as)
       \<and> (length as' < f PROB)
     )
   )"
   shows "(\<forall>PROB. 
     (P PROB) 
     \<and> finite PROB
     \<longrightarrow> (problem_plan_bound PROB < f PROB)
   )"
 proof -
   have 1: "\<forall>PROB x. 
     P PROB 
     \<and> finite PROB 
     \<longrightarrow> x \<in> MPLS PROB   
     \<longrightarrow> x < f PROB
   "
     using assms bound_on_all_plans_bounds_MPLS_finite
     by blast
   {
     fix PROB x
     assume "P PROB \<and> finite PROB 
       \<longrightarrow> x \<in> MPLS PROB   
       \<longrightarrow> x < f PROB
     "
     then have "\<forall>PROB.
       P PROB \<and> finite PROB 
       \<longrightarrow> problem_plan_bound PROB < f PROB
     " 
       unfolding problem_plan_bound_def
       using 1 bound_child_parent_not_eq_last_diff_paths 1 MPLS_nempty
       by metis
     then have "\<forall>PROB.
       P PROB \<and> finite PROB 
       \<longrightarrow> problem_plan_bound PROB < f PROB
     " 
       using MPLS_nempty
       by blast 
 
   }
   then show "(\<forall>PROB. 
     (P PROB) 
     \<and> finite PROB
     \<longrightarrow> (problem_plan_bound PROB < f PROB)
   )"
     using 1
     by blast
 qed
 
 
 lemma bound_child_parent_card_state_set_cons_thesis: 
   assumes "finite PROB" "(\<forall>as s. 
     as \<in> (valid_plans PROB) 
     \<and> s \<in> (valid_states PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as')
       \<and> subseq as' as 
       \<and> length as' < k
     ) 
   )" "as \<in> (valid_plans PROB)" "(s \<in> (valid_states PROB))" 
   shows "(\<exists>x. (x \<in> PLS s as) \<and> x < k)"
   unfolding PLS_def 
   using assms
   by fastforce
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 \<comment> \<open>TODO refactor/move up.\<close>
 lemma x_in_MPLS_if: 
   fixes x PROB 
   assumes "x \<in> MPLS PROB"  
   shows "\<exists>s as. s \<in> valid_states PROB \<and> as \<in> valid_plans PROB \<and> x = Inf (PLS s as)" 
   using assms
   unfolding MPLS_def
   by fast
 
 lemma bound_on_all_plans_bounds_MPLS_thesis: 
   assumes "finite PROB" "(\<forall>as s. 
     (s \<in> valid_states PROB) 
     \<and> (as \<in> valid_plans PROB)
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' < k)
     )
   )" "(x \<in> MPLS PROB)" 
   shows "(x < k)" 
 proof -
   obtain s as where 1: "s \<in> valid_states PROB" "as \<in> valid_plans PROB" "x = Inf (PLS s as)"
     using assms(3) x_in_MPLS_if 
     by blast
   then obtain x' :: nat where "x' \<in> PLS s as" "x' < k" 
     using assms(1, 2) bound_child_parent_card_state_set_cons_thesis 
     by blast
   then have "Inf (PLS s as) < k"
     using mem_lt_imp_MIN_lt 
     by blast
   then show "x < k" 
     using 1
     by simp
 qed
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 lemma bounded_MPLS_contains_supremum: 
   fixes PROB
   assumes "finite PROB" "(\<exists>k. \<forall>x \<in> MPLS PROB. x < k)" 
   shows "Sup (MPLS PROB) \<in> MPLS PROB" 
 proof -
   obtain k where "\<forall>x \<in> MPLS PROB. x < k" 
     using assms(2)
     by blast
   moreover have "finite (MPLS PROB)"
     using assms(2) finite_nat_set_iff_bounded
     by presburger
   moreover have "MPLS PROB \<noteq> {}" 
     using assms(1) MPLS_nempty
     by auto
   ultimately show "Sup (MPLS PROB) \<in> MPLS PROB"
     unfolding Sup_nat_def
     by simp
 qed
 
 lemma bound_on_all_plans_bounds_problem_plan_bound_thesis': 
   assumes "finite PROB" "(\<forall>as s. 
       s \<in> (valid_states PROB) 
       \<and> as \<in> (valid_plans PROB)
       \<longrightarrow> (\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> subseq as' as 
         \<and> length as' < k
       )
     )"
   shows "problem_plan_bound PROB < k" 
 proof -
   have 1: "\<forall>x \<in> MPLS PROB. x < k" 
     using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis 
     by blast
   then have "Sup (MPLS PROB) \<in> MPLS PROB" 
     using assms(1) bounded_MPLS_contains_supremum 
     by auto
   then have "Sup (MPLS PROB) < k" 
     using 1
     by blast
   then show ?thesis 
     unfolding problem_plan_bound_def
     by simp
 qed
 
 
 lemma bound_on_all_plans_bounds_problem_plan_bound_thesis: 
   assumes "finite PROB" "(\<forall>as s. 
       (s \<in> valid_states PROB) 
       \<and> (as \<in> valid_plans PROB) 
       \<longrightarrow> (\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> (subseq as' as)
         \<and> (length as' \<le> k)
       )
     )"
   shows "(problem_plan_bound PROB \<le> k)" 
 proof -
   have 1: "\<forall>x\<in>MPLS PROB. x < k + 1" 
     using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis[where k = "k + 1"] Suc_eq_plus1 
       less_Suc_eq_le
     by metis
   then have "Sup (MPLS PROB) \<in> MPLS PROB" 
     using assms(1) bounded_MPLS_contains_supremum 
     by fast
   then show "(problem_plan_bound PROB \<le> k)"
     unfolding problem_plan_bound_def 
     using 1
     by fastforce
 qed
 
 
 lemma  bound_on_all_plans_bounds_problem_plan_bound_: 
   fixes P f PROB
   assumes "(\<forall>PROB' as s. 
       finite PROB \<and> (P PROB') \<and> (s \<in> valid_states PROB') \<and> (as \<in> valid_plans PROB') 
       \<longrightarrow> (\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> (subseq as' as)
         \<and> (length as' < f PROB')
       )
     )" "(P PROB)" "finite PROB" 
   shows "(problem_plan_bound PROB < f PROB)"
   unfolding problem_plan_bound_def MPLS_def
   using assms bound_on_all_plans_bounds_problem_plan_bound_thesis' expanded_problem_plan_bound_thm_1
   by metis
 
 
 lemma S_VALID_AS_VALID_IMP_MIN_IN_PLS: 
   fixes PROB s as
   assumes "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)" 
   shows "(Inf (PLS s as) \<in> (MPLS PROB))" 
   unfolding MPLS_def
   using assms
   by fast
 
 
 \<comment> \<open>NOTE type of `s` had to be fixed (type mismatch in goal).\<close>
 \<comment> \<open>NOTE premises rewritten to implications for proof set up.\<close>
 lemma problem_plan_bound_ge_min_pls: 
   fixes PROB :: "'a problem" and s :: "'a state" and as k
   assumes "finite PROB" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)" 
     "(problem_plan_bound PROB \<le> k)"
   shows "(Inf (PLS s as) \<le> problem_plan_bound PROB)"
 proof -
   have "Inf (PLS s as) \<in> MPLS PROB" 
     using assms(2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS 
     by blast
   moreover have "finite (MPLS PROB)" 
     using assms(1) FINITE_MPLS 
     by blast
   ultimately have "Inf (PLS s as) \<le> Sup (MPLS PROB)"
     using le_cSup_finite
     by blast 
   then show ?thesis 
     unfolding problem_plan_bound_def
     by simp
 qed
 
 
 lemma  PLS_NEMPTY: 
   fixes s as 
   shows "PLS s as \<noteq> {}"
   unfolding PLS_def
   by blast
 
 
 lemma  PLS_nempty_and_has_min: 
   fixes s as 
   shows "(\<exists>x. (x \<in> PLS s as) \<and> (x = Inf (PLS s as)))"
 proof -
   have "PLS s as \<noteq> {}" 
     using PLS_NEMPTY 
     by blast
   then have "Inf (PLS s as) \<in> PLS s as"
     unfolding Inf_nat_def
     using LeastI_ex Max_in finite_PLS
     by metis 
   then show ?thesis 
     by blast
 qed
 
 
 lemma  PLS_works: 
   fixes x s as
   assumes "(x \<in> PLS s as)" 
   shows"(\<exists>as'. 
       (exec_plan s as = exec_plan s as')
       \<and> (length as' = x) 
       \<and> (subseq as' as)
     )"
   using assms
   unfolding PLS_def
   by (smt imageE mem_Collect_eq)
 
 
 \<comment> \<open>NOTE type of `s` had to be fixed (type mismatch in goal).\<close>
 lemma problem_plan_bound_works: 
   fixes PROB :: "'a problem" and as and s :: "'a state"
   assumes "finite PROB" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)" 
   shows "(\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' \<le> problem_plan_bound PROB)
     )"
 proof -
   have "problem_plan_bound PROB \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms(1) bound_main_lemma 
     by blast
   then have 1: "Inf (PLS s as) \<le> problem_plan_bound PROB"
     using 
       assms(1, 2, 3)
       problem_plan_bound_ge_min_pls
     by blast
   then have "\<exists>x. x \<in> PLS s as \<and> x = Inf (PLS s as)" 
     using PLS_nempty_and_has_min
     by blast 
   then have "Inf (PLS s as) \<in> (PLS s as)"
     by blast 
   then obtain as' where 2:
     "exec_plan s as = exec_plan s as'" "length as' = Inf (PLS s as)" "subseq as' as"
     using PLS_works
     by blast
   then have "length as' \<le> problem_plan_bound PROB" 
     using 1
     by argo
   then show "(\<exists>as'. 
     (exec_plan s as = exec_plan s as') 
     \<and> (subseq as' as)
     \<and> (length as' \<le> problem_plan_bound PROB)
   )"  
     using 2(1) 2(3)
     by blast
 qed
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition MPLS_s where
   "MPLS_s PROB s \<equiv> (\<lambda> (s, as). Inf (PLS s as)) ` {(s, as) | as. as \<in> valid_plans PROB}"
 
 
 \<comment> \<open>NOTE type of `PROB` had to be fixed (type mismatch in goal).\<close>
 lemma bound_main_lemma_s_3: 
   fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set" and s
   shows "MPLS_s PROB s \<noteq> {}"
 proof -
   \<comment> \<open>TODO @{term "(s, []) \<in> {}"} could be refactored (this is used in 'MPLS\_nempty' too).\<close>
   have "[] \<in> valid_plans PROB" 
     using empty_plan_is_valid 
     by blast
   then have "(s, []) \<in> {(s, as). as \<in> valid_plans PROB}" 
     by simp
   then show "MPLS_s PROB s \<noteq> {}"
     unfolding MPLS_s_def
     by blast
 qed
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition problem_plan_bound_s where
   "problem_plan_bound_s PROB s = Sup (MPLS_s PROB s)"
 
 
 \<comment> \<open>NOTE removed typing from assumption due to matching problems in later proofs.\<close>
 lemma  bound_on_all_plans_bounds_PLS_s: 
   fixes P f 
   assumes "(\<forall>PROB as s.  
     finite PROB \<and> (P PROB) \<and> (as \<in> valid_plans PROB) \<and> (s \<in> valid_states PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as')
       \<and> (subseq as' as)
       \<and> (length as' < f PROB s)
     )
   )"
   shows "(\<forall>PROB s as. 
     finite PROB \<and> (P PROB) \<and> (as \<in> valid_plans PROB) \<and> (s \<in> valid_states PROB)
     \<longrightarrow> (\<exists>x. 
       (x \<in> PLS s as) 
       \<and> (x < f PROB s)
     )
   )"
 
   using assms 
   unfolding PLS_def
   by fastforce
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 lemma bound_on_all_plans_bounds_MPLS_s_i:
   fixes PROB s x
   assumes "s \<in> valid_states PROB" "x \<in> MPLS_s PROB s" 
   shows "\<exists>as. x = Inf (PLS s as) \<and> as \<in> valid_plans PROB" 
 proof -
   let ?S="{(s, as) | as. as \<in> valid_plans PROB}"
   obtain x' where 1: 
     "x' \<in> ?S"
     "x = (\<lambda> (s, as). Inf (PLS s as)) x'"
     using assms 
     unfolding MPLS_s_def
     by blast
   let ?as="snd x'"
   let ?s="fst x'"
   have "?as \<in> valid_plans PROB"
     using 1(1) 
     by auto
   moreover have "?s = s"
     using 1(1)
     by fastforce
   moreover have "x = Inf (PLS ?s ?as)"
     using 1(2)
     by (simp add: case_prod_unfold)
   ultimately show ?thesis 
     by blast
 qed
 
 lemma bound_on_all_plans_bounds_MPLS_s: 
   fixes P f
   assumes "(\<forall>PROB as s.
     finite PROB \<and> (P PROB) \<and> (as \<in> valid_plans PROB)  \<and> (s \<in> valid_states PROB)
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' < f PROB s)
     )
   )"
   shows "(\<forall>PROB x s. 
     finite PROB \<and> (P PROB) \<and> (s \<in> valid_states PROB) \<longrightarrow> (x \<in> MPLS_s PROB s) 
      \<longrightarrow> (x < f PROB s)
   )"
   using assms
   unfolding MPLS_def
 
 proof -
   have 1: "\<forall>PROB s as.
      finite PROB \<and> P PROB \<and> as \<in> valid_plans PROB \<and> s \<in> valid_states PROB \<longrightarrow>
      (\<exists>x. x \<in> PLS s as \<and> x < f PROB s)"
     using bound_on_all_plans_bounds_PLS_s[OF assms] .
   {
     fix PROB x and s :: "('a, 'b) fmap"
     assume P1: "finite PROB" "(P PROB)" "(s \<in> valid_states PROB)" 
     {
       assume "(x \<in> MPLS_s PROB s)"
       then obtain as where i: "x = Inf (PLS s as)" "as \<in> valid_plans PROB"
         using P1 bound_on_all_plans_bounds_MPLS_s_i
         by blast
       then obtain x' where "x' \<in> PLS s as" "x' < f PROB s"
         using P1 i 1
         by blast
       then have "x < f PROB s"
         using mem_lt_imp_MIN_lt i(1) 
         by blast 
     }
     then have "(x \<in> MPLS_s PROB s) \<longrightarrow> (x < f PROB s)" 
       by blast
   }
   then show ?thesis
     by blast
 qed
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 lemma Sup_MPLS_s_lt_if: 
   fixes PROB s k
   assumes "(\<forall>x\<in>MPLS_s PROB s. x < k)"
   shows "Sup (MPLS_s PROB s) < k"
 proof -
   have "MPLS_s PROB s \<noteq> {}" 
     using bound_main_lemma_s_3
     by fast
   then have "Sup (MPLS_s PROB s) \<in> MPLS_s PROB s"
     using assms Sup_nat_def bounded_nat_set_is_finite
     by force
   then show "Sup (MPLS_s PROB s) < k"
     using assms
     by blast
 qed
 
 \<comment> \<open>NOTE type of `P` had to be fixed (type mismatch in goal).\<close>
 lemma bound_child_parent_lemma_s_2: 
   fixes PROB :: "'a problem" and P :: "'a problem \<Rightarrow> bool" and s f
   assumes "(\<forall>(PROB :: 'a problem) as s. 
     finite PROB \<and> (P PROB) \<and> (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' < f PROB s)
     )
   )"
   shows "(
     finite PROB \<and> (P PROB) \<and> (s \<in> valid_states PROB)
     \<longrightarrow> problem_plan_bound_s PROB s < f PROB s
   )"
 proof -
   \<comment> \<open>NOTE manual instantiation is required (automation fails otherwise).\<close>
   have "\<forall>(PROB :: 'a problem) x s. 
     finite PROB \<and> P PROB \<and> s \<in> valid_states PROB 
     \<longrightarrow> x \<in> MPLS_s PROB s 
     \<longrightarrow> x < f PROB s
   "
     using assms bound_on_all_plans_bounds_MPLS_s[of P f]
     by simp
   then show
     "finite PROB \<and> (P PROB) \<and> (s \<in> valid_states PROB) \<longrightarrow> (problem_plan_bound_s PROB s < f PROB s)"
     unfolding problem_plan_bound_s_def 
     using Sup_MPLS_s_lt_if problem_plan_bound_s_def
     by metis
 qed
 
 
 theorem bound_main_lemma_reachability_s: 
   fixes PROB :: "'a problem" and s
   assumes "finite PROB" "s \<in> valid_states PROB" 
   shows "(problem_plan_bound_s PROB s < card (reachable_s PROB s))"
 proof -
   \<comment> \<open>NOTE derive premise for MP of 'bound\_child\_parent\_lemma\_s\_2'.\<close>
   \<comment> \<open>NOTE type of `s` had to be fixed (warning in assumption declaration).\<close>
   {
     fix PROB :: "'a problem" and s :: "'a state" and as
     assume P1: "finite PROB" "s \<in> valid_states PROB" "as \<in> valid_plans PROB"
     then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as" 
       "length as' \<le> card (reachable_s PROB s) - 1"
       using P1 main_lemma_reachability_s
       by blast
     then have "length as' < card (reachable_s PROB s)"
       using P1(1, 2) card_reachable_s_non_zero
       by fastforce
     then have "(\<exists>as'. 
       exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' < card (reachable_s PROB s))
     "
       using a 
       by blast
   }
   then have "
     finite PROB \<and> True \<and> s \<in> valid_states PROB 
     \<longrightarrow> problem_plan_bound_s PROB s < card (reachable_s PROB s)
   "
     using bound_child_parent_lemma_s_2[where PROB = PROB and P = "\<lambda>_. True" and s = s
         and f = "\<lambda>PROB s. card (reachable_s PROB s)"]
     by blast
   then show ?thesis 
     using assms(1, 2)
     by blast
 qed
 
 
 lemma  problem_plan_bound_s_LESS_EQ_problem_plan_bound_thm: 
   fixes PROB :: "'a problem" and s :: "'a state"
   assumes "finite PROB" "(s \<in> valid_states PROB)"
   shows "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)"
 proof - 
   {
     fix PROB :: "'a problem" and s :: "'a state" and as
     assume "finite PROB" "s \<in> valid_states PROB" "as \<in> valid_plans PROB" 
     then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as" 
       "length as' \<le> problem_plan_bound PROB"
       using problem_plan_bound_works
       by blast
     then have "length as' < problem_plan_bound PROB + 1"
       by linarith
     then have "\<exists>as'. 
       exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' \<le> problem_plan_bound PROB + 1
     "
       using a 
       by fastforce
   }
     \<comment> \<open>TODO unsure why a proof is needed at all here.\<close>
   then have "\<forall>(PROB :: 'a problem) as s.
    finite PROB \<and> True \<and> s \<in> valid_states PROB \<and> as \<in> valid_plans PROB 
    \<longrightarrow> (\<exists>as'. 
     exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' < problem_plan_bound PROB + 1)
   "
     by (metis Suc_eq_plus1 problem_plan_bound_works le_imp_less_Suc)
   then show "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)" 
     using assms bound_child_parent_lemma_s_2[where PROB = PROB and s = s and P = "\<lambda>_. True" 
         and f = "\<lambda>PROB s. problem_plan_bound PROB + 1"]
     by fast
 qed
 
 
 \<comment> \<open>NOTE lemma `bound\_main\_lemma\_s\_1` skipped (this is being equivalently redeclared later).\<close>
 
 
 lemma AS_VALID_MPLS_VALID: 
   fixes PROB as 
   assumes "(as \<in> valid_plans PROB)" 
   shows "(Inf (PLS s as) \<in> MPLS_s PROB s)"
   using assms
   unfolding MPLS_s_def
   by fast
 
 
 \<comment> \<open>NOTE moved up because it's used in the following lemma.\<close>
 \<comment> \<open>NOTE type of `s` had to be fixed for 'in\_PLS\_leq\_2\_pow\_n'.\<close>
 lemma bound_main_lemma_s_1: 
   fixes PROB :: "'a problem" and s :: "'a state" and x
   assumes "finite PROB" "s \<in> (valid_states PROB)" "x \<in> MPLS_s PROB s"
   shows "(x \<le> (2 ^ card (prob_dom PROB)) - 1)"
 proof -
   obtain as :: "(('a, bool) fmap \<times> ('a, bool) fmap) list" where "as \<in> valid_plans PROB"
     using empty_plan_is_valid 
     by blast
   then obtain x where 1: "x \<in> PLS s as" "x \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms in_PLS_leq_2_pow_n
     by blast
   then have "Inf (PLS s as) \<le> 2 ^ card (prob_dom PROB) - 1" 
     using mem_le_imp_MIN_le[where s = "PLS s as" and k = "2 ^ card (prob_dom PROB) - 1"]
     by blast
   then have "x \<le> 2 ^ card (prob_dom PROB) - 1" 
     using assms(3) 1
     by blast
       \<comment> \<open>TODO unsure why a proof is needed here (typing problem?).\<close>
   then show ?thesis
     using assms(1, 2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS bound_on_all_plans_bounds_MPLS_s_i 
       in_MPLS_leq_2_pow_n
     by metis
 qed
 
 
 lemma problem_plan_bound_s_ge_min_pls: 
   fixes PROB :: "'a problem" and as k s
   assumes "finite PROB" "s \<in> (valid_states PROB)" "as \<in> (valid_plans PROB)" 
     "problem_plan_bound_s PROB s \<le> k"
   shows "(Inf (PLS s as) \<le> problem_plan_bound_s PROB s)"
 proof -
   have "\<forall>x\<in>MPLS_s PROB s. x \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms(1, 2) bound_main_lemma_s_1 by blast
   then have 1: "finite (MPLS_s PROB s)"
     using mems_le_finite[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"]
     by blast
   then have "MPLS_s PROB s \<noteq> {}" 
     using bound_main_lemma_s_3 
     by fast
   then have "Inf (PLS s as) \<in> MPLS_s PROB s" 
     using assms AS_VALID_MPLS_VALID 
     by blast 
   then show "(Inf (PLS s as) \<le> problem_plan_bound_s PROB s)"
     unfolding problem_plan_bound_s_def 
     using 1 le_cSup_finite 
     by blast
 qed
 
 
 theorem bound_main_lemma_s:
   fixes PROB :: "'a problem" and s
   assumes "finite PROB" "(s \<in> valid_states PROB)"
   shows "(problem_plan_bound_s PROB s \<le> 2 ^ (card (prob_dom PROB)) - 1)"
 proof -
   have 1: "\<forall>x\<in>MPLS_s PROB s. x \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms bound_main_lemma_s_1
     by metis 
   then have "MPLS_s PROB s \<noteq> {}" 
     using bound_main_lemma_s_3 
     by fast
   then have "Sup (MPLS_s PROB s) \<le> 2 ^ card (prob_dom PROB) - 1"
     using 1 bound_main_lemma_2[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"]
     by blast
   then show "problem_plan_bound_s PROB s \<le> 2 ^ card (prob_dom PROB) - 1"
     unfolding problem_plan_bound_s_def
     by blast
 qed
 
 
 lemma problem_plan_bound_s_works:
   fixes PROB :: "'a problem" and as s
   assumes "finite PROB" "(as \<in> valid_plans PROB)" "(s \<in> valid_states PROB)"
   shows "(\<exists>as'. 
     (exec_plan s as = exec_plan s as') 
     \<and> (subseq as' as) 
     \<and> (length as' \<le> problem_plan_bound_s PROB s)
   )"
 proof -
   have "problem_plan_bound_s PROB s \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms(1, 3) bound_main_lemma_s 
     by blast
   then have 1: "Inf (PLS s as) \<le> problem_plan_bound_s PROB s"
     using assms problem_plan_bound_s_ge_min_pls[of PROB s as " 2 ^ card (prob_dom PROB) - 1"]
     by blast
   then obtain x where obtain_x: "x \<in> PLS s as \<and> x = Inf (PLS s as)"
     using PLS_nempty_and_has_min
     by blast
   then have "\<exists>as'. exec_plan s as = exec_plan s as' \<and> length as' = Inf (PLS s as) \<and> subseq as' as"
     using PLS_works[where s = s and as = as and x = "Inf (PLS s as)"]
       obtain_x 
     by fastforce
   then show "(\<exists>as'. 
     (exec_plan s as = exec_plan s as') \<and> (subseq as' as) 
     \<and> (length as' \<le> problem_plan_bound_s PROB s)
   )" 
     using 1
     by metis
 qed
 
 
 \<comment> \<open>NOTE skipped second declaration (declared twice in source).\<close>
 lemma PLS_def_ITP2015: 
   fixes s as
   shows "PLS s as = {length as' | as'. (exec_plan s as' = exec_plan s as) \<and> (subseq as' as)}"
   using PLS_def 
   by blast
 
 
 \<comment> \<open>NOTE Set comprehension had to be rewritten to image (there is no pattern matching in the part 
 left of the pipe symbol).\<close>
 lemma expanded_problem_plan_bound_charles_thm: 
   fixes PROB :: "'a problem" 
   shows " 
     problem_plan_bound_charles PROB 
     = Sup (
       {
         Inf (PLS_charles (fst p) (snd p) PROB) 
         | p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)})
   "
   unfolding problem_plan_bound_charles_def MPLS_charles_def
   by blast
 
 
 lemma bound_main_lemma_charles_3:
   fixes PROB :: "'a problem"
   assumes "finite PROB"
   shows "MPLS_charles PROB \<noteq> {}"
 proof -
   have 1: "[] \<in> valid_plans PROB" 
     using empty_plan_is_valid
     by auto
   then obtain s :: "'a state" where obtain_s: "s \<in> valid_states PROB"
     using assms valid_states_nempty
     by auto
   then  have "Inf (PLS_charles s [] PROB) \<in> MPLS_charles PROB" 
     unfolding MPLS_charles_def
     using 1
     by auto
   then show "MPLS_charles PROB \<noteq> {}"
     by blast
 qed
 
 
 lemma in_PLS_charles_leq_2_pow_n: 
   fixes PROB :: "'a problem" and s as
   assumes "finite PROB" "s \<in> valid_states PROB" "as \<in> valid_plans PROB"
   shows "(\<exists>x. 
     (x \<in> PLS_charles s as PROB) 
     \<and> (x \<le> 2 ^ card (prob_dom PROB) - 1))
   "
 proof -
   obtain as' where 1:
     "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' \<le> 2 ^ card (prob_dom PROB) - 1" 
     using assms main_lemma
     by blast
   then have "as' \<in> valid_plans PROB"
     using assms(3) sublist_valid_plan 
     by blast 
   then have "length as' \<in> PLS_charles s as PROB"
     unfolding PLS_charles_def
     using 1
     by auto
   then show ?thesis 
     using 1(3)
     by fast
 qed
 
 
 \<comment> \<open>NOTE added lemma.\<close>
 \<comment> \<open>NOTE this lemma retrieves `s`, `as` for a given @{term "x \<in> MPLS_charles PROB"} and characterizes it as
 the minimum of 'PLS\_charles s as PROB'.\<close>
 lemma x_in_MPLS_charles_then: 
   fixes PROB s as
   assumes "x \<in> MPLS_charles PROB"
   shows "\<exists>s as. 
     s \<in> valid_states PROB \<and> as \<in> valid_plans PROB \<and> x = Inf (PLS_charles s as PROB)
   "
 proof -
   have "\<exists>p \<in> {p. (fst p) \<in> valid_states PROB \<and> (snd p) \<in> valid_plans PROB}. x = Inf (PLS_charles (fst p) (snd p) PROB)"
     using MPLS_charles_def assms 
     by fast
   then obtain p where 1:
     "p \<in> {p. (fst p) \<in> valid_states PROB \<and> (snd p) \<in> valid_plans PROB}" 
     "x = Inf (PLS_charles (fst p) (snd p) PROB)"
     by blast
   then have "fst p \<in> valid_states PROB" "snd p \<in> valid_plans PROB" 
     by blast+
   then show ?thesis 
     using 1 
     by fast
 qed
 
 lemma in_MPLS_charles_leq_2_pow_n:
   fixes PROB :: "'a problem" and x
   assumes "finite PROB" "x \<in> MPLS_charles PROB"
   shows "x \<le> 2 ^ card (prob_dom PROB) - 1"
 proof -
   obtain s as where 1:
     "s \<in> valid_states PROB" "as \<in> valid_plans PROB" "x = Inf (PLS_charles s as PROB)"
     using assms(2) x_in_MPLS_charles_then
     by blast
   then obtain x' where 2: "x' \<in> PLS_charles s as PROB""x' \<le> 2 ^ card (prob_dom PROB) - 1"
     using assms(1) in_PLS_charles_leq_2_pow_n 
     by blast
   then have "x \<le> x'" 
     using 1(3) mem_le_imp_MIN_le
     by blast
   then show ?thesis 
     using 1 2
     by linarith
 qed
 
 
 lemma bound_main_lemma_charles:
   fixes PROB :: "'a problem"
   assumes "finite PROB"
   shows "problem_plan_bound_charles PROB \<le> 2 ^ (card (prob_dom PROB)) - 1"
 proof -
   have 1: "\<forall>x\<in>MPLS_charles PROB. x \<le> 2 ^ (card (prob_dom PROB)) - 1"
     using assms in_MPLS_charles_leq_2_pow_n
     by blast
   then have "MPLS_charles PROB \<noteq> {}"
     using assms bound_main_lemma_charles_3
     by blast
   then have "Sup (MPLS_charles PROB) \<le> 2 ^ (card (prob_dom PROB)) - 1"
     using 1 bound_main_lemma_2 
     by meson
   then show ?thesis 
     using problem_plan_bound_charles_def
     by metis
 qed
 
 
 lemma bound_on_all_plans_bounds_PLS_charles:
   fixes P and f
   assumes "\<forall>(PROB :: 'a problem) as s.
     (P PROB) \<and> finite PROB \<and> (as \<in> valid_plans PROB) \<and> (s \<in> valid_states PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') \<and> (subseq as' as)\<and> (length as' < f PROB))
   "
   shows "(\<forall>PROB s as. 
     (P PROB) \<and> finite PROB \<and> (as \<in> valid_plans PROB)  \<and> (s \<in> valid_states PROB)
     \<longrightarrow> (\<exists>x. 
       (x \<in> PLS_charles s as PROB) 
       \<and> (x < f PROB)))
   "
 proof -
   {
     \<comment> \<open>NOTE type for 's' had to be fixed (type mismatch in first proof step.\<close>
     fix PROB :: "'a problem" and as and s :: "'a state"
     assume P: 
       "P PROB" "finite PROB" "as \<in> valid_plans PROB" "s \<in> valid_states PROB"
       "(\<exists>as'. 
         (exec_plan s as = exec_plan s as') 
         \<and> (subseq as' as)
         \<and> (length as' < f PROB)
       )"
     then obtain as' where 1:
       "(exec_plan s as = exec_plan s as')" "(subseq as' as)" "(length as' < f PROB)"
       using P(5) 
       by blast
     then have 2: "as' \<in> valid_plans PROB"
       using P(3) sublist_valid_plan 
       by blast 
     let ?x = "length as'"
     have "?x \<in> PLS_charles s as PROB"
       unfolding PLS_charles_def
       using 1 2
       by auto
     then have "\<exists>x. x \<in> PLS_charles s as PROB \<and> x < f PROB"
       using 1 2 
       by blast
   }
   then show ?thesis 
     using assms 
     by auto
 qed
 
 
 \<comment> \<open>NOTE added lemma (refactored from `bound\_on\_all\_plans\_bounds\_MPLS\_charles`).\<close>
 lemma bound_on_all_plans_bounds_MPLS_charles_i:
   assumes "\<forall>(PROB :: 'a problem) s as.
     (P PROB) \<and> finite PROB \<and> (as \<in> valid_plans PROB) \<and> (s \<in> valid_states PROB)
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') \<and> (subseq as' as) \<and> (length as' < f PROB))
   "
   shows "\<forall>(PROB :: 'a problem) s as.
     P PROB \<and> finite PROB \<and> as \<in> valid_plans PROB \<and> s \<in> valid_states PROB
     \<longrightarrow> Inf {n. n \<in> PLS_charles s as PROB} < f PROB
   "
 proof -
   {
     fix PROB :: "'a problem" and s as
     have "P PROB \<and> finite PROB \<and> as \<in> valid_plans PROB \<and> s \<in> valid_states PROB
      \<longrightarrow> (\<exists>x. x \<in> PLS_charles s as PROB \<and> x < f PROB)
     "
       using assms bound_on_all_plans_bounds_PLS_charles[of P f]
       by blast
     then have "
       P PROB \<and> finite PROB \<and> as \<in> valid_plans PROB \<and> s \<in> valid_states PROB
       \<longrightarrow> Inf {n. n \<in> PLS_charles s as PROB} < f PROB
     "
       using mem_lt_imp_MIN_lt CollectI
       by metis
   }
   then show ?thesis
     by blast
 qed
 
 lemma bound_on_all_plans_bounds_MPLS_charles:
   fixes P f
   assumes "(\<forall>(PROB :: 'a problem) as s. 
     (P PROB) \<and> finite PROB \<and> (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' < f PROB)
     )
   )"
   shows "(\<forall>PROB x. 
     (P PROB) \<and> finite PROB
     \<longrightarrow> (x \<in> MPLS_charles PROB) 
     \<longrightarrow> (x < f PROB)
   )"
 proof -
   have 1: "\<forall>(PROB :: 'a problem) s as. 
     P PROB \<and> finite PROB \<and> as \<in> valid_plans PROB \<and> s \<in> valid_states PROB
     \<longrightarrow> Inf {n. n \<in> PLS_charles s as PROB} < f PROB
   " 
     using assms bound_on_all_plans_bounds_MPLS_charles_i
     by blast
   moreover
   {
     fix PROB :: "'a problem" and x
     assume P1: "(P PROB)" "finite PROB" "x \<in> MPLS_charles PROB" 
     then obtain s as where a:
       "as \<in> valid_plans PROB" "s \<in> valid_states PROB" "x = Inf (PLS_charles s as PROB)"
       using x_in_MPLS_charles_then 
       by blast
     then have "Inf {n. n \<in> PLS_charles s as PROB} < f PROB"
       using 1 P1
       by blast
     then have "x < f PROB" 
       using a
       by simp
   }
   ultimately show ?thesis
     by blast
 qed
 
 
 \<comment> \<open>NOTE added lemma (refactored from 'bound\_on\_all\_plans\_bounds\_problem\_plan\_bound\_charles').\<close>
 lemma bound_on_all_plans_bounds_problem_plan_bound_charles_i: 
   fixes PROB :: "'a problem"
   assumes "finite PROB" "\<forall>x \<in> MPLS_charles PROB. x < k"
   shows "Sup (MPLS_charles PROB) \<in> MPLS_charles PROB"
 proof -
   have 1: "MPLS_charles PROB \<noteq> {}" 
     using assms(1) bound_main_lemma_charles_3 
     by auto
   then have "finite (MPLS_charles PROB)"
     using assms(2) finite_nat_set_iff_bounded
     by blast
   then show ?thesis 
     unfolding Sup_nat_def
     using 1
     by simp
 qed
 
 lemma bound_on_all_plans_bounds_problem_plan_bound_charles: 
   fixes P f
   assumes "(\<forall>(PROB :: 'a problem) as s. 
     (P PROB) \<and> finite PROB \<and> (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (\<exists>as'. 
       (exec_plan s as = exec_plan s as') 
       \<and> (subseq as' as)
       \<and> (length as' < f PROB)))
   "
   shows "(\<forall>PROB. 
     (P PROB) \<and> finite PROB \<longrightarrow> (problem_plan_bound_charles PROB < f PROB))
   "
 proof -
   have 1: "\<forall>PROB x. P PROB \<and> finite PROB \<longrightarrow> x \<in> MPLS_charles PROB \<longrightarrow> x < f PROB"
     using assms bound_on_all_plans_bounds_MPLS_charles
     by blast
   moreover
   {
     fix PROB
     assume P: "P PROB" "finite PROB" 
     moreover have 2: "\<forall>x. x \<in> MPLS_charles PROB \<longrightarrow> x < f PROB" 
       using 1 P 
       by blast
     moreover
     {
       fix x
       assume P1: "x \<in> MPLS_charles PROB" 
       moreover have "x < f PROB"
         using P(1, 2) P1 1
         by presburger
       moreover have "MPLS_charles PROB \<noteq> {}" 
         using P1
         by blast
       moreover have "Sup (MPLS_charles PROB) < f PROB"
         using calculation(3) 2 bound_child_parent_not_eq_last_diff_paths[of "MPLS_charles PROB" "f PROB"] 
         by blast
       ultimately have "(problem_plan_bound_charles PROB < f PROB)"
         unfolding problem_plan_bound_charles_def 
         by blast
     }
     moreover have "Sup (MPLS_charles PROB) \<in> MPLS_charles PROB" 
       using P(2) 2 bound_on_all_plans_bounds_problem_plan_bound_charles_i
       by blast
     ultimately have "problem_plan_bound_charles PROB < f PROB"
       unfolding problem_plan_bound_charles_def 
       by blast
   }
   ultimately show ?thesis
     by blast
 qed
 
 subsection "The Relation between Diameter, Sublist Diameter and Recurrence Diameter Bounds."
 
 text \<open> The goal of this subsection is to verify the relation between diameter, sublist diameter
 and recurrence diameter bounds given by HOL4 Theorem 1, i.e.
 
   @{term "\<d>(\<delta>) \<le> \<l>(\<delta>) \<and> \<l>(\<delta>) \<le> \<r>\<d>(\<delta>)"}
 
 where @{term "\<d>(\<delta>)"}, @{term "\<l>(\<delta>)"} and @{term "\<r>\<d>(\<delta>)"} denote the diameter, sublist diameter and recurrence diameter bounds.
 [Abdualaziz et al., p.20]
 
 The relevant lemmas are `sublistD\_bounds\_D` and `RD\_bounds\_sublistD` which culminate in 
 theorem `sublistD\_bounds\_D\_and\_RD\_bounds\_sublistD`. \<close>
 
 lemma sublistD_bounds_D:  
   fixes PROB :: "'a problem"
   assumes "finite PROB"
   shows "problem_plan_bound_charles PROB \<le> problem_plan_bound PROB"
 proof -
   \<comment> \<open>NOTE obtain the premise needed for MP of 'bound\_on\_all\_plans\_bounds\_problem\_plan\_bound\_charles'.\<close>
   {
     fix PROB :: "'a problem" and s :: "'a state" and as
     assume P: "finite PROB" "s \<in> valid_states PROB" "as \<in> valid_plans PROB" 
     then have "\<exists>as'. 
       exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' \<le> problem_plan_bound PROB
     " 
       using problem_plan_bound_works
       by blast
     then have "\<exists>as'. 
       exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' < problem_plan_bound PROB + 1
     " 
       by force
   }
   then have "problem_plan_bound_charles PROB < problem_plan_bound PROB + 1"
     using assms bound_on_all_plans_bounds_problem_plan_bound_charles[where f = "\<lambda>PROB. problem_plan_bound PROB + 1"
         and P = "\<lambda>_. True"]
     by blast
   then show ?thesis
     by simp
 qed
 
 
 \<comment> \<open>NOTE added lemma (this was adapted from pred\_setScript.sml:4887 with exlusion of the premise for 
 the empty set since `Max {}` is undefined in Isabelle/HOL.)\<close>
 lemma MAX_SET_ELIM':
   fixes P Q
   assumes "finite P" "P \<noteq> {}" "(\<forall>x. (\<forall>y. y \<in> P \<longrightarrow> y \<le> x) \<and> x \<in> P \<longrightarrow> R x)"
   shows "R (Max P)" 
   using assms
   by force
 
 \<comment> \<open>NOTE added lemma.\<close>
 \<comment> \<open>NOTE adapted from pred\_setScript.sml:4895 (premise `finite P` was added).\<close>
 lemma MIN_SET_ELIM':
   fixes P Q
   assumes "finite P" "P \<noteq> {}" "\<forall>x. (\<forall>y. y \<in> P \<longrightarrow> x \<le> y) \<and> x \<in> P \<longrightarrow> Q x"
   shows "Q (Min P)"
 proof -
   let ?x="Min P" 
   have "Min P \<in> P" 
     using Min_in[OF assms(1) assms(2)]
     by simp
   moreover {
     fix y
     assume P: "y \<in> P"
     then have "?x \<le> y"
       using Min.coboundedI[OF assms(1)]
       by blast
     then have "Q ?x" using P assms
       by auto
   }
   ultimately show ?thesis
     by blast
 qed
 
 \<comment> \<open>NOTE added lemma (refactored from `RD\_bounds\_sublistD`).\<close>
 lemma RD_bounds_sublistD_i_a:
   fixes Pi :: "'a problem" 
   assumes "finite Pi"
   shows "finite {length p - 1 |p. valid_path Pi p \<and> distinct p}" 
 proof -
   {
     let ?ss="{length p - 1 |p. valid_path Pi p \<and> distinct p}"
     let ?ss'="{p. valid_path Pi p \<and> distinct p}"
     have 1: "?ss = (\<lambda>x. length x - 1) ` ?ss'"
       by blast
     {
       \<comment> \<open>NOTE type of `valid\_states Pi` had to be asserted to match `FINITE\_valid\_states`.\<close>
       let ?S="{p. distinct p \<and> set p \<subseteq> (valid_states Pi :: 'a state set)}"
       {
         from assms have "finite (valid_states Pi :: 'a state set)" 
           using FINITE_valid_states[of Pi]
           by simp
         then have "finite ?S"
           using FINITE_ALL_DISTINCT_LISTS
           by blast
       }
       moreover {
         {
           fix x
           assume "x \<in> ?ss'"
           then have "x \<in> ?S" 
           proof (induction x)
             case (Cons a x)
             then have a: "valid_path Pi (a # x)" "distinct (a # x)"
               by blast+
             moreover {
               fix x' 
               assume P: "x' \<in> set (a # x)" 
               then have "x' \<in> valid_states Pi" 
               proof (cases "x")
                 case Nil
                 from a(1) Nil 
                 have "a \<in> valid_states Pi"
                   by simp
                 moreover from P Nil 
                 have "x' = a" 
                   by force
                 ultimately show ?thesis
                   by simp
               next
                 case (Cons a' list)
                 {
                   {
                     from Cons.prems have "valid_path Pi (a # x)"
                       by simp
                     then have "a \<in> valid_states Pi" "valid_path Pi (a' # list)"
                       using Cons 
                       by fastforce+
                   }
                   note a = this
                   moreover {
                     from Cons.prems have "distinct (a # x)"
                       by blast
                     then have "distinct (a' # list)" 
                       using Cons
                       by simp
                   }
                   ultimately 
                   have "(a' # list) \<in> ?ss'" 
                     by blast
                   then have "(a' # list) \<in> ?S" 
                     using Cons Cons.IH 
                     by argo
                 }
                 then show ?thesis
                   using P a(1) local.Cons set_ConsD
                   by fastforce
               qed
             }
             ultimately show ?case
               by blast
           qed simp
         }
         then have "?ss' \<subseteq> ?S"
           by blast
       }
       ultimately have "finite ?ss'"
         using rev_finite_subset 
         by auto
     }
     note 2 = this
     from 1 2 have "finite ?ss" 
       using finite_imageI
       by auto
   }
   then show ?thesis
     by blast
 qed
 
 \<comment> \<open>NOTE added lemma (refactored from `RD\_bounds\_sublistD`).\<close>
 lemma RD_bounds_sublistD_i_b:
   fixes Pi :: "'a problem" 
   shows "{length p - 1 |p. valid_path Pi p \<and> distinct p} \<noteq> {}"
 proof -
   let ?Q="{length p - 1 |p. valid_path Pi p \<and> distinct p}"
   let ?Q'="{p. valid_path Pi p \<and> distinct p}"
   {
     have "valid_path Pi []"
       by simp
     moreover have "distinct []"
       by simp
     ultimately have "[] \<in> ?Q'"
       by simp
   }
   note 1 = this
   have "?Q = (\<lambda>p. length p - 1) ` ?Q'" 
     by blast
   then have "length [] - 1 \<in> ?Q"
     using 1
     by (metis (mono_tags, lifting) image_iff list.size(3))
   then show ?thesis
     by blast
 qed
 
 \<comment> \<open>NOTE added lemma (refactored from `RD\_bounds\_sublistD`).\<close>
 lemma RD_bounds_sublistD_i_c:
   fixes Pi :: "'a problem" and as :: "(('a, bool) fmap \<times> ('a, bool) fmap) list" and x 
     and s :: "('a, bool) fmap" 
   assumes "s \<in> valid_states Pi" "as \<in> valid_plans Pi" 
     "(\<forall>y. y \<in> {length p - 1 |p. valid_path Pi p \<and> distinct p} \<longrightarrow> y \<le> x)" 
     "x \<in> {length p - 1 |p. valid_path Pi p \<and> distinct p}"
   shows "Min (PLS s as) \<le> Max {length p - 1 |p. valid_path Pi p \<and> distinct p}" 
 proof -
   let ?P="(PLS s as)"
   let ?Q="{length p - 1 |p. valid_path Pi p \<and> distinct p}"
   from assms(4) obtain p where 1:
     "x = length p - 1" "valid_path Pi p" "distinct p"
     by blast
   {
     fix p'
     assume "valid_path Pi p'" "distinct p'" 
     then obtain y where "y \<in> ?Q" "y = length p' - 1" 
       by blast
         \<comment> \<open>NOTE we cannot infer @{term "length p' - 1 \<le> length p - 1"} since `length p' = 0` might be true.\<close>
     then have a: "length p' - 1 \<le> length p - 1" 
       using assms(3) 1(1) 
       by meson
   }
   note 2 = this
   {
     from finite_PLS PLS_NEMPTY
     have "finite (PLS s as)" "PLS s as \<noteq> {}"
       by blast+
     moreover {
       fix n
       assume P: "(\<forall>y. y \<in> PLS s as \<longrightarrow> n \<le> y)" "n \<in> PLS s as"
       from P(2) obtain as' where i: 
         "n = length as'" "exec_plan s as' = exec_plan s as" "subseq as' as"
         unfolding PLS_def
         by blast
       let ?p'="statelist' s as'"
       {
         have "length as' = length ?p' - 1" 
           by (simp add: LENGTH_statelist')        
             \<comment> \<open>MARKER (topologicalPropsScript.sml:195)\<close>
         have "1 + (length p - 1) = length p - 1 + 1" 
           by presburger
             \<comment> \<open>MARKER (topologicalPropsScript.sml:200)\<close>
         {
           from assms(2) i(3) sublist_valid_plan
           have "as' \<in> valid_plans Pi" 
             by blast
           then have "valid_path Pi ?p'"
             using assms(1) valid_path_statelist'
             by auto
         }
         moreover {
           {
             assume C: "\<not>distinct ?p'"
               \<comment> \<open>NOTE renamed variable `drop` to `drop'` to avoid shadowing of the function by the 
             same name in Isabelle/HOL.\<close>
             then obtain rs pfx drop' tail where C_1: "?p' = pfx @ [rs] @ drop' @ [rs] @ tail" 
               using not_distinct_decomp[OF C]
               by fast
             let ?pfxn="length pfx"
             have C_2: "?p' ! ?pfxn = rs"
               by (simp add: C_1) 
             from LENGTH_statelist'
             have C_3: "length as' + 1 = length ?p'" 
               by metis
             then have "?pfxn \<le> length as'"
               using C_1
               by fastforce
             then have C_4: "exec_plan s (take ?pfxn as') = rs" 
               using C_2 statelist'_TAKE
               by blast
             let ?prsd = "length (pfx @ [rs] @ drop')"
             let ?ap1 = "take ?pfxn as'" 
               \<comment> \<open>MARKER (topologicalPropsScript.sml:215)\<close>
             from C_1 
             have C_5: "?p' ! ?prsd = rs"
               by (metis append_Cons length_append nth_append_length nth_append_length_plus)
             from C_1 C_3 
             have C_6: "?prsd \<le> length as'" 
               by simp
             then have C_7: "exec_plan s (take ?prsd as') = rs" 
               using C_5 statelist'_TAKE
               by auto
             let ?ap2="take ?prsd as'"
             let ?asfx="drop ?prsd as'" 
             have C_8: "as' = ?ap2 @ ?asfx"
               by force
             then have "exec_plan s as' = exec_plan (exec_plan s ?ap2) ?asfx"
               using exec_plan_Append
               by metis
             then have C_9: "exec_plan s as' = exec_plan s (?ap1 @ ?asfx)"
               using C_4 C_7 exec_plan_Append
               by metis
             from C_6 
             have C_10: "(length ?ap1 = ?pfxn) \<and> (length ?ap2 = ?prsd)" 
               by fastforce
             then have C_11: "length (?ap1 @ ?asfx) < length (?ap2 @ ?asfx)"
               by auto
             {         
               from C_10 
               have "?pfxn + length ?asfx = length (?ap1 @ ?asfx)"   
                 by simp
               from C_9 i(2)
               have C_12: "exec_plan s (?ap1 @ ?asfx) = exec_plan s as" 
                 by argo
               {
                 {
                   {
                     have "prefix ?ap1 ?ap2"
                       by (metis (no_types) length_append prefix_def take_add) 
                     then have "subseq ?ap1 ?ap2"
                       using isPREFIX_sublist
                       by blast
                   }
                   moreover have "sublist ?asfx ?asfx"
                     using sublist_refl
                     by blast
                   ultimately have "subseq (?ap1 @ ?asfx) as'"
                     using C_8 subseq_append
                     by metis
                 }
                 moreover from i(3)
                 have "subseq as' as"
                   by simp
                 ultimately have "subseq (?ap1 @ ?asfx) as"
                   using sublist_trans
                   by blast
               }
               then have "length (?ap1 @ ?asfx) \<in> PLS s as"
                 unfolding PLS_def 
                 using C_12 
                 by blast
             }
             then have False 
               using P(1) i(1) C_10
               by auto
           }
           hence "distinct ?p'" 
             by auto
         }
         ultimately have "length ?p' - 1 \<le> length p - 1" 
           using 2 
           by blast
       }
       note ii = this
       {
         from i(1) have "n + 1 = length ?p'"
           using LENGTH_statelist'[symmetric]
           by blast
         also have "\<dots> \<le> 1 + (length p - 1)"
           using ii
           by linarith
         finally have "n \<le> length p - 1" 
           by fastforce
       }
       then have "n \<le> length p - 1"
         by blast
     }
     ultimately have "Min ?P \<le> length p - 1" 
       using MIN_SET_ELIM'[where P="?P" and Q="\<lambda>x. x \<le> length p - 1"]
       by blast
   }
   note 3 = this
   {
     have "length p - 1 \<le> Max {length p - 1 |p. valid_path Pi p \<and> distinct p}" 
       using assms(3, 4) 1(1)
-      by (metis (no_types, lifting) Sup_nat_def assms(3) cSup_eq_maximum)  
+      by (smt Max.coboundedI bdd_aboveI bdd_above_nat)
     moreover 
     have "Min (PLS s as) \<le> length p - 1"
       using 3
       by blast
     ultimately 
     have "Min (PLS s as) \<le> Max {length p - 1 |p. valid_path Pi p \<and> distinct p}"
       by linarith
   }
   then show ?thesis
     by blast
 qed
 
 \<comment> \<open>NOTE added lemma (refactored from `RD\_bounds\_sublistD`).\<close>
 lemma RD_bounds_sublistD_i:
   fixes Pi :: "'a problem" and x
   assumes "finite Pi" "(\<forall>y. y \<in> MPLS Pi \<longrightarrow> y \<le> x)" "x \<in> MPLS Pi" 
   shows "x \<le> Max {length p - 1 |p. valid_path Pi p \<and> distinct p}" 
 proof -
   {
     let ?P="MPLS Pi"
     let ?Q="{length p - 1 |p. valid_path Pi p \<and> distinct p}"
     from assms(3) 
     obtain s as where 1:
       "s \<in> valid_states Pi" "as \<in> valid_plans Pi" "x = Inf (PLS s as)"
       unfolding MPLS_def
       by fast
     have "x \<le> Max ?Q" proof -
       text \<open> Show that `x` is not only the infimum but also the minimum of `PLS s as`.\<close>
       {
         have "finite (PLS s as)" 
           using finite_PLS 
           by auto
         moreover 
         have "PLS s as \<noteq> {}" 
           using PLS_NEMPTY
           by auto
         ultimately 
         have a: "Inf (PLS s as) = Min (PLS s as)" 
           using cInf_eq_Min[of "PLS s as"]
           by blast
         from 1(3) a have "x = Min (PLS s as)"
           by blast
       }
       note a = this
       {
         let ?limit="Min (PLS s as)"
         from assms(1) 
         have a: "finite ?Q" 
           using RD_bounds_sublistD_i_a
           by blast
         have b: "?Q \<noteq> {}"
           using RD_bounds_sublistD_i_b 
           by fast
         from 1(1, 2) 
         have c: "\<forall>x. (\<forall>y. y \<in> ?Q \<longrightarrow> y \<le> x) \<and> x \<in> ?Q \<longrightarrow> ?limit \<le> Max ?Q" 
           using RD_bounds_sublistD_i_c
           by blast
         have "?limit \<le> Max ?Q" 
           using MAX_SET_ELIM'[where P="?Q" and R="\<lambda>x. ?limit \<le> Max ?Q", OF a b c]
           by blast
       }
       note b = this
       from a b show "x \<le> Max ?Q"
         by blast
     qed
   }
   then show ?thesis
     using assms
     unfolding MPLS_def
     by blast
 qed
 
 \<comment> \<open>NOTE type of `Pi` had to be fixed for use of `FINITE\_valid\_states`.\<close>
 lemma RD_bounds_sublistD: 
   fixes Pi :: "'a problem"
   assumes "finite Pi"
   shows "problem_plan_bound Pi \<le> RD Pi"
 proof -
   let ?P="MPLS Pi"
   let ?Q="{length p - 1 |p. valid_path Pi p \<and> distinct p}"
   {
     from assms 
     have 1: "finite ?P" 
       using FINITE_MPLS
       by blast
     from assms 
     have 2: "?P \<noteq> {}"
       using MPLS_nempty
       by blast
     from assms 
     have 3: "\<forall>x. (\<forall>y. y \<in> ?P \<longrightarrow> y \<le> x) \<and> x \<in> ?P \<longrightarrow> x \<le> Max ?Q"
       using RD_bounds_sublistD_i 
       by blast
     have "Max ?P \<le> Max ?Q"
       using MAX_SET_ELIM'[OF 1 2 3]
       by blast
   }
   then show ?thesis 
     unfolding problem_plan_bound_def RD_def Sup_nat_def
     by blast
 qed
 
 
 \<comment> \<open>NOTE type for `PROB` had to be fixed in order to be able to match `sublistD\_bounds\_D`.\<close>
 theorem sublistD_bounds_D_and_RD_bounds_sublistD: 
   fixes PROB :: "'a problem"
   assumes "finite PROB"
   shows "
     problem_plan_bound_charles PROB \<le> problem_plan_bound PROB 
     \<and> problem_plan_bound PROB \<le> RD PROB
   "
   using assms sublistD_bounds_D RD_bounds_sublistD 
   by auto
 
 
 \<comment> \<open>NOTE type of `PROB` had to be fixed for MP of lemmas.\<close>
 lemma empty_problem_bound: 
   fixes PROB :: "'a problem"
   assumes "(prob_dom PROB = {})"
   shows "(problem_plan_bound PROB = 0)"
 proof -
   {
     fix PROB' and as :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) list" and s :: "('a, 'b) fmap"
     assume 
       "finite PROB" "prob_dom PROB' = {}" "s \<in> valid_states PROB'" "as \<in> valid_plans PROB'"
     then have "exec_plan s [] = exec_plan s as"
       using empty_prob_dom_imp_empty_plan_always_good
       by blast
     then have "(\<exists>as'. exec_plan s as = exec_plan s as' \<and> subseq as' as \<and> length as' < 1)"
       by force
   }
   then show ?thesis 
     using bound_on_all_plans_bounds_problem_plan_bound_[where P="\<lambda>P. prob_dom P = {}" and f="\<lambda>P. 1", of PROB]
     using assms empty_prob_dom_finite 
     by blast 
 qed
 
 
 lemma problem_plan_bound_works':
   fixes PROB :: "'a problem" and as s
   assumes "finite PROB" "(s \<in> valid_states PROB)" "(as \<in> valid_plans PROB)"
   shows "(\<exists>as'. 
     (exec_plan s as' = exec_plan s as) 
     \<and> (subseq as' as)
     \<and> (length as' \<le> problem_plan_bound PROB) 
     \<and> (sat_precond_as s as')
   )"
 proof -
   obtain as' where 1:
     "exec_plan s as = exec_plan s as'" "subseq as' as" "length as' \<le> problem_plan_bound PROB"
     using assms problem_plan_bound_works 
     by blast
       \<comment> \<open>NOTE this step seems to be handled implicitely in original proof.\<close>
   moreover have "rem_condless_act s [] as' \<in> valid_plans PROB"
     using assms(3) 1(2) rem_condless_valid_10 sublist_valid_plan
     by blast
   moreover have "subseq (rem_condless_act s [] as') as'" 
     using rem_condless_valid_8 
     by blast
   moreover have "length (rem_condless_act s [] as') \<le> length as'" 
     using rem_condless_valid_3
     by blast
   moreover have "sat_precond_as s (rem_condless_act s [] as')"
     using rem_condless_valid_2
     by blast
   moreover have "exec_plan s as' = exec_plan s (rem_condless_act s [] as')"
     using rem_condless_valid_1
     by blast
   ultimately show ?thesis
     by fastforce
 qed
 
 
 \<comment> \<open>TODO remove? Can be solved directly with 'TopologicalProps.bound\_on\_all\_plans\_bounds\_problem\_plan\_bound\_thesis'.\<close>
 lemma problem_plan_bound_UBound: 
   assumes "(\<forall>as s.
     (s \<in> valid_states PROB) 
     \<and> (as \<in> valid_plans PROB)
     \<longrightarrow> (\<exists>as'.
       (exec_plan s as = exec_plan s as') 
       \<and> subseq as' as 
       \<and> (length as' < f PROB)
     )
   )" "finite PROB"
   shows "(problem_plan_bound PROB < f PROB)"
 proof -
   let ?P = "\<lambda>Pr. PROB = Pr"
   have "?P PROB" by simp
   then show ?thesis
     using assms bound_on_all_plans_bounds_problem_plan_bound_[where P = ?P] 
     by force
 qed 
 
 subsection "Traversal Diameter"
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition traversed_states where
   "traversed_states s as \<equiv> set (state_list s as)" 
 
 
 lemma finite_traversed_states: "finite (traversed_states s as)"
   unfolding traversed_states_def
   by simp
 
 
 lemma traversed_states_nempty: "traversed_states s as \<noteq> {}"
   unfolding traversed_states_def 
   by (induction as) auto
 
 
 lemma traversed_states_geq_1: 
   fixes s
   shows "1 \<le> card (traversed_states s as)"
 proof -
   have "card (traversed_states s as) \<noteq> 0"
     using traversed_states_nempty finite_traversed_states card_0_eq
     by blast
   then show "1 \<le> card (traversed_states s as)"
     by linarith 
 qed
 
 
 lemma init_is_traversed: "s \<in> traversed_states s as"
   unfolding traversed_states_def
   by (induction as) auto
 
 
 \<comment> \<open>NOTE name shortened.\<close>
 definition td where
   "td PROB \<equiv> Sup {
     (card (traversed_states (fst p) (snd p))) - 1 
     | p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)}
   "
 
 
 lemma traversed_states_rem_condless_act: "\<And>s. 
   traversed_states s (rem_condless_act s [] as) = traversed_states s as
 "
   apply(induction as)
   apply(auto simp add: traversed_states_def rem_condless_act_cons)
   subgoal by (simp add: state_succ_pair)
   subgoal using init_is_traversed traversed_states_def by blast
   subgoal by (simp add: state_succ_pair) 
   done
 
 \<comment> \<open>NOTE added lemma.\<close>
 lemma td_UBound_i: 
   fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set"
   assumes "finite PROB" 
   shows "
   {
     (card (traversed_states (fst p) (snd p))) - 1 
     | p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)}
   \<noteq> {}
   "
 proof -
   let ?S="{p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)}"
   obtain s :: "'a state" where "s \<in> valid_states PROB" 
     using assms valid_states_nempty
     by blast
   moreover have "[] \<in> valid_plans PROB"
     using empty_plan_is_valid
     by auto
   ultimately have "?S \<noteq> {}"
     using assms valid_states_nempty 
     by auto  
   then show ?thesis
     by blast 
 qed
 
 lemma td_UBound: 
   fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set" 
   assumes "finite PROB" "(\<forall>s as. 
     (sat_precond_as s as) \<and> (s \<in> valid_states PROB) \<and> (as \<in> valid_plans PROB) 
     \<longrightarrow> (card (traversed_states s as) \<le> k)
   )"
   shows "(td PROB \<le> k - 1)"
 proof -
   let ?S="{
     (card (traversed_states (fst p) (snd p))) - 1 
     | p. (fst p \<in> valid_states PROB) \<and> (snd p \<in> valid_plans PROB)}
   "
   {
     fix x
     assume "x \<in> ?S"
     then obtain p where 1:
       "x = card (traversed_states (fst p) (snd p)) - 1" "fst p \<in> valid_states PROB" 
       "snd p \<in> valid_plans PROB"
       by blast
     let ?s="fst p"
     let ?as="snd p" 
     {
       let ?as'="(rem_condless_act ?s [] ?as)"
       have 2: "traversed_states ?s ?as = traversed_states ?s ?as'"
         using traversed_states_rem_condless_act
         by blast
       moreover have "sat_precond_as ?s ?as'"
         using rem_condless_valid_2
         by blast
       moreover have "?as' \<in> valid_plans PROB"
         using 1(3) rem_condless_valid_10
         by blast
       ultimately have "card (traversed_states ?s ?as') \<le> k"
         using assms(2) 1(2)
         by blast 
       then have "card (traversed_states ?s ?as) \<le> k"
         using 2
         by argo
     }
     then have "x \<le> k - 1" 
       using 1
       by linarith
   }
   moreover have "?S \<noteq> {}"
     using assms td_UBound_i
     by fast
   ultimately show ?thesis
     unfolding td_def
     using td_UBound_i bound_main_lemma_2[of ?S "k - 1"]
     by presburger
 qed
 
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy b/thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy
--- a/thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy
+++ b/thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy
@@ -1,1012 +1,1007 @@
 (*  Title:      NatInt.thy
     Author:     Sven Linker, University of Liverpool
 
 Intervals based on natural numbers. Defines a 
 bottom element (empty set), infimum (set intersection),
 partial order (subset relation), cardinality (set cardinality).
 
 The union of intervals i and j can only be created, if they are consecutive, i.e.,
 max i +1 = min j (or vice versa). To express consecutiveness, we employ the 
 predicate consec.
 
 Also contains a "chopping" predicate N_Chop(i,j,k): i can be divided into
 consecutive intervals j and k.
 *)
 
 section \<open>Discrete Intervals based on Natural Numbers\<close>
 
 text\<open>We define a type of intervals based on the natural numbers. To that 
 end, we employ standard operators of Isabelle, but in addition prove some
 structural properties of the intervals. In particular, we show that this type
 constitutes a meet-semilattice with a bottom element and equality.
 
 Furthermore, we show that this semilattice allows for a constrained join, i.e.,
 the union of two intervals is defined, if either one of them is empty, or they are
 consecutive. Finally, we define the notion of \emph{chopping} an interval into
 two consecutive subintervals.\<close>
 
 theory NatInt
   imports Main 
 begin
 
 text \<open>A discrete interval is a set of consecutive natural numbers, or the empty 
 set.\<close>
 
 typedef nat_int = "{S . (\<exists> (m::nat) n . {m..n }=S) }"  
   by auto
 setup_lifting type_definition_nat_int
 
 subsection \<open>Basic properties of discrete intervals.\<close>
   
 locale nat_int 
 interpretation nat_int_class?: nat_int .
 
 context nat_int
 begin
   
 lemma un_consec_seq: "(m::nat)\<le> n \<and> n+1 \<le> l \<longrightarrow> {m..n} \<union> {n+1..l} = {m..l}" 
   by auto
     
 lemma int_conseq_seq: " {(m::nat)..n} \<inter> {n+1..l} = {}"
   by auto
         
 lemma empty_type: "{} \<in> { S . \<exists> (m:: nat) n . {m..n}=S}"
   by auto
     
 lemma inter_result: "\<forall>x \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }. 
          \<forall>y \<in> {S . (\<exists> (m::nat) n . {m..n }=S) }. 
            x \<inter> y \<in>{S . (\<exists> (m::nat) n .  {m..n }=S)}" 
   using Int_atLeastAtMost by blast      
     
 lemma union_result: "\<forall>x \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }. 
          \<forall>y \<in> {S . (\<exists> (m::nat) n .  {m..n }=S)  }. 
            x \<noteq> {} \<and> y \<noteq> {} \<and> Max x +1 = Min y 
             \<longrightarrow> x \<union> y \<in>{S . (\<exists> (m::nat) n . {m..n }=S)  }"  
 proof (rule ballI)+
   fix x y
   assume "x\<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }" 
     and "y\<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }"
   then have x_def:"(\<exists>m n.  {m..n} = x) "  
     and y_def:"(\<exists>m n.  {m..n} = y) " by blast+    
   show   " x \<noteq> {} \<and> y \<noteq> {} \<and>   Max x+1 = Min y 
             \<longrightarrow> x \<union>  y \<in> {S. (\<exists>m n.  {m..n} = S) }"
   proof
     assume pre:"x \<noteq> {} \<and> y \<noteq> {} \<and> Max x + 1 = Min y"
     then have x_int:"\<exists>m n. m \<le> n \<and> {m..n} = x" 
           and y_int:"(\<exists>m n. m \<le> n \<and> {m..n} = y)"
       using  x_def y_def by force+      
     {
       fix ya yb xa xb
-      assume y_prop:"ya \<le> yb \<and> {ya..yb} = y"
-      assume x_prop:"xa \<le> xb \<and> {xa..xb} = x"          
-      from  x_prop have upper_x:"Max x = xb" 
-        by (metis Sup_nat_def cSup_atLeastAtMost)
-      from y_prop have lower_y:"Min y = ya" 
-        by (metis Inf_fin.coboundedI Inf_fin_Min Min_in add.right_neutral finite_atLeastAtMost
-            le_add1 ord_class.atLeastAtMost_iff order_class.antisym pre)
+      assume y_prop:"ya \<le> yb \<and> {ya..yb} = y" and x_prop:"xa \<le> xb \<and> {xa..xb} = x"          
+      then have upper_x:"Max x = xb" and lower_y: "Min y = ya" 
+        by (auto simp: Max_eq_iff Min_eq_iff)
       from upper_x and lower_y and pre have upper_eq_lower: "xb+1 = ya" 
         by blast
       hence "y= {xb+1 .. yb}" using y_prop by blast
       hence "x \<union> y = {xa..yb}" 
         using un_consec_seq upper_eq_lower x_prop y_prop by blast
       then have " x \<union> y \<in> {S.(\<exists>m n.  {m..n} = S) }"
         by auto
     }      
     then show "x \<union> y \<in> {S.(\<exists>m n.  {m..n} = S)}" 
       using x_int y_int by blast
   qed
 qed
   
   
 
 lemma union_empty_result1: "\<forall>i \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }.
                                   i \<union> {} \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) }" 
   by blast   
 
 lemma union_empty_result2: "\<forall>i \<in> {S . (\<exists> (m::nat) n . {m..n }=S)  }.
                                   {} \<union> i \<in> {S . (\<exists> (m::nat) n . {m..n }=S)  }" 
   by blast 
     
 lemma finite:" \<forall>i \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) } . (finite i)"
   by blast
     
 lemma not_empty_means_seq:"\<forall>i \<in> {S . (\<exists> (m::nat) n .  {m..n }=S) } . i \<noteq> {}
                             \<longrightarrow> ( \<exists>m n . m \<le> n \<and> {m..n} = i)" 
   using atLeastatMost_empty_iff 
   by force   
 end
   
 text \<open>The empty set is the bottom element of the type. The infimum/meet of 
 the semilattice is set intersection. The order is given by the subset relation.
 \<close>
 
 instantiation nat_int :: bot
 begin
 lift_definition bot_nat_int :: "nat_int" is Set.empty by force
 instance by standard
 end
 
 instantiation nat_int ::  inf
 begin
 lift_definition inf_nat_int  ::"nat_int \<Rightarrow> nat_int \<Rightarrow> nat_int" is Set.inter  by force
 instance
 proof qed
 end
 
 instantiation nat_int :: "order_bot"
 begin
 lift_definition less_eq_nat_int :: "nat_int \<Rightarrow> nat_int \<Rightarrow> bool" is Set.subset_eq .
 lift_definition less_nat_int :: "nat_int \<Rightarrow> nat_int \<Rightarrow> bool" is Set.subset .
 instance
 proof
   fix i j k ::nat_int
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" 
     by (simp add: less_eq_nat_int.rep_eq less_le_not_le less_nat_int.rep_eq)
   show "i \<le> i" by (simp add:less_eq_nat_int.rep_eq) 
   show " i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" by (simp add:less_eq_nat_int.rep_eq)
   show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"  
     by (simp add: Rep_nat_int_inject less_eq_nat_int.rep_eq )
   show "bot \<le> i" using  less_eq_nat_int.rep_eq 
     using bot_nat_int.rep_eq by blast
 qed
 end  
 
 instantiation nat_int ::  "semilattice_inf"
 begin
 instance 
 proof
   fix i j k :: nat_int
   show "i \<le> j \<Longrightarrow> i \<le> k \<Longrightarrow> i \<le> inf j k" 
     by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq)
   show " inf i   j \<le> i" 
     by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
   show "inf i  j \<le> j" 
     by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
 qed      
 end
 
 instantiation nat_int:: "equal"
 begin
 definition equal_nat_int :: "nat_int \<Rightarrow> nat_int \<Rightarrow> bool"  
   where "equal_nat_int i  j \<equiv> i \<le> j \<and> j \<le> i"
 instance 
 proof
   fix i j :: nat_int
   show " equal_class.equal i j = (i = j)" using equal_nat_int_def  by auto
 qed
 end
   
   
 context nat_int 
 begin
 abbreviation subseteq :: "nat_int \<Rightarrow> nat_int\<Rightarrow> bool" (infix "\<sqsubseteq>" 30)
   where  "i \<sqsubseteq> j == i \<le> j "
 abbreviation empty :: "nat_int" ("\<emptyset>")
   where "\<emptyset> \<equiv> bot"
     
 notation inf (infix "\<sqinter>" 70)
 
 
 text \<open>The union of two intervals is only defined, if it is also
 a discrete interval.\<close>
 definition union :: "nat_int \<Rightarrow> nat_int \<Rightarrow> nat_int" (infix "\<squnion>" 65)
   where "i \<squnion> j = Abs_nat_int (Rep_nat_int i \<union> Rep_nat_int j)"
 
 text \<open>Non-empty intervals contain a minimal and maximal element. 
 Two non-empty intervals \(i\) and \(j\) are 
 consecutive, if the minimum of \(j\) is the successor of the
 maximum of \(i\).
 Furthermore, the interval \(i\) can be chopped into the intervals \(j\)
 and \(k\), if the union of \(j\) and \(k\) equals \(i\), and if \(j\)
 and \(k\) are not-empty, they must be consecutive. Finally, we define
 the cardinality of discrete intervals by lifting the cardinality of
 sets. 
 \<close>
 definition maximum :: "nat_int \<Rightarrow> nat"
   where maximum_def: "i \<noteq> \<emptyset> \<Longrightarrow> maximum (i) =   Max (Rep_nat_int i)" 
     
 definition minimum :: "nat_int \<Rightarrow> nat"
   where minimum_def: "i \<noteq> \<emptyset> \<Longrightarrow> minimum(i) = Min (Rep_nat_int i)"
 
 definition consec:: "nat_int\<Rightarrow>nat_int \<Rightarrow> bool" 
   where "consec i j \<equiv> (i\<noteq>\<emptyset> \<and> j \<noteq> \<emptyset> \<and> (maximum(i)+1 = minimum j))"
     
 definition N_Chop :: "nat_int \<Rightarrow> nat_int \<Rightarrow> nat_int \<Rightarrow> bool" ("N'_Chop'(_,_,_')" 51)
   where nchop_def :
     "N_Chop(i,j,k) \<equiv> (i =  j \<squnion> k   \<and> (j = \<emptyset> \<or>  k = \<emptyset> \<or> consec j k))"
 
 lift_definition card' ::"nat_int \<Rightarrow> nat"  ( "|_|" 70) is card .
 
 
 text\<open>For convenience, we also lift the membership relation and its negation
 to discrete intervals.\<close>
 
 lift_definition el::"nat \<Rightarrow> nat_int \<Rightarrow> bool" (infix "\<^bold>\<in>" 50) is "Set.member" .
 
 lift_definition not_in ::"nat \<Rightarrow> nat_int \<Rightarrow> bool" (infix "\<^bold>\<notin>" 40)  is Set.not_member . 
 end
   
 lemmas[simp] = nat_int.el.rep_eq nat_int.not_in.rep_eq nat_int.card'.rep_eq
 
 context nat_int 
 begin
   
 lemma in_not_in_iff1 :"n \<^bold>\<in> i \<longleftrightarrow> \<not> n\<^bold>\<notin> i" by simp
 lemma in_not_in_iff2: "n\<^bold>\<notin> i \<longleftrightarrow> \<not> n \<^bold>\<in> i" by simp
     
     
 lemma rep_non_empty_means_seq:"i \<noteq>\<emptyset> 
                                 \<longrightarrow> (\<exists>m n. m \<le> n \<and> ({m..n} =( Rep_nat_int i)))" 
   by (metis Rep_nat_int Rep_nat_int_inject bot_nat_int.rep_eq nat_int.not_empty_means_seq)
   
 lemma non_empty_max: "i \<noteq> \<emptyset> \<longrightarrow> (\<exists>m . maximum(i) = m)" 
   by auto
     
 lemma non_empty_min: "i \<noteq> \<emptyset> \<longrightarrow> (\<exists>m . minimum(i) = m)" 
   by auto
     
 lemma minimum_in: "i \<noteq> \<emptyset> \<longrightarrow> minimum i \<^bold>\<in> i"
   by (metis Min_in atLeastatMost_empty_iff2 finite_atLeastAtMost minimum_def
       el.rep_eq rep_non_empty_means_seq)
     
 lemma maximum_in: "i \<noteq> \<emptyset> \<longrightarrow> maximum i \<^bold>\<in> i"
   by (metis Max_in atLeastatMost_empty_iff2 finite_atLeastAtMost maximum_def 
       el.rep_eq rep_non_empty_means_seq)
     
 lemma non_empty_elem_in:"i \<noteq> \<emptyset> \<longleftrightarrow> (\<exists>n. n \<^bold>\<in> i)"   
 proof
   assume assm:"i \<noteq> \<emptyset>"
   show "\<exists>n . n \<^bold>\<in> i" 
     by (metis assm Rep_nat_int_inverse all_not_in_conv el.rep_eq bot_nat_int_def)
 next
   assume assm:"\<exists>n. n \<^bold>\<in> i"
   show "i \<noteq> \<emptyset>" 
     using Abs_nat_int_inverse assm el.rep_eq bot_nat_int_def by fastforce
 qed
   
 lemma leq_nat_non_empty:"(m::nat) \<le> n \<longrightarrow> Abs_nat_int{m..n} \<noteq> \<emptyset>"  
 proof
   assume assm:"m \<le>n"
   then have non_empty:"{m..n} \<noteq> {} " 
     using atLeastatMost_empty_iff by blast
   with assm have "{m..n} \<in> {S . (\<exists> (m::nat) n .  {m..n }=S)  }" by blast
   then show "Abs_nat_int {m..n} \<noteq> \<emptyset>" 
     using Abs_nat_int_inject empty_type non_empty bot_nat_int_def 
     by (simp add: bot_nat_int.abs_eq)
 qed
   
 lemma leq_max_sup:"(m::nat) \<le> n \<longrightarrow> Max {m..n} = n" 
-  by (metis Sup_nat_def cSup_atLeastAtMost)
+  by (auto simp: Max_eq_iff)
     
 lemma leq_min_inf: "(m::nat) \<le> n \<longrightarrow> Min {m..n} = m"
-  by (meson Min_in Min_le antisym atLeastAtMost_iff atLeastatMost_empty_iff 
-      eq_imp_le finite_atLeastAtMost)
+  by (auto simp: Min_eq_iff)
     
 lemma leq_max_sup':"(m::nat) \<le> n \<longrightarrow> maximum(Abs_nat_int{m..n}) = n" 
 proof 
   assume assm:"m \<le> n"
   hence in_type:"{m..n} \<in> {S . (\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={} }" by blast
   from assm have "Abs_nat_int{m..n} \<noteq> \<emptyset>" using leq_nat_non_empty by blast
   hence max:"maximum(Abs_nat_int{m..n}) = Max (Rep_nat_int (Abs_nat_int {m..n}))"
     using maximum_def by blast
   from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}" 
     using Abs_nat_int_inverse by blast
   hence  "Max (Rep_nat_int (Abs_nat_int{m..n})) = Max {m..n}" by simp
   with max have simp_max:"maximum(Abs_nat_int{m..n}) = Max {m..n}" by simp
   from assm have "Max {m..n} = n" using leq_max_sup by blast
   with simp_max show "maximum(Abs_nat_int{m..n}) = n" by simp
 qed
   
 lemma leq_min_inf':"(m::nat) \<le> n \<longrightarrow> minimum(Abs_nat_int{m..n}) = m" 
 proof 
   assume assm:"m \<le> n"
   hence in_type:"{m..n} \<in> {S . (\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={} }" by blast
   from assm have "Abs_nat_int{m..n} \<noteq> \<emptyset>" using leq_nat_non_empty by blast
   hence min:"minimum(Abs_nat_int{m..n}) = Min(Rep_nat_int (Abs_nat_int {m..n}))"
     using  minimum_def by blast
   from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}" 
     using Abs_nat_int_inverse by blast
   hence  "Min (Rep_nat_int (Abs_nat_int{m..n})) = Min {m..n}" by simp
   with min have simp_min:"minimum(Abs_nat_int{m..n}) = Min {m..n}" by simp
   from assm have "Min {m..n} = m" using leq_min_inf by blast
   with simp_min show "minimum(Abs_nat_int{m..n}) = m" by simp
 qed
   
 lemma in_refl:"(n::nat)  \<^bold>\<in> Abs_nat_int {n}"
 proof -
   have "(n::nat) \<le> n" by simp
   hence "{n} \<in> {S . (\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={} }" by auto
   then show "n \<^bold>\<in> Abs_nat_int {n}" 
     by (simp add: Abs_nat_int_inverse el_def)
 qed
   
 lemma in_singleton:" m \<^bold>\<in> Abs_nat_int{n} \<longrightarrow> m = n"
 proof
   assume assm:" m \<^bold>\<in> Abs_nat_int{n}"
   have "(n::nat) \<le> n" by simp
   hence "{n} \<in> {S . (\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={} }" by auto
   with assm show "m=n" by (simp add: Abs_nat_int_inverse el_def)
 qed
 
 subsection \<open>Algebraic properties of intersection and union.\<close>
   
 lemma inter_empty1:"(i::nat_int) \<sqinter> \<emptyset> = \<emptyset>" 
   using Rep_nat_int_inject inf_nat_int.rep_eq bot_nat_int.abs_eq bot_nat_int.rep_eq 
   by fastforce 
     
 lemma inter_empty2:"\<emptyset> \<sqinter> (i::nat_int) = \<emptyset>" 
   by (metis inf_commute nat_int.inter_empty1)
         
 lemma un_empty_absorb1:"i \<squnion> \<emptyset> = i" 
   using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
   by auto
     
 lemma un_empty_absorb2:"\<emptyset> \<squnion> i = i" 
   using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
   by auto
 
 text \<open>Most properties of the union of two intervals depends on them being consectuive,
 to ensure that their union exists.\<close>
 
 lemma consec_un:"consec i j \<and> n \<notin> Rep_nat_int(i) \<union> Rep_nat_int j 
                   \<longrightarrow> n \<^bold>\<notin>  (i \<squnion> j)"
 proof
   assume assm:"consec i j \<and> n \<notin>  Rep_nat_int i \<union> Rep_nat_int j" 
   thus "n \<^bold>\<notin> (i \<squnion> j)" 
   proof -
     have f1: "Abs_nat_int (Rep_nat_int (i \<squnion> j)) 
               = Abs_nat_int (Rep_nat_int i \<union> Rep_nat_int j)"
       using Rep_nat_int_inverse union_def by presburger
     have "i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> maximum i + 1 = minimum j"
       using assm consec_def by auto
     then have "\<exists>n na. {n..na} = Rep_nat_int i \<union> Rep_nat_int j" 
       by (metis (no_types) leq_max_sup leq_min_inf maximum_def minimum_def 
           rep_non_empty_means_seq un_consec_seq)
     then show ?thesis
       using f1 Abs_nat_int_inject Rep_nat_int not_in.rep_eq assm by auto
   qed
 qed
     
 lemma un_subset1: "consec i j \<longrightarrow> i \<sqsubseteq> i \<squnion> j" 
 proof
   assume "consec i j"
   then have assm:"i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> maximum i+1 = minimum j" 
     using consec_def by blast
   have "Rep_nat_int i \<union> Rep_nat_int j =  {minimum i.. maximum j}" 
     by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def 
         nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
   then show "i \<sqsubseteq> i \<squnion> j" using Abs_nat_int_inverse Rep_nat_int 
     by (metis (mono_tags, lifting) Un_upper1 less_eq_nat_int.rep_eq mem_Collect_eq
         nat_int.union_def)
 qed
   
 lemma un_subset2: "consec i j \<longrightarrow> j \<sqsubseteq> i \<squnion> j"
 proof
   assume "consec i j"
   then have assm:"i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> maximum i+1 = minimum j" 
     using consec_def by blast
   have "Rep_nat_int i \<union> Rep_nat_int j =  {minimum i.. maximum j}" 
     by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def 
         nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
   then show "j \<sqsubseteq> i \<squnion> j" using Abs_nat_int_inverse Rep_nat_int
     by (metis (mono_tags, lifting) Un_upper2 less_eq_nat_int.rep_eq mem_Collect_eq
         nat_int.union_def)
 qed
  
 lemma inter_distr1:"consec j k \<longrightarrow> i \<sqinter> (j \<squnion> k) = (i \<sqinter> j) \<squnion> (i \<sqinter> k)"  
   unfolding consec_def
 proof  
   assume assm:"j \<noteq> \<emptyset> \<and> k \<noteq> \<emptyset> \<and> maximum j +1 = minimum k"
   then show " i \<sqinter> (j \<squnion> k) = (i \<sqinter> j) \<squnion> (i \<sqinter> k)"  
   proof -
     have f1: "\<forall>n. n = \<emptyset> \<or> maximum n = Max (Rep_nat_int n)"
       using nat_int.maximum_def by auto
     have f2: "Rep_nat_int j \<noteq> {}"
       using assm nat_int.maximum_in by auto
     have f3: "maximum j = Max (Rep_nat_int j)"
       using f1 by (meson assm)
     have "maximum k \<^bold>\<in> k"
       using assm nat_int.maximum_in by blast
     then have "Rep_nat_int k \<noteq> {}"
       by fastforce
     then have "Rep_nat_int (j \<squnion> k) = Rep_nat_int j \<union> Rep_nat_int k"
       using f3 f2 Abs_nat_int_inverse Rep_nat_int assm nat_int.minimum_def 
         nat_int.union_def union_result 
         by auto
     then show ?thesis
       by (metis Rep_nat_int_inverse inf_nat_int.rep_eq inf_sup_distrib1 nat_int.union_def)
   qed
 qed
   
 lemma inter_distr2:"consec j k \<longrightarrow> (j \<squnion> k) \<sqinter> i = (j \<sqinter> i) \<squnion> (k \<sqinter> i)"
   by (simp add: inter_distr1 inf_commute)
     
 lemma consec_un_not_elem1:"consec i j \<and> n\<^bold>\<notin> i \<squnion> j \<longrightarrow>  n \<^bold>\<notin> i"
   using un_subset1 less_eq_nat_int.rep_eq not_in.rep_eq by blast 
     
 lemma consec_un_not_elem2:"consec i j \<and> n\<^bold>\<notin> i \<squnion> j \<longrightarrow>  n \<^bold>\<notin> j"
   using  un_subset2 less_eq_nat_int.rep_eq not_in.rep_eq by blast
     
 lemma consec_un_element1:"consec i j \<and> n \<^bold>\<in> i \<longrightarrow> n \<^bold>\<in> i \<squnion> j" 
   using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset1 by blast
     
 lemma consec_un_element2:"consec i j \<and> n \<^bold>\<in> j \<longrightarrow> n \<^bold>\<in> i \<squnion> j"
   using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset2 by blast
     
 lemma consec_lesser:" consec i j  \<longrightarrow> (\<forall>n m. (n \<^bold>\<in> i \<and> m \<^bold>\<in> j \<longrightarrow> n < m))" 
 proof (rule allI|rule impI)+
   assume "consec i j"
   fix n and m  
   assume assump:"n \<^bold>\<in> i \<and> m \<^bold>\<in> j "
   then have  max:"n \<le> maximum i" 
     by (metis \<open>consec i j\<close> atLeastAtMost_iff leq_max_sup maximum_def consec_def
         el.rep_eq rep_non_empty_means_seq)
   from assump have min: "m \<ge> minimum j" 
     by (metis Min_le \<open>consec i j\<close> finite_atLeastAtMost minimum_def consec_def
         el.rep_eq rep_non_empty_means_seq)
   from min and max show less:"n < m" 
     using One_nat_def Suc_le_lessD \<open>consec i j\<close> add.right_neutral add_Suc_right
       dual_order.trans leD leI consec_def by auto
 qed
 
 lemma consec_in_exclusive1:"consec i j \<and> n \<^bold>\<in> i \<longrightarrow> n \<^bold>\<notin> j" 
   using nat_int.consec_lesser nat_int.in_not_in_iff2 by blast
 
 lemma consec_in_exclusive2:"consec i j \<and> n \<^bold>\<in> j \<longrightarrow> n \<^bold>\<notin> i"
   using consec_in_exclusive1 el.rep_eq not_in.rep_eq by blast
 
 lemma consec_un_max:"consec i j \<longrightarrow> maximum j = maximum (i \<squnion> j)"
 proof
   assume assm:"consec i j"
   then have "(\<forall>n m. (n \<^bold>\<in> i \<and> m \<^bold>\<in> j \<longrightarrow> n < m))" 
     using nat_int.consec_lesser by blast
   then have "\<forall>n . (n \<^bold>\<in> i \<longrightarrow> n < maximum j)" 
     using assm local.consec_def nat_int.maximum_in by auto
   then have "\<forall>n. (n \<^bold>\<in> i \<squnion> j \<longrightarrow> n \<le> maximum j)" 
     by (metis (no_types, lifting) Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff
         bot_nat_int.rep_eq less_imp_le_nat local.consec_def local.not_empty_means_seq 
         nat_int.consec_un nat_int.el.rep_eq nat_int.in_not_in_iff1 nat_int.leq_max_sup')
   then show "maximum j = maximum (i \<squnion> j)" 
     by (metis Rep_nat_int_inverse assm atLeastAtMost_iff bot.extremum_uniqueI
         le_antisym local.consec_def nat_int.consec_un_element2 nat_int.el.rep_eq
         nat_int.leq_max_sup' nat_int.maximum_in nat_int.un_subset2 rep_non_empty_means_seq)
 qed
 
 lemma consec_un_min:"consec i j \<longrightarrow> minimum i = minimum (i \<squnion> j)"
 proof
   assume assm:"consec i j"
   then have "(\<forall>n m. (n \<^bold>\<in> i \<and> m \<^bold>\<in> j \<longrightarrow> n < m))" 
     using nat_int.consec_lesser by blast
   then have "\<forall>n . (n \<^bold>\<in> j \<longrightarrow> n > minimum i)" 
     using assm local.consec_def nat_int.minimum_in by auto
   then have 1:"\<forall>n. (n \<^bold>\<in> i \<squnion> j \<longrightarrow> n \<ge> minimum i)"  
     using Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff bot_nat_int.rep_eq
       less_imp_le_nat local.consec_def local.not_empty_means_seq nat_int.consec_un 
       nat_int.el.rep_eq nat_int.in_not_in_iff1
     by (metis (no_types, lifting) leq_min_inf local.minimum_def)
   from assm have "i \<squnion> j \<noteq> \<emptyset>" 
     by (metis bot.extremum_uniqueI nat_int.consec_def nat_int.un_subset2)
   then show "minimum i = minimum (i \<squnion> j)" 
     by (metis "1" antisym assm atLeastAtMost_iff leq_min_inf nat_int.consec_def 
         nat_int.consec_un_element1 nat_int.el.rep_eq nat_int.minimum_def nat_int.minimum_in
         rep_non_empty_means_seq)
 qed
 
 lemma consec_un_defined:
   "consec i j \<longrightarrow> (Rep_nat_int (i \<squnion> j) \<in> {S . (\<exists> (m::nat) n . {m..n }=S) })"
   using Rep_nat_int by auto
 
 lemma consec_un_min_max:
   "consec i j \<longrightarrow> Rep_nat_int(i \<squnion> j) = {minimum i .. maximum j}"
 proof
   assume assm:"consec i j"
   then have 1:"minimum j = maximum i +1" 
     by (simp add: nat_int.consec_def)
   have i:"Rep_nat_int i = {minimum i..maximum i}" 
     by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
         rep_non_empty_means_seq)
   have j:"Rep_nat_int j = {minimum j..maximum j}" 
     by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
         rep_non_empty_means_seq)
   show "Rep_nat_int(i \<squnion> j) = {minimum i .. maximum j}" 
     by (metis Rep_nat_int_inverse antisym assm bot.extremum i nat_int.consec_un_max
         nat_int.consec_un_min nat_int.leq_max_sup' nat_int.leq_min_inf' nat_int.un_subset1
         rep_non_empty_means_seq)
 qed
 
 lemma consec_un_equality: 
   "(consec i j \<and> k \<noteq> \<emptyset>) 
     \<longrightarrow>( minimum (i \<squnion> j) = minimum (k) \<and> maximum (i \<squnion> j) = maximum (k))
       \<longrightarrow> i \<squnion> j = k"
 proof (rule impI)+
   assume cons:"consec i j \<and> k \<noteq> \<emptyset>"
   assume endpoints:" minimum(i \<squnion> j) = minimum(k) \<and> maximum(i \<squnion> j) = maximum(k)"
   have "Rep_nat_int( i \<squnion> j) = {minimum(i \<squnion> j)..maximum(i \<squnion> j)}" 
     by (metis cons leq_max_sup leq_min_inf local.consec_def nat_int.consec_un_element2
         nat_int.maximum_def nat_int.minimum_def nat_int.non_empty_elem_in rep_non_empty_means_seq)
   then have 1:"Rep_nat_int( i \<squnion> j) = {minimum(k) .. maximum(k)}" 
     using endpoints by simp
   have "Rep_nat_int( k) = {minimum(k) .. maximum(k)}" 
     by (metis cons leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
         rep_non_empty_means_seq)
   then  show " i \<squnion> j = k" using 1 
     by (metis Rep_nat_int_inverse)
 qed
 
 lemma consec_trans_lesser:
   "consec i j \<and> consec j k \<longrightarrow> (\<forall>n m. (n \<^bold>\<in> i \<and> m \<^bold>\<in> k \<longrightarrow> n < m))"
 proof (rule allI|rule impI)+
   assume cons:" consec i j \<and> consec j k"
   fix n and m
   assume assump:"n \<^bold>\<in> i \<and> m \<^bold>\<in> k "
   have "\<forall>k . k \<^bold>\<in> j \<longrightarrow> k < m" using consec_lesser assump cons by blast
   hence m_greater:"maximum j < m" using cons maximum_in consec_def by blast
   then show "n < m" 
     by (metis assump cons consec_def dual_order.strict_trans nat_int.consec_lesser
         nat_int.maximum_in)      
 qed
   
 lemma consec_inter_empty:"consec i j \<Longrightarrow> i \<sqinter> j = \<emptyset>" 
 proof -
   assume "consec i j"
   then have "i \<noteq> bot \<and> j \<noteq> bot \<and> maximum i + 1 = minimum j"
     using consec_def by force
   then show ?thesis
     by (metis (no_types) Rep_nat_int_inverse bot_nat_int_def inf_nat_int.rep_eq int_conseq_seq
         nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def nat_int.minimum_def
         nat_int.rep_non_empty_means_seq)
 qed 
   
 lemma consec_intermediate1:"consec j k \<and> consec i (j \<squnion> k) \<longrightarrow> consec i j "
 proof
   assume assm:"consec j k \<and> consec i (j \<squnion> k)"
   hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast 
   hence min_max_xyz:"maximum i +1 = minimum (j \<squnion> k)" 
       using consec_def assm by blast
   have min_y_yz:"minimum j = minimum (j \<squnion> k)" 
     by (simp add: assm nat_int.consec_un_min)
   hence min_max_xy:"maximum i+1 = minimum j" 
     using min_max_xyz by simp
   thus consec_x_y:"consec i j" using assm consec_def by auto
 qed
   
 lemma consec_intermediate2:"consec i j \<and> consec (i \<squnion> j) k \<longrightarrow> consec j k "
 proof
   assume assm:"consec i j \<and> consec (i \<squnion> j) k"
   hence min_max_yz:"maximum i +1=minimum j" using consec_def by blast 
   hence min_max_xyz:"maximum (i \<squnion> j) +1 = minimum ( k)" 
       using consec_def assm by blast
   have min_y_yz:"maximum j = maximum (i \<squnion> j)" 
     using assm nat_int.consec_un_max by blast
   then have min_max_xy:"maximum j+1 = minimum k" 
     using min_max_xyz by simp
   thus consec_x_y:"consec j k" using assm consec_def by auto
 qed
 
 lemma un_assoc: "consec i j \<and> consec j k \<longrightarrow> (i \<squnion> j) \<squnion> k = i \<squnion> (j \<squnion> k)" 
 proof 
   assume assm:"consec i j \<and> consec j k"
   from assm have 3:"maximum (i \<squnion> j) = maximum j" 
     using nat_int.consec_un_max by auto
   from assm have 4:"minimum (j \<squnion> k) = minimum (j)" 
     using nat_int.consec_un_min by auto
   have "i \<squnion> j  = Abs_nat_int{minimum i .. maximum j}" 
     by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
   then have 5:"(i \<squnion> j) \<squnion> k = Abs_nat_int{minimum i .. maximum k}" 
     by (metis (no_types, hide_lams) "3" Rep_nat_int_inverse antisym assm bot.extremum
         nat_int.consec_def nat_int.consec_un_min nat_int.consec_un_min_max nat_int.un_subset1)
   have "j \<squnion> k = Abs_nat_int{minimum j .. maximum k}" 
     by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
   then have 6:"i \<squnion> (j \<squnion> k) = Abs_nat_int{minimum i .. maximum k}" 
     by (metis (no_types, hide_lams) "4" Rep_nat_int_inverse antisym assm bot.extremum
         nat_int.consec_def nat_int.consec_un_max nat_int.consec_un_min_max nat_int.un_subset2)
   from 5 and 6 show " (i \<squnion> j) \<squnion> k = i \<squnion> (j \<squnion> k)" by simp
 qed
 
 lemma consec_assoc1:"consec j k \<and> consec i (j \<squnion> k) \<longrightarrow> consec (i \<squnion> j) k "
 proof
   assume assm:"consec j k \<and> consec i (j \<squnion> k)"
   hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast 
   hence min_max_xyz:"maximum i +1 = minimum (j \<squnion> k)" 
       using consec_def assm by blast
   have min_y_yz:"minimum j = minimum (j \<squnion> k)" 
     by (simp add: assm nat_int.consec_un_min) 
   hence min_max_xy:"maximum i+1 = minimum j" using min_max_xyz by simp
   hence consec_x_y:"consec i j" using assm _consec_def by auto
   hence max_y_xy:"maximum j = maximum (i \<squnion> j)" using consec_lesser assm 
     by (simp add: nat_int.consec_un_max)
   have none_empty:"i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> k \<noteq> \<emptyset>" using assm by (simp add: consec_def)
   hence un_non_empty:"i\<squnion>j \<noteq> \<emptyset>" 
     using bot.extremum_uniqueI consec_x_y nat_int.un_subset2 by force
   have max:"maximum (i\<squnion>j) +1 = minimum k" 
     using min_max_yz max_y_xy by auto  
   thus "consec (i \<squnion> j) k"  using max un_non_empty none_empty consec_def by blast
 qed
   
 lemma consec_assoc2:"consec i j \<and> consec (i\<squnion> j) k \<longrightarrow> consec i  (j\<squnion> k) "
 proof
   assume assm:"consec i j \<and> consec (i\<squnion> j) k"
   hence consec_y_z:"consec j k" using assm consec_def consec_intermediate2 
     by blast
   hence max_y_xy:"maximum j = maximum (i \<squnion> j)" 
     by (simp add: assm nat_int.consec_un_max)  
   have min_y_yz:"minimum j = minimum (j \<squnion> k)" 
     by (simp add: consec_y_z nat_int.consec_un_min)
   have none_empty:"i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> k \<noteq> \<emptyset>" using assm by (simp add: consec_def)
   then have un_non_empty:"j\<squnion>k \<noteq> \<emptyset>" 
     by (metis  bot_nat_int.rep_eq Rep_nat_int_inject consec_y_z  less_eq_nat_int.rep_eq
         un_subset1 subset_empty)
   have max:"maximum (i) +1 = minimum (j\<squnion> k)" 
     using assm min_y_yz consec_def by auto
   thus "consec i ( j \<squnion> k)"  using max un_non_empty none_empty consec_def by blast
 qed
   
   
 lemma consec_assoc_mult:
   "(i2=\<emptyset>\<or> consec i1 i2 ) \<and> (i3 =\<emptyset> \<or> consec i3 i4) \<and> (consec (i1 \<squnion> i2) (i3 \<squnion> i4)) 
       \<longrightarrow> (i1 \<squnion> i2) \<squnion> (i3 \<squnion> i4) = (i1 \<squnion> (i2 \<squnion> i3)) \<squnion> i4"
 proof
   assume assm:"(i2=\<emptyset>\<or> consec i1 i2 ) \<and> (i3 =\<emptyset> \<or> consec i3 i4) 
                 \<and> (consec (i1 \<squnion> i2) (i3 \<squnion> i4))"
   hence "(i2=\<emptyset>\<or> consec i1 i2 )" by simp
   thus " (i1 \<squnion> i2) \<squnion> (i3 \<squnion> i4) = (i1 \<squnion> (i2 \<squnion> i3)) \<squnion> i4" 
   proof
     assume empty2:"i2 = \<emptyset>"
     hence only_l1:"(i1 \<squnion> i2) = i1" using un_empty_absorb1 by simp
     from assm have "(i3 =\<emptyset> \<or> consec i3 i4)" by simp
     thus " (i1 \<squnion> i2) \<squnion> (i3 \<squnion> i4) = (i1 \<squnion> (i2 \<squnion> i3)) \<squnion> i4" 
       by (metis Rep_nat_int_inverse assm bot_nat_int.rep_eq empty2 local.union_def 
           nat_int.consec_intermediate1 nat_int.un_assoc only_l1 sup_bot.left_neutral)
   next
     assume consec12:" consec i1 i2"
     from assm have "(i3 =\<emptyset> \<or> consec i3 i4)" by simp
     thus " (i1 \<squnion> i2) \<squnion> (i3 \<squnion> i4) = (i1 \<squnion> (i2 \<squnion> i3)) \<squnion> i4" 
     proof
       assume empty3:"i3 = \<emptyset>"
       hence only_l4:"(i3 \<squnion> i4) = i4 " using un_empty_absorb2 by simp
       have "(i1 \<squnion> (i2 \<squnion> i3)) = i1 \<squnion> i2" using empty3 by (simp add: un_empty_absorb1)
       thus ?thesis by (simp add: only_l4)
     next
       assume  consec34:" consec i3 i4"
       have consec12_3:"consec (i1 \<squnion> i2) i3" 
         using assm consec34 consec_intermediate1 by blast
       show ?thesis 
         by (metis consec12 consec12_3 consec34 consec_intermediate2 un_assoc)
     qed
   qed
 qed
   
 lemma card_subset_le: "i \<sqsubseteq> i' \<longrightarrow> |i| \<le> |i'|"  
   by (metis bot_nat_int.rep_eq card_mono finite.intros(1) finite_atLeastAtMost 
       less_eq_nat_int.rep_eq local.card'.rep_eq rep_non_empty_means_seq)
   
 lemma card_subset_less:"(i::nat_int) < i' \<longrightarrow> |i|<|i'|"  
   by (metis bot_nat_int.rep_eq finite.intros(1) finite_atLeastAtMost less_nat_int.rep_eq
       local.card'.rep_eq psubset_card_mono rep_non_empty_means_seq) 
   
 lemma card_empty_zero:"|\<emptyset>| = 0"  
   using Abs_nat_int_inverse empty_type card'.rep_eq bot_nat_int.rep_eq by auto
     
 lemma card_non_empty_geq_one:"i \<noteq> \<emptyset> \<longleftrightarrow> |i| \<ge> 1" 
 proof
   assume "i \<noteq> \<emptyset>"
   hence "Rep_nat_int i \<noteq> {}" by (metis Rep_nat_int_inverse bot_nat_int.rep_eq)
   hence "card (Rep_nat_int i) > 0" 
     by (metis \<open>i \<noteq> \<emptyset>\<close> card_0_eq finite_atLeastAtMost gr0I rep_non_empty_means_seq)
   thus "|i| \<ge> 1" by (simp add: card'_def) 
 next
   assume "|i| \<ge> 1" thus "i \<noteq>\<emptyset>" 
     using card_empty_zero by auto
 qed
 
 lemma card_min_max:"i \<noteq> \<emptyset> \<longrightarrow> |i| = (maximum i - minimum i) + 1" 
 proof
   assume assm:"i \<noteq> \<emptyset>"
   then have "Rep_nat_int i = {minimum i .. maximum i}" 
     by (metis leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
         rep_non_empty_means_seq) 
   then have "card (Rep_nat_int i) = maximum i - minimum i + 1" 
     using Rep_nat_int_inject assm bot_nat_int.rep_eq by fastforce
   then show " |i| = (maximum i - minimum i) + 1"  by simp
 qed
 
 lemma card_un_add: " consec i j \<longrightarrow> |i \<squnion> j| = |i| + |j|"
 proof 
   assume assm:"consec i j" 
   then have 0:"i \<sqinter> j = \<emptyset>" 
     using nat_int.consec_inter_empty by auto
   then have "(Rep_nat_int i) \<inter> (Rep_nat_int j) = {}" 
     by (metis bot_nat_int.rep_eq inf_nat_int.rep_eq)
   then have 1: 
     "card((Rep_nat_int i)\<union>(Rep_nat_int j))=card(Rep_nat_int i)+card(Rep_nat_int j)"
     by (metis Int_iff add.commute add.left_neutral assm card.infinite card_Un_disjoint
         emptyE le_add1 le_antisym local.consec_def nat_int.card'.rep_eq
         nat_int.card_min_max nat_int.el.rep_eq nat_int.maximum_in nat_int.minimum_in)
   then show "|i \<squnion> j| = |i| + |j|" 
   proof -
     have f1: "i \<noteq> \<emptyset> \<and> j \<noteq> \<emptyset> \<and> maximum i + 1 = minimum j"
       using assm nat_int.consec_def by blast
     then have f2: "Rep_nat_int i \<noteq> {}"
       using Rep_nat_int_inject bot_nat_int.rep_eq by auto
     have "Rep_nat_int j \<noteq> {}"
       using f1 Rep_nat_int_inject bot_nat_int.rep_eq by auto
     then show ?thesis
       using f2 f1 Abs_nat_int_inverse Rep_nat_int 1 local.union_result
         nat_int.union_def nat_int_class.maximum_def nat_int_class.minimum_def
         by force
   qed
 qed
 
 lemma singleton:"|i| = 1 \<longrightarrow> (\<exists>n. Rep_nat_int i = {n})"
   using card_1_singletonE card'.rep_eq by fastforce
     
 lemma singleton2:" (\<exists>n. Rep_nat_int i = {n}) \<longrightarrow> |i| = 1"
   using card_1_singletonE card'.rep_eq by fastforce
     
     
 lemma card_seq:"
   \<forall>i .|i| = x \<longrightarrow> (Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n..n+(x-1)}))" 
 proof (induct x)
   show IB:
     "\<forall>i. |i| = 0 \<longrightarrow> (Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n..n+(0-1)}))" 
     by (metis  card_non_empty_geq_one bot_nat_int.rep_eq  not_one_le_zero)
   fix x
   assume IH:
       "\<forall>i. |i| = x \<longrightarrow> Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n..n+(x-1)})"
   show   " \<forall>i. |i| = Suc x \<longrightarrow>
              Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
   proof (rule allI|rule impI)+
     fix i
     assume assm_IS:"|i| = Suc x"
     show " Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n.. n + (Suc x -1)})"
     proof (cases "x = 0")
       assume "x=0"
       hence "|i| = 1" 
         using assm_IS by auto 
       then have "\<exists>n'. Rep_nat_int i = {n'}" 
         using nat_int.singleton by blast 
       hence "\<exists>n'. Rep_nat_int i = {n'.. n' + (Suc x) -1}"
         by (simp add: \<open>x = 0\<close>)
       thus "Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
         by simp
     next
       assume x_neq_0:"x \<noteq>0 "
       hence x_ge_0:"x > 0" using gr0I by blast
       from assm_IS have i_is_seq:"\<exists>n m. n \<le> m \<and> Rep_nat_int i = {n..m}" 
         by (metis One_nat_def Suc_le_mono card_non_empty_geq_one le0 rep_non_empty_means_seq)
       obtain n and m where seq_def:" n  \<le> m \<and> Rep_nat_int i = {n..m}" 
         using i_is_seq by auto
       have n_le_m:"n < m"
       proof (rule ccontr)
         assume "\<not>n < m"
         hence "n = m" by (simp add: less_le seq_def)
         hence "Rep_nat_int i = {n}" by (simp add: seq_def)
         hence "x = 0" using assm_IS card'.rep_eq by auto
         thus False by (simp add: x_neq_0)
       qed
       hence "n \<le> (m-1)" by simp
       obtain i' where  i_def:"i' = Abs_nat_int {n..m-1}" by blast
       then have card_i':"|i'| = x" 
         using assm_IS leq_nat_non_empty n_le_m
           nat_int_class.card_min_max nat_int_class.leq_max_sup' nat_int_class.leq_min_inf'
           seq_def by auto
       hence "Rep_nat_int i' = {} \<or> (\<exists>n. Rep_nat_int i' = {n.. n + (x - 1)})" 
         using IH by auto
       hence " (\<exists>n. Rep_nat_int i' = {n.. n + (x - 1)})" using x_neq_0 
         using card.empty card_i' card'.rep_eq by auto
       hence "m-1 = n + x -1" using assm_IS card'.rep_eq seq_def by auto
       hence "m = n +x" using n_le_m x_ge_0 by linarith
       hence "( Rep_nat_int i = {n.. n + (Suc x -1) })" using seq_def by (simp )
       hence "\<exists>n. (Rep_nat_int i = {n.. n + (Suc x -1) })" ..
       then show "Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i ={n.. n + (Suc x-1)})"
         by blast
     qed
   qed
 qed
     
 lemma rep_single: "Rep_nat_int (Abs_nat_int {m..m}) = {m}"
   by (simp add: Abs_nat_int_inverse)
 
 lemma chop_empty_right: "\<forall>i. N_Chop(i,i,\<emptyset>)"  
   using bot_nat_int.abs_eq nat_int.inter_empty1 nat_int.nchop_def nat_int.un_empty_absorb1
   by auto
     
 lemma chop_empty_left: "\<forall>i. N_Chop(i, \<emptyset>, i)"
   using bot_nat_int.abs_eq nat_int.inter_empty2 nat_int.nchop_def nat_int.un_empty_absorb2
   by auto
     
 lemma chop_empty : "N_Chop(\<emptyset>,\<emptyset>,\<emptyset>)"
   by (simp add: chop_empty_left)
     
 lemma chop_always_possible:"\<forall>i.\<exists> j k. N_Chop(i,j,k)" 
   by (metis  chop_empty_right)
     
 lemma chop_add1: "N_Chop(i,j,k) \<longrightarrow> |i| = |j| + |k|"
   using card_empty_zero card_un_add un_empty_absorb1 un_empty_absorb2 nchop_def by auto
     
 lemma chop_add2:"|i| = x+y \<longrightarrow> (\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y)" 
 proof
   assume assm:"|i| = x+y"
   show "(\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y)"
   proof (cases "x+y = 0")
     assume "x+y =0"
     then show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" 
       using assm chop_empty_left nat_int.chop_add1 by fastforce
   next 
     assume "x+y \<noteq> 0"
     show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" 
     proof (cases "x = 0")
       assume x_eq_0:"x=0"
       then show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" 
         using assm nat_int.card_empty_zero nat_int.chop_empty_left by auto
     next
       assume x_neq_0:"x \<noteq>0"
       show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" 
       proof (cases "y = 0")
         assume y_eq_0:"y=0"
         then show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" 
           using assm nat_int.card_empty_zero nat_int.chop_empty_right by auto
       next
         assume y_neq_0:"y \<noteq> 0"
         have rep_i:"\<exists>n. Rep_nat_int i = {n..n + (x+y)-1}" 
           using assm card'.rep_eq card_seq x_neq_0 by fastforce
         obtain n where n_def:"Rep_nat_int i = {n..n + (x+y) -1}" 
           using rep_i by auto
         have n_le:"n \<le> n+(x-1)" by simp
         have x_le:"n+(x) \<le> n + (x+y)-1" using y_neq_0 by linarith
         obtain j  where j_def:" j = Abs_nat_int {n..n+(x-1)}" by blast
         from n_le have j_in_type:
           "{n..n+(x-1)} \<in> {S . (\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={}}"
           by blast
         obtain k where k_def:" k =Abs_nat_int {n+x..n+(x+y)-1}" by blast
         from x_le have k_in_type:
           "{n+x..n+(x+y)-1} \<in> {S.(\<exists> (m::nat) n . m \<le> n \<and> {m..n }=S) \<or> S={}}"
           by blast
         have consec: "consec j k" 
           by (metis j_def k_def One_nat_def Suc_leI add.assoc diff_add n_le consec_def
               leq_max_sup' leq_min_inf' leq_nat_non_empty neq0_conv x_le x_neq_0)
         have union:"i = j \<squnion> k" 
           by (metis Rep_nat_int_inverse consec j_def k_def n_def n_le nat_int.consec_un_min_max
               nat_int.leq_max_sup' nat_int.leq_min_inf' x_le)
         have disj:"j \<sqinter> k = \<emptyset>" using consec by (simp add: consec_inter_empty)
         have chop:"N_Chop(i,j,k)" using consec union disj nchop_def by simp
         have card_j:"|j| = x" 
           using Abs_nat_int_inverse j_def n_le card'.rep_eq x_neq_0 by auto
         have card_k:"|k| = y"
           using Abs_nat_int_inverse k_def x_le card'.rep_eq x_neq_0 y_neq_0 by auto
         have "N_Chop(i,j,k) \<and> |j| = x \<and> |k| = y" using chop card_j card_k by blast
         then show "\<exists> j k. N_Chop(i,j,k) \<and> |j|=x \<and> |k|=y" by blast
       qed
     qed
   qed
 qed
   
 lemma chop_single:"(N_Chop(i,j,k) \<and> |i| = 1) \<longrightarrow> ( |j| =0 \<or> |k|=0)"
   using chop_add1 by force
     
 lemma chop_leq_max:"N_Chop(i,j,k) \<and> consec j k \<longrightarrow> 
   (\<forall>n . n \<in> Rep_nat_int i \<and> n \<le> maximum j \<longrightarrow> n \<in> Rep_nat_int j)" 
   by (metis Un_iff le_antisym less_imp_le_nat nat_int.consec_def nat_int.consec_lesser
       nat_int.consec_un nat_int.el.rep_eq nat_int.maximum_in nat_int.nchop_def
       nat_int.not_in.rep_eq)
     
 lemma chop_geq_min:"N_Chop(i,j,k) \<and> consec j k \<longrightarrow> 
   (\<forall>n . n \<in> Rep_nat_int i \<and> minimum k \<le> n \<longrightarrow> n \<in> Rep_nat_int k)" 
   by (metis atLeastAtMost_iff bot_nat_int.rep_eq equals0D leq_max_sup leq_min_inf 
       nat_int.consec_def nat_int.consec_un_max nat_int.maximum_def nat_int.minimum_def
       nat_int.nchop_def rep_non_empty_means_seq)
      
 lemma chop_min:"N_Chop(i,j,k) \<and> consec j k \<longrightarrow> minimum i = minimum j" 
   using nat_int.consec_un_min nat_int.nchop_def by auto
   
 lemma chop_max:"N_Chop(i,j,k) \<and> consec j k \<longrightarrow> maximum i = maximum k"
   using nat_int.consec_un_max nat_int.nchop_def by auto
   
 lemma chop_assoc1:
   "N_Chop(i,i1,i2) \<and> N_Chop(i2,i3,i4) 
     \<longrightarrow> (N_Chop(i, i1 \<squnion> i3, i4) \<and> N_Chop(i1 \<squnion> i3, i1, i3))" 
 proof 
   assume assm:"N_Chop(i,i1,i2) \<and> N_Chop(i2,i3,i4)"
   then have chop_def:"(i =  i1 \<squnion> i2   \<and>
         (i1 = \<emptyset> \<or>  i2 = \<emptyset> \<or> ( consec i1 i2)))"
     using nchop_def by blast
   hence "(i1 = \<emptyset> \<or>  i2 = \<emptyset> \<or> ( consec i1 i2))" by simp 
   then show "N_Chop(i, i1 \<squnion> i3, i4) \<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
   proof 
     assume empty:"i1 = \<emptyset>"
     then show "N_Chop(i,i1 \<squnion> i3, i4) \<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
       by (simp add: assm chop_def nat_int.chop_empty_left nat_int.un_empty_absorb2)
   next
     assume "i2 = \<emptyset> \<or> ( consec i1 i2)"
     then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
     proof 
       assume empty:"i2 = \<emptyset>"
       then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
         by (metis assm bot.extremum_uniqueI nat_int.chop_empty_right nat_int.nchop_def
             nat_int.un_empty_absorb2 nat_int.un_subset1)
     next
       assume " consec i1 i2"
       then have consec_i1_i2:"i1 \<noteq>\<emptyset> \<and> i2 \<noteq>\<emptyset> \<and> maximum i1 +1 = minimum i2" 
         using consec_def by blast
       from assm have "i3 = \<emptyset> \<or> i4 = \<emptyset> \<or> consec i3 i4" 
         using nchop_def by blast
       then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
       proof
         assume i3_empty:"i3 = \<emptyset>"
         then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
           using assm nat_int.chop_empty_right nat_int.nchop_def nat_int.un_empty_absorb2
             by auto
       next 
         assume "i4 = \<emptyset> \<or> consec i3 i4"
         then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
         proof
           assume i4_empty:"i4 = \<emptyset>"
           then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
             using assm nat_int.chop_empty_right nat_int.nchop_def by auto
         next
           assume consec_i3_i4:"consec i3 i4"
           then show "N_Chop(i, i1 \<squnion> i3, i4)\<and> N_Chop(i1 \<squnion> i3, i1, i3)" 
             by (metis \<open>consec i1 i2\<close> assm nat_int.consec_assoc1 nat_int.consec_intermediate1
                 nat_int.nchop_def nat_int.un_assoc)
         qed
       qed
     qed
   qed
 qed
   
 lemma chop_assoc2:
   "N_Chop(i,i1,i2) \<and> N_Chop(i1,i3,i4) 
     \<longrightarrow> N_Chop(i, i3, i4 \<squnion> i2) \<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
 proof 
   assume assm: "N_Chop(i,i1,i2) \<and> N_Chop(i1,i3,i4)"
   hence "(i1 = \<emptyset> \<or>  i2 = \<emptyset> \<or> ( consec i1 i2))" 
     using nchop_def by blast 
   then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)"
   proof
     assume i1_empty:"i1 = \<emptyset>"
    then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
      by (metis assm nat_int.chop_empty_left nat_int.consec_un_not_elem1 nat_int.in_not_in_iff1
          nat_int.nchop_def nat_int.non_empty_elem_in nat_int.un_empty_absorb1)
   next
     assume "i2 = \<emptyset> \<or> consec i1 i2"
     then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)"
     proof
       assume i2_empty:"i2=\<emptyset>"
       then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
         using assm nat_int.chop_empty_right nat_int.nchop_def by auto
     next
       assume consec_i1_i2:"consec i1 i2"
       from assm have "(i3 = \<emptyset> \<or>  i4 = \<emptyset> \<or> ( consec i3 i4))" 
         by (simp add: nchop_def)
       then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)"
       proof
         assume i3_empty:"i3=\<emptyset>"
         then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
           using assm nat_int.chop_empty_left nat_int.nchop_def by auto
       next
         assume " i4 = \<emptyset> \<or> ( consec i3 i4)"
         then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
         proof
           assume i4_empty:"i4=\<emptyset>"
           then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
             using assm nat_int.nchop_def nat_int.un_empty_absorb1 nat_int.un_empty_absorb2
             by auto
         next
           assume consec_i3_i4:"consec i3 i4"
           then show "N_Chop(i, i3, i4 \<squnion> i2)\<and> N_Chop(i4 \<squnion> i2, i4,i2)" 
             by (metis assm consec_i1_i2 nat_int.consec_assoc2 nat_int.consec_intermediate2
                 nat_int.nchop_def nat_int.un_assoc)
         qed
       qed
     qed
   qed
 qed
   
 lemma chop_subset1:"N_Chop(i,j,k) \<longrightarrow> j \<sqsubseteq> i"
   using nat_int.chop_empty_right nat_int.nchop_def nat_int.un_subset1 by auto
     
 lemma chop_subset2:"N_Chop(i,j,k) \<longrightarrow> k \<sqsubseteq> i" 
   using nat_int.chop_empty_left nat_int.nchop_def nat_int.un_subset2 by auto
     
 end
 end