[STATEMENT]
lemma (in Order) BNTr4_1:"\<lbrakk>f \<in> carrier D \<rightarrow> carrier D;  a \<in> carrier D; 
     b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> (f x); W1 \<in> WWa D f a; W2 \<in> WWa D f a;
     ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g\<rbrakk> \<Longrightarrow> 
     \<forall>x\<in>W1. g x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
[PROOF STEP]
apply (frule mem_wwa_Worder[of "W1" "f" "a"],
        frule mem_wwa_Worder[of "W2" "f" "a"],
        frule Worder.Order[of "Iod D W2"],
        frule mem_WWa_sub_carrier[of "W2" "f" "a"],
        frule mem_WWa_sub_carrier[of "W1" "f" "a"],
        cut_tac  Worder.segment_Worder[of "Iod D W2" "b"],
        simp add:Worder.Order)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (cut_tac Order.segment_sub[of "Iod D W2" "b"],
                   simp add:Iod_carrier,
         frule subset_trans[of "segment (Iod D W2) b" "W2" "carrier D"],
                   assumption+,
         frule Iod_Order[of "segment (Iod D W2) b"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule Worder.Order[of "Iod D W1"],
         frule Order.ord_isom_onto[of "Iod D W1" 
                      "Iod D (segment (Iod D W2) b)" "g"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` carrier (Iod D W1) = carrier (Iod D (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
(** transfinite induction **)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` carrier (Iod D W1) = carrier (Iod D (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule Order.ord_isom_minimum[of "Iod D W1" 
         "Iod D (segment (Iod D W2) b)" "g" "W1" "a"], assumption+,
         simp add:Iod_carrier, simp add:Iod_carrier mem_WWa_inc_a,
         simp add:BNTr3)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` carrier (Iod D W1) = carrier (Iod D (segment (Iod D W2) b)); minimum_elem (Iod D (segment (Iod D W2) b)) (g ` W1) (g a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule Order.ord_isom_onto[of "Iod D W1" 
                      "Iod D (segment (Iod D W2) b)" "g"], assumption+,
        simp add:Iod_carrier, frule Worder.Torder[of "Iod D W2"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; minimum_elem (Iod D (segment (Iod D W2) b)) (segment (Iod D W2) b) (g a); Torder (Iod D W2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:minimum_elem_sub[THEN sym, of "segment (Iod D W2) b" 
                           "segment (Iod D W2) b"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; minimum_elem D (segment (Iod D W2) b) (g a); Torder (Iod D W2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:minimum_elem_sub[of "W2" "segment (Iod D W2) b"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; minimum_elem (Iod D W2) (segment (Iod D W2) b) (g a); Torder (Iod D W2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule Torder.minimum_segment_of_sub[of "Iod D W2" "W2" "b" "g a"],
        simp add:Iod_carrier, cut_tac subset_self[of "W2"],
        simp add:Iod_sub_sub[of "W2" "W2"],
         thin_tac "minimum_elem (Iod D W2) (segment (Iod D W2) b) (g a)",
        frule BNTr3[of "f" "a" "W2"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 (g a); minimum_elem (Iod D W2) W2 a\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule Worder.Order[of "Iod D W2"],
        frule Order.minimum_elem_unique[of "Iod D W2" "W2" "g a" "a"],
         simp add:Iod_carrier, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod D (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 (g a); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:Iod_sub_sub[THEN sym, of "segment (Iod D W2) b" "W2"],
        frule Worder.transfinite_induction[of "Iod D W1" "a" "fixp g"],
        simp add:Iod_carrier, simp add:BNTr3, simp add:fixp_def,
        rule ballI, rule impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> carrier (Iod D W1); \<forall>u\<in>segment (Iod D W1) t. fixp g u\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = t in Worder_ord_isom_mem[of "Iod D W1" 
          "Iod (Iod D W2) (segment (Iod D W2) b)" "g"], assumption+,
        frule Iod_carrier[THEN sym, of "W2"],
        frule subset_trans[of "segment (Iod D W2) b" "W2" 
                        "carrier (Iod D W2)"], simp,
        thin_tac "W2 = carrier (Iod D W2)",
        simp add:Order.Iod_carrier[of "Iod D W2" "segment (Iod D W2) b"],
        frule_tac c = "g t" in subsetD[of "segment (Iod D W2) b" 
                                   "carrier (Iod D W2)"], assumption+,
        simp add:Iod_carrier)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (case_tac "t = a")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t = a\<rbrakk> \<Longrightarrow> fixp g t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:fixp_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (case_tac "ExPre (Iod D W1) t",
        frule_tac a = t in Worder.ord_isom_Pre1[of "Iod D W1" 
                  "Iod (Iod D W2) (segment (Iod D W2) b)" _ "g"], assumption+,
        simp add:Iod_carrier, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t)\<rbrakk> \<Longrightarrow> fixp g t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = t in Worder.ord_isom_Pre2[of "Iod D W1"
            "Iod (Iod D W2) (segment (Iod D W2) b)" _ "g"], assumption+,
       simp add:Iod_carrier, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t)\<rbrakk> \<Longrightarrow> fixp g t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = t in Order.Pre_in_segment[of "Iod D W1"],
        simp add:Iod_carrier, assumption)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); Pre (Iod D W1) t \<in> segment (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac x = "Pre (Iod D W1) t" in bspec, assumption,
        thin_tac "\<forall>u\<in>segment (Iod D W1) t. fixp g u")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); Pre (Iod D W1) t \<in> segment (Iod D W1) t; fixp g (Pre (Iod D W1) t)\<rbrakk> \<Longrightarrow> fixp g t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:fixp_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t; Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t) = Pre (Iod D W1) t\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = "g t" in Worder.Pre_segment[of "Iod D W2" _ "b"],
        simp add:Iod_carrier, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t; Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t) = Pre (Iod D W1) t; ExPre (Iod D W2) (g t) \<and> Pre (Iod D W2) (g t) = Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t)\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (rotate_tac -2, frule sym, thin_tac "Pre (Iod D W1) t =
         Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t)", simp,
        thin_tac "Pre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t) =
         Pre (Iod D W1) t")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>ExPre (Iod D W2) (g t) \<and> Pre (Iod D W2) (g t) = Pre (Iod D W1) t; f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t; ExPre (Iod D W2) (g t); Pre (Iod D W2) (g t) = Pre (Iod D W1) t\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:WWa_def Wa_def, (erule conjE)+,
        thin_tac "\<forall>x\<in>W1. a \<preceq> x", thin_tac "\<forall>x\<in>W2. a \<preceq> x",
        thin_tac "\<forall>x\<in>carrier D. x \<preceq> f x")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t; ExPre (Iod D W2) (g t); Pre (Iod D W2) (g t) = Pre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. if ExPre (Iod D W1) x then f (Pre (Iod D W1) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W1) x) = x else a = a; \<forall>x\<in>W2. if ExPre (Iod D W2) x then f (Pre (Iod D W2) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W2) x) = x else a = a\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac x = t in bspec, assumption+,
        thin_tac "\<forall>x\<in>W1.
            if ExPre (Iod D W1) x then f (Pre (Iod D W1) x) = x
            else if a \<noteq> x then Sup D (segment (Iod D W1) x) = x else a = a",
        frule_tac x = "g t" in bspec, assumption+,
        thin_tac "\<forall>x\<in>W2.
            if ExPre (Iod D W2) x then f (Pre (Iod D W2) x) = x
            else if a \<noteq> x then Sup D (segment (Iod D W2) x) = x else a = a")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; ExPre (Iod D W1) t; ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); g (Pre (Iod D W1) t) = Pre (Iod D W1) t; Pre (Iod D W1) t \<in> segment (Iod D W1) t; ExPre (Iod D W2) (g t); Pre (Iod D W2) (g t) = Pre (Iod D W1) t; a \<in> W1; a \<in> W2; if ExPre (Iod D W1) t then f (Pre (Iod D W1) t) = t else if a \<noteq> t then Algebra2.Sup D (segment (Iod D W1) t) = t else a = a; if ExPre (Iod D W2) (g t) then f (Pre (Iod D W2) (g t)) = g t else if a \<noteq> g t then Algebra2.Sup D (segment (Iod D W2) (g t)) = g t else a = a\<rbrakk> \<Longrightarrow> g t = t
 2. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 5. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = t in Worder.ord_isom_Pre11[of "Iod D W1"
                 "Iod (Iod D W2) (segment (Iod D W2) b)" _ "g"], assumption+,
        simp add:Iod_carrier, assumption, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t); \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac a = "g t" in Worder.segment_Expre[of "Iod D W2" _ "b"],
        assumption, simp,
        thin_tac "\<not> ExPre (Iod (Iod D W2) (segment (Iod D W2) b)) (g t)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:WWa_def Wa_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. a \<preceq> x; \<forall>x\<in>W1. if ExPre (Iod D W1) x then f (Pre (Iod D W1) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W1) x) = x else a = a; \<forall>x\<in>W2. a \<preceq> x; \<forall>x\<in>W2. if ExPre (Iod D W2) x then f (Pre (Iod D W2) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W2) x) = x else a = a\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (rotate_tac -3,
        frule_tac x = t in bspec, assumption,
        thin_tac "\<forall>x\<in>W1.
            if ExPre (Iod D W1) x then f (Pre (Iod D W1) x) = x
            else if a \<noteq> x then Sup D (segment (Iod D W1) x) = x else a = a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>\<forall>x\<in>W2. a \<preceq> x; \<forall>x\<in>W2. if ExPre (Iod D W2) x then f (Pre (Iod D W2) x) = x else if a \<noteq> x then Algebra2.Sup D (segment (Iod D W2) x) = x else a = a; f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. a \<preceq> x; if ExPre (Iod D W1) t then f (Pre (Iod D W1) t) = t else if a \<noteq> t then Algebra2.Sup D (segment (Iod D W1) t) = t else a = a\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (rotate_tac 1,
        frule_tac x = "g t" in bspec, assumption,
        thin_tac "\<forall>x\<in>W2.
            if ExPre (Iod D W2) x then f (Pre (Iod D W2) x) = x
            else if a \<noteq> x then Sup D (segment (Iod D W2) x) = x else a = a",
        simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; t \<noteq> a; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. a \<preceq> x; Algebra2.Sup D (segment (Iod D W1) t) = t; \<forall>x\<in>W2. a \<preceq> x; if a \<noteq> g t then Algebra2.Sup D (segment (Iod D W2) (g t)) = g t else a = a\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac t = t and s = a in not_sym, thin_tac " t \<noteq> a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. a \<preceq> x; Algebra2.Sup D (segment (Iod D W1) t) = t; \<forall>x\<in>W2. a \<preceq> x; if a \<noteq> g t then Algebra2.Sup D (segment (Iod D W2) (g t)) = g t else a = a; a \<noteq> t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac b = t in Order.ord_isom_inj[of "Iod D W1" 
                "Iod (Iod D W2) (segment (Iod D W2) b)" "g" "a"], assumption+,
                simp add:Iod_carrier, simp add:Iod_carrier, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; t \<in> W1; \<forall>u\<in>segment (Iod D W1) t. fixp g u; g t \<in> segment (Iod D W2) b; g t \<in> W2; \<not> ExPre (Iod D W2) (g t); \<not> ExPre (Iod D W1) t; a \<in> W1; a \<in> W2; \<forall>x\<in>W1. a \<preceq> x; Algebra2.Sup D (segment (Iod D W1) t) = t; \<forall>x\<in>W2. a \<preceq> x; Algebra2.Sup D (segment (Iod D W2) (g t)) = g t; a \<noteq> g t; a \<noteq> t\<rbrakk> \<Longrightarrow> fixp g t
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 4. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (frule_tac t1 = t in fixp_same[THEN sym, of "W1" "W2" _ "b" "g"], 
        assumption+, simp, simp add:fixp_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod (Iod D W2) (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b)); segment (Iod D W2) b \<subseteq> W2; segment (Iod D W2) b \<subseteq> carrier D; Order (Iod (Iod D W2) (segment (Iod D W2) b)); Order (Iod D W1); g ` W1 = segment (Iod D W2) b; Torder (Iod D W2); minimum_elem (Iod D W2) W2 a; Order (Iod D W2); g a = a; \<forall>x\<in>carrier (Iod D W1). fixp g x\<rbrakk> \<Longrightarrow> \<forall>x\<in>W1. g x = x
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 3. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (rule ballI,
        frule_tac x = x in bspec,
        simp add:subsetD[of "W1" "carrier D"], 
        simp add:Iod_carrier fixp_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D; Worder (Iod (Iod D W2) (segment (Iod D W2) b))\<rbrakk> \<Longrightarrow> Order (Iod D W2)
 2. \<lbrakk>f \<in> carrier D \<rightarrow> carrier D; a \<in> carrier D; b \<in> carrier D; \<forall>x\<in>carrier D. x \<preceq> f x; W1 \<in> WWa D f a; W2 \<in> WWa D f a; ord_isom (Iod D W1) (Iod D (segment (Iod D W2) b)) g; Worder (Iod D W1); Worder (Iod D W2); Order (Iod D W2); W2 \<subseteq> carrier D; W1 \<subseteq> carrier D\<rbrakk> \<Longrightarrow> Worder (Iod D W2)
[PROOF STEP]
apply (simp add:Worder.Order, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done