theory Prefix_Refinement

lemma prefix_refinement_repeat:
  "prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>AR\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>
    \<Longrightarrow> \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat f) (repeat g)" apply (simp add: repeat_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind, rule prefix_refinement_select[where rvr="(=)"]) apply simp apply simp apply (rule prefix_refinement_repeat_n, assumption+) apply (rule rg_weaken_pre, assumption, simp) apply wp apply wp apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (repeat f) (repeat g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R (do n <- select UNIV;
repeat_n n f
od) (do n <- select UNIV;
repeat_n n g
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) ?P' ?Q' AR R (do n <- select UNIV;
repeat_n n f
od) (do n <- select UNIV;
repeat_n n g
od)
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ?P' s0 s
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ?Q' t0 t proof (prove)
goal (6 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>UNIV. \<exists>y\<in>UNIV. y = x
 2. \<And>x y. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>; x = y\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R (repeat_n x f) (repeat_n y g)
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> select UNIV -, \<lbrace>?P''4\<rbrace>
 4. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>?Q''4\<rbrace>
 5. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 6. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>; x = y\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R (repeat_n x f) (repeat_n y g)
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> select UNIV -, \<lbrace>?P''4\<rbrace>
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>?Q''4\<rbrace>
 4. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>; x = y\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 y) (?Q''4 y) AR R (repeat_n y f) (repeat_n y g)
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> select UNIV -, \<lbrace>?P''4\<rbrace>
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>?Q''4\<rbrace>
 4. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>; x = y\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> select UNIV -, \<lbrace>\<lambda>y. P\<rbrace>
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>y. Q\<rbrace>
 4. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> select UNIV -, \<lbrace>\<lambda>y. P\<rbrace>
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>y. Q\<rbrace>
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 4. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>y. Q\<rbrace>
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>UNIV. P s0 s)) s0 s
 3. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>UNIV. P s0 s)) s0 s
 2. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>UNIV. Q s0 s)) t0 t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr iosr iosr (\<lambda>_ _. True) P Q AR R f g; \<lbrace>P\<rbrace>, \<lbrace>AR\<rbrace> f -, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>\<lambda>t0 t. Q t0 t \<and> (\<exists>s0. sr s0 t0) \<and> (\<exists>s. iosr s t)\<rbrace>, \<lbrace>R\<rbrace> g -, \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>UNIV. Q s0 s)) t0 t proof (prove)
goal:
No subgoals!