theory Nondet_While_Loop_Rules_Completeness

lemma not_snd_whileLoop_complete:
  shows "(\<not> snd (whileLoop C B r s)) = (\<exists>I R . I r s \<and> wf R \<and>
           (\<forall>r s r' s'. (I r s \<and> C r s \<and> (r', s') \<in> fst (B r s)) \<longrightarrow> I r' s')
           \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s))
           \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), (r, s)) \<in> R))"
   (is "?LHS = ?RHS") proof (rule iffI) assume "?RHS" thus "?LHS" apply (clarsimp) apply (erule make_pos_goal, rule not_snd_whileLoop) apply assumption defer apply assumption apply (clarsimp simp: validNF_def no_fail_def valid_def) done next assume no_fail: "?LHS" define I where "I \<equiv> \<lambda>r s. \<not> snd (whileLoop C B r s)" define R where "R \<equiv> {((r', s'), (r, s)). C r s \<and> (r', s') \<in> fst (B r s) \<and>
                                            whileLoop_terminates C B r s}" have "I r s" by (clarsimp simp: I_def no_fail) moreover have "wf R" apply (rule wf_subset [OF whileLoop_terminates_wf [where C=C and B=B]]) apply (clarsimp simp: R_def) done moreover have "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'" apply (clarsimp simp: I_def whileLoop_def) apply (rule conjI) apply (metis whileLoop_results_simps) apply (erule whileLoop_terminates_cases) apply clarsimp apply fastforce done moreover have "\<And>r s. \<lbrakk> I r s; C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)" apply (clarsimp simp: I_def) apply (subst (asm) whileLoop_unroll) apply (clarsimp simp: condition_true bind_def) done moreover have "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> ((r', s'), (r, s)) \<in> R" apply (clarsimp simp: R_def) apply (metis I_def snd_conv whileLoop_def) done ultimately show ?RHS by (metis (mono_tags)) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> snd (whileLoop C
  B r s)) = (\<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)) proof (state)
goal (2 subgoals):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)
 2. \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) \<Longrightarrow> \<not> snd (whileLoop C
  B r s) proof (state)
this:
\<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)

goal (2 subgoals):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)
 2. \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) \<Longrightarrow> \<not> snd (whileLoop C
  B r s) proof (prove)
using this:
\<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<And>I R. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>I R. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> ?I12 I R r s
 2. \<And>I R ra sa. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. ?I12 I R ra s' \<and> C ra s' \<and> s' = sa\<rbrace> B ra \<lbrace>\<lambda>r' s'. ?I12 I R r' s' \<and> ((r', s'), ra, sa) \<in> ?R12 I R\<rbrace>!
 3. \<And>I R. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> wf (?R12 I R) proof (prove)
goal (2 subgoals):
 1. \<And>I R ra sa. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. I ra s' \<and> C ra s' \<and> s' = sa\<rbrace> B ra \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ra, sa) \<in> ?R12 I R\<rbrace>!
 2. \<And>I R. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> wf (?R12 I R) proof (prove)
goal (2 subgoals):
 1. \<And>I R. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> wf (?R12 I R)
 2. \<And>I R ra sa. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. I ra s' \<and> C ra s' \<and> s' = sa\<rbrace> B ra \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ra, sa) \<in> ?R12 I R\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>I R ra sa. \<lbrakk>I r s; wf R; \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s'; \<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s); \<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. I ra s' \<and> C ra s' \<and> s' = sa\<rbrace> B ra \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ra, sa) \<in> R\<rbrace>! proof (prove)
goal:
No subgoals! proof (state)
this:
\<not> snd (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
\<not> snd (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
I \<equiv> \<lambda>r s. \<not> snd (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
R \<equiv> {((r', s'), r, s). C r s \<and> (r', s') \<in> fst (B r s) \<and> whileLoop_terminates C B r s}

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (prove)
goal (1 subgoal):
 1. I r s proof (state)
this:
I r s

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
I r s

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (prove)
goal (1 subgoal):
 1. wf R proof (prove)
goal (1 subgoal):
 1. R \<subseteq> {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)} proof (prove)
goal:
No subgoals! proof (state)
this:
wf R

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
wf R

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>I r s; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> I r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> (Some (r', s'), None) \<notin> whileLoop_results C B \<and> whileLoop_terminates C B r' s' proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> (Some (r', s'), None) \<notin> whileLoop_results C B
 2. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s' proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; \<not> C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s'
 2. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; C r s; \<forall>(x, y)\<in>fst (B r s). whileLoop_terminates C B x y\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; C r s; \<forall>(x, y)\<in>fst (B r s). whileLoop_terminates C B x y\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s' proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> I ?r' ?s'

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> I ?r' ?s'

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; C r s\<rbrakk> \<Longrightarrow> \<not> snd (B r s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<not> snd (whileLoop C
  B r s); C r s; snd (B r s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<not> snd (condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) s); C r s; snd (B r s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<not> snd (B ?r ?s)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<not> snd (B ?r ?s)

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>I r s; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> ((r', s'), r, s) \<in> R proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>I r s; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> ((?r', ?s'), ?r, ?s) \<in> R

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (chain)
picking this:
I r s
wf R
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> I ?r' ?s'
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<not> snd (B ?r ?s)
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> ((?r', ?s'), ?r, ?s) \<in> R proof (prove)
using this:
I r s
wf R
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> I ?r' ?s'
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<not> snd (B ?r ?s)
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> ((?r', ?s'), ?r, ?s) \<in> R

goal (1 subgoal):
 1. \<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R) proof (state)
this:
\<exists>I R. I r s \<and> wf R \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> I r' s') \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s)) \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), r, s) \<in> R)

goal:
No subgoals!