theory Nondet_While_Loop_Rules

lemma whileLoopE_liftE:
  "whileLoopE C (\<lambda>r. liftE (B r)) r = liftE (whileLoop C B r)" apply (rule ext) apply (clarsimp simp: whileLoopE_def) apply (rule prod_eqI) apply (rule set_eqI, rule iffI) apply clarsimp apply (clarsimp simp: in_liftE whileLoop_def)
    \<comment> \<open>The schematic existential is instantiated by @{text "subst isr_Inr_projr ... rule refl"} in two lines\<close> apply (rule exI) apply (rule conjI) apply (subst isr_Inr_projr) prefer 2 apply (rule refl) apply (drule whileLoop_results_induct_lemma2[where P="\<lambda>(r, s). \<not> isl r"]) apply (rule refl) apply (rule refl) apply clarsimp apply (clarsimp simp: return_def bind_def lift_def liftE_def split: sum.splits) apply clarsimp apply (erule whileLoop_results_bisim[where rt=projr
                                           and st="\<lambda>x. x"
                                           and I="\<lambda>r s. \<not> isl r"],
           auto intro: whileLoop_results.intros simp: bind_def return_def lift_def liftE_def split: sum.splits)[1] apply (clarsimp simp: in_liftE whileLoop_def) apply (erule whileLoop_results_bisim[where rt=Inr and st="\<lambda>x. x" and I="\<lambda>r s. True"],
          auto intro: whileLoop_results.intros intro!: bexI
               simp: bind_def return_def lift_def liftE_def split: sum.splits)[1] apply (rule iffI) apply (clarsimp simp: whileLoop_def liftE_def del: notI) apply (erule disjE) apply (erule whileLoop_results_bisim[where rt=projr
                                           and st="\<lambda>x. x"
                                           and I="\<lambda>r s. \<not> isl r"],
           auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1] apply (subst (asm) whileLoop_terminates_liftE [symmetric]) apply (fastforce simp: whileLoop_def liftE_def whileLoop_terminatesE_def) apply (clarsimp simp: whileLoop_def liftE_def del: notI) apply (subst (asm) whileLoop_terminates_liftE [symmetric]) apply (clarsimp simp: whileLoop_def liftE_def whileLoop_terminatesE_def) apply (erule disjE) apply (erule whileLoop_results_bisim [where rt=Inr and st="\<lambda>x. x" and I="\<lambda>r s. True"]) apply (clarsimp split: option.splits) apply (clarsimp split: option.splits) apply (clarsimp split: option.splits) apply (auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def
                  split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoopE C
  (\<lambda>r. liftE (B r)) r = liftE (whileLoop C
  B r) proof (prove)
goal (1 subgoal):
 1. \<And>x. whileLoopE C
  (\<lambda>r. liftE (B r)) r x = liftE (whileLoop C
  B r) x proof (prove)
goal (1 subgoal):
 1. \<And>x. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x = liftE (whileLoop C
  B r) x proof (prove)
goal (2 subgoals):
 1. \<And>x. fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = fst (liftE (whileLoop C
  B r) x)
 2. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) \<Longrightarrow> xa \<in> fst (liftE (whileLoop C
  B r) x)
 2. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 3. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. (a, b) \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) \<Longrightarrow> (a, b) \<in> fst (liftE (whileLoop C
  B r) x)
 2. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 3. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> \<exists>v'. a = Inr v' \<and> (Some (r, x), Some (v', b)) \<in> whileLoop_results C B
 2. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 3. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> a = Inr (?v'19 x a b) \<and> (Some (r, x), Some (?v'19 x a b, b)) \<in> whileLoop_results C B
 2. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 3. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (4 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> a = Inr (?v'19 x a b)
 2. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (?v'19 x a b, b)) \<in> whileLoop_results C B
 3. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 4. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (5 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> \<not> isl a
 2. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> ?v'25 x a b (?x25 x a b) a (?b25 x a b) = projr a
 3. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (?v'25 x a b (?x25 x a b) a (?b25 x a b), b)) \<in> whileLoop_results C B
 4. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 5. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (5 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> ?v'25 x a b (?x25 x a b) a (?b25 x a b) = projr a
 2. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> \<not> isl a
 3. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (?v'25 x a b (?x25 x a b) a (?b25 x a b), b)) \<in> whileLoop_results C B
 4. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 5. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (4 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> \<not> isl a
 2. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 3. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 4. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (8 subgoals):
 1. \<And>x a b. Some (Inr r, x) = Some (?x28 x a b)
 2. \<And>x a b. Some (a, b) = Some (?y28 x a b)
 3. \<And>x a b. case ?x28 x a b of (r, s) \<Rightarrow> \<not> isl r
 4. \<And>x a b s t. \<lbrakk>case s of (r, s) \<Rightarrow> \<not> isl r; t \<in> fst (lift (\<lambda>r. liftE (B r)) (fst s) (snd s)); case fst s of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v (snd s)\<rbrakk> \<Longrightarrow> case t of (r, s) \<Rightarrow> \<not> isl r
 5. \<And>x a b. case ?y28 x a b of (r, s) \<Rightarrow> \<not> isl r \<Longrightarrow> \<not> isl a
 6. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 7. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 8. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (7 subgoals):
 1. \<And>x a b. Some (a, b) = Some (?y28 x a b)
 2. \<And>x a b. case (Inr r, x) of (r, s) \<Rightarrow> \<not> isl r
 3. \<And>x a b s t. \<lbrakk>case s of (r, s) \<Rightarrow> \<not> isl r; t \<in> fst (lift (\<lambda>r. liftE (B r)) (fst s) (snd s)); case fst s of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v (snd s)\<rbrakk> \<Longrightarrow> case t of (r, s) \<Rightarrow> \<not> isl r
 4. \<And>x a b. case ?y28 x a b of (r, s) \<Rightarrow> \<not> isl r \<Longrightarrow> \<not> isl a
 5. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 6. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 7. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (6 subgoals):
 1. \<And>x a b. case (Inr r, x) of (r, s) \<Rightarrow> \<not> isl r
 2. \<And>x a b s t. \<lbrakk>case s of (r, s) \<Rightarrow> \<not> isl r; t \<in> fst (lift (\<lambda>r. liftE (B r)) (fst s) (snd s)); case fst s of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v (snd s)\<rbrakk> \<Longrightarrow> case t of (r, s) \<Rightarrow> \<not> isl r
 3. \<And>x a b. case (a, b) of (r, s) \<Rightarrow> \<not> isl r \<Longrightarrow> \<not> isl a
 4. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 5. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 6. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (5 subgoals):
 1. \<And>x a b s t. \<lbrakk>case s of (r, s) \<Rightarrow> \<not> isl r; t \<in> fst (lift (\<lambda>r. liftE (B r)) (fst s) (snd s)); case fst s of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v (snd s)\<rbrakk> \<Longrightarrow> case t of (r, s) \<Rightarrow> \<not> isl r
 2. \<And>x a b. case (a, b) of (r, s) \<Rightarrow> \<not> isl r \<Longrightarrow> \<not> isl a
 3. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 4. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 5. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (4 subgoals):
 1. \<And>x a b. case (a, b) of (r, s) \<Rightarrow> \<not> isl r \<Longrightarrow> \<not> isl a
 2. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 3. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 4. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. (Some (Inr r, x), Some (a, b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) \<Longrightarrow> (Some (r, x), Some (projr a, b)) \<in> whileLoop_results C B
 2. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 3. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> fst (liftE (whileLoop C
  B r) x) \<Longrightarrow> xa \<in> fst (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x)
 2. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x b v'. (Some (r, x), Some (v', b)) \<in> whileLoop_results C B \<Longrightarrow> (Some (Inr r, x), Some (Inr v', b)) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r)))
 2. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) = snd (liftE (whileLoop C
  B r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) \<Longrightarrow> snd (liftE (whileLoop C
  B r) x)
 2. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) \<or> \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; whileLoop_terminates C B r x\<rbrakk> \<Longrightarrow> (Some (r, x), None) \<in> whileLoop_results C B
 2. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>whileLoop_terminates C B r x; (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))\<rbrakk> \<Longrightarrow> (Some (r, x), None) \<in> whileLoop_results C B
 2. \<And>x. \<lbrakk>whileLoop_terminates C B r x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (r, x), None) \<in> whileLoop_results C B
 3. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>whileLoop_terminates C B r x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (r, x), None) \<in> whileLoop_results C B
 2. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (r, x), None) \<in> whileLoop_results C B
 2. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. snd (liftE (whileLoop C
  B r) x) \<Longrightarrow> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift (\<lambda>r. liftE (B r))) (Inr r) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(Some (r, x), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B r x; whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(Some (r, x), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r x; whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(Some (r, x), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; (Some (r, x), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))
 2. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (8 subgoals):
 1. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> Some (Inr r, x) = (case Some (r, x) of None \<Rightarrow> None | Some (r, s) \<Rightarrow> Some (Inr r, s))
 2. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> None = (case None of None \<Rightarrow> None | Some (r, s) \<Rightarrow> Some (Inr r, s))
 3. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> case Some (r, x) of None \<Rightarrow> True | Some (r, s) \<Rightarrow> True
 4. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> True
 5. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True\<rbrakk> \<Longrightarrow> C ra s = (case Inr ra of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
 6. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; C ra s; snd (B ra s); True\<rbrakk> \<Longrightarrow> (Some (Inr ra, s), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))
 7. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> (Inr r', s') \<in> fst (lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr ra) s)
 8. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (7 subgoals):
 1. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> None = (case None of None \<Rightarrow> None | Some (r, s) \<Rightarrow> Some (Inr r, s))
 2. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> case Some (r, x) of None \<Rightarrow> True | Some (r, s) \<Rightarrow> True
 3. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> True
 4. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True\<rbrakk> \<Longrightarrow> C ra s = (case Inr ra of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
 5. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; C ra s; snd (B ra s); True\<rbrakk> \<Longrightarrow> (Some (Inr ra, s), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))
 6. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> (Inr r', s') \<in> fst (lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr ra) s)
 7. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (6 subgoals):
 1. \<And>x. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x \<Longrightarrow> case Some (r, x) of None \<Rightarrow> True | Some (r, s) \<Rightarrow> True
 2. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> True
 3. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True\<rbrakk> \<Longrightarrow> C ra s = (case Inr ra of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
 4. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; C ra s; snd (B ra s); True\<rbrakk> \<Longrightarrow> (Some (Inr ra, s), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))
 5. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> (Inr r', s') \<in> fst (lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr ra) s)
 6. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> True
 2. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True\<rbrakk> \<Longrightarrow> C ra s = (case Inr ra of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
 3. \<And>x ra s. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; C ra s; snd (B ra s); True\<rbrakk> \<Longrightarrow> (Some (Inr ra, s), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od))
 4. \<And>x ra s r' s'. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; True; C ra s; (r', s') \<in> fst (B ra s)\<rbrakk> \<Longrightarrow> (Inr r', s') \<in> fst (lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr ra) s)
 5. \<And>x. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x; \<not> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr r) x\<rbrakk> \<Longrightarrow> (Some (Inr r, x), None) \<in> whileLoop_results (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. do r <- B r;
return (Inr r)
od)) proof (prove)
goal:
No subgoals!