[STATEMENT]
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (\<alpha> m) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk> 
        c \<sigma>; 
        k \<in> it; 
        \<forall>j\<in>it. k\<le>j; 
        \<forall>j\<in>\<alpha> m - it. j\<le>k; 
        it \<subseteq> \<alpha> m; 
        I it \<sigma> 
      \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      assumes II: "!!\<sigma> it. \<lbrakk> 
        it \<subseteq> \<alpha> m; 
        it \<noteq> {}; 
        \<not> c \<sigma>; 
        I it \<sigma>; 
        \<forall>k\<in>it. \<forall>j\<in>\<alpha> m - it. j\<le>k 
      \<rbrakk> \<Longrightarrow> P \<sigma>"
      shows "P (iterateoi m c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iterateoi m c f \<sigma>0)
[PROOF STEP]
using set_iterator_linord_rule_P [OF iterateoi_rule, OF MINV, of I \<sigma>0 c f P,
       OF I0 _ IF] IP II
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> \<alpha> m; \<And>x'. x' \<in> \<alpha> m - S \<Longrightarrow> x' \<le> x; \<And>x'. x' \<in> S \<Longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> I (S - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> I {} \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> \<alpha> m; S \<noteq> {}; \<And>x x'. \<lbrakk>x \<in> S; x' \<in> \<alpha> m - S\<rbrakk> \<Longrightarrow> x' \<le> x; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iterateoi m c f \<sigma>0)
\<lbrakk>c ?\<sigma>1; ?k1 \<in> ?it1; \<forall>j\<in>?it1. ?k1 \<le> j; \<forall>j\<in>\<alpha> m - ?it1. j \<le> ?k1; ?it1 \<subseteq> \<alpha> m; I ?it1 ?\<sigma>1\<rbrakk> \<Longrightarrow> I (?it1 - {?k1}) (f ?k1 ?\<sigma>1)
\<lbrakk>?it1 \<subseteq> \<alpha> m; ?it1 \<noteq> {}; \<not> c ?\<sigma>1; I ?it1 ?\<sigma>1; \<forall>k\<in>?it1. \<forall>j\<in>\<alpha> m - ?it1. j \<le> k\<rbrakk> \<Longrightarrow> P ?\<sigma>1

goal (1 subgoal):
 1. P (iterateoi m c f \<sigma>0)
[PROOF STEP]
by simp