[STATEMENT]
lemma sat_push_nonsat_potential:
  assumes PRE: "sat_push_precond f l e"
  shows "nonsat_potential (push_effect f e) l
      \<le> nonsat_potential f l + 2 * card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
obtain u v where [simp]: "e = (u, v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v. e = (u, v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases e) auto
[PROOF STATE]
proof (state)
this:
e = (u, v)

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
interpret push_effect_locale c s t f l u v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. push_effect_locale c s t f l u v
[PROOF STEP]
using PRE
[PROOF STATE]
proof (prove)
using this:
sat_push_precond f l e

goal (1 subgoal):
 1. push_effect_locale c s t f l u v
[PROOF STEP]
by unfold_locales (simp add: push_precond_eq_sat_or_nonsat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have [simp, intro!]: "finite {v\<in>V. excess f v > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
text \<open>Only target node may get activated\<close>
[PROOF STATE]
proof (state)
this:
finite {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have "{v\<in>V. excess f' v > 0} \<subseteq> insert v {v\<in>V. excess f v > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
using \<Delta>_positive
[PROOF STATE]
proof (prove)
using this:
(0::'a) < \<Delta>

goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
by (auto simp: excess'_if)
[PROOF STATE]
proof (state)
this:
{v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
text \<open>Thus, potential increases by at most \<open>l v\<close>\<close>
[PROOF STATE]
proof (state)
this:
{v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
with sum_mono2[OF _ this, of l]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (insert v {v \<in> V. (0::'a) < excess f v}); \<And>b. b \<in> insert v {v \<in> V. (0::'a) < excess f v} - {v \<in> V. (0::'a) < excess f' v} \<Longrightarrow> 0 \<le> l b\<rbrakk> \<Longrightarrow> sum l {v \<in> V. (0::'a) < excess f' v} \<le> sum l (insert v {v \<in> V. (0::'a) < excess f v})
{v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
have "nonsat_potential f' l \<le> nonsat_potential f l + l v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (insert v {v \<in> V. (0::'a) < excess f v}); \<And>b. b \<in> insert v {v \<in> V. (0::'a) < excess f v} - {v \<in> V. (0::'a) < excess f' v} \<Longrightarrow> 0 \<le> l b\<rbrakk> \<Longrightarrow> sum l {v \<in> V. (0::'a) < excess f' v} \<le> sum l (insert v {v \<in> V. (0::'a) < excess f v})
{v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential f' l \<le> nonsat_potential f l + l v
[PROOF STEP]
unfolding nonsat_potential_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (insert v {v \<in> V. (0::'a) < excess f v}); \<And>b. b \<in> insert v {v \<in> V. (0::'a) < excess f v} - {v \<in> V. (0::'a) < excess f' v} \<Longrightarrow> 0 \<le> l b\<rbrakk> \<Longrightarrow> sum l {v \<in> V. (0::'a) < excess f' v} \<le> sum l (insert v {v \<in> V. (0::'a) < excess f v})
{v \<in> V. (0::'a) < excess f' v} \<subseteq> insert v {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. sum l {v \<in> V. (0::'a) < excess f' v} \<le> sum l {v \<in> V. (0::'a) < excess f v} + l v
[PROOF STEP]
by (auto simp: sum.insert_if split: if_splits)
[PROOF STATE]
proof (state)
this:
nonsat_potential f' l \<le> nonsat_potential f l + l v

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
text \<open>Which is bounded by \<open>O(V)\<close>\<close>
[PROOF STATE]
proof (state)
this:
nonsat_potential f' l \<le> nonsat_potential f l + l v

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nonsat_potential f' l \<le> nonsat_potential f l + l v

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
note height_bound'[of v]
[PROOF STATE]
proof (state)
this:
v \<in> V \<Longrightarrow> l v \<le> 2 * card V - 1

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>v \<in> V; \<And>x y. x \<le> y \<Longrightarrow> nonsat_potential f l + x \<le> nonsat_potential f l + y\<rbrakk> \<Longrightarrow> nonsat_potential f' l \<le> nonsat_potential f l + (2 * card V - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v \<in> V; \<And>x y. x \<le> y \<Longrightarrow> nonsat_potential f l + x \<le> nonsat_potential f l + y\<rbrakk> \<Longrightarrow> nonsat_potential f' l \<le> nonsat_potential f l + (2 * card V - 1)

goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nonsat_potential (push_effect f e) l \<le> nonsat_potential f l + 2 * card V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relabel_nonsat_potential:
  assumes PRE: "relabel_precond f l u"
  shows "nonsat_potential f (relabel_effect f l u)
       \<le> nonsat_potential f l + 2 * card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have [simp, intro!]: "finite {v\<in>V. excess f v > 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
let ?l' = "relabel_effect f l u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
interpret l': Height_Bounded_Labeling c s t f ?l'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
using relabel_pres_height_bound[OF assms]
[PROOF STATE]
proof (prove)
using this:
Height_Bounded_Labeling c s t f (relabel_effect f l u)

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
from PRE
[PROOF STATE]
proof (chain)
picking this:
relabel_precond f l u
[PROOF STEP]
have U_ACTIVE: "u \<in> {v\<in>V. excess f v > 0}" and [simp]: "u\<in>V"
[PROOF STATE]
proof (prove)
using this:
relabel_precond f l u

goal (1 subgoal):
 1. u \<in> {v \<in> V. (0::'a) < excess f v} &&& u \<in> V
[PROOF STEP]
unfolding relabel_precond_def
[PROOF STATE]
proof (prove)
using this:
u \<noteq> t \<and> (0::'a) < excess f u \<and> (\<forall>v. (u, v) \<in> cf.E \<longrightarrow> l u \<noteq> l v + 1)

goal (1 subgoal):
 1. u \<in> {v \<in> V. (0::'a) < excess f v} &&& u \<in> V
[PROOF STEP]
using excess_nodes_only
[PROOF STATE]
proof (prove)
using this:
u \<noteq> t \<and> (0::'a) < excess f u \<and> (\<forall>v. (u, v) \<in> cf.E \<longrightarrow> l u \<noteq> l v + 1)
(0::'a) < excess f ?v \<Longrightarrow> ?v \<in> V

goal (1 subgoal):
 1. u \<in> {v \<in> V. (0::'a) < excess f v} &&& u \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> {v \<in> V. (0::'a) < excess f v}
u \<in> V

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have "nonsat_potential f ?l'
      = sum ?l' ({v \<in> V. 0 < excess f v} - {u}) + ?l' u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) = sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) + relabel_effect f l u u
[PROOF STEP]
unfolding nonsat_potential_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (relabel_effect f l u) {v \<in> V. (0::'a) < excess f v} = sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) + relabel_effect f l u u
[PROOF STEP]
using U_ACTIVE
[PROOF STATE]
proof (prove)
using this:
u \<in> {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. sum (relabel_effect f l u) {v \<in> V. (0::'a) < excess f v} = sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) + relabel_effect f l u u
[PROOF STEP]
by (auto intro: sum_arb)
[PROOF STATE]
proof (state)
this:
nonsat_potential f (relabel_effect f l u) = sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) + relabel_effect f l u u

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nonsat_potential f (relabel_effect f l u) = sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) + relabel_effect f l u u

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have "sum ?l' ({v \<in> V. 0 < excess f v} - {u})
      = sum l ({v \<in> V. 0 < excess f v} - {u})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) = sum l ({v \<in> V. (0::'a) < excess f v} - {u})
[PROOF STEP]
using relabel_preserve_other
[PROOF STATE]
proof (prove)
using this:
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v

goal (1 subgoal):
 1. sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) = sum l ({v \<in> V. (0::'a) < excess f v} - {u})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) = sum l ({v \<in> V. (0::'a) < excess f v} - {u})

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (relabel_effect f l u) ({v \<in> V. (0::'a) < excess f v} - {u}) = sum l ({v \<in> V. (0::'a) < excess f v} - {u})

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have "?l' u \<le> l u + 2*card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relabel_effect f l u u \<le> l u + 2 * card V
[PROOF STEP]
using l'.height_bound'[OF \<open>u\<in>V\<close>]
[PROOF STATE]
proof (prove)
using this:
relabel_effect f l u u \<le> 2 * card V - 1

goal (1 subgoal):
 1. relabel_effect f l u u \<le> l u + 2 * card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
relabel_effect f l u u \<le> l u + 2 * card V

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + x \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + y) \<Longrightarrow> nonsat_potential f (relabel_effect f l u) \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + (l u + 2 * card V)
[PROOF STEP]
have "nonsat_potential f ?l'
              \<le> sum l ({v \<in> V. 0 < excess f v} - {u}) + l u + 2 * card V"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + x \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + y) \<Longrightarrow> nonsat_potential f (relabel_effect f l u) \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + (l u + 2 * card V)

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u + 2 * card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nonsat_potential f (relabel_effect f l u) \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u + 2 * card V

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nonsat_potential f (relabel_effect f l u) \<le> sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u + 2 * card V

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
have "sum l ({v \<in> V. 0 < excess f v} - {u}) + l u
           = nonsat_potential f l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u = nonsat_potential f l
[PROOF STEP]
unfolding nonsat_potential_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u = sum l {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
using U_ACTIVE
[PROOF STATE]
proof (prove)
using this:
u \<in> {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u = sum l {v \<in> V. (0::'a) < excess f v}
[PROOF STEP]
by (auto intro: sum_arb[symmetric])
[PROOF STATE]
proof (state)
this:
sum l ({v \<in> V. (0::'a) < excess f v} - {u}) + l u = nonsat_potential f l

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V

goal (1 subgoal):
 1. nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nonsat_potential f (relabel_effect f l u) \<le> nonsat_potential f l + 2 * card V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonsat_push_action_bound':
  assumes A: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'"
  shows "length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
have B1: "length (filter is_NONSAT_PUSH' p)
    \<le>   nonsat_potential f l
      + 2 * card V * (length (filter is_SAT_PUSH' p))
      + 2 * card V * (length (filter is_RELABEL' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)
[PROOF STEP]
proof (induction p arbitrary: f l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f l. ((f, l), [], f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' []) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' []) + 2 * card V * length (filter is_RELABEL' [])
 2. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'

goal (2 subgoals):
 1. \<And>f l. ((f, l), [], f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' []) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' []) + 2 * card V * length (filter is_RELABEL' [])
 2. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' []) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' []) + 2 * card V * length (filter is_RELABEL' [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' []) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' []) + 2 * card V * length (filter is_RELABEL' [])

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
case [simp]: (Cons a p)
[PROOF STATE]
proof (state)
this:
((?f1, ?l1), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential ?f1 ?l1 + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((?f1, ?l1), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential ?f1 ?l1 + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
obtain fh lh
      where FIRST: "((f,l),a,(fh,lh))\<in>pr_algo_lts'"
          and PP: "((fh,lh),p,(f',l')) \<in> trcl pr_algo_lts'"
[PROOF STATE]
proof (prove)
using this:
((?f1, ?l1), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential ?f1 ?l1 + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. (\<And>fh lh. \<lbrakk>((f, l), a, fh, lh) \<in> pr_algo_lts'; ((fh, lh), p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: trcl_conv)
[PROOF STATE]
proof (state)
this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
((fh, lh), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
note IH = Cons.IH[OF PP]
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential fh lh + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
from FIRST
[PROOF STATE]
proof (chain)
picking this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
[PROOF STEP]
interpret Height_Bounded_Labeling c s t f l
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
using FIRST IH
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential fh lh + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>((f, l), a, fh, lh) \<in> pr_algo_lts'; length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential fh lh + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); a = RELABEL'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
 2. \<lbrakk>((f, l), a, fh, lh) \<in> pr_algo_lts'; length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential fh lh + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); a = NONSAT_PUSH'\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
 3. \<And>x3. \<lbrakk>((f, l), a, fh, lh) \<in> pr_algo_lts'; length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential fh lh + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); a = SAT_PUSH' x3\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))
[PROOF STEP]
apply (auto
          elim!: pr_algo_lts'.cases
          dest!: relabel_nonsat_potential nonsat_push_decr_nonsat_potential
          dest!: sat_push_nonsat_potential
      )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' (a # p)) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' (a # p)) + 2 * card V * length (filter is_RELABEL' (a # p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
(* TODO: Technical case distinction, as we do not assume invariant on f,l! *)
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
 2. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
 2. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
case (Cons a' p')
[PROOF STATE]
proof (state)
this:
p = a' # p'

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = a' # p'
[PROOF STEP]
interpret Height_Bounded_Labeling c s t f l
[PROOF STATE]
proof (prove)
using this:
p = a' # p'

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
p = a' # p'
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l
[PROOF STEP]
by (auto simp: trcl_conv elim!: pr_algo_lts'.cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
note B1
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> nonsat_potential f l + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p)

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
note nonsat_potential_bound
[PROOF STATE]
proof (state)
this:
nonsat_potential f l \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nonsat_potential f l \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
note sat_push_action_bound'[OF A]
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
note relabel_action_bound'[OF A]
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p) \<le> y + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); \<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 2 * card V * x + 2 * card V * length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2 + 2 * card V * y + 2 * card V * length (filter is_RELABEL' p); \<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * x \<le> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * y\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * (2 * (card V)\<^sup>2)
[PROOF STEP]
have "length (filter is_NONSAT_PUSH' p)
      \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * (card V)^3"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p) \<le> y + 2 * card V * length (filter is_SAT_PUSH' p) + 2 * card V * length (filter is_RELABEL' p); \<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 2 * card V * x + 2 * card V * length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2 + 2 * card V * y + 2 * card V * length (filter is_RELABEL' p); \<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * x \<le> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * y\<rbrakk> \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 2 * card V * (4 * card V * card E) + 2 * card V * (2 * (card V)\<^sup>2)

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * card V ^ 3
[PROOF STEP]
by (simp add: power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * card V ^ 3

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * card V ^ 3

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "(card V)^3 \<le> 2 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V ^ 3 \<le> 2 * (card V)\<^sup>2 * card E
[PROOF STEP]
by (simp add: card_V_est_E power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
card V ^ 3 \<le> 2 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * x \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * y) \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * (2 * (card V)\<^sup>2 * card E)
[PROOF STEP]
have "length (filter is_NONSAT_PUSH' p)
      \<le> 2 * (card V)\<^sup>2 + 16 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * x \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * y) \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 8 * (card V)\<^sup>2 * card E + 4 * (2 * (card V)\<^sup>2 * card E)

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 16 * (card V)\<^sup>2 * card E
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 16 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 + 16 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "2 * (card V)\<^sup>2 \<le> 2*(card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (card V)\<^sup>2 \<le> 2 * (card V)\<^sup>2 * card E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * (card V)\<^sup>2 \<le> 2 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 16 * (card V)\<^sup>2 * card E \<le> y + 16 * (card V)\<^sup>2 * card E) \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 * card E + 16 * (card V)\<^sup>2 * card E
[PROOF STEP]
show "length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 16 * (card V)\<^sup>2 * card E \<le> y + 16 * (card V)\<^sup>2 * card E) \<Longrightarrow> length (filter is_NONSAT_PUSH' p) \<le> 2 * (card V)\<^sup>2 * card E + 16 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p) \<le> 18 * (card V)\<^sup>2 * card E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Height_Bounded_Labeling) push_action_bound:
  assumes A: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  shows "length (filter (is_PUSH) p) \<le> 22 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
apply (rule order_trans[OF xfer_push_bounds[OF _ _ A]]; (intro allI impI)?)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p'. ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_SAT_PUSH' p') \<le> ?B1.2
 2. \<And>p'. ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p') \<le> ?B2.2
 3. ?B1.2 + ?B2.2 \<le> 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
apply (erule sat_push_action_bound'; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p'. ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_NONSAT_PUSH' p') \<le> ?B2.2
 2. 4 * card V * card E + ?B2.2 \<le> 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
apply (erule nonsat_push_action_bound'; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * card V * card E + 18 * (card V)\<^sup>2 * card E \<le> 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
apply (auto simp: power2_eq_square)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem (in Height_Bounded_Labeling) pr_algo_cost_bound:
  assumes A: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  shows "(\<Sum>a\<leftarrow>p. cost_estimate a) \<le> 26 * (card V)^2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "(\<Sum>a\<leftarrow>p. cost_estimate a)
    = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sum_list (map cost_estimate []) = card V * length (filter is_RELABEL []) + length (filter is_PUSH [])
 2. \<And>a p. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p) \<Longrightarrow> sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. sum_list (map cost_estimate []) = card V * length (filter is_RELABEL []) + length (filter is_PUSH [])
 2. \<And>a p. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p) \<Longrightarrow> sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map cost_estimate []) = card V * length (filter is_RELABEL []) + length (filter is_PUSH [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate []) = card V * length (filter is_RELABEL []) + length (filter is_PUSH [])

goal (1 subgoal):
 1. \<And>a p. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p) \<Longrightarrow> sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p) \<Longrightarrow> sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)

goal (1 subgoal):
 1. \<And>a p. sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p) \<Longrightarrow> sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)

goal (1 subgoal):
 1. sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate (a # p)) = card V * length (filter is_RELABEL (a # p)) + length (filter is_PUSH (a # p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) = card V * length (filter is_RELABEL p) + length (filter is_PUSH p)

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "card V * length (filter is_RELABEL p) \<le> 2 * (card V)^3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V * length (filter is_RELABEL p) \<le> 2 * card V ^ 3
[PROOF STEP]
using relabel_action_bound[OF A]
[PROOF STATE]
proof (prove)
using this:
length (filter is_RELABEL p) \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. card V * length (filter is_RELABEL p) \<le> 2 * card V ^ 3
[PROOF STEP]
by (auto simp: power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
card V * length (filter is_RELABEL p) \<le> 2 * card V ^ 3

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card V * length (filter is_RELABEL p) \<le> 2 * card V ^ 3

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
note push_action_bound[OF A]
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) \<le> 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_PUSH p) \<le> y + length (filter is_PUSH p); \<And>x y. x \<le> y \<Longrightarrow> 2 * card V ^ 3 + x \<le> 2 * card V ^ 3 + y\<rbrakk> \<Longrightarrow> sum_list (map cost_estimate p) \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "sum_list (map cost_estimate p)
              \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_PUSH p) \<le> y + length (filter is_PUSH p); \<And>x y. x \<le> y \<Longrightarrow> 2 * card V ^ 3 + x \<le> 2 * card V ^ 3 + y\<rbrakk> \<Longrightarrow> sum_list (map cost_estimate p) \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) \<le> 2 * card V ^ 3 + 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
have "(card V)^3 \<le> 2 * (card V)\<^sup>2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V ^ 3 \<le> 2 * (card V)\<^sup>2 * card E
[PROOF STEP]
by (simp add: card_V_est_E power2_eq_square power3_eq_cube)
[PROOF STATE]
proof (state)
this:
card V ^ 3 \<le> 2 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> 2 * x + 22 * (card V)\<^sup>2 * card E \<le> 2 * y + 22 * (card V)\<^sup>2 * card E) \<Longrightarrow> sum_list (map cost_estimate p) \<le> 2 * (2 * (card V)\<^sup>2 * card E) + 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> 2 * x + 22 * (card V)\<^sup>2 * card E \<le> 2 * y + 22 * (card V)\<^sup>2 * card E) \<Longrightarrow> sum_list (map cost_estimate p) \<le> 2 * (2 * (card V)\<^sup>2 * card E) + 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Network) generic_preflow_push_OV2E_and_correct:
  assumes A: "((pp_init_f, pp_init_l), p, (f, l)) \<in> trcl pr_algo_lts"
  shows "(\<Sum>x\<leftarrow>p. cost_estimate x) \<le> 26 * (card V)^2 * card E" (is ?G1)
    and "(f,l)\<notin>Domain pr_algo_lts \<longrightarrow> isMaxFlow f" (is ?G2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E &&& (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
 2. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
show ?G1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
using pp_init_height_bound Height_Bounded_Labeling.pr_algo_cost_bound A
[PROOF STATE]
proof (prove)
using this:
Height_Bounded_Labeling c s t pp_init_f pp_init_l
\<lbrakk>Height_Bounded_Labeling ?c ?s ?t ?f ?l; ((?f, ?l), ?p, ?f', ?l') \<in> trcl (Network.pr_algo_lts ?c ?t)\<rbrakk> \<Longrightarrow> sum_list (map (Network.cost_estimate ?c) ?p) \<le> 26 * (card (Graph.V ?c))\<^sup>2 * card (Graph.E ?c)
((pp_init_f, pp_init_l), p, f, l) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum_list (map cost_estimate p) \<le> 26 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
show ?G2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
((pp_init_f, pp_init_l), p, f, l) \<in> trcl pr_algo_lts
[PROOF STEP]
interpret Height_Bounded_Labeling c s t f l
[PROOF STATE]
proof (prove)
using this:
((pp_init_f, pp_init_l), p, f, l) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l
[PROOF STEP]
apply (induction p arbitrary: f l rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f l. ((pp_init_f, pp_init_l), [], f, l) \<in> trcl pr_algo_lts \<Longrightarrow> Height_Bounded_Labeling c s t f l
 2. \<And>x xs f l. \<lbrakk>\<And>f l. ((pp_init_f, pp_init_l), xs, f, l) \<in> trcl pr_algo_lts \<Longrightarrow> Height_Bounded_Labeling c s t f l; ((pp_init_f, pp_init_l), xs @ [x], f, l) \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> Height_Bounded_Labeling c s t f l
[PROOF STEP]
apply (auto
        simp: pp_init_height_bound trcl_conv
        intro: Height_Bounded_Labeling.pr_algo_maintains_hb_labeling)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
from pr_algo_term_maxflow
[PROOF STATE]
proof (chain)
picking this:
(f, l) \<notin> Domain pr_algo_lts \<Longrightarrow> isMaxFlow f
[PROOF STEP]
show ?G2
[PROOF STATE]
proof (prove)
using this:
(f, l) \<notin> Domain pr_algo_lts \<Longrightarrow> isMaxFlow f

goal (1 subgoal):
 1. (f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f, l) \<notin> Domain pr_algo_lts \<longrightarrow> isMaxFlow f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pr_algo_rel_alt: "pr_algo_rel =
    { ((push_effect f e,l),(f,l)) | f e l.
        Height_Bounded_Labeling c s t f l \<and> push_precond f l e }
  \<union> { ((f, relabel_effect f l u), (f,l)) | f u l.
        Height_Bounded_Labeling c s t f l \<and> relabel_precond f l u }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_algo_rel = {((push_effect f e, l), f, l) |f e l. Height_Bounded_Labeling c s t f l \<and> push_precond f l e} \<union> {((f, relabel_effect f l u), f, l) |f u l. Height_Bounded_Labeling c s t f l \<and> relabel_precond f l u}
[PROOF STEP]
by (auto elim!: pr_algo_rel.cases intro: pr_algo_rel.intros)


[STATEMENT]
lemma (in Height_Bounded_Labeling) pr_algo_lts_length_bound:
  assumes A: "((f, l), p, (f', l')) \<in> trcl pr_algo_lts"
  shows "length p \<le> pr_algo_len_bound"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
have "length p = length (filter is_PUSH p) + length (filter is_RELABEL p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p = length (filter is_PUSH p) + length (filter is_RELABEL p)
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length [] = length (filter is_PUSH []) + length (filter is_RELABEL [])
 2. \<And>a p. length p = length (filter is_PUSH p) + length (filter is_RELABEL p) \<Longrightarrow> length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. length [] = length (filter is_PUSH []) + length (filter is_RELABEL [])
 2. \<And>a p. length p = length (filter is_PUSH p) + length (filter is_RELABEL p) \<Longrightarrow> length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [] = length (filter is_PUSH []) + length (filter is_RELABEL [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length [] = length (filter is_PUSH []) + length (filter is_RELABEL [])

goal (1 subgoal):
 1. \<And>a p. length p = length (filter is_PUSH p) + length (filter is_RELABEL p) \<Longrightarrow> length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. length p = length (filter is_PUSH p) + length (filter is_RELABEL p) \<Longrightarrow> length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
length p = length (filter is_PUSH p) + length (filter is_RELABEL p)

goal (1 subgoal):
 1. \<And>a p. length p = length (filter is_PUSH p) + length (filter is_RELABEL p) \<Longrightarrow> length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length p = length (filter is_PUSH p) + length (filter is_RELABEL p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length p = length (filter is_PUSH p) + length (filter is_RELABEL p)

goal (1 subgoal):
 1. length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
length (a # p) = length (filter is_PUSH (a # p)) + length (filter is_RELABEL (a # p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length p = length (filter is_PUSH p) + length (filter is_RELABEL p)

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length p = length (filter is_PUSH p) + length (filter is_RELABEL p)

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
note push_action_bound[OF A]
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) \<le> 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) \<le> 22 * (card V)\<^sup>2 * card E

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
note relabel_action_bound[OF A]
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL p) \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_RELABEL p) \<le> y + length (filter is_RELABEL p); \<And>x y. x \<le> y \<Longrightarrow> 22 * (card V)\<^sup>2 * card E + x \<le> 22 * (card V)\<^sup>2 * card E + y\<rbrakk> \<Longrightarrow> length p \<le> 22 * (card V)\<^sup>2 * card E + 2 * (card V)\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_RELABEL p) \<le> y + length (filter is_RELABEL p); \<And>x y. x \<le> y \<Longrightarrow> 22 * (card V)\<^sup>2 * card E + x \<le> 22 * (card V)\<^sup>2 * card E + y\<rbrakk> \<Longrightarrow> length p \<le> 22 * (card V)\<^sup>2 * card E + 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. length p \<le> pr_algo_len_bound
[PROOF STEP]
unfolding pr_algo_len_bound_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_RELABEL p) \<le> y + length (filter is_RELABEL p); \<And>x y. x \<le> y \<Longrightarrow> 22 * (card V)\<^sup>2 * card E + x \<le> 22 * (card V)\<^sup>2 * card E + y\<rbrakk> \<Longrightarrow> length p \<le> 22 * (card V)\<^sup>2 * card E + 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. length p \<le> 2 * (card V)\<^sup>2 + 22 * (card V)\<^sup>2 * card E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length p \<le> pr_algo_len_bound

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Height_Bounded_Labeling) path_set_finite:
  "finite {p. \<exists>f' l'. ((f,l),p,(f',l')) \<in> trcl pr_algo_lts}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
have FIN_OPS: "finite (UNIV::pr_operation set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV
[PROOF STEP]
apply (rule finite_subset[where B="{PUSH,RELABEL}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. UNIV \<subseteq> {PUSH, RELABEL}
 2. finite {PUSH, RELABEL}
[PROOF STEP]
using pr_operation.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = PUSH \<Longrightarrow> ?P; ?y = RELABEL \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (2 subgoals):
 1. UNIV \<subseteq> {PUSH, RELABEL}
 2. finite {PUSH, RELABEL}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite UNIV

goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
have "{p. \<exists>f' l'. ((f,l),p,(f',l')) \<in> trcl pr_algo_lts}
    \<subseteq> {p. length p \<le> pr_algo_len_bound}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts} \<subseteq> {p. length p \<le> pr_algo_len_bound}
[PROOF STEP]
by (auto simp: pr_algo_lts_length_bound)
[PROOF STATE]
proof (state)
this:
{p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts} \<subseteq> {p. length p \<le> pr_algo_len_bound}

goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts} \<subseteq> {p. length p \<le> pr_algo_len_bound}

goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
note finite_lists_length_le[OF FIN_OPS, simplified]
[PROOF STATE]
proof (state)
this:
finite {xs. length xs \<le> ?n}

goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
finally (finite_subset)
[PROOF STATE]
proof (chain)
picking this:
finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pr_algo_measure:
  assumes "(fl',fl) \<in> pr_algo_rel"
  shows "pr_algo_measure fl' < pr_algo_measure fl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_algo_measure fl' < pr_algo_measure fl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(fl', fl) \<in> pr_algo_rel

goal (1 subgoal):
 1. pr_algo_measure fl' < pr_algo_measure fl
[PROOF STEP]
proof (cases fl'; cases fl; simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
fix f l f' l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
assume A: "((f',l'),(f,l)) \<in> pr_algo_rel"
[PROOF STATE]
proof (state)
this:
((f', l'), f, l) \<in> pr_algo_rel

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((f', l'), f, l) \<in> pr_algo_rel
[PROOF STEP]
obtain a where LTS_STEP: "((f,l),a,(f',l'))\<in>pr_algo_lts"
[PROOF STATE]
proof (prove)
using this:
((f', l'), f, l) \<in> pr_algo_rel

goal (1 subgoal):
 1. (\<And>a. ((f, l), a, f', l') \<in> pr_algo_lts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases (auto intro: pr_algo_lts.intros)
[PROOF STATE]
proof (state)
this:
((f, l), a, f', l') \<in> pr_algo_lts

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
((f', l'), f, l) \<in> pr_algo_rel
[PROOF STEP]
interpret Height_Bounded_Labeling c s t f l
[PROOF STATE]
proof (prove)
using this:
((f', l'), f, l) \<in> pr_algo_rel

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
from pr_algo_maintains_hb_labeling[OF LTS_STEP]
[PROOF STATE]
proof (chain)
picking this:
Height_Bounded_Labeling c s t f' l'
[PROOF STEP]
interpret f': Height_Bounded_Labeling c s t f' l'
[PROOF STATE]
proof (prove)
using this:
Height_Bounded_Labeling c s t f' l'

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f' l'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
let ?S1 = "{length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
let ?S2 = "{length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
have "finite ?S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
using finite_image_set path_set_finite
[PROOF STATE]
proof (prove)
using this:
finite {x. ?P x} \<Longrightarrow> finite {?f x |x. ?P x}
finite {p. \<exists>f' l'. ((f, l), p, f', l') \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
have "?S1 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}
[PROOF STEP]
by (auto intro: exI[where x="[]"])
[PROOF STATE]
proof (state)
this:
{length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
{length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}
[PROOF STEP]
obtain p fx lx where
    "length p = Max ?S1"
    "((f, l), p, fx, lx) \<in> trcl pr_algo_lts"
[PROOF STATE]
proof (prove)
using this:
finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
{length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}

goal (1 subgoal):
 1. (\<And>p fx lx. \<lbrakk>length p = Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}; ((f, l), p, fx, lx) \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p fx lx. \<lbrakk>length p = Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}; ((f, l), p, fx, lx) \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> thesis; finite {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}; {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (drule (1) Max_in)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p fx lx. \<lbrakk>length p = Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}; ((f, l), p, fx, lx) \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> thesis; {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}; Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<in> {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p = Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
((f, l), p, fx, lx) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
have "finite ?S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
using finite_image_set f'.path_set_finite
[PROOF STATE]
proof (prove)
using this:
finite {x. ?P x} \<Longrightarrow> finite {?f x |x. ?P x}
finite {p. \<exists>f'a l'a. ((f', l'), p, f'a, l'a) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. finite {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
have "?S2 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}
[PROOF STEP]
by (auto intro: exI[where x="[]"])
[PROOF STATE]
proof (state)
this:
{length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
{length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<noteq> {}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
assume MG: "Max ?S2 \<ge> Max ?S1"
[PROOF STATE]
proof (state)
this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
from Max_in[OF \<open>finite ?S2\<close> \<open>?S2\<noteq>{}\<close>]
[PROOF STATE]
proof (chain)
picking this:
Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<in> {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
obtain p fx lx where
      "length p = Max ?S2"
      "((f', l'), p, fx, lx) \<in> trcl pr_algo_lts"
[PROOF STATE]
proof (prove)
using this:
Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<in> {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. (\<And>p fx lx. \<lbrakk>length p = Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}; ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p = Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
((f', l'), p, fx, lx) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
with MG LTS_STEP
[PROOF STATE]
proof (chain)
picking this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
((f, l), a, f', l') \<in> pr_algo_lts
length p = Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
((f', l'), p, fx, lx) \<in> trcl pr_algo_lts
[PROOF STEP]
have
      LEN: "length (a#p) > Max ?S1"
      and P: "((f,l),a#p,(fx,lx)) \<in> trcl pr_algo_lts"
[PROOF STATE]
proof (prove)
using this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
((f, l), a, f', l') \<in> pr_algo_lts
length p = Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts}
((f', l'), p, fx, lx) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} < length (a # p) &&& ((f, l), a # p, fx, lx) \<in> trcl pr_algo_lts
[PROOF STEP]
by (auto simp: trcl_conv)
[PROOF STATE]
proof (state)
this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} < length (a # p)
((f, l), a # p, fx, lx) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
((f, l), a # p, fx, lx) \<in> trcl pr_algo_lts
[PROOF STEP]
have "length (a#p) \<in> ?S1"
[PROOF STATE]
proof (prove)
using this:
((f, l), a # p, fx, lx) \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. length (a # p) \<in> {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (a # p) \<in> {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
from Max_ge[OF \<open>finite ?S1\<close> this] LEN
[PROOF STATE]
proof (chain)
picking this:
length (a # p) \<le> Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} < length (a # p)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
length (a # p) \<le> Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts}
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} < length (a # p)

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

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> pr_algo_rel; fl' = (a, b); fl = (aa, ba)\<rbrakk> \<Longrightarrow> pr_algo_measure (a, b) < pr_algo_measure (aa, ba)
[PROOF STEP]
thus "pr_algo_measure (f', l') < pr_algo_measure (f, l)"
[PROOF STATE]
proof (prove)
using this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<Longrightarrow> False

goal (1 subgoal):
 1. pr_algo_measure (f', l') < pr_algo_measure (f, l)
[PROOF STEP]
unfolding pr_algo_measure_def
[PROOF STATE]
proof (prove)
using this:
Max {length p |p. \<exists>fx lx. ((f, l), p, fx, lx) \<in> trcl pr_algo_lts} \<le> Max {length p |p. \<exists>fx lx. ((f', l'), p, fx, lx) \<in> trcl pr_algo_lts} \<Longrightarrow> False

goal (1 subgoal):
 1. (case (f', l') of (f, l) \<Rightarrow> Max {length p |p. \<exists>aa ba. ((f, l), p, aa, ba) \<in> trcl pr_algo_lts}) < (case (f, l) of (f, l) \<Rightarrow> Max {length p |p. \<exists>aa ba. ((f, l), p, aa, ba) \<in> trcl pr_algo_lts})
[PROOF STEP]
by (rule ccontr) auto
[PROOF STATE]
proof (state)
this:
pr_algo_measure (f', l') < pr_algo_measure (f, l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_pr_algo_rel[simp, intro!]: "wf pr_algo_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf pr_algo_rel
[PROOF STEP]
apply (rule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf ?r
 2. pr_algo_rel \<subseteq> ?r
[PROOF STEP]
apply (rule wf_measure[where f=pr_algo_measure])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_algo_rel \<subseteq> measure pr_algo_measure
[PROOF STEP]
by (auto simp: pr_algo_measure)


[STATEMENT]
lemma (in Labeling) gap_pres_Labeling:
  assumes PRE: "gap_precond l k"
  defines "l' \<equiv> gap_effect l k"
  shows "Labeling c s t f l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t f l'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
 2. l' s = card V
 3. l' t = 0
[PROOF STEP]
from lab_src
[PROOF STATE]
proof (chain)
picking this:
l s = card V
[PROOF STEP]
show "l' s = card V"
[PROOF STATE]
proof (prove)
using this:
l s = card V

goal (1 subgoal):
 1. l' s = card V
[PROOF STEP]
unfolding l'_def gap_effect_def
[PROOF STATE]
proof (prove)
using this:
l s = card V

goal (1 subgoal):
 1. (if k < l s \<and> l s < card V then card V + 1 else l s) = card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' s = card V

goal (2 subgoals):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
 2. l' t = 0
[PROOF STEP]
from lab_sink
[PROOF STATE]
proof (chain)
picking this:
l t = 0
[PROOF STEP]
show "l' t = 0"
[PROOF STATE]
proof (prove)
using this:
l t = 0

goal (1 subgoal):
 1. l' t = 0
[PROOF STEP]
unfolding l'_def gap_effect_def
[PROOF STATE]
proof (prove)
using this:
l t = 0

goal (1 subgoal):
 1. (if k < l t \<and> l t < card V then card V + 1 else l t) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' t = 0

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
[PROOF STEP]
have l'_incr: "l' v \<ge> l v" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l v \<le> l' v
[PROOF STEP]
unfolding l'_def gap_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l v \<le> (if k < l v \<and> l v < card V then card V + 1 else l v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l ?v3 \<le> l' ?v3

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
[PROOF STEP]
assume A: "(u,v) \<in> cf.E"
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cf.E

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
[PROOF STEP]
hence "u\<in>V" "v\<in>V"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cf.E

goal (1 subgoal):
 1. u \<in> V &&& v \<in> V
[PROOF STEP]
using cfE_ss_invE E_ss_VxV
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cf.E
cf.E \<subseteq> E \<union> E\<inverse>
E \<subseteq> V \<times> V

goal (1 subgoal):
 1. u \<in> V &&& v \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> V
v \<in> V

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cf.E \<Longrightarrow> l' u \<le> l' v + 1
[PROOF STEP]
thus "l' u \<le> l' v + 1"
[PROOF STATE]
proof (prove)
using this:
u \<in> V
v \<in> V

goal (1 subgoal):
 1. l' u \<le> l' v + 1
[PROOF STEP]
unfolding l'_def gap_effect_def
[PROOF STATE]
proof (prove)
using this:
u \<in> V
v \<in> V

goal (1 subgoal):
 1. (if k < l u \<and> l u < card V then card V + 1 else l u) \<le> (if k < l v \<and> l v < card V then card V + 1 else l v) + 1
[PROOF STEP]
using valid[OF A] PRE
[PROOF STATE]
proof (prove)
using this:
u \<in> V
v \<in> V
l u \<le> l v + 1
gap_precond l k

goal (1 subgoal):
 1. (if k < l u \<and> l u < card V then card V + 1 else l u) \<le> (if k < l v \<and> l v < card V then card V + 1 else l v) + 1
[PROOF STEP]
unfolding gap_precond_def
[PROOF STATE]
proof (prove)
using this:
u \<in> V
v \<in> V
l u \<le> l v + 1
\<forall>v\<in>V. l v \<noteq> k

goal (1 subgoal):
 1. (if k < l u \<and> l u < card V then card V + 1 else l u) \<le> (if k < l v \<and> l v < card V then card V + 1 else l v) + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' u \<le> l' v + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Height_Bounded_Labeling) gap_pres_hb_labeling:
  assumes PRE: "gap_precond l k"
  defines "l' \<equiv> gap_effect l k"
  shows "Height_Bounded_Labeling c s t f l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l'
[PROOF STEP]
from gap_pres_Labeling[OF PRE]
[PROOF STATE]
proof (chain)
picking this:
Labeling c s t f (gap_effect l k)
[PROOF STEP]
interpret Labeling c s t f l'
[PROOF STATE]
proof (prove)
using this:
Labeling c s t f (gap_effect l k)

goal (1 subgoal):
 1. Labeling c s t f l'
[PROOF STEP]
unfolding l'_def
[PROOF STATE]
proof (prove)
using this:
Labeling c s t f (gap_effect l k)

goal (1 subgoal):
 1. Labeling c s t f (gap_effect l k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l'
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>V. l' u \<le> 2 * card V - 1
[PROOF STEP]
unfolding l'_def gap_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>V. (if k < l u \<and> l u < card V then card V + 1 else l u) \<le> 2 * card V - 1
[PROOF STEP]
using height_bound
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>V. l u \<le> 2 * card V - 1

goal (1 subgoal):
 1. \<forall>u\<in>V. (if k < l u \<and> l u < card V then card V + 1 else l u) \<le> 2 * card V - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t f l'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Labeling) gap_relabel_pres_Labeling:
  assumes PRE: "relabel_precond f l u"
  defines "l' \<equiv> gap_relabel_effect f l u"
  shows "Labeling c s t f l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t f l'
[PROOF STEP]
unfolding l'_def gap_relabel_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t f (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l')
[PROOF STEP]
using relabel_pres_Labeling[OF PRE] Labeling.gap_pres_Labeling
[PROOF STATE]
proof (prove)
using this:
Labeling c s t f (relabel_effect f l u)
\<lbrakk>Labeling ?c ?s ?t ?f ?l; Network.gap_precond ?c ?l ?k\<rbrakk> \<Longrightarrow> Labeling ?c ?s ?t ?f (Network.gap_effect ?c ?l ?k)

goal (1 subgoal):
 1. Labeling c s t f (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l')
[PROOF STEP]
by (fastforce simp: Let_def)


[STATEMENT]
lemma (in Height_Bounded_Labeling) gap_relabel_pres_hb_labeling:
  assumes PRE: "relabel_precond f l u"
  defines "l' \<equiv> gap_relabel_effect f l u"
  shows "Height_Bounded_Labeling c s t f l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f l'
[PROOF STEP]
unfolding l'_def gap_relabel_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l')
[PROOF STEP]
using relabel_pres_height_bound[OF PRE] Height_Bounded_Labeling.gap_pres_hb_labeling
[PROOF STATE]
proof (prove)
using this:
Height_Bounded_Labeling c s t f (relabel_effect f l u)
\<lbrakk>Height_Bounded_Labeling ?c ?s ?t ?f ?l; Network.gap_precond ?c ?l ?k\<rbrakk> \<Longrightarrow> Height_Bounded_Labeling ?c ?s ?t ?f (Network.gap_effect ?c ?l ?k)

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l')
[PROOF STEP]
by (fastforce simp: Let_def)


[STATEMENT]
lemma (in Height_Bounded_Labeling) gap_measure:
  assumes "gap_precond l k"
  shows "sum_heights_measure (gap_effect l k) \<le> sum_heights_measure l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_heights_measure (gap_effect l k) \<le> sum_heights_measure l
[PROOF STEP]
unfolding gap_effect_def sum_heights_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - (if k < l v \<and> l v < card V then card V + 1 else l v)) \<le> (\<Sum>v\<in>V. 2 * card V - l v)
[PROOF STEP]
by (auto intro!: sum_mono)


[STATEMENT]
lemma (in Height_Bounded_Labeling) gap_relabel_measure:
  assumes PRE: "relabel_precond f l u"
  shows "sum_heights_measure (gap_relabel_effect f l u) < sum_heights_measure l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_heights_measure (gap_relabel_effect f l u) < sum_heights_measure l
[PROOF STEP]
unfolding gap_relabel_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_heights_measure (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l') < sum_heights_measure l
[PROOF STEP]
using relabel_measure[OF PRE] relabel_pres_height_bound[OF PRE] Height_Bounded_Labeling.gap_measure
[PROOF STATE]
proof (prove)
using this:
sum_heights_measure (relabel_effect f l u) < sum_heights_measure l
Height_Bounded_Labeling c s t f (relabel_effect f l u)
\<lbrakk>Height_Bounded_Labeling ?c ?s ?t ?f ?l; Network.gap_precond ?c ?l ?k\<rbrakk> \<Longrightarrow> Network.sum_heights_measure ?c (Network.gap_effect ?c ?l ?k) \<le> Network.sum_heights_measure ?c ?l

goal (1 subgoal):
 1. sum_heights_measure (let l' = relabel_effect f l u in if gap_precond l' (l u) then gap_effect l' (l u) else l') < sum_heights_measure l
[PROOF STEP]
by (fastforce simp: Let_def)


[STATEMENT]
lemma wf_gap_algo_rel[simp, intro!]: "wf gap_algo_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf gap_algo_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf gap_algo_rel
[PROOF STEP]
have "gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f,l). (sum_heights_measure l, pr_algo_measure (f,l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f, l). (sum_heights_measure l, pr_algo_measure (f, l)))
[PROOF STEP]
using pr_algo_measure
[PROOF STATE]
proof (prove)
using this:
(?fl', ?fl) \<in> pr_algo_rel \<Longrightarrow> pr_algo_measure ?fl' < pr_algo_measure ?fl

goal (1 subgoal):
 1. gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f, l). (sum_heights_measure l, pr_algo_measure (f, l)))
[PROOF STEP]
using Height_Bounded_Labeling.gap_relabel_measure
[PROOF STATE]
proof (prove)
using this:
(?fl', ?fl) \<in> pr_algo_rel \<Longrightarrow> pr_algo_measure ?fl' < pr_algo_measure ?fl
\<lbrakk>Height_Bounded_Labeling ?c ?s ?t ?f ?l; Network.relabel_precond ?c ?t ?f ?l ?u\<rbrakk> \<Longrightarrow> Network.sum_heights_measure ?c (Network.gap_relabel_effect ?c ?f ?l ?u) < Network.sum_heights_measure ?c ?l

goal (1 subgoal):
 1. gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f, l). (sum_heights_measure l, pr_algo_measure (f, l)))
[PROOF STEP]
by (fastforce elim!: gap_algo_rel.cases intro: pr_algo_rel.intros )
[PROOF STATE]
proof (state)
this:
gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f, l). (sum_heights_measure l, pr_algo_measure (f, l)))

goal (1 subgoal):
 1. wf gap_algo_rel
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
gap_algo_rel \<subseteq> inv_image (less_than <*lex*> less_than) (\<lambda>(f, l). (sum_heights_measure l, pr_algo_measure (f, l)))

goal (1 subgoal):
 1. wf gap_algo_rel
[PROOF STEP]
by (rule_tac wf_subset; auto)
[PROOF STATE]
proof (state)
this:
wf gap_algo_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mapL_strict [simp]: "mapL\<cdot>f\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapL\<cdot>f\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma filterL_strict [simp]: "filterL\<cdot>p\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterL\<cdot>p\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma foldrL_strict [simp]: "foldrL\<cdot>f\<cdot>z\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldrL\<cdot>f\<cdot>z\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma enumFromToL_simps' [simp]:
  "x \<le> y \<Longrightarrow>
    enumFromToL\<cdot>(up\<cdot>x)\<cdot>(up\<cdot>y) = LCons\<cdot>(up\<cdot>x)\<cdot>(enumFromToL\<cdot>(up\<cdot>(x+1))\<cdot>(up\<cdot>y))"
  "\<not> x \<le> y \<Longrightarrow> enumFromToL\<cdot>(up\<cdot>x)\<cdot>(up\<cdot>y) = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y \<Longrightarrow> enumFromToL\<cdot>(up\<cdot>x)\<cdot>(up\<cdot>y) = LCons\<cdot>(up\<cdot>x)\<cdot>(enumFromToL\<cdot>(up\<cdot>(x + 1))\<cdot>(up\<cdot>y))) &&& (\<not> x \<le> y \<Longrightarrow> enumFromToL\<cdot>(up\<cdot>x)\<cdot>(up\<cdot>y) = LNil)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma enumFromToL_strict [simp]:
  "enumFromToL\<cdot>\<bottom>\<cdot>y = \<bottom>"
  "enumFromToL\<cdot>x\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumFromToL\<cdot>\<bottom>\<cdot>y = \<bottom> &&& enumFromToL\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply (subst enumFromToL.unfold, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumFromToL\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply (induct x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. enumFromToL\<cdot>\<bottom>\<cdot>\<bottom> = \<bottom>
 2. \<And>x. enumFromToL\<cdot>(up\<cdot>x)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply (subst enumFromToL.unfold, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma appendL_strict [simp]: "appendL\<cdot>\<bottom>\<cdot>ys = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appendL\<cdot>\<bottom>\<cdot>ys = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma appendL_LNil_right: "appendL\<cdot>xs\<cdot>LNil = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appendL\<cdot>xs\<cdot>LNil = xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma zipWithL_strict [simp]:
  "zipWithL\<cdot>f\<cdot>\<bottom>\<cdot>ys = \<bottom>"
  "zipWithL\<cdot>f\<cdot>(LCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zipWithL\<cdot>f\<cdot>\<bottom>\<cdot>ys = \<bottom> &&& zipWithL\<cdot>f\<cdot>(LCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp+


[STATEMENT]
lemma concatMapL_strict [simp]: "concatMapL\<cdot>f\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concatMapL\<cdot>f\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp