[STATEMENT]
lemma betw_total_order_on_path:
  fixes a b :: 'a
    and Q :: "'a set"
  assumes "Q \<in> \<P>"
      and "a \<in> Q"
      and "b \<in> Q"
      and "a \<noteq> b"
  shows "total_order (betw_gorder a b Q)" (is "total_order ?o")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total_order (betw_gorder a b Q)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> x
 2. \<And>x y. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> y .=\<^bsub>betw_gorder a b Q\<^esub> x
 3. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
 4. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 5. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 6. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 7. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 8. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 9. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x. x \<in> carrier ?o \<Longrightarrow> x .=\<^bsub>?o\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> ?x .=\<^bsub>betw_gorder a b Q\<^esub> ?x

goal (8 subgoals):
 1. \<And>x y. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> y .=\<^bsub>betw_gorder a b Q\<^esub> x
 2. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
 3. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 4. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 5. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 6. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 7. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 8. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> y .=\<^bsub>betw_gorder a b Q\<^esub> x
 2. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
 3. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 4. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 5. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 6. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 7. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 8. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y. \<lbrakk>x .=\<^bsub>?o\<^esub> y; x \<in> carrier ?o; y \<in> carrier ?o\<rbrakk> \<Longrightarrow> y .=\<^bsub>?o\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> y .=\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x .=\<^bsub>betw_gorder a b Q\<^esub> ?y; ?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> ?y .=\<^bsub>betw_gorder a b Q\<^esub> ?x

goal (7 subgoals):
 1. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
 2. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 3. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 4. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 5. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 6. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 7. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
 2. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 3. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 4. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 5. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 6. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 7. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y z. \<lbrakk>x .=\<^bsub>?o\<^esub> y; y .=\<^bsub>?o\<^esub> z; x \<in> carrier ?o;
                 y \<in> carrier ?o; z \<in> carrier ?o\<rbrakk>
        \<Longrightarrow> x .=\<^bsub>?o\<^esub> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; y .=\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x .=\<^bsub>betw_gorder a b Q\<^esub> ?y; ?y .=\<^bsub>betw_gorder a b Q\<^esub> ?z; ?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q); ?z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> ?x .=\<^bsub>betw_gorder a b Q\<^esub> ?z

goal (6 subgoals):
 1. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 2. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 3. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 4. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 5. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 6. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
 2. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 3. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 4. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 5. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 6. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x. x \<in> carrier ?o \<Longrightarrow> x \<sqsubseteq>\<^bsub>?o\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> carrier (betw_gorder a b Q) \<Longrightarrow> ?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?x

goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 2. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 3. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 4. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 5. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
 2. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 3. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 4. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 5. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>?o\<^esub> y; y \<sqsubseteq>\<^bsub>?o\<^esub> x; x \<in> carrier ?o; y \<in> carrier ?o\<rbrakk> \<Longrightarrow> x .=\<^bsub>?o\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x .=\<^bsub>betw_gorder a b Q\<^esub> y
[PROOF STEP]
by (smt abc_abc_neq abcd_dcba_only(18) betw4_sym betw4_weak eq_object.select_convs(1)
      gorder.select_convs(1))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?y; ?y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?x; ?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> ?x .=\<^bsub>betw_gorder a b Q\<^esub> ?y

goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 2. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 3. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 4. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
 2. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 3. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 4. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y z.
       \<lbrakk>x \<sqsubseteq>\<^bsub>?o\<^esub> y; y \<sqsubseteq>\<^bsub>?o\<^esub> z; x \<in> carrier ?o;
        y \<in> carrier ?o; z \<in> carrier ?o\<rbrakk>
       \<Longrightarrow> x \<sqsubseteq>\<^bsub>?o\<^esub> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y; y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z
[PROOF STEP]
by (smt (z3) abc_acd_abd abc_acd_bcd abc_bcd_acd abc_only_cba(1,4) assms(1)
      gorder.select_convs(1) partial_object.select_convs(1) some_betw2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?y; ?y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?z; ?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q); ?z \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> ?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?z

goal (3 subgoals):
 1. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 2. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 3. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
 2. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 3. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y z w.
       \<lbrakk>x .=\<^bsub>?o\<^esub> y; z .=\<^bsub>?o\<^esub> w; x \<in> carrier ?o;
        y \<in> carrier ?o; z \<in> carrier ?o; w \<in> carrier ?o\<rbrakk>
       \<Longrightarrow> (x \<sqsubseteq>\<^bsub>?o\<^esub> z) = (y \<sqsubseteq>\<^bsub>?o\<^esub> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z w. \<lbrakk>x .=\<^bsub>betw_gorder a b Q\<^esub> y; z .=\<^bsub>betw_gorder a b Q\<^esub> w; x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q); z \<in> carrier (betw_gorder a b Q); w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> z) = (y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x .=\<^bsub>betw_gorder a b Q\<^esub> ?y; ?z .=\<^bsub>betw_gorder a b Q\<^esub> ?w; ?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q); ?z \<in> carrier (betw_gorder a b Q); ?w \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> (?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?z) = (?y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?w)

goal (2 subgoals):
 1. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 2. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
 2. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "(.=\<^bsub>?o\<^esub>) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(.=\<^bsub>betw_gorder a b Q\<^esub>) = (=)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
show "\<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk>
           \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier (betw_gorder a b Q); y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> y \<or> y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> x
[PROOF STEP]
by (smt (z3) abc_sym assms gorder.select_convs(1) partial_object.select_convs(1)
      some_betw2 some_betw4b)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> carrier (betw_gorder a b Q); ?y \<in> carrier (betw_gorder a b Q)\<rbrakk> \<Longrightarrow> ?x \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?y \<or> ?y \<sqsubseteq>\<^bsub>betw_gorder a b Q\<^esub> ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relpow_impl_main:
  "set_of (relpow_i new have n) =
    {b | a b m. a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union>
    set_of have"
  (is "?l new have n = ?r new have n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (relpow_i new have n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
[PROOF STEP]
proof (induction n arbitrary: "have" new)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>have new. set_of (relpow_i new have 0) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> 0 \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
 2. \<And>n have new. (\<And>have new. set_of (relpow_i new have n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have) \<Longrightarrow> set_of (relpow_i new have (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
[PROOF STEP]
case (Suc n hhave nnew)
[PROOF STATE]
proof (state)
this:
set_of (relpow_i ?new ?have n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set ?new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of ?have}) ^^ m} \<union> set_of ?have

goal (2 subgoals):
 1. \<And>have new. set_of (relpow_i new have 0) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> 0 \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
 2. \<And>n have new. (\<And>have new. set_of (relpow_i new have n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have) \<Longrightarrow> set_of (relpow_i new have (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
proof (cases "nnew = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nnew = [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
 2. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
nnew = []

goal (2 subgoals):
 1. nnew = [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
 2. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nnew = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nnew = []

goal (1 subgoal):
 1. set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
nnew \<noteq> []

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?have = "set_of hhave"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?new = "set nnew"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
obtain "have" new where hav: "have = ?have" and new: "new = ?new"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>have new. \<lbrakk>have = set_of hhave; new = set nnew\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
have = set_of hhave
new = set nnew

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?reln = "\<lambda> m. (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^  m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?rel = "\<lambda> m. (rel \<inter> {(a, b). b \<notin> have}) ^^  m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
have idl: "?l nnew hhave (Suc n) =
      {uu. \<exists>a. (\<exists>aa\<in> new. (aa,a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m \<le> n. (a, uu) \<in> ?reln m)} \<union>
      (new \<union> have)"
      (is "_ = ?l1 \<union> (?l2 \<union> ?l3)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (relpow_i nnew hhave (Suc n)) = {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
by (simp add: hav new False Let_def Suc, simp add: memb un succ)
[PROOF STATE]
proof (state)
this:
set_of (relpow_i nnew hhave (Suc n)) = {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?l = "?l1 \<union> (?l2 \<union> ?l3)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
have idr: "?r nnew hhave (Suc n) = {b. \<exists> a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> ?rel m} \<union> have"
      (is "_ = (?r1 \<union> ?r2)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave = {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
by (simp add: hav new)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave = {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
let ?r = "?r1 \<union> ?r2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
assume b: "b \<in> ?l"
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
have "b \<in> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
proof (cases "b \<in> new \<or> b \<in> have")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<in> new \<or> b \<in> have \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
 2. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b \<in> new \<or> b \<in> have

goal (2 subgoals):
 1. b \<in> new \<or> b \<in> have \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
 2. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> new \<or> b \<in> have
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> new \<or> b \<in> have

goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
 2. b \<in> have \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
assume "b \<in> have"
[PROOF STATE]
proof (state)
this:
b \<in> have

goal (2 subgoals):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
 2. b \<in> have \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> have
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> have

goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
assume b: "b \<in> new"
[PROOF STATE]
proof (state)
this:
b \<in> new

goal (1 subgoal):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
have "b \<in> ?r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
by (intro CollectI, rule exI, rule exI [of _ 0], intro conjI, rule b, auto)
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. b \<in> new \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (b \<in> new \<or> b \<in> have)

goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
\<not> (b \<in> new \<or> b \<in> have)
[PROOF STEP]
have "b \<in> ?l1"
[PROOF STATE]
proof (prove)
using this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
\<not> (b \<in> new \<or> b \<in> have)

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)}

goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)}
[PROOF STEP]
obtain a2 a1 m where a2n: "a2 \<notin> new" and a2h: "a2 \<notin> have" and a1: "a1 \<in> new"
          and a1a2: "(a1,a2) \<in> rel" and m: "m \<le> n" and a2b: "(a2,b) \<in> ?reln m"
[PROOF STATE]
proof (prove)
using this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)}

goal (1 subgoal):
 1. (\<And>a2 a1 m. \<lbrakk>a2 \<notin> new; a2 \<notin> have; a1 \<in> new; (a1, a2) \<in> rel; m \<le> n; (a2, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a2 \<notin> new
a2 \<notin> have
a1 \<in> new
(a1, a2) \<in> rel
m \<le> n
(a2, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m

goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
have "b \<in> ?r1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
by (rule CollectI, rule exI, rule exI [of _ "Suc m"], intro conjI, rule a1, simp add: m, rule relpow_Suc_I2, rule, rule a1a2, simp add: a2h, insert a2b, induct m arbitrary: a2 b, auto)
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. \<not> (b \<in> new \<or> b \<in> have) \<Longrightarrow> b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
assume b: "b \<in> ?r"
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
have "b \<in> ?l"
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
proof (cases "b \<in> have")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<in> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
 2. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b \<in> have

goal (2 subgoals):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<in> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
 2. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> have
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> have

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<notin> have

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
b \<notin> have
[PROOF STEP]
have "b \<in> ?r1"
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
b \<notin> have

goal (1 subgoal):
 1. b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}
[PROOF STEP]
obtain a m where a: "a \<in> new" and m: "m \<le> Suc n" and ab: "(a, b) \<in> ?rel m"
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m}

goal (1 subgoal):
 1. (\<And>a m. \<lbrakk>a \<in> new; m \<le> Suc n; (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> new
m \<le> Suc n
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have seq: "\<exists> a \<in> new. (a, b) \<in> ?rel m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m
[PROOF STEP]
using a  ab
[PROOF STATE]
proof (prove)
using this:
a \<in> new
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m

goal (1 subgoal):
 1. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
obtain l where l: "l = (LEAST m. (\<exists> a \<in> new. (a, b) \<in> ?rel m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. l = (LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = (LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m)

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have least: "(\<exists> a \<in> new. (a, b) \<in> ?rel l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l
[PROOF STEP]
by (unfold l, rule LeastI, rule seq)
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have lm: "l \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> m
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) \<le> m
[PROOF STEP]
by (rule Least_le, rule seq)
[PROOF STATE]
proof (state)
this:
l \<le> m

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
m \<le> Suc n
l \<le> m
[PROOF STEP]
have ln: "l \<le> Suc n"
[PROOF STATE]
proof (prove)
using this:
m \<le> Suc n
l \<le> m

goal (1 subgoal):
 1. l \<le> Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<le> Suc n

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
from least
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l
[PROOF STEP]
obtain a where a: "a \<in> new"
          and ab: "(a, b) \<in> ?rel l"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> new; (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> new
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ l

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
from ab [unfolded relpow_fun_conv]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. f 0 = a \<and> f l = b \<and> (\<forall>i<l. (f i, f (Suc i)) \<in> rel \<inter> {(a, b). b \<notin> have})
[PROOF STEP]
obtain f where fa: "f 0 = a" and fb: "b = f l"
          and steps: "\<And> i. i < l \<Longrightarrow> (f i, f (Suc i)) \<in> ?rel 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. f 0 = a \<and> f l = b \<and> (\<forall>i<l. (f i, f (Suc i)) \<in> rel \<inter> {(a, b). b \<notin> have})

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = a; b = f l; \<And>i. i < l \<Longrightarrow> (f i, f (Suc i)) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = a
b = f l
?i < l \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f 0 = a
b = f l
?i < l \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
assume i: "i < l"
[PROOF STATE]
proof (state)
this:
i < l

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have main: "f (Suc i) \<notin> new"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc i) \<notin> new
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
assume new: "f (Suc i) \<in> new"
[PROOF STATE]
proof (state)
this:
f (Suc i) \<in> new

goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
let ?f = "\<lambda> j. f (Suc i + j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
have seq: "(f (Suc i), b) \<in> ?rel (l - Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f (Suc i), b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)
[PROOF STEP]
unfolding relpow_fun_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fa. fa 0 = f (Suc i) \<and> fa (l - Suc i) = b \<and> (\<forall>ia<l - Suc i. (fa ia, fa (Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have})
[PROOF STEP]
proof (rule exI[of _ ?f], intro conjI allI impI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. f (Suc i + (l - Suc i)) = b
 3. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < l
[PROOF STEP]
show "f (Suc i + (l - Suc i)) = b"
[PROOF STATE]
proof (prove)
using this:
i < l

goal (1 subgoal):
 1. f (Suc i + (l - Suc i)) = b
[PROOF STEP]
unfolding fb
[PROOF STATE]
proof (prove)
using this:
i < l

goal (1 subgoal):
 1. f (Suc i + (l - Suc i)) = f l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc i + (l - Suc i)) = b

goal (2 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
assume "j < l - Suc i"
[PROOF STATE]
proof (state)
this:
j < l - Suc i

goal (2 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < l - Suc i
[PROOF STEP]
have small: "Suc i + j < l"
[PROOF STATE]
proof (prove)
using this:
j < l - Suc i

goal (1 subgoal):
 1. Suc i + j < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i + j < l

goal (2 subgoals):
 1. f (Suc i + 0) = f (Suc i)
 2. \<And>ia. ia < l - Suc i \<Longrightarrow> (f (Suc i + ia), f (Suc i + Suc ia)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
show "(?f j, ?f (Suc j)) \<in> rel \<inter> {(a, b). b \<notin> have}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f (Suc i + j), f (Suc i + Suc j)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
using steps [OF small]
[PROOF STATE]
proof (prove)
using this:
(f (Suc i + j), f (Suc (Suc i + j))) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. (f (Suc i + j), f (Suc i + Suc j)) \<in> rel \<inter> {(a, b). b \<notin> have}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f (Suc i + j), f (Suc i + Suc j)) \<in> rel \<inter> {(a, b). b \<notin> have}

goal (1 subgoal):
 1. f (Suc i + 0) = f (Suc i)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(f (Suc i), b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)

goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < l
[PROOF STEP]
have small: "l - Suc i < l"
[PROOF STATE]
proof (prove)
using this:
i < l

goal (1 subgoal):
 1. l - Suc i < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l - Suc i < l

goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
from seq new
[PROOF STATE]
proof (chain)
picking this:
(f (Suc i), b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)
f (Suc i) \<in> new
[PROOF STEP]
have "\<exists> a \<in> new. (a, b) \<in> ?rel (l - Suc i)"
[PROOF STATE]
proof (prove)
using this:
(f (Suc i), b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)
f (Suc i) \<in> new

goal (1 subgoal):
 1. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)

goal (1 subgoal):
 1. f (Suc i) \<in> new \<Longrightarrow> False
[PROOF STEP]
with not_less_Least [OF small [unfolded l]]
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ ((LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) - Suc i))
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ ((LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) - Suc i))
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ (l - Suc i)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ ((LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) - Suc i))
\<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ ((LEAST m. \<exists>a\<in>new. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m) - Suc i)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (Suc i) \<notin> new

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (Suc i) \<notin> new
[PROOF STEP]
have "(f i, f (Suc i)) \<in> ?reln 1"
[PROOF STATE]
proof (prove)
using this:
f (Suc i) \<notin> new

goal (1 subgoal):
 1. (f i, f (Suc i)) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ 1
[PROOF STEP]
using steps [OF i]
[PROOF STATE]
proof (prove)
using this:
f (Suc i) \<notin> new
(f i, f (Suc i)) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. (f i, f (Suc i)) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f i, f (Suc i)) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < l \<Longrightarrow> (f ?i2, f (Suc ?i2)) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
note steps = this
[PROOF STATE]
proof (state)
this:
?i2 < l \<Longrightarrow> (f ?i2, f (Suc ?i2)) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ 1

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have ab: "(a, b) \<in> ?reln l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ l
[PROOF STEP]
unfolding relpow_fun_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f 0 = a \<and> f l = b \<and> (\<forall>i<l. (f i, f (Suc i)) \<in> rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have})
[PROOF STEP]
by (intro exI conjI, insert fa fb steps, auto)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ l

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
have "b \<in> ?l1 \<union> ?l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = 0 \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
 2. \<And>nat. l = Suc nat \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
l = 0

goal (2 subgoals):
 1. l = 0 \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
 2. \<And>nat. l = Suc nat \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
with ab a
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ l
a \<in> new
l = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ l
a \<in> new
l = 0

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new

goal (1 subgoal):
 1. \<And>nat. l = Suc nat \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. l = Suc nat \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
case (Suc ll)
[PROOF STATE]
proof (state)
this:
l = Suc ll

goal (1 subgoal):
 1. \<And>nat. l = Suc nat \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
from relpow_Suc_D2 [OF ab [unfolded Suc]] a ln Suc
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. (a, y) \<in> rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have} \<and> (y, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ ll
a \<in> new
l \<le> Suc n
l = Suc ll
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>y. (a, y) \<in> rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have} \<and> (y, b) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ ll
a \<in> new
l \<le> Suc n
l = Suc ll

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new

goal (1 subgoal):
 1. \<lbrakk>b \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have; b \<notin> have\<rbrakk> \<Longrightarrow> b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> new

goal (1 subgoal):
 1. b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
b \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have \<Longrightarrow> ?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. nnew \<noteq> [] \<Longrightarrow> set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have \<Longrightarrow> ?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have \<Longrightarrow> ?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave
[PROOF STEP]
unfolding idl idr
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) \<Longrightarrow> ?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
?b2 \<in> {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have \<Longrightarrow> ?b2 \<in> {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have)

goal (1 subgoal):
 1. {uu. \<exists>a. (\<exists>aa\<in>new. (aa, a) \<in> rel) \<and> a \<notin> new \<and> a \<notin> have \<and> (\<exists>m\<le>n. (a, uu) \<in> (rel \<inter> {(a, b). b \<notin> new \<and> b \<notin> have}) ^^ m)} \<union> (new \<union> have) = {b. \<exists>a m. a \<in> new \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> have}) ^^ m} \<union> have
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_of (relpow_i nnew hhave (Suc n)) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set nnew \<and> m \<le> Suc n \<and> (a, b) \<in> (rel \<inter> {a. case a of (a, b) \<Rightarrow> b \<notin> set_of hhave}) ^^ m} \<union> set_of hhave

goal (1 subgoal):
 1. \<And>have new. set_of (relpow_i new have 0) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> 0 \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> set_of have}) ^^ m} \<union> set_of have
[PROOF STEP]
qed (simp add: un)


[STATEMENT]
lemma relpow_impl:
  "set_of (relpow_i new empty n) = {b | a b m. a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (relpow_i new empty n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_of (relpow_i new empty n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}
[PROOF STEP]
have id: "rel \<inter> {(a ,b). True} = rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel \<inter> {(a, b). True} = rel
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel \<inter> {(a, b). True} = rel

goal (1 subgoal):
 1. set_of (relpow_i new empty n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (relpow_i new empty n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}
[PROOF STEP]
unfolding relpow_impl_main empty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> (rel \<inter> {(a, b). b \<notin> {}}) ^^ m} \<union> {} = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}
[PROOF STEP]
by (simp add: id)
[PROOF STATE]
proof (state)
this:
set_of (relpow_i new empty n) = {uu_. \<exists>a b m. uu_ = b \<and> a \<in> set new \<and> m \<le> n \<and> (a, b) \<in> rel ^^ m}

goal:
No subgoals!
[PROOF STEP]
qed