[STATEMENT]
lemma (in Height_Bounded_Labeling) xfer_run:
  assumes "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  obtains p' where "((f,l),p',(f',l')) \<in> trcl pr_algo_lts'"
               and "p = map project_operation p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>p'.
      Height_Bounded_Labeling c s t f' l'
    \<and> ((f,l),p',(f',l')) \<in> trcl pr_algo_lts'
    \<and> p = map project_operation p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'
[PROOF STEP]
proof (induction p arbitrary: f' l' rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f' l'. ((f, l), [], f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> [] = map project_operation p'
 2. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation 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> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> [] = map project_operation p'
 2. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((f, l), [], f', l') \<in> trcl pr_algo_lts

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

goal (1 subgoal):
 1. \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> [] = map project_operation p'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> [] = map project_operation p'

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
case (snoc a p)
[PROOF STATE]
proof (state)
this:
((f, l), p, ?f', ?l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t ?f' ?l' \<and> ((f, l), p', ?f', ?l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'
((f, l), p @ [a], f', l') \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
from snoc.prems
[PROOF STATE]
proof (chain)
picking this:
((f, l), p @ [a], f', l') \<in> trcl pr_algo_lts
[PROOF STEP]
obtain fh lh
      where PP: "((f, l), p, fh, lh) \<in> trcl pr_algo_lts"
        and LAST: "((fh,lh),a,(f',l'))\<in>pr_algo_lts"
[PROOF STATE]
proof (prove)
using this:
((f, l), p @ [a], f', l') \<in> trcl pr_algo_lts

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

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
from snoc.IH[OF PP]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'. Height_Bounded_Labeling c s t fh lh \<and> ((f, l), p', fh, lh) \<in> trcl pr_algo_lts' \<and> p = map project_operation p'
[PROOF STEP]
obtain p'
      where HBL: "Height_Bounded_Labeling c s t fh lh"
        and PP': "((f, l), p', fh, lh) \<in> trcl pr_algo_lts'"
        and [simp]: "p = map project_operation p'"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'. Height_Bounded_Labeling c s t fh lh \<and> ((f, l), p', fh, lh) \<in> trcl pr_algo_lts' \<and> p = map project_operation p'

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>Height_Bounded_Labeling c s t fh lh; ((f, l), p', fh, lh) \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t fh lh
((f, l), p', fh, lh) \<in> trcl pr_algo_lts'
p = map project_operation p'

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
from LAST
[PROOF STATE]
proof (chain)
picking this:
((fh, lh), a, f', l') \<in> pr_algo_lts
[PROOF STEP]
obtain a'
      where LAST': "((fh,lh),a',(f',l'))\<in>pr_algo_lts'"
        and [simp]: "a = project_operation a'"
[PROOF STATE]
proof (prove)
using this:
((fh, lh), a, f', l') \<in> pr_algo_lts

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>((fh, lh), a', f', l') \<in> pr_algo_lts'; a = project_operation a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e. \<lbrakk>\<And>a'. \<lbrakk>((fh, lh), a', f', l') \<in> pr_algo_lts'; a = project_operation a'\<rbrakk> \<Longrightarrow> thesis; a = PUSH; f' = push_effect fh e; l' = lh; push_precond fh lh e\<rbrakk> \<Longrightarrow> thesis
 2. \<And>u. \<lbrakk>\<And>a'. \<lbrakk>((fh, lh), a', f', l') \<in> pr_algo_lts'; a = project_operation a'\<rbrakk> \<Longrightarrow> thesis; a = RELABEL; f' = fh; l' = relabel_effect fh lh u; relabel_precond fh lh u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto
          simp: push_precond_eq_sat_or_nonsat
          dest: relabel'[OF HBL] nonsat_push'[OF HBL] sat_push'[OF HBL])
[PROOF STATE]
proof (state)
this:
((fh, lh), a', f', l') \<in> pr_algo_lts'
a = project_operation a'

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
note HBL' =
      Height_Bounded_Labeling.pr_algo_maintains_hb_labeling[OF HBL LAST]
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t f' l'

goal (1 subgoal):
 1. \<And>x xs f' l'. \<lbrakk>\<And>f' l'. ((f, l), xs, f', l') \<in> trcl pr_algo_lts \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs = map project_operation p'; ((f, l), xs @ [x], f', l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> xs @ [x] = map project_operation p'
[PROOF STEP]
from HBL' trcl_rev_cons[OF PP' LAST']
[PROOF STATE]
proof (chain)
picking this:
Height_Bounded_Labeling c s t f' l'
((f, l), p' @ [a'], f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Height_Bounded_Labeling c s t f' l'
((f, l), p' @ [a'], f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. \<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p @ [a] = map project_operation p'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p @ [a] = map project_operation p'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with assms that
[PROOF STATE]
proof (chain)
picking this:
((f, l), p, f', l') \<in> trcl pr_algo_lts
\<lbrakk>((f, l), ?p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation ?p'\<rbrakk> \<Longrightarrow> thesis
\<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts
\<lbrakk>((f, l), ?p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation ?p'\<rbrakk> \<Longrightarrow> thesis
\<exists>p'. Height_Bounded_Labeling c s t f' l' \<and> ((f, l), p', f', l') \<in> trcl pr_algo_lts' \<and> p = map project_operation p'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma xfer_relabel_bound:
  assumes BOUND: "\<forall>p'. ((f,l),p',(f',l')) \<in> trcl pr_algo_lts'
          \<longrightarrow> length (filter is_RELABEL' p') \<le> B"
  assumes RUN: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  shows "length (filter is_RELABEL p) \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
from xfer_run[OF RUN]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p'
    where RUN': "((f,l),p',(f',l')) \<in> trcl pr_algo_lts'"
      and [simp]: "p = map project_operation p'"
[PROOF STATE]
proof (prove)
using this:
(\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((f, l), p', f', l') \<in> trcl pr_algo_lts'
p = map project_operation p'

goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
have "length (filter is_RELABEL p) = length (filter is_RELABEL' p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_RELABEL p) = length (filter is_RELABEL' p')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL p) = length (filter is_RELABEL' p')

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

goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
from BOUND[rule_format,OF RUN']
[PROOF STATE]
proof (chain)
picking this:
length (filter is_RELABEL' p') \<le> B
[PROOF STEP]
have "length (filter is_RELABEL' p') \<le> B"
[PROOF STATE]
proof (prove)
using this:
length (filter is_RELABEL' p') \<le> B

goal (1 subgoal):
 1. length (filter is_RELABEL' p') \<le> B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL' p') \<le> B

goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (filter is_RELABEL p) \<le> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (filter is_RELABEL p) \<le> B

goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL p) \<le> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma xfer_push_bounds:
  assumes BOUND_SAT: "\<forall>p'. ((f,l),p',(f',l')) \<in> trcl pr_algo_lts'
          \<longrightarrow> length (filter is_SAT_PUSH' p') \<le> B1"
  assumes BOUND_NONSAT: "\<forall>p'. ((f,l),p',(f',l')) \<in> trcl pr_algo_lts'
          \<longrightarrow> length (filter is_NONSAT_PUSH' p') \<le> B2"
  assumes RUN: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  shows "length (filter is_PUSH p) \<le> B1 + B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
from xfer_run[OF RUN]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p'
    where RUN': "((f,l),p',(f',l')) \<in> trcl pr_algo_lts'"
      and [simp]: "p = map project_operation p'"
[PROOF STATE]
proof (prove)
using this:
(\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>((f, l), p', f', l') \<in> trcl pr_algo_lts'; p = map project_operation p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((f, l), p', f', l') \<in> trcl pr_algo_lts'
p = map project_operation p'

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
have [simp]: "length [x\<leftarrow>p' . is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x]
    = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x) p') = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')
[PROOF STEP]
by (induction p') auto
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x) p') = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
have "length (filter is_PUSH p)
    = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_PUSH p) = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) = length (filter is_SAT_PUSH' p') + length (filter is_NONSAT_PUSH' p')

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
note BOUND_SAT[rule_format,OF RUN']
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p') \<le> B1

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p') \<le> B1

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
note BOUND_NONSAT[rule_format,OF RUN']
[PROOF STATE]
proof (state)
this:
length (filter is_NONSAT_PUSH' p') \<le> B2

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_NONSAT_PUSH' p') \<le> y + length (filter is_NONSAT_PUSH' p'); \<And>x y. x \<le> y \<Longrightarrow> B1 + x \<le> B1 + y\<rbrakk> \<Longrightarrow> length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + length (filter is_NONSAT_PUSH' p') \<le> y + length (filter is_NONSAT_PUSH' p'); \<And>x y. x \<le> y \<Longrightarrow> B1 + x \<le> B1 + y\<rbrakk> \<Longrightarrow> length (filter is_PUSH p) \<le> B1 + B2

goal (1 subgoal):
 1. length (filter is_PUSH p) \<le> B1 + B2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter is_PUSH p) \<le> B1 + B2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Network) relabel_action_bound':
  assumes A: "(fxl,p,fxl') \<in> trcl pr_algo_lts'"
  shows "length (filter (is_RELABEL') p) \<le> 2 * (card V)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
(fxl, p, fxl') \<in> trcl pr_algo_lts'
[PROOF STEP]
have "length (filter (is_RELABEL') p) \<le> sum_heights_measure (snd fxl)"
[PROOF STATE]
proof (prove)
using this:
(fxl, p, fxl') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> sum_heights_measure (snd fxl)
[PROOF STEP]
apply (induction rule: trcl.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. length (filter is_RELABEL' []) \<le> sum_heights_measure (snd c)
 2. \<And>c a c' w c''. \<lbrakk>(c, a, c') \<in> pr_algo_lts'; (c', w, c'') \<in> trcl pr_algo_lts'; length (filter is_RELABEL' w) \<le> sum_heights_measure (snd c')\<rbrakk> \<Longrightarrow> length (filter is_RELABEL' (a # w)) \<le> sum_heights_measure (snd c)
[PROOF STEP]
apply (auto elim!: pr_algo_lts'.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w ac bb f l u. \<lbrakk>((f, relabel_effect f l u), w, ac, bb) \<in> trcl pr_algo_lts'; length (filter is_RELABEL' w) \<le> sum_heights_measure (relabel_effect f l u); Height_Bounded_Labeling c s t f l; relabel_precond f l u\<rbrakk> \<Longrightarrow> Suc (length (filter is_RELABEL' w)) \<le> sum_heights_measure l
[PROOF STEP]
apply (drule (1) Height_Bounded_Labeling.relabel_measure)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w ac bb f l u. \<lbrakk>((f, relabel_effect f l u), w, ac, bb) \<in> trcl pr_algo_lts'; length (filter is_RELABEL' w) \<le> sum_heights_measure (relabel_effect f l u); relabel_precond f l u; sum_heights_measure (relabel_effect f l u) < sum_heights_measure l\<rbrakk> \<Longrightarrow> Suc (length (filter is_RELABEL' w)) \<le> sum_heights_measure l
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL' p) \<le> sum_heights_measure (snd fxl)

goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_RELABEL' p) \<le> sum_heights_measure (snd fxl)

goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
note sum_height_measure_is_OV2
[PROOF STATE]
proof (state)
this:
sum_heights_measure ?l \<le> 2 * (card V)\<^sup>2

goal (1 subgoal):
 1. length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
show "length (filter (is_RELABEL') p) \<le> 2 * (card V)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
length (filter is_RELABEL' p) \<le> 2 * (card V)\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Height_Bounded_Labeling) relabel_action_bound:
  assumes A: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts"
  shows "length (filter (is_RELABEL) p) \<le> 2 * (card V)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
using xfer_relabel_bound relabel_action_bound' A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>p'. ((f, l), p', ?f', ?l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter is_RELABEL' p') \<le> ?B; ((f, l), ?p, ?f', ?l') \<in> trcl pr_algo_lts\<rbrakk> \<Longrightarrow> length (filter is_RELABEL ?p) \<le> ?B
(?fxl, ?p, ?fxl') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter is_RELABEL' ?p) \<le> 2 * (card V)\<^sup>2
((f, l), p, f', l') \<in> trcl pr_algo_lts

goal (1 subgoal):
 1. length (filter is_RELABEL p) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
by meson


[STATEMENT]
lemma labels_path_increasing:
  assumes "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'"
  shows "l u \<le> l' u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l u \<le> l' u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. l u \<le> l' u
[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> l u \<le> l' u
 2. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[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> l u \<le> l' u
 2. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. l u \<le> l' u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l u \<le> l' u

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. ((f, l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[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> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
((?f, ?l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> ?l u \<le> l' u
((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> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((?f, ?l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> ?l u \<le> l' u
((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')): trcl pr_algo_lts'"
[PROOF STATE]
proof (prove)
using this:
((?f, ?l), p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> ?l u \<le> l' u
((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> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[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> l u \<le> l' u; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
from FIRST Cons.IH[OF PP]
[PROOF STATE]
proof (chain)
picking this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
lh u \<le> l' u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
lh u \<le> l' u

goal (1 subgoal):
 1. l u \<le> l' u
[PROOF STEP]
apply (auto elim!: pr_algo_lts'.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>relabel_effect f l ua u \<le> l' u; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
using relabel_increase_u relabel_preserve_other
[PROOF STATE]
proof (prove)
using this:
relabel_precond f l ?u \<Longrightarrow> l ?u < relabel_effect f l ?u ?u
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v

goal (1 subgoal):
 1. \<And>ua. \<lbrakk>relabel_effect f l ua u \<le> l' u; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua\<rbrakk> \<Longrightarrow> l u \<le> l' u
[PROOF STEP]
by (metis le_trans nat_le_linear not_less)
[PROOF STATE]
proof (state)
this:
l u \<le> l' u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma edge_reappears_at_increased_labeling:
  assumes "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'"
  assumes "l u \<ge> l v + 1"
  assumes "(u,v) \<notin> cfE_of f"
  assumes E': "(u,v) \<in> cfE_of f'"
  shows "l v < l' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
proof (induction p arbitrary: f l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f l. \<lbrakk>((f, l), [], f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f

goal (2 subgoals):
 1. \<And>f l. \<lbrakk>((f, l), [], f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
using E'
[PROOF STATE]
proof (prove)
using this:
((f, l), [], f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f
(u, v) \<in> cfE_of f'

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l v < l' v

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>((?f, ?l), p, f', l') \<in> trcl pr_algo_lts'; ?l v + 1 \<le> ?l u; (u, v) \<notin> cfE_of ?f\<rbrakk> \<Longrightarrow> ?l v < l' v
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>((?f, ?l), p, f', l') \<in> trcl pr_algo_lts'; ?l v + 1 \<le> ?l u; (u, v) \<notin> cfE_of ?f\<rbrakk> \<Longrightarrow> ?l v < l' v
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f
[PROOF STEP]
obtain fh lh
    where FIRST: "((f,l),a,(fh,lh)) \<in> pr_algo_lts'"
      and PP: "((fh,lh),p,(f',l')): trcl pr_algo_lts'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>((?f, ?l), p, f', l') \<in> trcl pr_algo_lts'; ?l v + 1 \<le> ?l u; (u, v) \<notin> cfE_of ?f\<rbrakk> \<Longrightarrow> ?l v < l' v
((f, l), a # p, f', l') \<in> trcl pr_algo_lts'
l v + 1 \<le> l u
(u, v) \<notin> cfE_of f

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. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[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. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
consider
    (push) u' v'
      where "push_precond f l (u',v')" "fh = push_effect f (u',v')" "lh=l"
  | (relabel) u'
      where "relabel_precond f l u'" "fh=f" "lh=relabel_effect f l u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> thesis; \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using FIRST
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'

goal (1 subgoal):
 1. \<lbrakk>\<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> thesis; \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: pr_algo_lts'.cases simp: push_precond_eq_sat_or_nonsat)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> ?thesis; \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; l v + 1 \<le> l u; (u, v) \<notin> cfE_of f\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> ?thesis; \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> ?thesis; \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
case push
[PROOF STATE]
proof (state)
this:
push_precond f l (u', v')
fh = push_effect f (u', v')
lh = l

goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
note [simp] = push(2,3)
[PROOF STATE]
proof (state)
this:
fh = push_effect f (u', v')
lh = l

goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
text \<open>The push operation cannot go on edge \<open>(u,v)\<close> or \<open>(v,u)\<close>\<close>
[PROOF STATE]
proof (state)
this:
fh = push_effect f (u', v')
lh = l

goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
from push(1)
[PROOF STATE]
proof (chain)
picking this:
push_precond f l (u', v')
[PROOF STEP]
have "(u',v')\<noteq>(u,v)" "(u',v')\<noteq>(v,u)" "(u',v')\<in>cf.E"
[PROOF STATE]
proof (prove)
using this:
push_precond f l (u', v')

goal (1 subgoal):
 1. (u', v') \<noteq> (u, v) &&& (u', v') \<noteq> (v, u) &&& (u', v') \<in> cf.E
[PROOF STEP]
using \<open>l u \<ge> l v + 1\<close> \<open>(u,v)\<notin>cf.E\<close>
[PROOF STATE]
proof (prove)
using this:
push_precond f l (u', v')
l v + 1 \<le> l u
(u, v) \<notin> cf.E

goal (1 subgoal):
 1. (u', v') \<noteq> (u, v) &&& (u', v') \<noteq> (v, u) &&& (u', v') \<in> cf.E
[PROOF STEP]
by (auto simp: push_precond_def)
[PROOF STATE]
proof (state)
this:
(u', v') \<noteq> (u, v)
(u', v') \<noteq> (v, u)
(u', v') \<in> cf.E

goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
hence NE': "(u,v)\<notin>cfE_of fh"
[PROOF STATE]
proof (prove)
using this:
(u', v') \<noteq> (u, v)
(u', v') \<noteq> (v, u)
(u', v') \<in> cf.E

goal (1 subgoal):
 1. (u, v) \<notin> cfE_of fh
[PROOF STEP]
using \<open>(u,v)\<notin>cf.E\<close>
[PROOF STATE]
proof (prove)
using this:
(u', v') \<noteq> (u, v)
(u', v') \<noteq> (v, u)
(u', v') \<in> cf.E
(u, v) \<notin> cf.E

goal (1 subgoal):
 1. (u, v) \<notin> cfE_of fh
[PROOF STEP]
using cfE_augment_ss[of u' v' f]
[PROOF STATE]
proof (prove)
using this:
(u', v') \<noteq> (u, v)
(u', v') \<noteq> (v, u)
(u', v') \<in> cf.E
(u, v) \<notin> cf.E
(u', v') \<in> cf.E \<Longrightarrow> cfE_of (augment_edge f (u', v') ?\<Delta>) \<subseteq> insert (v', u') cf.E

goal (1 subgoal):
 1. (u, v) \<notin> cfE_of fh
[PROOF STEP]
by (auto simp: push_effect_def)
[PROOF STATE]
proof (state)
this:
(u, v) \<notin> cfE_of fh

goal (2 subgoals):
 1. \<And>u' v'. \<lbrakk>push_precond f l (u', v'); fh = push_effect f (u', v'); lh = l\<rbrakk> \<Longrightarrow> l v < l' v
 2. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
from Cons.IH[OF PP _ NE'] \<open>l u \<ge> l v + 1\<close>
[PROOF STATE]
proof (chain)
picking this:
lh v + 1 \<le> lh u \<Longrightarrow> lh v < l' v
l v + 1 \<le> l u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lh v + 1 \<le> lh u \<Longrightarrow> lh v < l' v
l v + 1 \<le> l u

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l v < l' v

goal (1 subgoal):
 1. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
case relabel
[PROOF STATE]
proof (state)
this:
relabel_precond f l u'
fh = f
lh = relabel_effect f l u'

goal (1 subgoal):
 1. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
note [simp] = relabel(2)
[PROOF STATE]
proof (state)
this:
fh = f

goal (1 subgoal):
 1. \<And>u'. \<lbrakk>relabel_precond f l u'; fh = f; lh = relabel_effect f l u'\<rbrakk> \<Longrightarrow> l v < l' v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
proof (cases "u'=v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u' = v \<Longrightarrow> l v < l' v
 2. u' \<noteq> v \<Longrightarrow> l v < l' v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u' \<noteq> v

goal (2 subgoals):
 1. u' = v \<Longrightarrow> l v < l' v
 2. u' \<noteq> v \<Longrightarrow> l v < l' v
[PROOF STEP]
from False relabel(3) relabel_preserve_other
[PROOF STATE]
proof (chain)
picking this:
u' \<noteq> v
lh = relabel_effect f l u'
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v
[PROOF STEP]
have [simp]: "lh v = l v"
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> v
lh = relabel_effect f l u'
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v

goal (1 subgoal):
 1. lh v = l v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lh v = l v

goal (2 subgoals):
 1. u' = v \<Longrightarrow> l v < l' v
 2. u' \<noteq> v \<Longrightarrow> l v < l' v
[PROOF STEP]
from False relabel(3)
           relabel_preserve_other relabel_increase_u[OF relabel(1)]
[PROOF STATE]
proof (chain)
picking this:
u' \<noteq> v
lh = relabel_effect f l u'
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v
l u' < relabel_effect f l u' u'
[PROOF STEP]
have "lh u \<ge> l u"
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> v
lh = relabel_effect f l u'
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v
l u' < relabel_effect f l u' u'

goal (1 subgoal):
 1. l u \<le> lh u
[PROOF STEP]
by (cases "u'=u") auto
[PROOF STATE]
proof (state)
this:
l u \<le> lh u

goal (2 subgoals):
 1. u' = v \<Longrightarrow> l v < l' v
 2. u' \<noteq> v \<Longrightarrow> l v < l' v
[PROOF STEP]
with \<open>l u \<ge> l v + 1\<close>
[PROOF STATE]
proof (chain)
picking this:
l v + 1 \<le> l u
l u \<le> lh u
[PROOF STEP]
have LHG: "lh u \<ge> lh v + 1"
[PROOF STATE]
proof (prove)
using this:
l v + 1 \<le> l u
l u \<le> lh u

goal (1 subgoal):
 1. lh v + 1 \<le> lh u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lh v + 1 \<le> lh u

goal (2 subgoals):
 1. u' = v \<Longrightarrow> l v < l' v
 2. u' \<noteq> v \<Longrightarrow> l v < l' v
[PROOF STEP]
from Cons.IH[OF PP LHG] \<open>(u,v)\<notin>cf.E\<close>
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<notin> cfE_of fh \<Longrightarrow> lh v < l' v
(u, v) \<notin> cf.E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(u, v) \<notin> cfE_of fh \<Longrightarrow> lh v < l' v
(u, v) \<notin> cf.E

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l v < l' v

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u' = v

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
note [simp] = relabel(3)
[PROOF STATE]
proof (state)
this:
lh = relabel_effect f l u'

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
from True relabel_increase_u[OF relabel(1)]
[PROOF STATE]
proof (chain)
picking this:
u' = v
l u' < relabel_effect f l u' u'
[PROOF STEP]
have "l v < lh v"
[PROOF STATE]
proof (prove)
using this:
u' = v
l u' < relabel_effect f l u' u'

goal (1 subgoal):
 1. l v < lh v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l v < lh v

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l v < lh v

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
note labels_path_increasing[OF PP, of v]
[PROOF STATE]
proof (state)
this:
lh v \<le> l' v

goal (1 subgoal):
 1. u' = v \<Longrightarrow> l v < l' v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l v < l' v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l v < l' v

goal (1 subgoal):
 1. l v < l' v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l v < l' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l v < l' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l v < l' v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sat_push_edge_action_bound':
  assumes "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'"
  shows "length (filter ((=) (SAT_PUSH' e)) p) \<le> 2*card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 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)
[PROOF STATE]
proof (state)
this:
e = (u, v)

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V
[PROOF STEP]
have "length (filter ((=) (SAT_PUSH' (u,v))) p) \<le> 2*card V - l v"
    if "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
proof (induction p arbitrary: f l rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs f l. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), xs, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) xs) \<le> 2 * card V - l v
[PROOF STEP]
case (1 p)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v)
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. \<And>xs f l. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), xs, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) xs) \<le> 2 * card V - l v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v)
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = []\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. \<And>a list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = []\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. \<And>a list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case [simp]: (Cons a p')
[PROOF STATE]
proof (state)
this:
p = a # p'

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from "1.prems"
[PROOF STATE]
proof (chain)
picking this:
((f, l), 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:
((f, l), 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 dest!: trcl_uncons)
[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 list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[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 list. \<lbrakk>\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v); ((f, l), p, f', l') \<in> trcl pr_algo_lts'; p = a # list\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
proof (cases "a = SAT_PUSH' (u,v)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. a \<noteq> SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
a \<noteq> SAT_PUSH' (u, v)

goal (2 subgoals):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. a \<noteq> SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from "1.IH" PP
[PROOF STATE]
proof (chain)
picking this:
\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v)
((fh, lh), p', f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
have
          "length (filter ((=) (SAT_PUSH' (u, v))) p')
          \<le> 2 * card V - lh v"
[PROOF STATE]
proof (prove)
using this:
\<forall>ys. length ys < length p \<longrightarrow> (\<forall>x xa. ((x, xa), ys, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ys) \<le> 2 * card V - xa v)
((fh, lh), p', f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - lh v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - lh v

goal (2 subgoals):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. a \<noteq> SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
with FIRST
[PROOF STATE]
proof (chain)
picking this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - lh v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - lh v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
apply (cases; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
fix ua :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
assume a1: "length (filter ((=) (SAT_PUSH' (u, v))) p')
                    \<le> 2 * card V - relabel_effect f l ua v"
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v

goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
assume a2: "relabel_precond f l ua"
[PROOF STATE]
proof (state)
this:
relabel_precond f l ua

goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
have "2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v
          \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
using a1 order_trans
[PROOF STATE]
proof (prove)
using this:
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. 2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v

goal (1 subgoal):
 1. \<And>ua. \<lbrakk>length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v; a = RELABEL'; fh = f; lh = relabel_effect f l ua; Height_Bounded_Labeling c s t f l; relabel_precond f l ua; ((f, l), RELABEL', f, relabel_effect f l ua) \<in> pr_algo_lts'\<rbrakk> \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
show "length (filter ((=) (SAT_PUSH' (u, v))) p')
                    \<le> 2 * card V - l v"
[PROOF STATE]
proof (prove)
using this:
2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
using a2 a1
[PROOF STATE]
proof (prove)
using this:
2 * card V - relabel_effect f l ua v \<le> 2 * card V - l v \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
relabel_precond f l ua
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - relabel_effect f l ua v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v
[PROOF STEP]
by (metis (no_types) Labeling.relabel_increase_u
                Labeling_axioms diff_le_mono2 nat_less_le
                relabel_preserve_other)
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p') \<le> 2 * card V - l v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case [simp]: True
[PROOF STATE]
proof (state)
this:
a = SAT_PUSH' (u, v)

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from FIRST
[PROOF STATE]
proof (chain)
picking this:
((f, l), a, fh, lh) \<in> pr_algo_lts'
[PROOF STEP]
have
          [simp]: "fh = push_effect f (u,v)" "lh = l"
          and PRE: "sat_push_precond f l (u,v)"
[PROOF STATE]
proof (prove)
using this:
((f, l), a, fh, lh) \<in> pr_algo_lts'

goal (1 subgoal):
 1. (fh = push_effect f (u, v) &&& lh = l) &&& sat_push_precond f l (u, v)
[PROOF STEP]
by (auto elim !: pr_algo_lts'.cases)
[PROOF STATE]
proof (state)
this:
fh = push_effect f (u, v)
lh = l
sat_push_precond f l (u, v)

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from PRE
[PROOF STATE]
proof (chain)
picking this:
sat_push_precond f l (u, v)
[PROOF STEP]
have "(u,v)\<in>cf.E" "l u = l v + 1"
[PROOF STATE]
proof (prove)
using this:
sat_push_precond f l (u, v)

goal (1 subgoal):
 1. (u, v) \<in> cf.E &&& l u = l v + 1
[PROOF STEP]
unfolding sat_push_precond_def
[PROOF STATE]
proof (prove)
using this:
case (u, v) of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> cf (u, v) \<le> excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1

goal (1 subgoal):
 1. (u, v) \<in> cf.E &&& l u = l v + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cf.E
l u = l v + 1

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
hence "u\<in>V" "v\<in>V" "u\<noteq>v"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cf.E
l u = l v + 1

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

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

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
have UVNEH: "(u,v)\<notin>cfE_of fh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<notin> cfE_of fh
[PROOF STEP]
using \<open>u\<noteq>v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v

goal (1 subgoal):
 1. (u, v) \<notin> cfE_of fh
[PROOF STEP]
apply (simp
                  add: sat_push_alt[OF PRE] augment_edge_cf'[OF \<open>(u,v)\<in>cf.E\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (u, v) \<notin> Graph.E (cf((u, v) := 0::'capacity, (v, u) := cf (v, u) + cf (u, v)))
[PROOF STEP]
unfolding Graph.E_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (u, v) \<notin> {(ua, va). (cf((u, v) := 0::'capacity, (v, u) := cf (v, u) + cf (u, v))) (ua, va) \<noteq> (0::'capacity)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(u, v) \<notin> cfE_of fh

goal (1 subgoal):
 1. a = SAT_PUSH' (u, v) \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
proof (cases "SAT_PUSH' (u,v) \<in> set p'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. SAT_PUSH' (u, v) \<notin> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
SAT_PUSH' (u, v) \<notin> set p'

goal (2 subgoals):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. SAT_PUSH' (u, v) \<notin> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
hence [simp]: "filter ((=) (SAT_PUSH' (u,v))) p' = []"
[PROOF STATE]
proof (prove)
using this:
SAT_PUSH' (u, v) \<notin> set p'

goal (1 subgoal):
 1. filter ((=) (SAT_PUSH' (u, v))) p' = []
[PROOF STEP]
by (induction p') auto
[PROOF STATE]
proof (state)
this:
filter ((=) (SAT_PUSH' (u, v))) p' = []

goal (2 subgoals):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
 2. SAT_PUSH' (u, v) \<notin> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
using bspec[OF height_bound \<open>u\<in>V\<close>]
[PROOF STATE]
proof (prove)
using this:
l u \<le> 2 * card V - 1

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
using bspec[OF height_bound \<open>v\<in>V\<close>]
[PROOF STATE]
proof (prove)
using this:
l u \<le> 2 * card V - 1
l v \<le> 2 * card V - 1

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
using card_V_ge2
[PROOF STATE]
proof (prove)
using this:
l u \<le> 2 * card V - 1
l v \<le> 2 * card V - 1
2 \<le> card V

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
SAT_PUSH' (u, v) \<in> set p'

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SAT_PUSH' (u, v) \<in> set p'
[PROOF STEP]
obtain p1 p2
            where [simp]: "p'=p1@SAT_PUSH' (u,v)#p2"
              and NP1: "SAT_PUSH' (u,v) \<notin> set p1"
[PROOF STATE]
proof (prove)
using this:
SAT_PUSH' (u, v) \<in> set p'

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p' = p1 @ SAT_PUSH' (u, v) # p2; SAT_PUSH' (u, v) \<notin> set p1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_decomp_first[of _ p']
[PROOF STATE]
proof (prove)
using this:
SAT_PUSH' (u, v) \<in> set p'
(?x \<in> set p') = (\<exists>ys zs. p' = ys @ ?x # zs \<and> ?x \<notin> set ys)

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p' = p1 @ SAT_PUSH' (u, v) # p2; SAT_PUSH' (u, v) \<notin> set p1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' = p1 @ SAT_PUSH' (u, v) # p2
SAT_PUSH' (u, v) \<notin> set p1

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from NP1
[PROOF STATE]
proof (chain)
picking this:
SAT_PUSH' (u, v) \<notin> set p1
[PROOF STEP]
have [simp]: "filter ((=) (SAT_PUSH' (u,v))) p1 = []"
[PROOF STATE]
proof (prove)
using this:
SAT_PUSH' (u, v) \<notin> set p1

goal (1 subgoal):
 1. filter ((=) (SAT_PUSH' (u, v))) p1 = []
[PROOF STEP]
by (induction p1) auto
[PROOF STATE]
proof (state)
this:
filter ((=) (SAT_PUSH' (u, v))) p1 = []

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from PP
[PROOF STATE]
proof (chain)
picking this:
((fh, lh), p', f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
obtain f2 l2 f3 l3
            where P1: "((fh,lh),p1,(f2,l2)) \<in> trcl pr_algo_lts'"
              and S: "((f2,l2),SAT_PUSH' (u,v),(f3,l3)) \<in> pr_algo_lts'"
              and P2: "((f3,l3),p2,(f',l'))\<in>trcl pr_algo_lts'"
[PROOF STATE]
proof (prove)
using this:
((fh, lh), p', f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. (\<And>f2 l2 f3 l3. \<lbrakk>((fh, lh), p1, f2, l2) \<in> trcl pr_algo_lts'; ((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'; ((f3, l3), p2, f', l') \<in> trcl pr_algo_lts'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: trcl_conv)
[PROOF STATE]
proof (state)
this:
((fh, lh), p1, f2, l2) \<in> trcl pr_algo_lts'
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'
((f3, l3), p2, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from S
[PROOF STATE]
proof (chain)
picking this:
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'
[PROOF STEP]
have "(u,v)\<in>cfE_of f2" and [simp]: "l3=l2"
[PROOF STATE]
proof (prove)
using this:
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'

goal (1 subgoal):
 1. (u, v) \<in> cfE_of f2 &&& l3 = l2
[PROOF STEP]
by (auto elim!: pr_algo_lts'.cases simp: sat_push_precond_def)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cfE_of f2
l3 = l2

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
with edge_reappears_at_increased_labeling[OF P1 _ UVNEH]
            \<open>l u = l v + 1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>lh v + 1 \<le> lh u; (u, v) \<in> cfE_of f2\<rbrakk> \<Longrightarrow> lh v < l2 v
l u = l v + 1
(u, v) \<in> cfE_of f2
l3 = l2
[PROOF STEP]
have AUX1: "l v < l2 v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>lh v + 1 \<le> lh u; (u, v) \<in> cfE_of f2\<rbrakk> \<Longrightarrow> lh v < l2 v
l u = l v + 1
(u, v) \<in> cfE_of f2
l3 = l2

goal (1 subgoal):
 1. l v < l2 v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l v < l2 v

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from S
[PROOF STATE]
proof (chain)
picking this:
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'
[PROOF STEP]
interpret l2: Height_Bounded_Labeling c s t f2 l2
[PROOF STATE]
proof (prove)
using this:
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f2 l2
[PROOF STEP]
by (auto elim!: pr_algo_lts'.cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
from spec[OF "1.IH", of "SAT_PUSH' (u,v)#p2"] S P2
[PROOF STATE]
proof (chain)
picking this:
length (SAT_PUSH' (u, v) # p2) < length p \<longrightarrow> (\<forall>x xa. ((x, xa), SAT_PUSH' (u, v) # p2, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) (SAT_PUSH' (u, v) # p2)) \<le> 2 * card V - xa v)
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'
((f3, l3), p2, f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
have
            "Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2))
            \<le> 2 * card V - l2 v"
[PROOF STATE]
proof (prove)
using this:
length (SAT_PUSH' (u, v) # p2) < length p \<longrightarrow> (\<forall>x xa. ((x, xa), SAT_PUSH' (u, v) # p2, f', l') \<in> trcl pr_algo_lts' \<longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) (SAT_PUSH' (u, v) # p2)) \<le> 2 * card V - xa v)
((f2, l2), SAT_PUSH' (u, v), f3, l3) \<in> pr_algo_lts'
((f3, l3), p2, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2)) \<le> 2 * card V - l2 v
[PROOF STEP]
by (auto simp: trcl_conv)
[PROOF STATE]
proof (state)
this:
Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2)) \<le> 2 * card V - l2 v

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2)) \<le> 2 * card V - l2 v

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
have "\<dots> + 1 \<le> 2*card V - l v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * card V - l2 v + 1 \<le> 2 * card V - l v
[PROOF STEP]
using AUX1
[PROOF STATE]
proof (prove)
using this:
l v < l2 v

goal (1 subgoal):
 1. 2 * card V - l2 v + 1 \<le> 2 * card V - l v
[PROOF STEP]
using bspec[OF l2.height_bound \<open>u\<in>V\<close>]
[PROOF STATE]
proof (prove)
using this:
l v < l2 v
l2 u \<le> 2 * card V - 1

goal (1 subgoal):
 1. 2 * card V - l2 v + 1 \<le> 2 * card V - l v
[PROOF STEP]
using bspec[OF l2.height_bound \<open>v\<in>V\<close>]
[PROOF STATE]
proof (prove)
using this:
l v < l2 v
l2 u \<le> 2 * card V - 1
l2 v \<le> 2 * card V - 1

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

goal (1 subgoal):
 1. SAT_PUSH' (u, v) \<in> set p' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 1 \<le> y + 1) \<Longrightarrow> Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2)) + 1 \<le> 2 * card V - l v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x + 1 \<le> y + 1) \<Longrightarrow> Suc (length (filter ((=) (SAT_PUSH' (u, v))) p2)) + 1 \<le> 2 * card V - l v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' (u, v))) p) \<le> 2 * card V - l v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((f, l), ?p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ?p) \<le> 2 * card V - l v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((f, l), ?p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ?p) \<le> 2 * card V - l v

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((f, l), ?p, f', l') \<in> trcl pr_algo_lts' \<Longrightarrow> length (filter ((=) (SAT_PUSH' (u, v))) ?p) \<le> 2 * card V - l v
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length (filter ((=) (SAT_PUSH' e)) p) \<le> 2 * card V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sat_push_action_bound':
  assumes A: "((f,l),p,(f',l')) \<in> trcl pr_algo_lts'"
  shows "length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'
[PROOF STEP]
have IN_E: "e\<in>E\<union>E\<inverse>" if "SAT_PUSH' e \<in> set p" for e
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'

goal (1 subgoal):
 1. e \<in> E \<union> E\<inverse>
[PROOF STEP]
using that cfE_of_ss_invE
[PROOF STATE]
proof (prove)
using this:
((f, l), p, f', l') \<in> trcl pr_algo_lts'
SAT_PUSH' e \<in> set p
cfE_of ?cf \<subseteq> E \<union> E\<inverse>

goal (1 subgoal):
 1. e \<in> E \<union> E\<inverse>
[PROOF STEP]
apply (induction p arbitrary: f l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f l. \<lbrakk>((f, l), [], f', l') \<in> trcl pr_algo_lts'; SAT_PUSH' e \<in> set []; \<And>cf. cfE_of cf \<subseteq> E \<union> E\<inverse>\<rbrakk> \<Longrightarrow> e \<in> E \<union> E\<inverse>
 2. \<And>a p f l. \<lbrakk>\<And>f l. \<lbrakk>((f, l), p, f', l') \<in> trcl pr_algo_lts'; SAT_PUSH' e \<in> set p; \<And>cf. cfE_of cf \<subseteq> E \<union> E\<inverse>\<rbrakk> \<Longrightarrow> e \<in> E \<union> E\<inverse>; ((f, l), a # p, f', l') \<in> trcl pr_algo_lts'; SAT_PUSH' e \<in> set (a # p); \<And>cf. cfE_of cf \<subseteq> E \<union> E\<inverse>\<rbrakk> \<Longrightarrow> e \<in> E \<union> E\<inverse>
[PROOF STEP]
apply (auto
        simp: trcl_conv sat_push_precond_def
        elim!: pr_algo_lts'.cases
      ; blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
SAT_PUSH' ?e \<in> set p \<Longrightarrow> ?e \<in> E \<union> E\<inverse>

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
have AUX: "length (filter (\<lambda>a. \<exists>e\<in>S. a = SAT_PUSH' e) p)
    = (\<Sum>e\<in>S. length (filter ((=) (SAT_PUSH' e)) p))" if "finite S" for S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>a. \<exists>e\<in>S. a = SAT_PUSH' e) p) = (\<Sum>e\<in>S. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. length (filter (\<lambda>a. \<exists>e\<in>S. a = SAT_PUSH' e) p) = (\<Sum>e\<in>S. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (filter (\<lambda>a. \<exists>e\<in>{}. a = SAT_PUSH' e) p) = (\<Sum>e\<in>{}. length (filter ((=) (SAT_PUSH' e)) p))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; length (filter (\<lambda>a. \<exists>e\<in>F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))\<rbrakk> \<Longrightarrow> length (filter (\<lambda>a. \<exists>e\<in>insert x F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>insert x F. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; length (filter (\<lambda>a. \<exists>e\<in>F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))\<rbrakk> \<Longrightarrow> length (filter (\<lambda>a. \<exists>e\<in>insert x F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>insert x F. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>finite F; (a, b) \<notin> F; length (filter (\<lambda>a. \<exists>e\<in>F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))\<rbrakk> \<Longrightarrow> length (filter (\<lambda>aa. aa = SAT_PUSH' (a, b) \<or> (\<exists>e\<in>F. aa = SAT_PUSH' e)) p) = length (filter ((=) (SAT_PUSH' (a, b))) p) + (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
apply (subst length_filter_disj_or_conv; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>finite F; (a, b) \<notin> F; length (filter (\<lambda>a. \<exists>e\<in>F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))\<rbrakk> \<Longrightarrow> length (filter (\<lambda>aa. aa = SAT_PUSH' (a, b)) p) = length (filter ((=) (SAT_PUSH' (a, b))) p)
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b F. \<lbrakk>finite F; (a, b) \<notin> F; length (filter (\<lambda>a. \<exists>e\<in>F. a = SAT_PUSH' e) p) = (\<Sum>e\<in>F. length (filter ((=) (SAT_PUSH' e)) p))\<rbrakk> \<Longrightarrow> filter (\<lambda>aa. aa = SAT_PUSH' (a, b)) p = filter ((=) (SAT_PUSH' (a, b))) p
[PROOF STEP]
subgoal premises
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>aa. aa = SAT_PUSH' (a_, b_)) p = filter ((=) (SAT_PUSH' (a_, b_))) p
[PROOF STEP]
by (induction p) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
finite ?S \<Longrightarrow> length (filter (\<lambda>a. \<exists>e\<in>?S. a = SAT_PUSH' e) p) = (\<Sum>e\<in>?S. length (filter ((=) (SAT_PUSH' e)) p))

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
have "is_SAT_PUSH' a = (\<exists>e\<in>E\<union>E\<inverse>. a = SAT_PUSH' e)" if "a\<in>set p" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_SAT_PUSH' a = (\<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e)
[PROOF STEP]
using IN_E that
[PROOF STATE]
proof (prove)
using this:
SAT_PUSH' ?e \<in> set p \<Longrightarrow> ?e \<in> E \<union> E\<inverse>
a \<in> set p

goal (1 subgoal):
 1. is_SAT_PUSH' a = (\<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
?a \<in> set p \<Longrightarrow> is_SAT_PUSH' ?a = (\<exists>e\<in>E \<union> E\<inverse>. ?a = SAT_PUSH' e)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
hence "length (filter is_SAT_PUSH' p)
    = length (filter (\<lambda>a. \<exists>e\<in>E\<union>E\<inverse>. a = SAT_PUSH' e) p)"
[PROOF STATE]
proof (prove)
using this:
?a \<in> set p \<Longrightarrow> is_SAT_PUSH' ?a = (\<exists>e\<in>E \<union> E\<inverse>. ?a = SAT_PUSH' e)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) = length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p)
[PROOF STEP]
by (auto cong: filter_cong)
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p) = length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p) = length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
have "\<dots> = (\<Sum>e\<in>E\<union>E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p) = (\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p))
[PROOF STEP]
by (auto simp: AUX)
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p) = (\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p))

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>a. \<exists>e\<in>E \<union> E\<inverse>. a = SAT_PUSH' e) p) = (\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p))

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
have "\<dots> \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p)) \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)
[PROOF STEP]
using sum_mono[OF sat_push_edge_action_bound'[OF A], where K="E\<union>E\<inverse>"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' (?e1 i))) p)) \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)

goal (1 subgoal):
 1. (\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p)) \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p)) \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>e\<in>E \<union> E\<inverse>. length (filter ((=) (SAT_PUSH' e)) p)) \<le> (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V)

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
have "\<dots> \<le> 4 * card V * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V) \<le> 4 * card V * card E
[PROOF STEP]
using card_Un_le[of E "E\<inverse>"]
[PROOF STATE]
proof (prove)
using this:
card (E \<union> E\<inverse>) \<le> card E + card (E\<inverse>)

goal (1 subgoal):
 1. (\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V) \<le> 4 * card V * card E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>E \<union> E\<inverse>. 2 * card V) \<le> 4 * card V * card E

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
show "length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E"
[PROOF STATE]
proof (prove)
using this:
length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E

goal (1 subgoal):
 1. length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (filter is_SAT_PUSH' p) \<le> 4 * card V * card E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonsat_potential_bound:
  shows "nonsat_potential f l \<le> 2 * (card V)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "nonsat_potential f l = (\<Sum>v\<in>{v \<in> V. 0 < excess f v}. l v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential f l = (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v)
[PROOF STEP]
unfolding nonsat_potential_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum l {v \<in> V. (0::'a) < excess f v} = (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nonsat_potential f l = (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nonsat_potential f l = (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "\<dots> \<le> (\<Sum>v\<in>V. l v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V
[PROOF STEP]
have f1:"{v \<in> V. 0 < excess f v} \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f v} \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v \<in> V. (0::'a) < excess f v} \<subseteq> V

goal (1 subgoal):
 1. (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{v \<in> V. (0::'a) < excess f v} \<subseteq> V

goal (1 subgoal):
 1. (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V
[PROOF STEP]
using sum.subset_diff[OF f1 finite_V, of l]
[PROOF STATE]
proof (prove)
using this:
{v \<in> V. (0::'a) < excess f v} \<subseteq> V
sum l V = sum l (V - {v \<in> V. (0::'a) < excess f v}) + sum l {v \<in> V. (0::'a) < excess f v}

goal (1 subgoal):
 1. (\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v | v \<in> V \<and> (0::'a) < excess f v. l v) \<le> sum l V

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "\<dots>  \<le> (\<Sum>v\<in>V. 2 * card V - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum l V \<le> (\<Sum>v\<in>V. 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. sum l V \<le> (\<Sum>v\<in>V. 2 * card V - 1)
[PROOF STEP]
by (meson sum_mono)
[PROOF STATE]
proof (state)
this:
sum l V \<le> (\<Sum>v\<in>V. 2 * card V - 1)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum l V \<le> (\<Sum>v\<in>V. 2 * card V - 1)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "\<dots> = card V * (2 * card V - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - 1) = card V * (2 * card V - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V - 1) = card V * (2 * card V - 1)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V - 1) = card V * (2 * card V - 1)

goal (1 subgoal):
 1. nonsat_potential f l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "card V * (2 * card V - 1) \<le> 2 * card V * card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V * (2 * card V - 1) \<le> 2 * card V * card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card V * (2 * card V - 1) \<le> 2 * card V * card V

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonsat_push_decr_nonsat_potential:
  assumes "nonsat_push_precond f l e"
  shows "nonsat_potential (push_effect f e) l < nonsat_potential f l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l < nonsat_potential f l
[PROOF STEP]
proof (cases e)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> nonsat_potential (push_effect f e) l < nonsat_potential f l
[PROOF STEP]
case [simp]: (Pair u v)
[PROOF STATE]
proof (state)
this:
e = (u, v)

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> nonsat_potential (push_effect f e) l < nonsat_potential f l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential (push_effect f e) l < nonsat_potential f l
[PROOF STEP]
proof simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential (push_effect f (u, v)) l < nonsat_potential f l
[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]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. push_precond f l (u, v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nonsat_push_precond f l e

goal (1 subgoal):
 1. push_precond f l (u, v)
[PROOF STEP]
by (simp add: push_precond_eq_sat_or_nonsat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
note [simp] = nonsat_push_\<Delta>[OF assms[simplified]]
[PROOF STATE]
proof (state)
this:
\<Delta> = excess f u

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
define S where "S={x\<in>V. x\<noteq>u \<and> x\<noteq>v \<and> 0<excess f x}"
[PROOF STATE]
proof (state)
this:
S = {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x}

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
have S_alt: "S = {x\<in>V. x\<noteq>u \<and> x\<noteq>v \<and> 0<excess f' x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x}
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x} = {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S = {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x}

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
have NES: "s\<notin>S" "u\<notin>S" "v\<notin>S"
      and [simp, intro!]: "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<notin> S &&& u \<notin> S &&& v \<notin> S) &&& finite S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<notin> {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x} &&& u \<notin> {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x} &&& v \<notin> {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x}) &&& finite {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x}
[PROOF STEP]
using excess_s_non_pos
[PROOF STATE]
proof (prove)
using this:
excess f s \<le> (0::'a)

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

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
have 1: "{v\<in>V. 0 < excess f' v} = (if s=v then S else insert v S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f' v} = (if s = v then S else insert v S)
[PROOF STEP]
unfolding S_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f' v} = (if s = v then {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x} else insert v {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x})
[PROOF STEP]
using excess_u_pos excess_non_negative' l'.excess_s_non_pos
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u
\<forall>v\<in>V - {s}. (0::'a) \<le> excess f v
excess f' s \<le> (0::'a)

goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f' v} = (if s = v then {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x} else insert v {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f' x})
[PROOF STEP]
by (auto intro!: add_nonneg_pos)
[PROOF STATE]
proof (state)
this:
{v \<in> V. (0::'a) < excess f' v} = (if s = v then S else insert v S)

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
have 2: "{v\<in>V. 0 < excess f v}
      = insert u S \<union> (if excess f v>0 then {v} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f v} = insert u S \<union> (if (0::'a) < excess f v then {v} else {})
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f v} = insert u {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x} \<union> (if (0::'a) < excess f v then {v} else {})
[PROOF STEP]
using excess_u_pos
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u

goal (1 subgoal):
 1. {v \<in> V. (0::'a) < excess f v} = insert u {x \<in> V. x \<noteq> u \<and> x \<noteq> v \<and> (0::'a) < excess f x} \<union> (if (0::'a) < excess f v then {v} else {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v \<in> V. (0::'a) < excess f v} = insert u S \<union> (if (0::'a) < excess f v then {v} else {})

goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
show "nonsat_potential f' l < nonsat_potential f l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_potential f' l < nonsat_potential f l
[PROOF STEP]
unfolding nonsat_potential_def 1 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum l (if s = v then S else insert v S) < sum l (insert u S \<union> (if (0::'a) < excess f v then {v} else {}))
[PROOF STEP]
by (cases "s=v"; cases "0<excess f v"; auto simp: NES)
[PROOF STATE]
proof (state)
this:
nonsat_potential f' l < nonsat_potential f l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nonsat_potential (push_effect f e) l < nonsat_potential f l

goal:
No subgoals!
[PROOF STEP]
qed