[STATEMENT]
lemma diff_solve_axiom2: 
  fixes c::"'a::{heine_borel, banach}"
  shows "wp (x\<acute>=(\<lambda>s. c) & G) \<lceil>Q\<rceil> = 
  \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp x\<acute>=\<lambda>t s. c & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 \<lceil>Q\<rceil> = \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>
[PROOF STEP]
apply(subst local_flow.wp_g_ode_subset[where \<phi>="(\<lambda>t s. s + t *\<^sub>R c)" and T=UNIV])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. local_flow (\<lambda>s. c) UNIV UNIV (\<lambda>t s. s + t *\<^sub>R c)
 2. \<And>s. s \<in> UNIV \<Longrightarrow> 0 \<in> Collect ((\<le>) 0) \<and> is_interval (Collect ((\<le>) 0)) \<and> Collect ((\<le>) 0) \<subseteq> UNIV
 3. \<lceil>\<lambda>s. s \<in> UNIV \<longrightarrow> (\<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c))\<rceil> = \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>
[PROOF STEP]
by (rule line_is_local_flow, auto)