[STATEMENT]
lemma count_it_ex:   
  assumes "\<pi>: (WHILE b DO c,s) \<Rightarrow> t"
  shows "\<exists>n. count_it \<pi> b c s n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. count_it \<pi> b c s n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi>: (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. \<exists>n. count_it \<pi> b c s n
[PROOF STEP]
apply (induction \<pi> "WHILE b DO c" s t arbitrary: b c)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s \<pi> c. \<not> bval b s \<Longrightarrow> Ex (count_it \<pi> b c s)
 2. \<And>b s\<^sub>1 \<pi> c s\<^sub>2 s\<^sub>3. \<lbrakk>bval b s\<^sub>1; \<pi>: (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>b ca. c = WHILE b DO ca \<Longrightarrow> \<exists>a. count_it \<pi> b ca s\<^sub>1 a; \<pi>: (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; Ex (count_it \<pi> b c s\<^sub>2)\<rbrakk> \<Longrightarrow> Ex (count_it \<pi> b c s\<^sub>1)
[PROOF STEP]
apply (auto intro: count_it.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done