Theory Safe_Distance_Reaction

✐‹creator "Albert Rizaldi" "Fabian Immler›

section ‹Safe Distance with Reaction Time›

theory Safe_Distance_Reaction
imports
  Safe_Distance
begin

subsection ‹Normal Safe Distance›
                                    
locale safe_distance_normal = safe_distance +
  fixes δ :: real
  assumes pos_react: "0 < δ"
begin

sublocale ego2: braking_movement ae ve "(ego.q δ)" ..

lemma ego2_s_init: "ego2.s 0 = ego.q δ" unfolding ego2.s_def by auto

definition τ :: "real ⇒ real" where
  "τ t = t - δ"

definition τ' :: "real ⇒ real" where
  "τ' t = 1"

lemma τ_continuous[continuous_intros]: "continuous_on T τ"
  unfolding τ_def by (auto intro: continuous_intros)

lemma isCont_τ[continuous_intros]: "isCont τ x"
  using τ_continuous[of UNIV] by (auto simp: continuous_on_eq_continuous_at)

lemma del_has_vector_derivative[derivative_intros]: "(τ has_vector_derivative τ' t) (at t within u)"
  by (auto simp: τ_def[abs_def] τ'_def has_vector_derivative_def algebra_simps
           intro!: derivative_eq_intros)
                                                             
lemma del_has_real_derivative[derivative_intros]: "(τ has_real_derivative τ' t) (at t within u)"
  using del_has_vector_derivative
  by (simp add:has_real_derivative_iff_has_vector_derivative)

lemma delay_image: "τ ` {δ..} = {0..}"
proof (rule subset_antisym, unfold image_def, unfold τ_def)
  show "{y. ∃x∈{δ..}. y = x - δ} ⊆ {0..}" by auto
next
  show "{0..} ⊆ {y. ∃x∈{δ..}. y = x - δ}"
  proof (rule subsetI)
    fix a
    assume "(a::real) ∈ {0..}"
    hence "0 ≤ a" by simp
    hence "∃x∈{δ..}. a = x - δ" using bexI[where x = "a + δ"] by auto
    thus "a ∈ {y. ∃x∈{δ..}. y = x - δ}" by auto
  qed
qed

lemma s_delayed_has_real_derivative[derivative_intros]:
  assumes "δ ≤ t"
  shows "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * τ' t) (at t within {δ..})"
proof (rule DERIV_image_chain)
  from assms have 0: "0 ≤ t - δ" by simp
  from ego2.t_stop_nonneg have 1: "ve / ae ≤ 0" unfolding ego2.t_stop_def by simp
  from ego2.decel have 2: "ae ≠ 0" by simp
  show "(ego2.s has_real_derivative ego2.s' (t - δ)) (at (τ t) within τ ` {δ..})"
  using ego2.s_has_real_derivative[OF 0 1 2] sym[OF delay_image]
  unfolding τ_def by simp
next
  from del_has_real_derivative show "(τ has_real_derivative τ' t) (at t within {δ..})" 
  by auto
qed

lemma s_delayed_has_real_derivative' [derivative_intros]:
  assumes "δ ≤ t"
  shows "((ego2.s ∘ τ) has_field_derivative (ego2.s' ∘ τ) t) (at t within {δ..})"
proof -
  from s_delayed_has_real_derivative[OF assms] have
  "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * τ' t) (at t within {δ..})"
  by auto
  hence "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ) * 1) (at t within {δ..})"
  using τ'_def[of t] by metis
  hence "((ego2.s ∘ τ) has_field_derivative ego2.s' (t - δ)) (at t within {δ..})"
  by (simp add:algebra_simps)  
  thus ?thesis unfolding comp_def τ_def by auto
qed

lemma s_delayed_has_vector_derivative' [derivative_intros]:
  assumes "δ ≤ t"
  shows "((ego2.s ∘ τ) has_vector_derivative (ego2.s' ∘ τ) t) (at t within {δ..})"
  using s_delayed_has_real_derivative'[OF assms]
  by (simp add:has_real_derivative_iff_has_vector_derivative)
  
definition u :: "real ⇒ real" where
  "u t = (     if t ≤ 0 then se
          else if t ≤ δ then ego.q t 
          else          (ego2.s ∘ τ) t)"

lemma init_u: "t ≤ 0 ⟹ u t = se" unfolding u_def by auto

lemma u_delta: "u δ = ego2.s 0"
proof -  
  have "u δ = ego.q δ" using pos_react unfolding u_def by auto
  also have "... = ego2.s 0" unfolding ego2.s_def by auto
  finally show "u δ = ego2.s 0" .
qed

lemma q_delta: "ego.q δ = ego2.s 0" using u_delta pos_react unfolding u_def by auto

definition u' :: "real ⇒ real" where
  "u' t = (if t ≤ δ then ego.q' t else ego2.s' (t - δ))"

lemma u'_delta: "u' δ = ego2.s' 0"
proof -
  have "u' δ = ego.q' δ" unfolding u'_def by auto
  also have "... = ve" unfolding ego2.q'_def by simp
  also have "... = ego2.p' 0" unfolding ego2.p'_def by simp
  also have "... = ego2.s' 0" using ego2.t_stop_nonneg unfolding ego2.s'_def by auto 
  finally show "u' δ = ego.s' 0" .
qed

lemma q'_delta: "ego.q' δ = ego2.s' 0" using u'_delta unfolding u'_def by auto

lemma u_has_real_derivative[derivative_intros]:
  assumes nonneg_t: "t ≥ 0"
  shows "(u has_real_derivative u' t) (at t within {0..})"
proof -
  from pos_react have "0 ≤ δ" by simp

  have temp: "((λt. if t ∈ {0 .. δ} then ego.q t else (ego2.s ∘ τ) t) has_real_derivative
    (if t ∈ {0..δ} then ego.q' t else (ego2.s' ∘ τ) t)) (at t within {0..})" (is "(?f1 has_real_derivative ?f2) (?net)")
    unfolding u_def[abs_def] u'_def 
      has_real_derivative_iff_has_vector_derivative
    apply (rule has_vector_derivative_If_within_closures[where T = "{δ..}"])
    using ‹0 ≤ δ› q_delta q'_delta ego.s_has_vector_derivative[OF assms] ego.decel ego.t_stop_nonneg 
    s_delayed_has_vector_derivative'[of "t"] τ_def
    unfolding comp_def
    by (auto simp: assms  max_def insert_absorb   
      intro!: ego.q_has_vector_derivative)
  show ?thesis
    unfolding has_vector_derivative_def has_real_derivative_iff_has_vector_derivative
      u'_def u_def[abs_def] 
    proof (rule has_derivative_transform[where f="(λt. if t ∈ {0..δ} then ego.q t else (ego2.s ∘ τ) t)"])
      from nonneg_t show " t ∈ {0..}" by auto
    next
      fix x
      assume "(x::real) ∈ {0..}"
      hence  "x ≤ δ ⟷ x ∈ {0 .. δ}" by simp
      thus  " (if x ≤ 0 then se else if x ≤ δ then ego.q x else (ego2.s ∘ τ) x) =
         (if x ∈ {0..δ} then ego.q x else (ego2.s ∘ τ) x)" using pos_react unfolding ego.q_def by auto
    next
      from temp have "(?f1 has_vector_derivative ?f2) ?net"
      using has_real_derivative_iff_has_vector_derivative by auto      
      moreover with assms have "t ∈ {0 .. δ} ⟷ t ≤ δ" by auto
      ultimately show " ((λt. if t ∈ {0..δ} then ego.q t else (ego2.s ∘ τ) t) has_derivative
              (λx. x *R (if t ≤ δ then ego2.q' t else ego2.s' (t - δ)))) (at t within {0..})" 
      unfolding comp_def τ_def has_vector_derivative_def by auto
    qed 
qed

definition t_stop :: real where 
  "t_stop = ego2.t_stop + δ"

lemma t_stop_nonneg: "0 ≤ t_stop"
  unfolding t_stop_def
  using ego2.t_stop_nonneg pos_react
  by auto

lemma t_stop_pos: "0 < t_stop"
  unfolding t_stop_def
  using ego2.t_stop_nonneg pos_react
  by auto

lemma t_stop_zero:
  assumes "t_stop ≤ x"
  assumes "x ≤ δ"
  shows "ve = 0"
  using assms unfolding t_stop_def using ego2.t_stop_nonneg pos_react ego2.t_stop_zero by auto

lemma u'_stop_zero: "u' t_stop = 0" 
  unfolding u'_def t_stop_def ego2.q'_def ego2.s'_def
  using ego2.t_stop_nonneg ego2.p'_stop_zero decelerate_ego ego2.t_stop_zero by auto

definition u_max :: real where 
  "u_max = u (ego2.t_stop + δ)"

lemma u_max_eq: "u_max = ego.q δ - ve2 / ae / 2"
proof (cases "ego2.t_stop = 0")
  assume "ego2.t_stop = 0"
  hence "ve = 0" using ego2.t_stop_zero by simp
  with ‹ego2.t_stop = 0› show "u_max = ego.q δ - ve2 / ae / 2"  unfolding u_max_def u_def using pos_react by auto
next
  assume "ego2.t_stop ≠ 0"
  hence "u_max = (ego2.s ∘ τ) (ego2.t_stop + δ)" 
    unfolding u_max_def u_def  using ego2.t_stop_nonneg pos_react by auto 
  moreover have "... = ego2.s ego2.t_stop" unfolding comp_def τ_def by auto
  moreover have "... = ego2.p_max" 
    unfolding ego2.s_def ego2.p_max_def using ‹ego2.t_stop ≠ 0› ego2.t_stop_nonneg by auto
  moreover have "... = ego.q δ - ve2 / ae / 2" using ego2.p_max_eq .
  ultimately show ?thesis by auto
qed

lemma u_mono: 
  assumes "x ≤ y" "y ≤ t_stop" 
  shows "u x ≤ u y"
proof -
  have "y ≤ 0 ∨ (0 < y ∧ y ≤ δ) ∨ δ < y" by auto

  moreover
  { assume "y ≤ 0"
    with assms have "x ≤ 0" by auto
    with ‹y ≤ 0› have "u x ≤ u y" unfolding u_def by auto }

  moreover
  { assume "0 < y ∧ y ≤ δ"
    with assms have "x ≤ δ" by auto
    hence "u x ≤ u y" 
    proof (cases "x ≤ 0")
      assume "x ≤ 0"
      with ‹x ≤ δ› and ‹0 < y ∧ y ≤ δ› show "u x ≤ u y"  unfolding u_def using ego.q_min by auto
    next
      assume "¬ x ≤ 0"
      with ‹0 < y ∧ y ≤ δ› and assms show "u x ≤ u y" 
        unfolding u_def  using ego.q_mono by auto
    qed }
  
  moreover
  { assume "δ < y"
    have "u x ≤ u y"
    proof (cases "δ < x")
      assume "δ < x" 
      with pos_react have "¬ x ≤ 0" by auto
      moreover from ‹δ < y› and pos_react have "¬ y ≤ 0" by auto
      ultimately show "u x ≤ u y"  unfolding u_def comp_def 
        using assms ego2.s_mono[of "x - δ" "y - δ"] ‹δ < y› ‹δ < x› by (auto simp:τ_def)
    next
      assume "¬ δ < x"
      hence "x ≤ δ" by simp
      hence "u x ≤ ego.q δ" unfolding u_def using pos_react nonneg_vel_ego
        by (auto simp add:ego.q_def mult_left_mono)
      also have "... = ego2.s (τ δ)" unfolding ego2.s_def unfolding τ_def by auto
      also have "... ≤ ego2.s (τ y)" unfolding τ_def using ‹δ < y› by (auto simp add:ego2.s_mono)
      also have "... = u y" unfolding u_def using ‹δ < y› pos_react by auto     
      ultimately show "u x ≤ u y" by auto
    qed }
  
  ultimately show "u x ≤ u y" by auto
qed

lemma u_antimono: "x ≤ y ⟹ t_stop ≤ x ⟹ u y ≤ u x"
proof -
  assume 1: "x ≤ y"
  assume 2: "t_stop ≤ x"
  hence "δ ≤ x" unfolding τ_def t_stop_def using pos_react ego2.t_stop_nonneg by auto
  with 1 have "δ ≤ y" by auto
  from 1 and 2 have 3: "t_stop ≤ y" by auto
  show "u y ≤ u x"
  proof (cases "x ≠ δ ∧ y ≠ δ")
    assume "x ≠ δ ∧ y ≠ δ"
    hence "x ≠ δ" and "y ≠ δ" by auto
    have "u y ≤ (ego2.s ∘ τ) y" unfolding u_def using ‹δ ≤ y› ‹y ≠ δ› pos_react by auto
    also have "... ≤ (ego2.s ∘ τ) x" unfolding comp_def
    proof (intro ego2.s_antimono)
      show "τ x ≤ τ y" unfolding τ_def using ‹x ≤ y› by auto
    next
      show "ego2.t_stop ≤ τ x" unfolding τ_def using ‹t_stop ≤ x› by (auto simp: t_stop_def)
    qed
    also have "... ≤ u x" unfolding u_def using ‹δ ≤ x›‹x ≠ δ› pos_react by auto
    ultimately show "u y ≤ u x" by auto
  next
    assume "¬ (x ≠ δ ∧ y ≠ δ)"
    have "x ≠ δ ⟶ y ≠ δ"
    proof (rule impI; erule contrapos_pp[where Q="¬ x = δ"])
      assume "¬ y ≠ δ"
      hence "y = δ" by simp
      with ‹t_stop ≤ y› have "ego2.t_stop = 0" unfolding t_stop_def 
        using ego2.t_stop_nonneg by auto
      with ‹t_stop ≤ x› have "x = δ" unfolding t_stop_def using ‹x ≤ y› ‹y = δ› by auto
      thus "¬ x ≠ δ" by auto
    qed
    with ‹¬ (x ≠ δ ∧ y ≠ δ)› have "(x = δ ∧ y = δ) ∨ (x = δ)" by auto
    
    moreover
    { assume "x = δ ∧ y = δ"
      hence "x = δ" and "y = δ" by auto
      hence "u y ≤ ego.q δ" unfolding u_def using pos_react by auto
      also have "... ≤ u x" unfolding u_def using ‹x = δ› pos_react by auto
      ultimately have "u y ≤ u x" by auto }

    moreover
    { assume "x = δ" 
      hence "ego2.t_stop = 0" using ‹t_stop ≤ x› ego2.t_stop_nonneg by (auto simp:t_stop_def)
      hence "ve = 0" by (rule ego2.t_stop_zero)
      hence "u y ≤ ego.q δ"
        using pos_react ‹x = δ› ‹x ≤ y› ‹ve = 0›
        unfolding u_def comp_def τ_def ego2.s_def ego2.p_def ego2.p_max_def ego2.t_stop_def 
        by auto
      also have "... ≤ u x" using ‹x = δ› pos_react unfolding u_def by auto       
      ultimately have "u y ≤ u x" by auto }

    ultimately show ?thesis by auto
  qed
qed

lemma u_max: "u x ≤ u_max" 
  unfolding u_max_def using t_stop_def        
  by (cases "x ≤ t_stop") (auto intro: u_mono u_antimono)

lemma u_eq_u_stop: "NO_MATCH t_stop x ⟹ x ≥ t_stop ⟹ u x = u_max"
proof -
  assume "t_stop ≤ x"
  with t_stop_pos have "0 < x" by auto
  from ‹t_stop ≤ x› have "δ ≤ x" unfolding t_stop_def using ego2.t_stop_nonneg by auto
  show  "u x = u_max"
  proof (cases "x ≤ δ")
    assume "x ≤ δ" 
    with ‹t_stop ≤ x› have "ve = 0" by (rule t_stop_zero)
    also have "x = δ" using ‹x ≤ δ› and ‹δ ≤ x› by auto
    ultimately have "u x = ego.q δ" unfolding u_def using pos_react by auto
    also have "... = u_max" unfolding u_max_eq using ‹ve = 0› by auto
    ultimately show "u x = u_max" by simp
  next
    assume "¬ x ≤ δ"
    hence "δ < x" by auto
    hence "u x = (ego2.s ∘ τ) x" unfolding u_def using pos_react by auto
    also have "... = ego2.s ego2.t_stop" 
      proof (unfold comp_def; unfold τ_def; intro order.antisym)
        have "x - δ ≥ ego2.t_stop" using ‹t_stop ≤ x› unfolding t_stop_def by auto
        thus "ego2.s (x - δ) ≤ ego2.s ego2.t_stop" by (rule ego2.s_antimono) simp
      next
        have "x - δ ≥ ego2.t_stop" using ‹t_stop ≤ x› unfolding t_stop_def by auto
        thus "ego2.s ego2.t_stop ≤ ego2.s (x - δ)" using ego2.t_stop_nonneg by (rule ego2.s_mono)
      qed
    also have "... = u_max" unfolding u_max_eq ego2.s_t_stop ego2.p_max_eq by auto
    ultimately show "u x = u_max" by auto
  qed
qed

lemma at_least_delta:
  assumes "x ≤ δ"
  assumes "t_stop ≤ x"
  shows "ego.q x = ego2.s (x - δ)"
  using assms ego2.t_stop_nonneg 
  unfolding t_stop_def ego2.s_def less_eq_real_def by auto

lemma continuous_on_u[continuous_intros]: "continuous_on T u"
  unfolding u_def[abs_def]
  using t_stop_nonneg pos_react at_least_delta
  proof (intro continuous_on_subset[where t=T and s = "{..0} ∪ ({0..δ} ∪ ({δ .. t_stop} ∪ {t_stop ..}))"] continuous_on_If continuous_intros)
    fix x
    assume " ¬ x ≤ δ"
    assume "x ∈ {0..δ}"
    hence "0 ≤ x" and "x ≤ δ" by auto
    thus "ego.q x = (ego2.s ∘ τ) x" 
      unfolding comp_def τ_def ego2.s_def 
      using ‹¬ x ≤ δ› by auto
  next
    fix x
    assume "x ∈ {δ..t_stop} ∪ {t_stop..}"
    hence "δ ≤ x" unfolding t_stop_def using pos_react ego.t_stop_nonneg by auto
    also assume "x ≤ δ"
    ultimately have "x = δ" by auto
    thus "ego.q x = (ego2.s ∘ τ) x" unfolding comp_def τ_def ego2.s_def by auto
  next
    fix t::real
    assume "t ∈ {.. 0}"
    hence "t ≤ 0" by auto
    also assume "¬ t ≤ 0"
    ultimately have "t = 0" by auto
    hence "se = ego.q t" unfolding ego.q_def by auto
    with pos_react ‹t = 0› show "se = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" by auto
  next
    fix t::real
    assume "t ∈ {0..δ} ∪ ({δ..t_stop} ∪ {t_stop..})"
    hence "0 ≤ t" using pos_react ego2.t_stop_nonneg by (auto simp: t_stop_def)
    also assume "t ≤ 0"
    ultimately have "t = 0" by auto
    hence " se = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" using pos_react ego.init_q by auto
    thus "se = (if t ≤ δ then ego.q t else (ego2.s ∘ τ) t)" by auto
  next
    show "T ⊆ {..0} ∪ ({0..δ} ∪ ({δ..t_stop} ∪ {t_stop..}))" by auto  
  qed

lemma isCont_u[continuous_intros]: "isCont u x"
  using continuous_on_u[of UNIV]
  by (auto simp:continuous_on_eq_continuous_at)

definition collision_react :: "real set ⇒ bool" where
  "collision_react time_set ≡ (∃t∈time_set. u t = other.s t )"

abbreviation no_collision_react :: "real set ⇒ bool" where
  "no_collision_react time_set ≡ ¬ collision_react time_set"

lemma no_collision_reactI:
  assumes "⋀t. t ∈ S ⟹ u t ≠ other.s t"
  shows "no_collision_react S"
  using assms
  unfolding collision_react_def
  by blast

lemma no_collision_union:
  assumes "no_collision_react S"
  assumes "no_collision_react T"
  shows "no_collision_react (S ∪ T)"
  using assms
  unfolding collision_react_def
  by auto

lemma collision_trim_subset:
  assumes "collision_react S"
  assumes "no_collision_react T"
  assumes "T ⊆ S"
  shows "collision_react (S - T)"
  using assms
  unfolding collision_react_def by auto

theorem cond_1r : "u_max < so ⟹ no_collision_react {0..}"
proof (rule no_collision_reactI, simp)
  fix t :: real
  assume "0 ≤ t"
  have "u t ≤ u_max" by (rule u_max)
  also assume "... < so"
  also have "... = other.s 0"
    by (simp add: other.init_s)
  also have "... ≤ other.s t"
    using ‹0 ≤ t› hyps
    by (intro other.s_mono) auto
  finally show "u t ≠ other.s t"
    by simp
qed

definition safe_distance_1r :: real where 
  "safe_distance_1r = ve * δ - ve2 / ae / 2"

lemma sd_1r_eq: "(so - se > safe_distance_1r) = (u_max < so)"
proof -
  have "(so - se > safe_distance_1r) = (so - se > ve * δ - ve2 / ae / 2)" unfolding safe_distance_1r_def by auto
  moreover have "... = (se + ve * δ - ve2 / ae / 2 < so)" by auto
  ultimately show ?thesis using u_max_eq ego.q_def by auto
qed

lemma sd_1r_correct:
  assumes "so - se > safe_distance_1r"
  shows "no_collision_react {0..}"
proof -
  from assms have "u_max < so" using sd_1r_eq by auto
  thus ?thesis by (rule cond_1r)
qed

lemma u_other_strict_ivt:
  assumes "u t > other.s t"
  shows "collision_react {0..<t}"
proof cases
  assume "0 ≤ t"
  with assms in_front
  have "∃x≥0. x ≤ t ∧ other.s x - u x = 0"
    by (intro IVT2) (auto simp: init_u other.init_s continuous_diff isCont_u other.isCont_s)
  then show ?thesis
    using assms
    by (auto simp add: algebra_simps collision_react_def Bex_def order.order_iff_strict)
qed(insert assms hyps, auto simp: collision_react_def init_u other.init_s)

lemma collision_react_subset: "collision_react s ⟹ s ⊆ t ⟹ collision_react t"
  by (auto simp:collision_react_def) 

lemma u_other_ivt:
  assumes "u t ≥ other.s t"
  shows "collision_react {0 .. t}"
proof cases
  assume "u t > other.s t"
  from u_other_strict_ivt[OF this]
  show ?thesis
    by (rule collision_react_subset) auto
qed (insert hyps assms; cases "t ≥ 0"; force simp: collision_react_def init_u other.init_s)

theorem cond_2r:
  assumes "u_max ≥ other.s_stop"
  shows "collision_react {0 ..}"
  using assms
  apply(intro collision_react_subset[where t="{0..}" and s ="{0 .. max t_stop other.t_stop}"])
   apply(intro u_other_ivt[where t ="max t_stop other.t_stop"])
   apply(auto simp: u_eq_u_stop other.s_eq_s_stop)
  done

definition ego_other2 :: "real ⇒ real" where
  "ego_other2 t = other.s t - u t"

lemma continuous_on_ego_other2[continuous_intros]: "continuous_on T ego_other2"
  unfolding ego_other2_def[abs_def]
  by (intro continuous_intros)

lemma isCont_ego_other2[continuous_intros]: "isCont ego_other2 x"
  using continuous_on_ego_other2[of UNIV]
  by (auto simp: continuous_on_eq_continuous_at)

definition ego_other2' :: "real ⇒ real" where
  "ego_other2' t  = other.s' t - u' t"

lemma ego_other2_has_real_derivative[derivative_intros]: 
  assumes "0 ≤ t"
  shows "(ego_other2 has_real_derivative ego_other2' t) (at t within {0..})"
  using assms other.t_stop_nonneg decelerate_other
  unfolding other.t_stop_def
  by (auto simp: ego_other2_def[abs_def] ego_other2'_def  algebra_simps
           intro!: derivative_eq_intros)

theorem cond_3r_1:
  assumes "u δ ≥ other.s δ"
  shows "collision_react {0 .. δ}"
  proof (unfold collision_react_def) 
  have 1: "∃t≥0. t ≤ δ ∧ ego_other2 t = 0"
    proof (intro IVT2)
      show "ego_other2 δ ≤ 0" unfolding ego_other2_def using assms by auto
    next
      show "0 ≤ ego_other2 0" unfolding ego_other2_def 
        using other.init_s[of 0] init_u[of 0] in_front by auto
    next
      show "0 ≤ δ" using pos_react by auto
    next
      show "∀t. 0 ≤ t ∧ t ≤ δ ⟶ isCont ego_other2 t" 
        using isCont_ego_other2 by auto
    qed
    then obtain t where "0 ≤ t ∧ t ≤ δ ∧ ego_other2 t = 0" by auto
    hence "t ∈ {0 .. δ}" and "u t = other.s t" unfolding ego_other2_def by auto
    thus "∃t∈{0..δ}. u t = other.s t" by (intro bexI)    
  qed

definition distance0 :: real where 
  "distance0 =  ve * δ - vo * δ - ao * δ2 / 2"

definition distance0_2 :: real where 
  "distance0_2 = ve * δ + 1 / 2 * vo2 / ao"

theorem cond_3r_1':
  assumes "so - se ≤ distance0"
  assumes "δ ≤ other.t_stop"
  shows "collision_react {0 .. δ}"
proof -
  from assms have "u δ ≥ other.s δ" unfolding distance0_def other.s_def
    other.p_def u_def ego.q_def using pos_react by auto
  thus ?thesis using cond_3r_1 by auto
qed

theorem distance0_2_eq:
  assumes "δ > other.t_stop"
  shows "(u δ < other.s δ) = (so - se > distance0_2)"
proof -
  from assms have "(u δ < other.s δ) = (ego.q δ < other.p_max)"
    using u_def other.s_def pos_react by auto
  also have "... = (se + ve * δ < so + vo * (- vo / ao) + 1 / 2 * ao * (- vo / ao)2)"
    using ego.q_def other.p_max_def other.p_def other.t_stop_def by auto
  also have "... = (ve * δ - vo * (- vo / ao) - 1 / 2 * ao * (- vo / ao)2 < so - se)" by linarith
  also have "... = (ve * δ + vo2 / ao - 1 / 2 * vo2 / ao < so - se)"
    using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  also have "... = (ve * δ + 1 / 2 * vo2 / ao < so - se)" by linarith
  thus ?thesis using distance0_2_def by (simp add: calculation)
qed

theorem cond_3r_1'_2:
  assumes "so - se ≤ distance0_2"
  assumes "δ > other.t_stop"
  shows "collision_react {0 .. δ}"
proof -
  from assms distance0_2_eq have "u δ ≥ other.s δ" unfolding distance0_def other.s_def
    other.p_def u_def ego.q_def using pos_react by auto
  thus ?thesis using cond_3r_1 by auto
qed

definition safe_distance_3r :: real where
  "safe_distance_3r = ve * δ - ve2 / 2 / ae - vo * δ - 1/2 * ao * δ2"

lemma distance0_at_most_sd3r:
  "distance0 ≤ safe_distance_3r"
  unfolding distance0_def safe_distance_3r_def using nonneg_vel_ego decelerate_ego
  by (auto simp add:field_simps)

definition safe_distance_4r :: real where 
  "safe_distance_4r = (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"

lemma distance0_at_most_sd4r:
  assumes "ao > ae"
  shows "distance0 ≤ safe_distance_4r"
proof -
  from assms have "ao ≥ ae" by auto
  have "0 ≤ (vo + ao * δ - ve)2 / (2 * ao - 2 * ae)"
    by (rule divide_nonneg_nonneg) (auto simp add:assms ‹ae ≤ ao›)
  thus ?thesis unfolding distance0_def safe_distance_4r_def
    by auto
qed

definition safe_distance_2r :: real where 
  "safe_distance_2r = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao"

lemma vo_start_geq_ve:
  assumes "δ ≤ other.t_stop"
  assumes "other.s' δ ≥ ve"
  shows "u δ < other.s δ"
proof -
    from assms have "ve ≤ vo + ao * δ" unfolding other.s'_def other.p'_def by auto
    with  mult_right_mono[OF this, of "δ"] have "ve * δ ≤ vo * δ + ao * δ2" (is "?l0 ≤ ?r0")
      using pos_react by (auto simp add:field_simps power_def)
    hence "se + ?l0 ≤ se + ?r0" by auto
    also have "... < so + ?r0" using in_front by auto
    also have "... < so + vo * δ + ao * δ2 / 2" using decelerate_other pos_react by auto
    finally show ?thesis using pos_react assms(1)
      unfolding u_def ego.q_def other.s_def other.t_stop_def other.p_def by auto
qed

theorem so_star_stop_leq_se_stop:
  assumes "δ ≤ other.t_stop"
  assumes "other.s' δ < ve"
  assumes "¬ (ao > ae ∧ other.s' δ < ve ∧ ve - ae / ao * other.s' δ < 0)"
  shows "0 ≤ - ve2 / ae / 2 + (vo + ao * δ)2 / ao / 2"
proof -
  consider "ve - ae / ao * other.s' δ ≥ 0" | "¬ (ve - ae / ao * other.s' δ ≥ 0)" by auto
  thus ?thesis
  proof (cases)
    case 1
    hence "ve - ae / ao * (vo + ao * δ) ≥ 0" unfolding other.s'_def other.p'_def
      by (auto simp add:assms(1))
    hence "ve - ae / ao * vo - ae * δ ≥ 0" (is "?l0 ≥ 0") using decelerate_other
      by (auto simp add:field_simps)
    hence "?l0 / ae ≤ 0" using divide_right_mono_neg[OF ‹?l0 ≥ 0›] decelerate_ego by auto
    hence "0 ≥ ve / ae - vo / ao - δ" using decelerate_ego by (auto simp add:field_simps)
    hence *: "- ve / ae ≥ - (vo + ao * δ) / ao" using decelerate_other by (auto simp add:field_simps)
    from assms have **: "vo + ao * δ ≤ ve" unfolding other.s'_def other.p'_def by auto
    have vo_star_nneg: "vo + ao * δ ≥ 0"
    proof -
      from assms(1) have "- vo ≤ ao * δ" unfolding other.t_stop_def using decelerate_other
        by (auto simp add:field_simps)
      thus ?thesis by auto
    qed
    from mult_mono[OF * ** _ ‹0 ≤ vo + ao * δ›]
    have "- (vo + ao * δ) / ao * (vo + ao * δ) ≤ - ve / ae * ve" using nonneg_vel_ego decelerate_ego
      by (auto simp add:field_simps)
    hence "- (vo + ao * δ)2 / ao ≤ - ve2 / ae " by (auto simp add: field_simps power_def)
    thus ?thesis by (auto simp add:field_simps)
  next
    case 2
    with assms have "ao ≤ ae" by auto
    from assms(2) have "(vo + ao * δ) ≤ ve" unfolding other.s'_def using assms unfolding other.p'_def
      by auto
    have vo_star_nneg: "vo + ao * δ ≥ 0"
    proof -
      from assms(1) have "- vo ≤ ao * δ" unfolding other.t_stop_def using decelerate_other
        by (auto simp add:field_simps)
      thus ?thesis by auto
    qed
    with mult_mono[OF ‹vo + ao * δ ≤ ve› ‹vo + ao * δ ≤ ve›] have *: "(vo + ao * δ)2 ≤ ve2"
      using nonneg_vel_ego by (auto simp add:power_def)
    from ‹ao ≤ ae› have "- 1 /ao ≤ - 1 / ae" using decelerate_ego decelerate_other
      by (auto simp add:field_simps)
    from mult_mono[OF * this] have "(vo + ao * δ)2 * (- 1 / ao) ≤ ve2 * (- 1 / ae)"
      using nonneg_vel_ego decelerate_other by (auto simp add:field_simps)
    then show ?thesis by auto
  qed
qed

theorem distance0_at_most_distance2r:
  assumes "δ ≤ other.t_stop"
  assumes "other.s' δ < ve"
  assumes "¬ (ao > ae ∧ other.s' δ < ve ∧ ve - ae / ao * other.s' δ < 0)"
  shows "distance0 ≤ safe_distance_2r"
proof -
  from so_star_stop_leq_se_stop[OF assms] have " 0 ≤ - ve2 / ae / 2 + (vo + ao * δ)2 / ao / 2 " (is "0 ≤ ?term")
    by auto
  have "safe_distance_2r = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  also have "... = ve * δ - ve2 / 2 / ae + (vo + ao * δ)2 / 2 / ao - vo * δ - ao * δ2 / 2"
    using decelerate_other by (auto simp add:field_simps power_def)
  also have "... = ve * δ - vo * δ - ao * δ2 / 2 + ?term" (is "_ = ?left + ?term")
    by (auto simp add:field_simps)
  finally have "safe_distance_2r = distance0 + ?term" unfolding distance0_def by auto
  with ‹0 ≤ ?term› show "distance0 ≤ safe_distance_2r" by auto
qed

theorem dist0_sd2r_1:
  assumes "δ ≤ other.t_stop"
  assumes "¬ (ao > ae ∧ other.s' δ < ve ∧ ve - ae / ao * other.s' δ < 0)"
  assumes "so - se > safe_distance_2r"
  shows "so - se > distance0"
proof (cases "other.s' δ ≥ ve")
  assume "ve ≤ other.s' δ"
  from vo_start_geq_ve[OF assms(1) this] have "u δ < other.s δ" by auto
  thus ?thesis unfolding distance0_def u_def using pos_react assms(1) unfolding ego.q_def
    other.s_def other.p_def by auto
next
  assume "¬ ve ≤ other.s' δ"
  hence "ve > other.s' δ" by auto
  from distance0_at_most_distance2r[OF assms(1) this assms(2)] have "distance0 ≤ safe_distance_2r"
    by auto
  with assms(3) show ?thesis by auto
qed

theorem sd2r_eq:
  assumes "δ > other.t_stop"
  shows "(u_max < other.s δ) = (so - se > safe_distance_2r)"
proof -
  from assms have "(u_max < other.s δ) = (ego2.s (- ve / ae) < other.p_max)"
    using u_max_def ego2.t_stop_def u_def other.s_def τ_def pos_react ego2.p_max_eq ego2.s_t_stop u_max_eq by auto
  also have "... = (se + ve * δ + ve * (- ve / ae) + 1 / 2 * ae * (- ve / ae)2 < so + vo * (- vo / ao) + 1 / 2 * ao * (- vo / ao)2)"
    using ego2.s_def ego2.p_def ego.q_def other.p_max_def other.p_def other.t_stop_def ego2.p_max_def ego2.s_t_stop ego2.t_stop_def by auto
  also have "... = (ve * δ + ve * (- ve / ae) + 1 / 2 * ae * (- ve / ae)2 - vo * (- vo / ao) - 1 / 2 * ao * (- vo / ao)2 < so  - se)" by linarith
  also have "... = (ve * δ - ve2 / ae + 1 / 2 * ve2 / ae + vo2 / ao - 1 / 2 * vo2 / ao < so  - se)"
    using ego2.p_def ego2.p_max_def ego2.p_max_eq ego2.t_stop_def other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  also have "... = (ve * δ - ve2 / 2 / ae + vo2 / 2 / ao  < so - se)" by linarith
  thus ?thesis using distance0_2_def by (simp add: calculation safe_distance_2r_def)
qed

theorem dist0_sd2r_2:
  assumes "δ > - vo / ao"
  assumes "so - se > safe_distance_2r"
  shows "so - se > distance0_2"
proof -
  have "- ve2 / 2 / ae ≥ 0" using zero_le_power2 hyps(3) divide_nonneg_neg by (auto simp add:field_simps)
  hence "ve * δ - ve2 / 2 / ae + vo2 / 2 / ao ≥ ve * δ + vo2 / 2 / ao" by simp
  hence "safe_distance_2r ≥ distance0_2" using safe_distance_2r_def distance0_2_def by auto
  thus ?thesis using assms(2) by linarith
qed
end

subsection ‹Safe Distance Delta›

locale safe_distance_no_collsion_delta = safe_distance_normal +
  assumes no_collision_delta: "u δ < other.s δ"
begin

sublocale delayed_safe_distance: safe_distance ae ve "ego.q δ" ao "other.s' δ" "other.s δ"
  proof (unfold_locales)
    from nonneg_vel_ego show "0 ≤ ve" by auto
  next
    from nonneg_vel_other show "0 ≤ other.s' δ" unfolding other.s'_def other.p'_def other.t_stop_def
      using decelerate_other by (auto simp add: field_split_simps)
  next
    from decelerate_ego show "ae < 0" by auto
  next
    from decelerate_other show "ao < 0" by auto
  next
    from no_collision_delta show "ego.q δ < other.s δ" unfolding u_def using pos_react by auto
  qed

lemma no_collision_react_initially_strict:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  shows "no_collision_react {0 <..< δ}"
proof (rule no_collision_reactI)
  fix t::real
  assume "t ∈ {0 <..< δ}" 
  show "u t ≠ other.s t"
  proof (rule ccontr)
    assume "¬ u t ≠ other.s t"
    hence "ego_other2 t = 0" unfolding ego_other2_def by auto
    from ‹t ∈ {0 <..< δ}› have "ego_other2 t = other.s t - ego.q t" 
      unfolding ego_other2_def u_def using ego.init_q by auto
    have "δ ≤ other.t_stop ∨ other.t_stop < δ" by auto
    
    moreover
    { assume le_t_stop: "δ ≤ other.t_stop"
      with ‹ego_other2 t = other.s t - ego.q t› have "ego_other2 t = other.p t - ego.q t"
        unfolding other.s_def using ‹t ∈ {0 <..< δ}› by auto
      with ‹ego_other2 t = 0› have "other.p t - ego.q t = 0" by auto
      hence eq: "(so- se) + (vo - ve) * t + (1/2 * ao) * t2 = 0"
        unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
      define p where "p ≡ λx. (1/2 * ao) * x2 + (vo - ve) * x + (so - se)"
      have "0 < 1/2 * ao"
      proof (intro p_convex[where p=p and b="vo - ve" and c="so - se"])
          show "0 < t" using ‹t ∈ {0 <..< δ}› by auto
        next
          show "t < δ" using  ‹t ∈ {0 <..< δ}› by auto
        next
          show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
        next
          from eq have "p t = 0" unfolding p_def by auto
          also have "... < p δ"  using no_collision_delta pos_react le_t_stop             
            unfolding p_def u_def other.s_def ego.q_def other.p_def by (auto simp:algebra_simps)
          finally have "p t < p δ" by simp
          thus "p t ≤ p δ" by auto
        next
          show "p = (λx. 1 / 2 * ao * x2 + (vo - ve) * x + (so - se))" unfolding p_def
          by (rule refl)
      qed
      hence "0 < ao" by auto
      with decelerate_other have False by simp }

    moreover
    { assume gt_t_stop: "δ > other.t_stop"
      have t_lt_t_stop: "t < other.t_stop"
      proof (rule ccontr)
        assume "¬ t < other.t_stop"
        hence "other.t_stop ≤ t" by simp
        from ‹ego_other2 t = 0› have "ego.q t = other.p_max"
          unfolding ego_other2_def u_def other.s_def comp_def τ_def other.p_max_def
          using ‹t ∈ {0 <..< δ}› ‹other.t_stop ≤ t› gt_t_stop by (auto split:if_splits)
        have "ego.q t = u t" unfolding u_def using ‹t ∈ {0 <..< δ}› by auto
        also have "... ≤ u_max" using u_max by auto
        also have "... < other.p_max" using assms(2) other.s_t_stop by auto
        finally have "ego.q t < other.p_max" by auto
        with ‹ego.q t = other.p_max› show False by auto  
      qed
      
      with ‹ego_other2 t = other.s t - ego.q t› have "ego_other2 t = other.p t - ego.q t"
        unfolding other.s_def using ‹t ∈ {0 <..< δ}› by auto
      with ‹ego_other2 t = 0› have "other.p t - ego.q t = 0" by auto
      hence eq: "(so- se) + (vo - ve) * t + (1/2 * ao) * t2 = 0"
        unfolding other.p_def ego.q_def by (auto simp: algebra_simps)
      define p where "p ≡ λx. (1/2 * ao) * x2 + (vo - ve) * x + (so - se)"
      have "0 < 1/2 * ao"
      proof (intro p_convex[where p=p and b="vo - ve" and c="so - se"])
          show "0 < t" using ‹t ∈ {0 <..< δ}› by auto
        next
          show "t < other.t_stop" using t_lt_t_stop by auto
        next
          show "p t < p 0" unfolding p_def using eq in_front by (auto simp: algebra_simps)
        next
          from eq have zero: "p t = 0" unfolding p_def by auto
          have eq: "p other.t_stop = ego_other2 other.t_stop" 
            unfolding ego_other2_def other.s_t_stop u_def ego.q_def 
                      other.s_def other.p_def p_def
            using ‹δ > other.t_stop› other.t_stop_nonneg other.t_stop_def
            by (auto simp: diff_divide_distrib left_diff_distrib')
          have "u other.t_stop ≤ u_max" using u_max by auto
          also have "... < other.s_stop" using assms by auto
          finally have "0 ≤ other.s_stop - u other.t_stop" by auto
          hence "0 ≤ ego_other2 other.t_stop" unfolding ego_other2_def by auto
          hence "0 ≤ p other.t_stop" using eq by auto
          with zero show "p t ≤ p other.t_stop" by auto
        next
          show "p = (λx. 1 / 2 * ao * x2 + (vo - ve) * x + (so - se))"
          unfolding p_def by (rule refl)
      qed 
      hence False using decelerate_other by auto }

     ultimately show False by auto
  qed
qed

lemma no_collision_react_initially:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  shows "no_collision_react {0 .. δ}"
proof -
  have "no_collision_react {0 <..< δ}" by (rule no_collision_react_initially_strict[OF assms])
  have "u 0 ≠ other.s 0" using init_u other.init_s in_front by auto
  hence "no_collision_react {0}" unfolding collision_react_def by auto
  with ‹no_collision_react {0 <..< δ}› have "no_collision_react ({0} ∪ {0 <..< δ})"
    using no_collision_union[of "{0}" "{0 <..< δ}"] by auto
  moreover have "{0} ∪ {0 <..< δ} = {0 ..< δ}" using pos_react by auto
  ultimately have "no_collision_react {0 ..< δ}" by auto

  have "u δ ≠ other.s δ" using no_collision_delta by auto
  hence "no_collision_react {δ}" unfolding collision_react_def by auto
  with ‹no_collision_react {0 ..< δ}› have "no_collision_react ({δ} ∪ {0 ..< δ})"
    using no_collision_union[of "{δ}" "{0 ..< δ}"] by auto
  moreover have "{δ} ∪ {0 ..< δ} = {0 .. δ}" using pos_react by auto
  ultimately show "no_collision_react {0 .. δ}" by auto
qed

lemma collision_after_delta:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  shows "collision_react {0 ..} ⟷ collision_react {δ..}" 
proof
  assume "collision_react {0 ..}"
  have "no_collision_react {0 .. δ}" by (rule no_collision_react_initially[OF assms])
  with ‹collision_react {0..}› have "collision_react ({0..} - {0 .. δ})"
  using pos_react by (auto intro: collision_trim_subset)
  
  moreover have "{0..} - {0 .. δ} = {δ <..}" using pos_react by auto
  ultimately have "collision_react {δ <..}" by auto
  thus "collision_react {δ ..}" by (auto intro:collision_react_subset)
next
  assume "collision_react {δ..}"
  moreover have "{δ..} ⊆ {0 ..}" using pos_react by auto
  ultimately show "collision_react {0 ..}" by (rule collision_react_subset)
qed

lemma collision_react_strict:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  shows "collision_react {δ ..} ⟷ collision_react {δ <..}"
proof
  assume asm: "collision_react {δ ..}"
  have "no_collision_react {δ}" using no_collision_delta unfolding collision_react_def by auto
  moreover have "{δ <..} ⊆ {δ ..}" by auto
  ultimately have "collision_react ({δ ..} - {δ})" using asm collision_trim_subset by simp
  moreover have "{δ <..} = {δ ..} - {δ}" by auto
  ultimately show "collision_react {δ <..}" by auto
next
  assume "collision_react {δ <..}"
  thus "collision_react {δ ..}" 
    using collision_react_subset[where t="{δ ..}" and s="{δ <..}"] by fastforce
qed

lemma delayed_other_s_stop_eq: "delayed_safe_distance.other.s_stop = other.s_stop"
proof (unfold other.s_t_stop; unfold delayed_safe_distance.other.s_t_stop; unfold movement.p_max_eq)
  have "δ ≤ other.t_stop ∨ other.t_stop < δ" by auto

  moreover
  { assume "δ ≤ other.t_stop"
    hence "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2"
    unfolding other.s_def other.s'_def
    using  pos_react decelerate_other
    by (auto simp add: other.p_def other.p'_def power2_eq_square field_split_simps) }

  moreover
  { assume "other.t_stop < δ"
    hence "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2"
    unfolding other.s_def other.s'_def other.p_max_eq
    using pos_react decelerate_other 
    by (auto) }

  ultimately show "other.s δ - (other.s' δ)2 / ao / 2 = so - vo2 / ao / 2" by auto
qed

lemma delayed_cond3':
  assumes "other.s δ ≤ u_max" 
  assumes "u_max < other.s_stop"
  shows "delayed_safe_distance.collision {0 ..} ⟷  
          (ao > ae ∧ other.s' δ < ve ∧ other.s δ - ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ ve - ae / ao * other.s' δ < 0)"
  proof (rule delayed_safe_distance.cond_3')
    have "other.s δ ≤ u_max" using ‹other.s δ ≤ u_max› . 
    also have "... = ego2.s_stop" unfolding u_max_eq ego2.s_t_stop ego2.p_max_eq by (rule refl)
    finally show "other.s δ ≤ ego2.s_stop" by auto
  next
    have "ego2.s_stop = u_max" unfolding ego2.s_t_stop ego2.p_max_eq u_max_eq by (rule refl)
    also have "... < other.s_stop" using assms by auto
    also have "... ≤ delayed_safe_distance.other.s_stop" using delayed_other_s_stop_eq by auto
    finally show "ego2.s_stop < delayed_safe_distance.other.s_stop" by auto
  qed

lemma delayed_other_t_stop_eq:
  assumes "δ ≤ other.t_stop"
  shows "delayed_safe_distance.other.t_stop + δ = other.t_stop"
  using assms decelerate_other
  unfolding delayed_safe_distance.other.t_stop_def other.t_stop_def other.s'_def
            movement.t_stop_def other.p'_def
  by (auto simp add: field_split_simps)

lemma delayed_other_s_eq:
  assumes "0 ≤ t"
  shows "delayed_safe_distance.other.s t = other.s (t + δ)"
proof (cases "δ ≤ other.t_stop")
  assume 1: "δ ≤ other.t_stop"
  have "t + δ ≤ other.t_stop ∨ other.t_stop < t + δ" by auto
  moreover
  { assume "t + δ ≤ other.t_stop"
    hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p t"    
      using delayed_other_t_stop_eq [OF 1] assms
      unfolding delayed_safe_distance.other.s_def by auto 
    
    also have "... = other.p (t + δ)" 
      unfolding movement.p_def other.s_def other.s'_def other.p'_def
      using pos_react 1 
      by (auto simp add: power2_eq_square field_split_simps)
      
    also have "... = other.s (t + δ)"
      unfolding other.s_def 
      using assms pos_react ‹t + δ ≤ other.t_stop› by auto

    finally have "delayed_safe_distance.other.s t = other.s (t + δ)" by auto }

  moreover
  { assume "other.t_stop < t + δ"
    hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p_max"
      using delayed_other_t_stop_eq [OF 1] assms delayed_safe_distance.other.t_stop_nonneg
      unfolding delayed_safe_distance.other.s_def by auto
    
    also have "... = other.p_max" 
      unfolding movement.p_max_eq other.s_def other.s'_def other.p_def other.p'_def
      using pos_react 1 decelerate_other 
      by (auto simp add: power2_eq_square field_split_simps)

    also have "... = other.s (t + δ)"
      unfolding other.s_def
      using assms pos_react ‹other.t_stop < t + δ› by auto

    finally have "delayed_safe_distance.other.s t = other.s (t + δ)" by auto }

  ultimately show ?thesis by auto
next
  assume "¬ δ ≤ other.t_stop"
  hence "other.t_stop < δ" by auto
  hence "other.s' δ = 0" and "other.s δ = other.p_max" 
    unfolding other.s'_def other.s_def using pos_react by auto
  hence "delayed_safe_distance.other.s t = delayed_safe_distance.other.p_max"
    unfolding delayed_safe_distance.other.s_def using assms decelerate_other 
    by (auto simp add:movement.p_max_eq movement.p_def movement.t_stop_def)
  also have "... = other.p_max" 
    unfolding movement.p_max_eq using ‹other.s' δ = 0› ‹other.s δ = other.p_max›
    using other.p_max_eq by auto
  also have "... = other.s (t + δ)" 
    unfolding other.s_def using pos_react assms ‹other.t_stop < δ› by auto
  finally show "delayed_safe_distance.other.s t = other.s (t + δ)" by auto
qed

lemma translate_collision_range:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  shows "delayed_safe_distance.collision {0 ..} ⟷ collision_react {δ ..}"
proof 
  assume "delayed_safe_distance.collision {0 ..}" 
  then obtain t where eq: "ego2.s t = delayed_safe_distance.other.s t" and "0 ≤ t"
    unfolding delayed_safe_distance.collision_def by auto

  have "ego2.s t = (ego2.s ∘ τ) (t + δ)" unfolding comp_def τ_def by auto
  also have "... = u (t + δ)" unfolding u_def using ‹0 ≤ t› pos_react 
    by (auto simp: τ_def ego2.init_s)
  finally have left:"ego2.s t = u (t + δ)" by auto

  have right: "delayed_safe_distance.other.s t = other.s (t + δ)"
    using delayed_other_s_eq pos_react ‹0 ≤ t› by auto

  with eq and left have "u (t + δ) = other.s (t + δ)" by auto
  moreover have "δ ≤ t + δ" using ‹0 ≤ t› by auto
  ultimately show "collision_react {δ ..}" unfolding collision_react_def by auto
next
  assume "collision_react {δ ..}"
  hence "collision_react {δ <..}" using collision_react_strict[OF assms] by simp
  then obtain t where eq: "u t = other.s t" and "δ < t"
    unfolding collision_react_def by auto
  moreover hence "u t = (ego2.s ∘ τ) t" unfolding u_def using pos_react by auto
  moreover have "other.s t = delayed_safe_distance.other.s (t - δ)"
    using delayed_other_s_eq ‹δ < t› by auto
  ultimately have "ego2.s (t - δ) = delayed_safe_distance.other.s (t - δ)"
    unfolding comp_def τ_def by auto
  with ‹δ < t› show "delayed_safe_distance.collision {0 ..}" 
    unfolding delayed_safe_distance.collision_def by auto
qed

theorem cond_3r_2:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  assumes "other.s δ ≤ u_max"
  shows "collision_react {0 ..} ⟷ 
         (ao > ae ∧ other.s' δ < ve ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ ve - ae / ao * other.s' δ < 0)"
proof -
  have "collision_react {0 ..} ⟷ collision_react {δ ..}" by (rule collision_after_delta[OF assms(1) assms(2)])
  also have "... ⟷ delayed_safe_distance.collision {0 ..}" by (simp add: translate_collision_range[OF assms(1) assms(2)])
  also have "... ⟷  (ao > ae ∧ other.s' δ < ve ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ ve - ae / ao * other.s' δ < 0)"
    by (rule delayed_cond3'[OF assms(3) assms(2)])
  finally show "collision_react {0 ..} ⟷  (ao > ae ∧ other.s' δ < ve ∧ other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance ∧ ve - ae / ao * other.s' δ < 0)"
    by auto
qed

lemma sd_2r_correct_for_3r_2:
  assumes "so - se > safe_distance_2r"
  assumes "other.s δ ≤ u_max"
  assumes "¬ (ao > ae ∧ other.s' δ < ve ∧ ve - ae / ao * other.s' δ < 0)"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  hence "so - vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so - vo2 / ao + vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so + vo * (- vo / ao) + 1/2 * ao * (-vo / ao)2 > se + ve * δ - ve2 / 2 / ae"
    using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  hence "other.s_stop > u_max" unfolding other.s_def using u_max_eq other.t_stop_def
    using ego.q_def other.p_def other.p_max_def other.s_def other.s_t_stop by auto
  thus ?thesis
    using assms(2) assms(3) collision_after_delta cond_1r delayed_cond3' translate_collision_range by linarith
qed

lemma sd2_at_most_sd4:
  assumes "ao > ae"
  shows "safe_distance_2r ≤ safe_distance_4r"
proof -
  have "ao ≠ 0" and "ae ≠ 0" and "ao - ae ≠ 0" and "0 < 2 * (ao - ae)" using hyps assms(1) by auto
  have "0 ≤ (- ve * ao + vo * ae + ao * ae * δ) * (- ve * ao + vo * ae + ao * ae * δ)"
    (is "0 ≤ (?l1 + ?l2 + ?l3) * ?r") by auto
  also have "... = ve2 * ao2 + vo2 * ae2 + ao2 * ae2 * δ2 - 2 * ve * ao * vo * ae - 2 * ao2 * ae * δ * ve + 2 * ao * ae2 * δ * vo"
    (is "?lhs = ?rhs")
    by (auto simp add:algebra_simps power_def)
  finally have "0 ≤ ?rhs" by auto
  hence "(- ve2 * ao / ae - vo2 * ae / ao) * (ao * ae) ≤ (ao * ae * δ2 - 2 * ve * vo - 2 * ao * δ * ve + 2 * ae * δ * vo) * (ao * ae)"
    by (auto simp add: algebra_simps power_def)
  hence "2 * ve * δ * (ao - ae) - ve2 * ao / ae + ve2 + vo2 - vo2 * ae / ao ≤ vo2 + ao2 * δ2 + ve2 + 2 * vo * δ * ao - 2 * ve * vo - 2 * ao * δ * ve - 2 * vo * δ * ao + 2 * ae * δ * vo - ao2 * δ2 + ao * ae * δ2 + 2 * ve * δ * (ao - ae)"
    by (auto simp add: ego2.decel other.decel)
  hence "2 * ve * δ * (ao - ae) - ve2 * ao / ae + ve2 + vo2 - vo2 * ae / ao ≤ (vo + δ * ao - ve)2 - 2 * vo * δ * ao + 2 * ae * δ * vo - ao2 * δ2 + ao * ae * δ2 + 2 * ve * δ * (ao - ae)"
    by (auto simp add: algebra_simps power_def)
  hence "ve * δ * 2 * (ao - ae) - ve2 / 2 / ae * 2 * ao + ve2 / 2 / ae * 2 * ae + vo2 / 2 / ao * 2 * ao - vo2 / 2 / ao * 2 * ae ≤ (vo + δ * ao - ve)2 - vo * δ * 2 * ao - vo * δ * 2 * -ae - ao * δ2 / 2 * 2 * ao - ao * δ2 / 2 * 2 * -ae + ve * δ * 2 * (ao - ae)"
    (is "?lhs1 ≤ ?rhs1")
    by (simp add: ‹ao ≠ 0› ‹ae ≠ 0› power2_eq_square algebra_simps)
  hence "ve * δ * 2 * (ao - ae) - ve2 / 2 / ae * 2 * (ao - ae) + vo2 / 2 / ao * 2 * (ao - ae) ≤ (vo + ao * δ - ve)2 / 2 / (ao - ae) * 2 * (ao - ae) - vo * δ * 2 * (ao - ae) - ao * δ2 / 2 * 2 * (ao - ae) + ve * δ * 2 *(ao - ae)"
    (is "?lhs2 ≤ ?rhs2")
  proof -
    assume "?lhs1 ≤ ?rhs1"
    have "?lhs1 = ?lhs2" by (auto simp add:field_simps)
    moreover
    have "?rhs1 = ?rhs2" using ‹ao - ae ≠ 0› by (auto simp add:field_simps)
    ultimately show ?thesis using ‹?lhs1 ≤ ?rhs1› by auto
  qed
  hence "(ve * δ - ve2 / 2 / ae + vo2 / 2 / ao) * 2 * (ao - ae) ≤ ((vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ) * 2 *(ao - ae)"
    by (simp add: algebra_simps)
  hence "ve * δ - ve2 / 2 / ae + vo2 / 2 / ao ≤ (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"
    using ‹ao > ae› mult_le_cancel_right_pos[OF ‹0 < 2 * (ao - ae)›, of "(ve * δ - ve2 / 2 / ae + vo2 / 2 / ao)"
    "(vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"] semiring_normalization_rules(18)
    by (metis (no_types, lifting))
  thus ?thesis using safe_distance_2r_def safe_distance_4r_def by auto
qed

lemma sd_4r_correct:
  assumes "so - se > safe_distance_4r"
  assumes "other.s δ ≤ u_max"
  assumes "δ ≤ other.t_stop"
  assumes "ao > ae"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1/2 * ao * δ2 + ve * δ"
    unfolding safe_distance_4r_def by auto
  hence "so + vo * δ + 1/2 * ao * δ2 - se - ve * δ > (vo + ao * δ - ve)2 / 2 / (ao - ae)" by linarith
  hence "other.s δ -  ego.q δ > (other.s' δ - ve)2 / 2 / (ao - ae)"
    using assms(3) ego.q_def other.p_def other.s_def other.p'_def other.s'_def pos_react by auto
  hence "other.s δ -  ego.q δ > delayed_safe_distance.snd_safe_distance"
    by (simp add: delayed_safe_distance.snd_safe_distance_def)
  hence c: "¬ (other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance)" by linarith
  have "u_max < other.s_stop"
    unfolding u_max_eq other.s_t_stop other.p_max_eq ego.q_def using assms(1) sd2_at_most_sd4[OF assms(4)]
    unfolding safe_distance_4r_def safe_distance_2r_def by auto
  consider "so ≤ u_max" | "so > u_max" by linarith
  thus ?thesis
  proof (cases)
    case 1
    from cond_3r_2[OF this ‹u_max < other.s_stop› assms(2)]  show ?thesis
      using c by auto
  next
    case 2
    then show ?thesis using cond_1r by auto
  qed
qed

text ‹Irrelevant, this Safe Distance is unreachable in the checker.›
definition safe_distance_5r :: real where 
  "safe_distance_5r = ve2 / 2 / (ao - ae) + vo2 / 2 / ao + ve * δ"

lemma sd_5r_correct:
  assumes "so - se > safe_distance_5r"
  assumes "u_max < other.s_stop"
  assumes "other.s δ ≤ u_max"
  assumes "δ > other.t_stop"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve2 / 2 / (ao - ae) + vo2 / 2 / ao + ve * δ"
    unfolding safe_distance_5r_def by auto
  hence "so + vo2 / 2 / ao - se - ve * δ > (0 - ve)2 / 2 / (ao - ae)"
    using assms(2-4) unfolding other.s_def other.s_t_stop
    apply (auto simp: movement.p_t_stop split: if_splits)
    using cond_1r cond_2r other.s_t_stop by linarith+
  hence "other.s δ -  ego.q δ > (other.s' δ - ve)2 / 2 / (ao - ae)"
    using assms(2) assms(3) assms(4) other.s_def other.s_t_stop by auto
  hence "other.s δ -  ego.q δ > delayed_safe_distance.snd_safe_distance"
    by (simp add: delayed_safe_distance.snd_safe_distance_def)
  hence "¬ (other.s δ -  ego.q δ ≤ delayed_safe_distance.snd_safe_distance)" by linarith
  thus ?thesis using assms(2) assms(3) cond_1r cond_3r_2 by linarith
qed

lemma translate_no_collision_range:
  "delayed_safe_distance.no_collision {0 ..} ⟷ no_collision_react {δ ..}"  
proof
  assume left: "delayed_safe_distance.no_collision {0 ..}" 
  show "no_collision_react {δ ..}" 
  proof (unfold collision_react_def; simp; rule ballI)
    fix t::real  
    assume "t ∈ {δ ..}"
    hence "δ ≤ t" by simp
    with pos_react have "0 ≤ t - δ" by simp
    with left have ineq: "ego2.s (t - δ) ≠ delayed_safe_distance.other.s (t - δ)"
      unfolding delayed_safe_distance.collision_def by auto
    have "ego2.s (t - δ) = (ego2.s ∘ τ) t" unfolding comp_def τ_def by auto
    also have "... = u t" unfolding u_def using ‹δ ≤ t› pos_react 
      by (auto simp: τ_def ego2.init_s)
    finally have "ego2.s (t - δ) = u t" by auto

    moreover have "delayed_safe_distance.other.s (t - δ) = other.s t"
      using delayed_other_s_eq pos_react ‹δ ≤ t› by auto
  
    ultimately show "u t ≠ other.s t" using ineq by auto
  qed
next
  assume right: "no_collision_react {δ ..}"
  show "delayed_safe_distance.no_collision {0 ..}"
  proof (unfold delayed_safe_distance.collision_def; simp; rule ballI)
    fix t ::real
    assume "t ∈ {0 ..}"
    hence "0 ≤ t" by auto
    hence "δ ≤ t + δ" by auto
    with right have ineq: "u (t + δ) ≠ other.s (t + δ)" unfolding collision_react_def by auto
            
    have "u (t + δ) = ego2.s t" unfolding u_def comp_def τ_def 
      using ‹0 ≤ t› pos_react ‹δ ≤ t+ δ› by (auto simp add:ego2.init_s)
    moreover have "other.s (t + δ) = delayed_safe_distance.other.s t"
      using delayed_other_s_eq[of t] using ‹0 ≤ t› by auto
    ultimately show "ego2.s t ≠ delayed_safe_distance.other.s t" using ineq by auto
  qed
qed

lemma delayed_cond1:
  assumes "other.s δ > u_max"
  shows "delayed_safe_distance.no_collision {0 ..}"
proof -
  have "ego2.s_stop = u_max"  unfolding ego2.s_t_stop ego2.p_max_eq u_max_eq by auto
  also have "... < other.s δ" using assms by simp
  finally have "ego2.s_stop < other.s δ" by auto
  thus "delayed_safe_distance.no_collision {0 ..}" by (simp add: delayed_safe_distance.cond_1)
qed

theorem cond_3r_3:
  assumes "so ≤ u_max"
  assumes "u_max < other.s_stop"
  assumes "other.s δ > u_max"
  shows "no_collision_react {0 ..}"
proof -
  have eq: "{0 ..} = {0 .. δ} ∪ {δ ..}" using pos_react by auto
  show ?thesis unfolding eq 
  proof (intro no_collision_union)
    show "no_collision_react {0 .. δ}" by (rule no_collision_react_initially[OF assms(1) assms(2)])  
  next
    have "delayed_safe_distance.no_collision {0 ..}" by (rule delayed_cond1[OF assms(3)])
    with translate_no_collision_range show "no_collision_react {δ ..}" by auto
  qed
qed

lemma sd_2r_correct_for_3r_3:
  assumes "so - se > safe_distance_2r"
  assumes "other.s δ > u_max"
  shows "no_collision_react {0..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae + vo2 / 2 / ao" unfolding safe_distance_2r_def by auto
  hence "so - vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so - vo2 / ao + vo2 / 2 / ao > se + ve * δ - ve2 / 2 / ae" by auto
  hence "so + vo * (- vo / ao) + 1/2 * ao * (-vo / ao)2 > se + ve * δ - ve2 / 2 / ae"
    using other.p_def other.p_max_def other.p_max_eq other.t_stop_def by auto
  hence "other.s_stop > u_max" unfolding other.s_def using u_max_eq other.t_stop_def
    using ego.q_def other.p_def other.p_max_def other.s_def other.s_t_stop by auto
  thus ?thesis
    using assms(2) cond_1r cond_3r_3 by linarith
qed

lemma sd_3r_correct:
  assumes "so - se > safe_distance_3r"
  assumes "δ ≤ other.t_stop"
  shows "no_collision_react {0 ..}"
proof -
  from assms have "so - se > ve * δ - ve2 / 2 / ae - vo * δ - 1/2 * ao * δ2" unfolding safe_distance_3r_def by auto
  hence "so + vo * δ + 1/2 * ao * δ2 > se + ve * δ - ve2 / 2 / ae" by auto
  hence "other.s δ > u_max" using other.s_def u_max_eq assms(2) ego.q_def other.p_def pos_react by auto
  thus ?thesis using cond_1r cond_3r_3 delayed_other_s_stop_eq delayed_safe_distance.other.s0_le_s_stop by linarith
qed

lemma sd_2_at_least_sd_3:
  assumes "δ ≤ other.t_stop"
  shows "safe_distance_3r ≥ safe_distance_2r"
proof -
  from assms have "δ = other.t_stop ∨ δ < other.t_stop" by auto
  then have "safe_distance_3r = safe_distance_2r ∨ safe_distance_3r > safe_distance_2r"
  proof (rule Meson.disj_forward)
      assume "δ = other.t_stop"
      hence "δ = - vo / ao" unfolding other.t_stop_def by auto
      hence "- vo * δ - 1/2 * ao * δ2 = - vo  * other.t_stop - 1/2 * ao * other.t_stop2" by (simp add: movement.t_stop_def)
      thus "safe_distance_3r = safe_distance_2r"
        using other.p_def other.p_max_def other.p_max_eq safe_distance_2r_def safe_distance_3r_def by auto
    next
      assume "δ < other.t_stop"
      hence "δ < - vo / ao" unfolding other.t_stop_def by auto
      hence "0 < vo + ao * δ"
        using other.decel other.p'_def other.p'_pos_iff by auto
      hence "0 < vo + 1/2 * ao * (δ + other.t_stop)" by (auto simp add:field_simps other.t_stop_def)
      hence "0 > vo * (δ - other.t_stop) + 1/2 * ao * (δ + other.t_stop) * (δ - other.t_stop)"
        using ‹δ < other.t_stop›  mult_less_cancel_left_neg[where c="δ - other.t_stop" and a ="vo + 1 / 2 * ao * (δ + other.t_stop)" and b="0"]
        by (auto simp add: field_simps)
      hence " (δ + other.t_stop) * (δ - other.t_stop) = (δ2 - other.t_stop2)"
        by (simp add: power2_eq_square square_diff_square_factored)
      hence "0 > vo * (δ - other.t_stop) + 1/2 * ao * (δ2 - other.t_stop2)"
        by (metis (no_types, opaque_lifting) ‹vo * (δ - other.t_stop) + 1 / 2 * ao * (δ + other.t_stop) * (δ - other.t_stop) < 0› divide_divide_eq_left divide_divide_eq_right times_divide_eq_left)
      hence "0 > vo * δ - vo * other.t_stop  + 1/2 * ao * δ2 -  1/2 * ao * other.t_stop2 "
        by (simp add: right_diff_distrib)
      hence "- vo * δ - 1/2 * ao * δ2 > - vo  * (- vo / ao) - 1/2 * ao * (- vo / ao)2"
        unfolding movement.t_stop_def by argo
      thus "safe_distance_3r > safe_distance_2r"
        using other.p_def other.p_max_def other.p_max_eq other.t_stop_def safe_distance_2r_def safe_distance_3r_def by auto
  qed
  thus ?thesis by auto
qed
end

subsection ‹Checker Design›

text ‹
  We define two checkers for different cases: 
  ▪ one checker for the case that ‹δ ≤ other.t_stop (other.t_stop = - vo / ao)›
  ▪ a second checker for the case that ‹δ > other.t_stop›
›

definition check_precond_r1 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "check_precond_r1 se ve ae so vo ao δ ⟷ so > se ∧ 0 ≤ ve ∧ 0 ≤ vo ∧ ae < 0 ∧ ao < 0 ∧ 0 < δ ∧ δ ≤ - vo / ao"

definition safe_distance0 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" where 
  "safe_distance0 ve ao vo δ = ve * δ - vo * δ - ao * δ2 / 2"

definition safe_distance_1r :: "real ⇒ real ⇒ real ⇒ real" where 
  "safe_distance_1r ae ve δ = ve * δ - ve2 / ae / 2"

definition safe_distance_2r :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real" where 
  "safe_distance_2r ae ve ao vo δ = ve * δ - ve2 / 2 / ae + vo2 / 2 / ao"

definition safe_distance_4r :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real" where
  "safe_distance_4r ae ve ao vo δ = (vo + ao * δ - ve)2 / 2 / (ao - ae) - vo * δ - 1 / 2 * ao * δ2 + ve * δ"

definition safe_distance_3r :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real" where 
  "safe_distance_3r ae ve ao vo δ = ve * δ - ve2 / 2 / ae - vo * δ - 1 / 2 * ao * δ2"

definition checker_r1 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "checker_r1 se ve ae so vo ao δ ≡ 
    let distance      = so - se;
				precond       = check_precond_r1 se ve ae so vo ao δ;
        vo_star       = vo + ao * δ;
        t_stop_o_star = - vo_star / ao;
        t_stop_e      = - ve / ae;
        safe_dist0    = safe_distance_1r ae ve δ;
        safe_dist1    = safe_distance_2r ae ve ao vo δ;
        safe_dist2    = safe_distance_4r ae ve ao vo δ;
        safe_dist3    = safe_distance_3r ae ve ao vo δ
    in
      if ¬ precond then False
      else if distance > safe_dist0 ∨ distance > safe_dist3 then True
      else if (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star) then distance > safe_dist2
      else distance > safe_dist1"

theorem checker_r1_correctness:
  "(checker_r1 se ve ae so vo ao δ ⟷ check_precond_r1 se ve ae so vo ao δ ∧ 
   safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
proof
  assume asm: "checker_r1 se ve ae so vo ao δ"
  have pre: "check_precond_r1 se ve ae so vo ao δ"
  proof (rule ccontr)
    assume "¬ check_precond_r1 se ve ae so vo ao δ"
    with asm show "False" unfolding checker_r1_def Let_def by auto
  qed
  from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
    by (unfold_locales) (auto simp add: check_precond_r1_def)
  interpret sdn: safe_distance_normal ae ve se ao vo so δ
    rewrites "sdn.distance0 = safe_distance0 ve ao vo δ" and
             "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
             "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ" and
             "sdn.safe_distance_4r = safe_distance_4r ae ve ao vo δ" and
             "sdn.safe_distance_3r = safe_distance_3r ae ve ao vo δ"
  proof -
    from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
  next
    show "safe_distance_normal.distance0 ve ao vo δ = safe_distance0 ve ao vo δ "
      unfolding safe_distance_normal.distance0_def[OF sdn'] safe_distance0_def by auto
  next
    show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
      unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
  next
    show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
  next
    show "safe_distance_normal.safe_distance_4r ae ve ao vo δ = safe_distance_4r ae ve ao vo δ "
      unfolding safe_distance_normal.safe_distance_4r_def[OF sdn'] safe_distance_4r_def by auto
  next
    show "safe_distance_normal.safe_distance_3r ae ve ao vo δ = safe_distance_3r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_3r_def[OF sdn'] safe_distance_3r_def by auto
  qed
  have "0 < δ" and "δ ≤ - vo / ao" using pre unfolding check_precond_r1_def by auto
  define so_delta where "so_delta = so + vo * δ + ao * δ2 / 2"
  define q_e_delta where "q_e_delta ≡ se + ve * δ"
  define u_stop_e where "u_stop_e ≡ q_e_delta - ve2 / (2 * ae)"
  define vo_star where "vo_star = vo + ao * δ"
  define t_stop_o_star where "t_stop_o_star ≡ - vo_star / ao"
  define t_stop_e where "t_stop_e = - ve / ae"
  define distance where "distance ≡ so - se"
  define distance0 where "distance0 = safe_distance0 ve ao vo δ"
  define safe_dist0 where "safe_dist0 = safe_distance_1r ae ve δ"
  define safe_dist2 where "safe_dist2 ≡ safe_distance_4r ae ve ao vo δ"
  define safe_dist1 where "safe_dist1 ≡ safe_distance_2r ae ve ao vo δ"
  define safe_dist3 where "safe_dist3 = safe_distance_3r ae ve ao vo δ"
  note abb = so_delta_def q_e_delta_def u_stop_e_def vo_star_def t_stop_o_star_def t_stop_e_def
             distance_def safe_dist2_def safe_dist1_def safe_dist0_def safe_dist3_def distance0_def
  consider "distance > safe_dist0" | "distance > safe_dist3" | "distance ≤ safe_dist0 ∧ distance ≤ safe_dist3"
    by linarith
  hence "sdn.no_collision_react {0..}"
  proof (cases)
    case 1
    then show ?thesis using sdn.sd_1r_correct unfolding  abb by auto
  next
    case 2
    hence pre2: "distance > distance0" using sdn.distance0_at_most_sd3r unfolding abb by auto
    hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
      sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
      by auto
    from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
      by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ›)
    show ?thesis using sdr.sd_3r_correct 2 pre unfolding check_precond_r1_def abb sdn.other.t_stop_def
      by auto
  next
    case 3
    hence "distance ≤ safe_dist3" by auto
    hence "sdn.other.s δ ≤ sdn.u_max" using pre unfolding check_precond_r1_def sdn.other.s_def sdn.other.t_stop_def
      sdn.other.p_def sdn.u_max_eq sdn.ego.q_def abb sdn.safe_distance_3r_def by auto
    have " (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star) ∨ ¬  (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star) "
      by auto
    moreover
    { assume cond: "(ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star)"
      with 3 pre have "distance > safe_dist2" using asm unfolding checker_r1_def
          Let_def abb by auto
      with sdn.distance0_at_most_sd4r have "distance > distance0" unfolding abb using cond by auto
      hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
        by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ›)
      from sdr.sd_4r_correct[OF _ ‹sdn.other.s δ ≤ sdn.u_max›] ‹distance > safe_dist2›
        have ?thesis using pre cond  unfolding check_precond_r1_def sdn.other.t_stop_def abb by auto }
    moreover
    { assume not_cond: "¬  (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star)"
      with 3 pre have "distance > safe_dist1" using asm unfolding checker_r1_def
        Let_def abb by auto
      with sdn.dist0_sd2r_1 have "distance > distance0" using pre not_cond unfolding check_precond_r1_def
        sdn.other.t_stop_def sdn.other.s'_def sdn.other.p'_def abb by (auto simp add:field_simps)
      hence "sdn.u δ < sdn.other.s δ" using pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
        by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ›)
      from sdr.sd_2r_correct_for_3r_2[OF _ ‹sdn.other.s δ ≤ sdn.u_max›] not_cond ‹distance > safe_dist1›
        have ?thesis using pre unfolding abb sdn.other.s'_def check_precond_r1_def sdn.other.t_stop_def sdn.other.p'_def
        by (auto simp add:field_simps) }
    ultimately show ?thesis by auto
  qed
  with pre show " check_precond_r1 se ve ae so vo ao δ ∧ sdn.no_collision_react {0..}" by auto
next
  assume "check_precond_r1 se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
  hence pre: "check_precond_r1 se ve ae so vo ao δ" and as2: "safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
  by auto
  show "checker_r1 se ve ae so vo ao δ "
  proof (rule ccontr)
    assume as1: "¬ checker_r1 se ve ae so vo ao δ"
    from pre have "0 < δ" and "δ ≤ - vo / ao" unfolding check_precond_r1_def by auto
    define so_delta where "so_delta = so + vo * δ + ao * δ2 / 2"
    define q_e_delta where "q_e_delta ≡ se + ve * δ"
    define u_stop_e where "u_stop_e ≡ q_e_delta - ve2 / (2 * ae)"
    define vo_star where "vo_star ≡ vo + ao * δ"
    define t_stop_o_star where "t_stop_o_star ≡ - vo_star / ao"
    define t_stop_e where "t_stop_e ≡ - ve / ae"
    define distance where "distance ≡ so - se"
    define distance0 where "distance0 ≡ safe_distance0 ve ao vo δ"
    define safe_dist0 where "safe_dist0 ≡ safe_distance_1r ae ve δ"
    define safe_dist2 where "safe_dist2 ≡ safe_distance_4r ae ve ao vo δ"
    define safe_dist1 where "safe_dist1 ≡ safe_distance_2r ae ve ao vo δ"
    define safe_dist3 where "safe_dist3 ≡ safe_distance_3r ae ve ao vo δ"
    note abb = so_delta_def q_e_delta_def u_stop_e_def vo_star_def t_stop_o_star_def t_stop_e_def
               distance_def safe_dist2_def safe_dist1_def safe_dist0_def safe_dist3_def distance0_def
    from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
      by (unfold_locales) (auto simp add: check_precond_r1_def)
    interpret sdn: safe_distance_normal ae ve se ao vo so δ
      rewrites "sdn.distance0 = safe_distance0 ve ao vo δ" and
               "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
               "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ" and
               "sdn.safe_distance_4r = safe_distance_4r ae ve ao vo δ" and
               "sdn.safe_distance_3r = safe_distance_3r ae ve ao vo δ"
    proof -
      from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
    next
      show "safe_distance_normal.distance0 ve ao vo δ = safe_distance0 ve ao vo δ "
        unfolding safe_distance_normal.distance0_def[OF sdn'] safe_distance0_def by auto
    next
      show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
        unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
    next
      show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
        unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
    next
      show "safe_distance_normal.safe_distance_4r ae ve ao vo δ = safe_distance_4r ae ve ao vo δ "
        unfolding safe_distance_normal.safe_distance_4r_def[OF sdn'] safe_distance_4r_def by auto
    next
      show "safe_distance_normal.safe_distance_3r ae ve ao vo δ = safe_distance_3r ae ve ao vo δ"
        unfolding safe_distance_normal.safe_distance_3r_def[OF sdn'] safe_distance_3r_def by auto
    qed
    have "¬ distance > distance0 ∨  distance > distance0" by auto
    moreover
    { assume "¬ distance > distance0"
      hence "distance ≤ distance0" by auto
      with sdn.cond_3r_1' have "sdn.collision_react {0..δ}" using pre unfolding check_precond_r1_def abb
        sdn.other.t_stop_def by auto
      with sdn.collision_react_subset have "sdn.collision_react {0..}" by auto
      with as2 have "False" by auto }
    moreover
    { assume if2: "distance > distance0"
      have "¬ (distance > safe_dist0 ∨ distance > safe_dist3)"
      proof (rule ccontr)
        assume "¬ ¬ (safe_dist0 < distance ∨ safe_dist3 < distance)"
        hence "(safe_dist0 < distance ∨ safe_dist3 < distance)" by auto
        with as1 show "False" using pre if2 unfolding checker_r1_def Let_def abb
          by auto
      qed
      hence if31: "distance ≤ safe_dist0" and if32: "distance ≤ safe_dist3" by auto
      have "sdn.u δ < sdn.other.s δ" using if2 pre unfolding sdn.u_def sdn.ego.q_def
          sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def abb check_precond_r1_def sdn.distance0_def
          by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r1_def ‹sdn.u δ < sdn.other.s δ›)
      have " so ≤ sdn.u_max" using if31 unfolding sdn.u_max_eq sdn.ego.q_def abb
        sdn.safe_distance_1r_def by auto
      have "sdn.other.s δ ≤ sdn.u_max" using if32 pre unfolding sdn.other.s_def check_precond_r1_def
        sdn.other.t_stop_def sdn.other.p_def sdn.u_max_eq sdn.ego.q_def abb sdn.safe_distance_3r_def
        by auto
      consider "(ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star)" |
               "¬ (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star)" by auto
      hence "False"
      proof (cases)
        case 1
        hence rest_conjunct:"(ae < ao ∧ sdn.other.s' δ < ve ∧ ve - ae / ao * sdn.other.s' δ < 0)"
          using pre unfolding check_precond_r1_def unfolding sdn.other.s'_def sdn.other.t_stop_def
          sdn.other.p'_def abb by (auto simp add:field_simps)
        from 1 have "distance ≤ safe_dist2" using as1 pre if2 if31 if32 unfolding checker_r1_def
          Let_def abb by auto
        hence cond_f: "sdn.other.s δ - sdn.ego.q δ ≤ sdr.delayed_safe_distance.snd_safe_distance"
          using pre unfolding check_precond_r1_def sdn.other.s_def sdn.other.t_stop_def sdn.other.p_def
          sdn.ego.q_def sdr.delayed_safe_distance.snd_safe_distance_def using sdn.other.s'_def[of "δ"]
          unfolding sdn.other.t_stop_def sdn.other.p'_def abb sdn.safe_distance_4r_def
          by auto
        have "distance > safe_dist1 ∨ distance ≤ safe_dist1" by auto
        moreover
        { assume "distance > safe_dist1"
          hence "sdn.u_max < sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
              sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
          from sdr.cond_3r_2[OF ‹so ≤ sdn.u_max› this ‹sdn.other.s δ ≤ sdn.u_max›]
          have "sdn.collision_react {0..}" using cond_f rest_conjunct by auto
          with as2 have "False" by auto }
        moreover
        { assume "distance ≤ safe_dist1"
          hence "sdn.u_max ≥ sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
              sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
          with sdn.cond_2r[OF this] have "sdn.collision_react {0..}" by auto
          with as2 have "False" by auto }
        ultimately show ?thesis by auto
      next
        case 2
        hence "distance ≤ safe_dist1" using as1 pre if2 if31 if32 unfolding checker_r1_def
          Let_def abb by auto
        hence "sdn.u_max ≥ sdn.other.s_stop" unfolding sdn.u_max_eq sdn.ego.q_def sdn.other.s_t_stop
          sdn.other.p_max_eq abb sdn.safe_distance_2r_def by (auto simp add:field_simps)
        with sdn.cond_2r[OF this] have "sdn.collision_react {0..}" by auto
        with as2 show "False" by auto
      qed }
    ultimately show "False" by auto
  qed
qed

definition check_precond_r2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where 
  "check_precond_r2 se ve ae so vo ao δ ⟷ so > se ∧ 0 ≤ ve ∧ 0 ≤ vo ∧ ae < 0 ∧ ao < 0 ∧ 0 < δ ∧ δ > - vo / ao"

definition safe_distance0_2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real" where 
  "safe_distance0_2 ve ao vo δ = ve * δ + 1 / 2 * vo2 / ao"

definition checker_r2 :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "checker_r2 se ve ae so vo ao δ ≡ 
    let distance   = so - se;
				precond    = check_precond_r2 se ve ae so vo ao δ;
        safe_dist0 = safe_distance_1r ae ve δ;
        safe_dist1 = safe_distance_2r ae ve ao vo δ 
    in
      if ¬ precond then False
      else if distance > safe_dist0 then True
      else distance > safe_dist1"

theorem checker_r2_correctness:
  "(checker_r2 se ve ae so vo ao δ ⟷ check_precond_r2 se ve ae so vo ao δ ∧ 
    safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
proof
  assume asm: "checker_r2 se ve ae so vo ao δ"
  have pre: "check_precond_r2 se ve ae so vo ao δ"
  proof (rule ccontr)
    assume "¬ check_precond_r2 se ve ae so vo ao δ"
      with asm show "False" unfolding checker_r2_def Let_def by auto
    qed
      from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
    by (unfold_locales) (auto simp add: check_precond_r2_def)
  interpret sdn: safe_distance_normal ae ve se ao vo so δ
    rewrites "sdn.distance0_2 = safe_distance0_2 ve ao vo δ" and
             "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
             "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ"
  proof -
    from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
  next
    show "safe_distance_normal.distance0_2 ve ao vo δ = safe_distance0_2 ve ao vo δ"
      unfolding safe_distance_normal.distance0_2_def[OF sdn'] safe_distance0_2_def by auto
  next
    show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
      unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
  next
    show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
      unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
  qed
  have "0 < δ" and "δ > - vo / ao" using pre unfolding check_precond_r2_def by auto
  define distance where "distance ≡ so - se"
  define distance0_2 where "distance0_2 = safe_distance0_2 ve ao vo δ"
  define safe_dist0 where "safe_dist0 = safe_distance_1r ae ve δ"
  define safe_dist1 where "safe_dist1 ≡ safe_distance_2r ae ve ao vo δ"
  note abb = distance_def safe_dist1_def safe_dist0_def distance0_2_def
  consider "distance > safe_dist0" | "distance ≤ safe_dist0"
    by linarith
  hence "sdn.no_collision_react {0..}"
  proof (cases)
    case 1
    then show ?thesis using sdn.sd_1r_correct unfolding abb by auto
  next
    case 2
    hence "(so ≤ sdn.u_max)" using distance_def safe_dist0_def sdn.sd_1r_eq by linarith
    with 2 pre have "distance > safe_dist1" using asm unfolding checker_r2_def Let_def abb by auto
    with sdn.dist0_sd2r_2 have "distance > distance0_2" using abb ‹- vo / ao < δ› by auto
    hence "sdn.u δ < sdn.other.s δ" using abb sdn.distance0_2_eq ‹δ > - vo / ao› sdn.other.t_stop_def by auto
    have "sdn.u_max < sdn.other.s δ" using abb sdn.sd2r_eq  ‹δ > - vo / ao› sdn.other.t_stop_def ‹distance > safe_dist1› by auto
    from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
        by (unfold_locales) (auto simp add:check_precond_r2_def ‹sdn.u δ < sdn.other.s δ›)
    from sdr.sd_2r_correct_for_3r_3[OF] ‹distance > safe_dist1› ‹sdn.u δ < sdn.other.s δ› ‹sdn.u_max < sdn.other.s δ›
       show ?thesis using pre unfolding abb sdn.other.s'_def check_precond_r2_def sdn.other.t_stop_def sdn.other.p'_def
            by (auto simp add:field_simps)
  qed
  with pre show " check_precond_r2 se ve ae so vo ao δ ∧ sdn.no_collision_react {0..}" by auto
next
  assume "check_precond_r2 se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
  hence pre: "check_precond_r2 se ve ae so vo ao δ" and as2: "safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
    by auto
  show "checker_r2 se ve ae so vo ao δ"
  proof (rule ccontr)
    assume as1: "¬ checker_r2 se ve ae so vo ao δ"
    from pre have "0 < δ" and "δ > - vo / ao" unfolding check_precond_r2_def by auto
    define distance where "distance ≡ so - se"
    define distance0_2 where "distance0_2 = safe_distance0_2 ve ao vo δ"
    define safe_dist0 where "safe_dist0 = safe_distance_1r ae ve δ"
    define safe_dist1 where "safe_dist1 ≡ safe_distance_2r ae ve ao vo δ"
    note abb = distance_def safe_dist1_def safe_dist0_def distance0_2_def
    from pre have sdn': "safe_distance_normal ae ve se ao vo so δ"
      by (unfold_locales) (auto simp add: check_precond_r2_def)
   interpret sdn: safe_distance_normal ae ve se ao vo so δ
    rewrites "sdn.distance0_2 = safe_distance0_2 ve ao vo δ" and
             "sdn.safe_distance_1r = safe_distance_1r ae ve δ" and
             "sdn.safe_distance_2r = safe_distance_2r ae ve ao vo δ"
    proof -
      from sdn' show "safe_distance_normal ae ve se ao vo so δ" by auto
    next
      show "safe_distance_normal.distance0_2 ve ao vo δ = safe_distance0_2 ve ao vo δ"
        unfolding safe_distance_normal.distance0_2_def[OF sdn'] safe_distance0_2_def by auto
    next
      show "safe_distance_normal.safe_distance_1r ae ve δ = safe_distance_1r ae ve δ"
        unfolding safe_distance_normal.safe_distance_1r_def[OF sdn'] safe_distance_1r_def by auto
    next
      show "safe_distance_normal.safe_distance_2r ae ve ao vo δ = safe_distance_2r ae ve ao vo δ"
        unfolding safe_distance_normal.safe_distance_2r_def[OF sdn'] safe_distance_2r_def by auto
    qed
    have "¬ distance > distance0_2 ∨  distance > distance0_2" by auto
    moreover
    { assume "¬ distance > distance0_2"
      hence "distance ≤ distance0_2" by auto
      with sdn.cond_3r_1'_2 have "sdn.collision_react {0..δ}" using pre unfolding check_precond_r2_def abb sdn.other.t_stop_def by auto
      with sdn.collision_react_subset have "sdn.collision_react {0..}" by auto
      with as2 have "False" by auto }
    moreover
    { assume if2: "distance > distance0_2"
      have "¬ (distance > safe_dist0)"
      proof (rule ccontr)
        assume "¬ ¬ (safe_dist0 < distance)"
        hence "(safe_dist0 < distance)" by auto
        with as1 show "False" using pre if2 unfolding checker_r2_def Let_def abb by auto
      qed
      hence if3: "distance ≤ safe_dist0" by auto
      with pre have "distance ≤ safe_dist1" using as1 unfolding checker_r2_def Let_def abb by auto

      have "sdn.u δ < sdn.other.s δ" using abb if2 sdn.distance0_2_eq ‹δ > - vo / ao› sdn.other.t_stop_def by auto
      from pre interpret sdr: safe_distance_no_collsion_delta ae ve se ao vo so δ
          by (unfold_locales) (auto simp add:check_precond_r2_def ‹sdn.u δ < sdn.other.s δ›)
      have "sdn.u_max ≥ sdn.other.s δ" using abb sdn.sd2r_eq  ‹δ > - vo / ao› sdn.other.t_stop_def ‹distance ≤ safe_dist1› by auto
      with ‹δ > - vo / ao› have "sdn.u_max ≥ sdn.other.s_stop"
        using sdn.other.s_mono sdn.other.t_stop_nonneg sdn.other.p_t_stop sdn.other.p_zero sdn.other.t_stop_def
        apply (auto simp: sdn.other.s_def movement.t_stop_def split: if_splits)
        using sdn.other.p_zero by auto
      hence "sdn.collision_react {0..}" using sdn.cond_2r by auto
      with as2 have "False" by auto }
    ultimately show "False" by auto
  qed
qed

text ‹Combine the two checkers into one.›

definition check_precond_r :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where 
  "check_precond_r se ve ae so vo ao δ ⟷ so > se ∧ 0 ≤ ve ∧ 0 ≤ vo ∧ ae < 0 ∧ ao < 0 ∧ 0 < δ"

definition checker_r :: "real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ real ⇒ bool" where
  "checker_r se ve ae so vo ao δ ≡ 
    let distance      = so - se;
				precond       = check_precond_r se ve ae so vo ao δ;
        vo_star       = vo + ao * δ;
        t_stop_o_star = -vo_star / ao;
        t_stop_e      = -ve / ae;
        t_stop_o      = -vo / ao;
        safe_dist0    = safe_distance_1r ae ve δ;
        safe_dist1    = safe_distance_2r ae ve ao vo δ;
        safe_dist2    = safe_distance_4r ae ve ao vo δ;
        safe_dist3    = safe_distance_3r ae ve ao vo δ 
    in
      if ¬ precond then False
      else if distance > safe_dist0 then True
      else if δ ≤ t_stop_o ∧ distance > safe_dist3 then True
      else if δ ≤ t_stop_o ∧ (ao > ae ∧ vo_star < ve ∧ t_stop_e < t_stop_o_star) then distance > safe_dist2
      else distance > safe_dist1"

theorem checker_eq_1:
  "checker_r se ve ae so vo ao δ ∧ δ ≤ - vo / ao  ⟷ checker_r1 se ve ae so vo ao δ"
proof -
  have "checker_r se ve ae so vo ao δ ∧ δ ≤ - vo / ao ⟷ check_precond_r se ve ae so vo ao δ
    ∧ (so - se > safe_distance_1r ae ve δ
        ∨ so - se > safe_distance_3r ae ve ao vo δ
        ∨ (((ao > ae ∧ vo + ao * δ < ve ∧ - ve / ae < - (vo + ao * δ) / ao) ⟶ so - se > safe_distance_4r ae ve ao vo δ)
            ∧ (¬ (ao > ae ∧ vo + ao * δ < ve ∧ - ve / ae < - (vo + ao * δ) / ao) ⟶ so - se > safe_distance_2r ae ve ao vo δ)))
    ∧ δ ≤ - vo / ao" using checker_r_def by metis
  also have "... ⟷ check_precond_r1 se ve ae so vo ao δ
    ∧ (so - se > safe_distance_1r ae ve δ
        ∨ so - se > safe_distance_3r ae ve ao vo δ
        ∨ (((ao > ae ∧ vo + ao * δ < ve ∧ - ve / ae < - (vo + ao * δ) / ao) ⟶ so - se > safe_distance_4r ae ve ao vo δ)
            ∧ (¬ (ao > ae ∧ vo + ao * δ < ve ∧ - ve / ae < - (vo + ao * δ) / ao) ⟶ so - se > safe_distance_2r ae ve ao vo δ)))"
    by (auto simp add:check_precond_r_def check_precond_r1_def)
  also have "... ⟷ checker_r1 se ve ae so vo ao δ" by (metis checker_r1_def)
  finally show ?thesis by auto
qed

theorem checker_eq_2:
  "checker_r se ve ae so vo ao δ ∧ δ > - vo / ao ⟷ checker_r2 se ve ae so vo ao δ"
proof -
  have "checker_r se ve ae so vo ao δ ∧ δ > - vo / ao ⟷ check_precond_r se ve ae so vo ao δ ∧ (¬ check_precond_r se ve ae so vo ao δ ∨
   so - se > safe_distance_1r ae ve δ ∨
   (δ ≤ - vo / ao ∧ so - se > safe_distance_3r ae ve ao vo δ) ∨
   (δ ≤ - vo / ao ∧ ao > ae ∧ vo + ao * δ < ve ∧ - ve / ae < - (vo + ao * δ) / ao ∧ so - se > safe_distance_4r ae ve ao vo δ) ∨
   so - se > safe_distance_2r ae ve ao vo δ) ∧ δ > - vo / ao" unfolding checker_r_def Let_def if_splits by auto
  also have
   "... ⟷ check_precond_r se ve ae so vo ao δ
   ∧ (so - se > safe_distance_1r ae ve δ ∨ so - se > safe_distance_2r ae ve ao vo δ)
   ∧ δ > - vo / ao"  by (auto simp add:HOL.disjE)
  also have
    "... ⟷ check_precond_r2 se ve ae so vo ao δ
   ∧ (so - se > safe_distance_1r ae ve δ ∨ so - se > safe_distance_2r ae ve ao vo δ)"
    by (auto simp add:check_precond_r_def check_precond_r2_def)
  also have "... ⟷ checker_r2 se ve ae so vo ao δ" by (auto simp add:checker_r2_def Let_def if_splits)
  thus ?thesis using calculation by auto
qed

theorem checker_r_correctness:
  "(checker_r se ve ae so vo ao δ ⟷ check_precond_r se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
proof -
  have "checker_r se ve ae so vo ao δ ⟷ (checker_r se ve ae so vo ao δ ∧ δ ≤ - vo / ao) ∨ (checker_r se ve ae so vo ao δ ∧ δ > - vo / ao)" by auto
  also have "... ⟷ checker_r1 se ve ae so vo ao δ ∨ checker_r2 se ve ae so vo ao δ" using checker_eq_1 checker_eq_2 by auto
  also have "... ⟷ (check_precond_r1 se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})
      ∨ (check_precond_r2 se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
    using checker_r1_correctness checker_r2_correctness by auto
  also have "... ⟷ (δ ≤ - vo / ao ∧ check_precond_r se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})
      ∨ (δ > - vo / ao ∧ check_precond_r se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..})"
    by (auto simp add:check_precond_r_def check_precond_r1_def check_precond_r2_def)
  also have "... ⟷ check_precond_r se ve ae so vo ao δ ∧ safe_distance_normal.no_collision_react ae ve se ao vo so δ {0..}"
    by auto
  finally show ?thesis by auto
qed

end