[STATEMENT]
lemma sestoftUnGC:
  assumes "(to_gc_conf r c) \<Rightarrow>\<^sub>G\<^sup>* d" and "heap_upds_ok_conf c" and "closed c" and "r_ok r c"
  shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d
heap_upds_ok_conf c
closed c
r_ok r c

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
proof(induction rule: rtranclp_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> to_gc_conf r c = to_gc_conf r' c' \<and> r_ok r' c'
 2. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
heap_upds_ok_conf c
closed c
r_ok r c

goal (2 subgoals):
 1. \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> to_gc_conf r c = to_gc_conf r' c' \<and> r_ok r' c'
 2. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok_conf c
closed c
r_ok r c

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> to_gc_conf r c = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> to_gc_conf r c = to_gc_conf r' c' \<and> r_ok r' c'

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
case (step d' d'')
[PROOF STATE]
proof (state)
this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d'
d' \<Rightarrow>\<^sub>G d''
\<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d' = to_gc_conf r' c' \<and> r_ok r' c'
heap_upds_ok_conf c
closed c
r_ok r c

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d'
d' \<Rightarrow>\<^sub>G d''
\<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d' = to_gc_conf r' c' \<and> r_ok r' c'
heap_upds_ok_conf c
closed c
r_ok r c
[PROOF STEP]
obtain r' c' where "c \<Rightarrow>\<^sup>*  c'" and "d' = to_gc_conf r' c'" and "r_ok r' c'"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d'
d' \<Rightarrow>\<^sub>G d''
\<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d' = to_gc_conf r' c' \<and> r_ok r' c'
heap_upds_ok_conf c
closed c
r_ok r c

goal (1 subgoal):
 1. (\<And>c' r'. \<lbrakk>c \<Rightarrow>\<^sup>* c'; d' = to_gc_conf r' c'; r_ok r' c'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<Rightarrow>\<^sup>* c'
d' = to_gc_conf r' c'
r_ok r' c'

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> heap_upds_ok_invariant]  \<open>heap_upds_ok _\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_upds_ok_conf c \<Longrightarrow> heap_upds_ok_conf c'
heap_upds_ok_conf c
[PROOF STEP]
have "heap_upds_ok_conf c'"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok_conf c \<Longrightarrow> heap_upds_ok_conf c'
heap_upds_ok_conf c

goal (1 subgoal):
 1. heap_upds_ok_conf c'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
heap_upds_ok_conf c'

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> closed_invariant]  \<open>closed _\<close>
[PROOF STATE]
proof (chain)
picking this:
closed c \<Longrightarrow> closed c'
closed c
[PROOF STEP]
have "closed c'"
[PROOF STATE]
proof (prove)
using this:
closed c \<Longrightarrow> closed c'
closed c

goal (1 subgoal):
 1. closed c'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
closed c'

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from step \<open>d' = to_gc_conf r' c'\<close>
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d'
d' \<Rightarrow>\<^sub>G d''
\<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d' = to_gc_conf r' c' \<and> r_ok r' c'
heap_upds_ok_conf c
closed c
r_ok r c
d' = to_gc_conf r' c'
[PROOF STEP]
have "to_gc_conf r' c' \<Rightarrow>\<^sub>G d''"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* d'
d' \<Rightarrow>\<^sub>G d''
\<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d' = to_gc_conf r' c' \<and> r_ok r' c'
heap_upds_ok_conf c
closed c
r_ok r c
d' = to_gc_conf r' c'

goal (1 subgoal):
 1. to_gc_conf r' c' \<Rightarrow>\<^sub>G d''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
to_gc_conf r' c' \<Rightarrow>\<^sub>G d''

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from this \<open>heap_upds_ok_conf c'\<close> \<open>closed c'\<close> \<open>r_ok r' c'\<close>
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r' c' \<Rightarrow>\<^sub>G d''
heap_upds_ok_conf c'
closed c'
r_ok r' c'
[PROOF STEP]
have "\<exists> r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r' c' \<Rightarrow>\<^sub>G d''
heap_upds_ok_conf c'
closed c'
r_ok r' c'

goal (1 subgoal):
 1. \<exists>r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''
[PROOF STEP]
by (rule sestoftUnGCstep)
[PROOF STATE]
proof (state)
this:
\<exists>r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''
[PROOF STEP]
obtain r'' c'' where "c' \<Rightarrow>\<^sup>* c''" and "d'' = to_gc_conf r'' c''" and "r_ok r'' c''"
[PROOF STATE]
proof (prove)
using this:
\<exists>r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''

goal (1 subgoal):
 1. (\<And>c'' r''. \<lbrakk>c' \<Rightarrow>\<^sup>* c''; d'' = to_gc_conf r'' c''; r_ok r'' c''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c' \<Rightarrow>\<^sup>* c''
d'' = to_gc_conf r'' c''
r_ok r'' c''

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from \<open>c' \<Rightarrow>\<^sup>*  c''\<close> \<open>c \<Rightarrow>\<^sup>*  c'\<close>
[PROOF STATE]
proof (chain)
picking this:
c' \<Rightarrow>\<^sup>* c''
c \<Rightarrow>\<^sup>* c'
[PROOF STEP]
have "c \<Rightarrow>\<^sup>* c''"
[PROOF STATE]
proof (prove)
using this:
c' \<Rightarrow>\<^sup>* c''
c \<Rightarrow>\<^sup>* c'

goal (1 subgoal):
 1. c \<Rightarrow>\<^sup>* c''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<Rightarrow>\<^sup>* c''

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>to_gc_conf r c \<Rightarrow>\<^sub>G\<^sup>* y; y \<Rightarrow>\<^sub>G z; \<lbrakk>heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> y = to_gc_conf r' c' \<and> r_ok r' c'; heap_upds_ok_conf c; closed c; r_ok r c\<rbrakk> \<Longrightarrow> \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> z = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
with \<open>d'' = _\<close> \<open>r_ok r'' c''\<close>
[PROOF STATE]
proof (chain)
picking this:
d'' = to_gc_conf r'' c''
r_ok r'' c''
c \<Rightarrow>\<^sup>* c''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
d'' = to_gc_conf r'' c''
r_ok r'' c''
c \<Rightarrow>\<^sup>* c''

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d'' = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d'' = to_gc_conf r' c' \<and> r_ok r' c'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dummies_unchanged_invariant:
  "invariant step (\<lambda> (\<Gamma>, e, S) . dummies S = V)" (is "invariant _ ?I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant (\<Rightarrow>) (\<lambda>(\<Gamma>, e, S). dummies S = V)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; case x of (\<Gamma>, e, S) \<Rightarrow> dummies S = V\<rbrakk> \<Longrightarrow> case y of (\<Gamma>, e, S) \<Rightarrow> dummies S = V
[PROOF STEP]
fix c c'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; case x of (\<Gamma>, e, S) \<Rightarrow> dummies S = V\<rbrakk> \<Longrightarrow> case y of (\<Gamma>, e, S) \<Rightarrow> dummies S = V
[PROOF STEP]
assume "c \<Rightarrow> c'" and "?I c"
[PROOF STATE]
proof (state)
this:
c \<Rightarrow> c'
case c of (\<Gamma>, e, S) \<Rightarrow> dummies S = V

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; case x of (\<Gamma>, e, S) \<Rightarrow> dummies S = V\<rbrakk> \<Longrightarrow> case y of (\<Gamma>, e, S) \<Rightarrow> dummies S = V
[PROOF STEP]
thus "?I c'"
[PROOF STATE]
proof (prove)
using this:
c \<Rightarrow> c'
case c of (\<Gamma>, e, S) \<Rightarrow> dummies S = V

goal (1 subgoal):
 1. case c' of (\<Gamma>, e, S) \<Rightarrow> dummies S = V
[PROOF STEP]
by (induction) auto
[PROOF STATE]
proof (state)
this:
case c' of (\<Gamma>, e, S) \<Rightarrow> dummies S = V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sestoftUnGC':
  assumes "([], e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>, e', map Dummy r)"
  assumes "isVal e'"
  assumes "fv e = ({}::var set)"
  shows   "\<exists> \<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1,3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>r' a aa b. ([], e, []) \<Rightarrow>\<^sup>* (a, aa, b) \<and> (\<Gamma>, e', map Dummy r) = (restrictA (- set r') a, aa, restr_stack (- set r') b @ map Dummy (rev r')) \<and> set r' \<subseteq> domA a \<union> upds b
[PROOF STEP]
obtain r' \<Gamma>' S'
  where "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')"
    and "\<Gamma> = restrictA (- set r') \<Gamma>'"
    and "map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')"
    and "r_ok r' (\<Gamma>', e', S')"
[PROOF STATE]
proof (prove)
using this:
\<exists>r' a aa b. ([], e, []) \<Rightarrow>\<^sup>* (a, aa, b) \<and> (\<Gamma>, e', map Dummy r) = (restrictA (- set r') a, aa, restr_stack (- set r') b @ map Dummy (rev r')) \<and> set r' \<subseteq> domA a \<union> upds b

goal (1 subgoal):
 1. (\<And>\<Gamma>' S' r'. \<lbrakk>([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S'); \<Gamma> = restrictA (- set r') \<Gamma>'; map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r'); r_ok r' (\<Gamma>', e', S')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')
\<Gamma> = restrictA (- set r') \<Gamma>'
map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')
r_ok r' (\<Gamma>', e', S')

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from invariant_starE[OF \<open>([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')\<close> dummies_unchanged_invariant]
[PROOF STATE]
proof (chain)
picking this:
case ([], e, []) of (\<Gamma>, e, S) \<Rightarrow> dummies S = ?V1 \<Longrightarrow> case (\<Gamma>', e', S') of (\<Gamma>, e, S) \<Rightarrow> dummies S = ?V1
[PROOF STEP]
have "dummies S' = {}"
[PROOF STATE]
proof (prove)
using this:
case ([], e, []) of (\<Gamma>, e, S) \<Rightarrow> dummies S = ?V1 \<Longrightarrow> case (\<Gamma>', e', S') of (\<Gamma>, e, S) \<Rightarrow> dummies S = ?V1

goal (1 subgoal):
 1. dummies S' = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dummies S' = {}

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
with  \<open>map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')\<close>
[PROOF STATE]
proof (chain)
picking this:
map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')
dummies S' = {}
[PROOF STEP]
have "restr_stack (- set r') S' = []" and [simp]: "r = rev r'"
[PROOF STATE]
proof (prove)
using this:
map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')
dummies S' = {}

goal (1 subgoal):
 1. restr_stack (- set r') S' = [] &&& r = rev r'
[PROOF STEP]
by (induction S' rule: restr_stack.induct) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
restr_stack (- set r') S' = []
r = rev r'

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> heap_upds_ok_invariant]
[PROOF STATE]
proof (chain)
picking this:
heap_upds_ok_conf ([], e, []) \<Longrightarrow> heap_upds_ok_conf (\<Gamma>', e', S')
[PROOF STEP]
have "heap_upds_ok (\<Gamma>', S')"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok_conf ([], e, []) \<Longrightarrow> heap_upds_ok_conf (\<Gamma>', e', S')

goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>', S')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
heap_upds_ok (\<Gamma>', S')

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from \<open>isVal e'\<close> sestoftUnGCStack[where e = e', OF \<open>heap_upds_ok (\<Gamma>', S')\<close> ]
[PROOF STATE]
proof (chain)
picking this:
isVal e'
(\<And>\<Gamma>'' S'a. \<lbrakk>(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'a); to_gc_conf ?r (\<Gamma>', e', S') = to_gc_conf ?r (\<Gamma>'', e', S'a); \<not> isVal e' \<or> safe_hd S'a = safe_hd (restr_stack (- set ?r) S'a)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<Gamma>'' S''
    where "(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')"
    and "to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')"
    and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
[PROOF STATE]
proof (prove)
using this:
isVal e'
(\<And>\<Gamma>'' S'a. \<lbrakk>(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'a); to_gc_conf ?r (\<Gamma>', e', S') = to_gc_conf ?r (\<Gamma>'', e', S'a); \<not> isVal e' \<or> safe_hd S'a = safe_hd (restr_stack (- set ?r) S'a)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<Gamma>'' S''. \<lbrakk>(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S''); to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S''); safe_hd S'' = safe_hd (restr_stack (- set r) S'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')
to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')
safe_hd S'' = safe_hd (restr_stack (- set r) S'')

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from this (2,3) \<open>restr_stack (- set r') S' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')
safe_hd S'' = safe_hd (restr_stack (- set r) S'')
restr_stack (- set r') S' = []
[PROOF STEP]
have "S'' = []"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')
safe_hd S'' = safe_hd (restr_stack (- set r) S'')
restr_stack (- set r') S' = []

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

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from  \<open>([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')\<close>  and \<open>(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')\<close> and \<open>S'' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')
(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')
S'' = []
[PROOF STEP]
have "([], e, []) \<Rightarrow>\<^sup>*  (\<Gamma>'', e', [])"
[PROOF STATE]
proof (prove)
using this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')
(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')
S'' = []

goal (1 subgoal):
 1. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
have "\<Gamma> = restrictA (- set r) \<Gamma>''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> = restrictA (- set r) \<Gamma>''
[PROOF STEP]
using \<open>to_gc_conf r _ = _\<close> \<open>\<Gamma> = _\<close>
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')
\<Gamma> = restrictA (- set r') \<Gamma>'

goal (1 subgoal):
 1. \<Gamma> = restrictA (- set r) \<Gamma>''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = restrictA (- set r) \<Gamma>''

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> = restrictA (- set r) \<Gamma>''

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
from invariant_starE[OF \<open>(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')\<close> subset_bound_invariant \<open>r_ok r' (\<Gamma>', e', S')\<close>]
[PROOF STATE]
proof (chain)
picking this:
r_ok r' (\<Gamma>'', e', S'')
[PROOF STEP]
have "set r \<subseteq> domA \<Gamma>''"
[PROOF STATE]
proof (prove)
using this:
r_ok r' (\<Gamma>'', e', S'')

goal (1 subgoal):
 1. set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
using \<open>S'' = []\<close>
[PROOF STATE]
proof (prove)
using this:
r_ok r' (\<Gamma>'', e', S'')
S'' = []

goal (1 subgoal):
 1. set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set r \<subseteq> domA \<Gamma>''

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])
\<Gamma> = restrictA (- set r) \<Gamma>''
set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])
\<Gamma> = restrictA (- set r) \<Gamma>''
set r \<subseteq> domA \<Gamma>''

goal (1 subgoal):
 1. \<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "a * b = c"
      "b * a = c"
      "b * d * a = c * d"
      "d * b * a = c * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * b = c &&& b * a = c) &&& b * d * a = c * d &&& d * b * a = c * d
[PROOF STEP]
by (subst_mod_mult_ac foo, rule refl)+


[STATEMENT]
lemma "gee a \<Longrightarrow> a * b = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gee a \<Longrightarrow> a * b = c
[PROOF STEP]
by (subst_mod_mult_ac foo, rule refl)


[STATEMENT]
lemma "d * b * a = c * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d * b * a = c * d
[PROOF STEP]
apply (subst_mod_mult_ac bar)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. gee a
 2. gee b
 3. c * d = c * d
[PROOF STEP]
oops


[STATEMENT]
lemma "f (a * b) (a * b) = rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) (a * b) = rhs
[PROOF STEP]
apply (subst_mod_mult_ac foo)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c (a * b) = rhs
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (a * b) c = rhs
[PROOF STEP]
oops


[STATEMENT]
lemma "serialize_mac 0xdeadbeefcafe = ''de:ad:be:ef:ca:fe''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_mac 244837814094590 = ''de:ad:be:ef:ca:fe''
[PROOF STEP]
by eval


[STATEMENT]
lemma "serialize_actions (\<lambda>oif. ''42'') (ofe_action serialization_test_entry) =
  ''mod_dl_dst:a6:41:f1:85:e8:62,output:42''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_actions (\<lambda>oif. ''42'') (ofe_action serialization_test_entry) = ''mod_dl_dst:a6:41:f1:85:e8:62,output:42''
[PROOF STEP]
by eval


[STATEMENT]
lemma "serialize_actions anything [] = ''drop''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_actions anything [] = ''drop''
[PROOF STEP]
by(simp add: serialize_actions_def)


[STATEMENT]
lemma "serialize_of_matches pids of_matches=
(List.append ''hard_timeout=0,idle_timeout=0,'')
  (intersperse (CHR '','') (map (serialize_of_match pids) (sorted_list_of_set of_matches)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_of_matches pids of_matches = ''hard_timeout=0,idle_timeout=0,'' @ intersperse CHR '','' (map (serialize_of_match pids) (sorted_list_of_set of_matches))
[PROOF STEP]
by (simp add: serialize_of_matches_def)


[STATEMENT]
lemma "serialize_of_matches (\<lambda>oif. ''42'') (ofe_fields serialization_test_entry) =
  ''hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_of_matches (\<lambda>oif. ''42'') (ofe_fields serialization_test_entry) = ''hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000''
[PROOF STEP]
by eval


[STATEMENT]
lemma "serialize_of_entry (the \<circ> map_of [(''s1-lan'',''42''),(''s1-wan'',''1337'')]) serialization_test_entry =
  ''priority=7,hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000,action=mod_dl_dst:a6:41:f1:85:e8:62,output:1337''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serialize_of_entry (the \<circ> map_of [(''s1-lan'', ''42''), (''s1-wan'', ''1337'')]) serialization_test_entry = ''priority=7,hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000,action=mod_dl_dst:a6:41:f1:85:e8:62,output:1337''
[PROOF STEP]
by eval


[STATEMENT]
lemma SINK_plus_current: "SINK (plus_current f g) = SINK f \<inter> SINK g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SINK (plus_current f g) = SINK f \<inter> SINK g
[PROOF STEP]
by(auto simp add: SINK.simps set_eq_iff d_OUT_def nn_integral_0_iff emeasure_count_space_eq_0 add_eq_0_iff_both_eq_0)


[STATEMENT]
lemma d_OUT_plus_web:
  fixes \<Gamma> (structure)
  shows "d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
have "?lhs = d_OUT f x + (\<Sum>\<^sup>+ y. (if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y)
[PROOF STEP]
unfolding d_OUT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. (f \<frown> g) (x, y)) = (\<Sum>\<^sup>+ y. f (x, y)) + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y)
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_OUT (f \<frown> g) x = d_OUT f x + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y)

goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_OUT (f \<frown> g) x = d_OUT f x + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y)

goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT f x + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y) = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
by(auto simp add: d_OUT_def intro!: arg_cong2[where f="(+)"] nn_integral_cong)
[PROOF STATE]
proof (state)
this:
d_OUT f x + (\<Sum>\<^sup>+ y. if x \<in> RF\<^sup>\<circ> (TER f) then 0 else g (x, y) * indicator (- RF (TER f)) y) = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x

goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x

goal (1 subgoal):
 1. d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
d_OUT (f \<frown> g) x = d_OUT f x + d_OUT (g \<upharpoonleft> \<Gamma> / f) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d_IN_plus_web:
  fixes \<Gamma> (structure)
  shows "d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
have "?lhs = d_IN f y + (\<Sum>\<^sup>+ x. (if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x)
[PROOF STEP]
unfolding d_IN_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. (f \<frown> g) (x, y)) = (\<Sum>\<^sup>+ x. f (x, y)) + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x)
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_IN (f \<frown> g) y = d_IN f y + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x)

goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_IN (f \<frown> g) y = d_IN f y + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x)

goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f y + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x) = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
by(auto simp add: d_IN_def intro!: arg_cong2[where f="(+)"] nn_integral_cong)
[PROOF STATE]
proof (state)
this:
d_IN f y + (\<Sum>\<^sup>+ x. if y \<in> RF (TER f) then 0 else g (x, y) * indicator (- RF\<^sup>\<circ> (TER f)) x) = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y

goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y

goal (1 subgoal):
 1. d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
d_IN (f \<frown> g) y = d_IN f y + d_IN (g \<upharpoonleft> \<Gamma> / f) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plus_web_greater: "f e \<le> (f \<frown>\<^bsub>\<Gamma>\<^esub> g) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e \<le> (f \<frown>\<^bsub>\<Gamma>\<^esub> g) e
[PROOF STEP]
by(cases e)(auto split: split_indicator)


[STATEMENT]
lemma current_plus_web:
  fixes \<Gamma> (structure)
  shows "\<lbrakk> current \<Gamma> f; wave \<Gamma> f; current \<Gamma> g \<rbrakk> \<Longrightarrow> current \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>current \<Gamma> f; wave \<Gamma> f; current \<Gamma> g\<rbrakk> \<Longrightarrow> current \<Gamma> (f \<frown> g)
[PROOF STEP]
by(blast intro: current_plus_current current_restrict_current)


[STATEMENT]
lemma RF_f: "x \<notin> RF\<^sup>\<circ> (TER f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> RF\<^sup>\<circ> (TER f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
assume *: "x \<in> RF\<^sup>\<circ> (TER f)"
[PROOF STATE]
proof (state)
this:
x \<in> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f \<union> TER g)
[PROOF STEP]
obtain p y where p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
    and bypass: "\<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f \<union> TER g)

goal (1 subgoal):
 1. (\<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>; \<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<E>_E) blast
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
from rtrancl_path_distinct[OF p]
[PROOF STATE]
proof (chain)
picking this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p'
    where p: "path \<Gamma> x p' y" and p': "set p' \<subseteq> set p" and distinct: "distinct (x # p')"
[PROOF STATE]
proof (prove)
using this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>path \<Gamma> x p' y; set p' \<subseteq> set p; distinct (x # p')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p' y
set p' \<subseteq> set p
distinct (x # p')

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
x \<in> RF\<^sup>\<circ> (TER f)
[PROOF STEP]
have x': "x \<in> RF (TER f)" and \<E>: "x \<notin> \<E> (TER f)"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. x \<in> RF (TER f) &&& x \<notin> \<E> (TER f)
[PROOF STEP]
by(auto simp add: roofed_circ_def)
[PROOF STATE]
proof (state)
this:
x \<in> RF (TER f)
x \<notin> \<E> (TER f)

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
hence "x \<notin> TER f"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (TER f)
x \<notin> \<E> (TER f)

goal (1 subgoal):
 1. x \<notin> TER f
[PROOF STEP]
using not_essentialD[OF _ p y] p' bypass
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (TER f)
x \<notin> \<E> (TER f)
\<not> essential \<Gamma> (B \<Gamma>) ?S x \<Longrightarrow> x \<noteq> y \<and> (\<exists>z\<in>set p'. z \<noteq> x \<and> z \<in> ?S)
set p' \<subseteq> set p
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g

goal (1 subgoal):
 1. x \<notin> TER f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<notin> TER f

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
with roofedD[OF x' p y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p'. z \<in> TER f) \<or> x \<in> TER f
x \<notin> TER f
[PROOF STEP]
obtain z where z: "z \<in> set p'" "z \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p'. z \<in> TER f) \<or> x \<in> TER f
x \<notin> TER f

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> set p'; z \<in> TER f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> set p'
z \<in> TER f

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p' y
z \<in> set p'
z \<in> TER f
[PROOF STEP]
have "y \<in> set p'"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p' y
z \<in> set p'
z \<in> TER f

goal (1 subgoal):
 1. y \<in> set p'
[PROOF STEP]
by(auto dest!: rtrancl_path_last intro: last_in_set)
[PROOF STATE]
proof (state)
this:
y \<in> set p'

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
with distinct
[PROOF STATE]
proof (chain)
picking this:
distinct (x # p')
y \<in> set p'
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
distinct (x # p')
y \<in> set p'

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> False
[PROOF STEP]
with bypass z p' distinct
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g
z \<in> set p'
z \<in> TER f
set p' \<subseteq> set p
distinct (x # p')
x \<noteq> y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g
z \<in> set p'
z \<in> TER f
set p' \<subseteq> set p
distinct (x # p')
x \<noteq> y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma RF_g: "x \<notin> RF\<^sup>\<circ> (TER g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> RF\<^sup>\<circ> (TER g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
assume *: "x \<in> RF\<^sup>\<circ> (TER g)"
[PROOF STATE]
proof (state)
this:
x \<in> RF\<^sup>\<circ> (TER g)

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f \<union> TER g)
[PROOF STEP]
obtain p y where p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
    and bypass: "\<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f \<union> TER g)

goal (1 subgoal):
 1. (\<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>; \<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<E>_E) blast
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
from rtrancl_path_distinct[OF p]
[PROOF STATE]
proof (chain)
picking this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p'
    where p: "path \<Gamma> x p' y" and p': "set p' \<subseteq> set p" and distinct: "distinct (x # p')"
[PROOF STATE]
proof (prove)
using this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>path \<Gamma> x p' y; set p' \<subseteq> set p; distinct (x # p')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p' y
set p' \<subseteq> set p
distinct (x # p')

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
x \<in> RF\<^sup>\<circ> (TER g)
[PROOF STEP]
have x': "x \<in> RF (TER g)" and \<E>: "x \<notin> \<E> (TER g)"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF\<^sup>\<circ> (TER g)

goal (1 subgoal):
 1. x \<in> RF (TER g) &&& x \<notin> \<E> (TER g)
[PROOF STEP]
by(auto simp add: roofed_circ_def)
[PROOF STATE]
proof (state)
this:
x \<in> RF (TER g)
x \<notin> \<E> (TER g)

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
hence "x \<notin> TER g"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (TER g)
x \<notin> \<E> (TER g)

goal (1 subgoal):
 1. x \<notin> TER g
[PROOF STEP]
using not_essentialD[OF _ p y] p' bypass
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (TER g)
x \<notin> \<E> (TER g)
\<not> essential \<Gamma> (B \<Gamma>) ?S x \<Longrightarrow> x \<noteq> y \<and> (\<exists>z\<in>set p'. z \<noteq> x \<and> z \<in> ?S)
set p' \<subseteq> set p
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g

goal (1 subgoal):
 1. x \<notin> TER g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<notin> TER g

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
with roofedD[OF x' p y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p'. z \<in> TER g) \<or> x \<in> TER g
x \<notin> TER g
[PROOF STEP]
obtain z where z: "z \<in> set p'" "z \<in> TER g"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p'. z \<in> TER g) \<or> x \<in> TER g
x \<notin> TER g

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> set p'; z \<in> TER g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> set p'
z \<in> TER g

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p' y
z \<in> set p'
z \<in> TER g
[PROOF STEP]
have "y \<in> set p'"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p' y
z \<in> set p'
z \<in> TER g

goal (1 subgoal):
 1. y \<in> set p'
[PROOF STEP]
by(auto dest!: rtrancl_path_last intro: last_in_set)
[PROOF STATE]
proof (state)
this:
y \<in> set p'

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
with distinct
[PROOF STATE]
proof (chain)
picking this:
distinct (x # p')
y \<in> set p'
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
distinct (x # p')
y \<in> set p'

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<in> RF\<^sup>\<circ> (TER g) \<Longrightarrow> False
[PROOF STEP]
with bypass z p' distinct
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g
z \<in> set p'
z \<in> TER g
set p' \<subseteq> set p
distinct (x # p')
x \<noteq> y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g
z \<in> set p'
z \<in> TER g
set p' \<subseteq> set p
distinct (x # p')
x \<noteq> y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TER_plus_web_aux:
  assumes SINK: "x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)" (is "_ \<in> SINK ?g")
  shows "x \<in> TER (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> TER (f \<frown> g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<in> SINK (f \<frown> g)
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f \<union> TER g)
[PROOF STEP]
obtain p y where p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
    and bypass: "\<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f \<union> TER g)

goal (1 subgoal):
 1. (\<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>; \<And>z. \<lbrakk>x \<noteq> y; z \<in> set p\<rbrakk> \<Longrightarrow> z = x \<or> z \<notin> TER f \<union> TER g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<E>_E) blast
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>
\<lbrakk>x \<noteq> y; ?z \<in> set p\<rbrakk> \<Longrightarrow> ?z = x \<or> ?z \<notin> TER f \<union> TER g

goal (2 subgoals):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<in> SINK (f \<frown> g)
[PROOF STEP]
from rtrancl_path_distinct[OF p]
[PROOF STATE]
proof (chain)
picking this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain p'
    where p: "path \<Gamma> x p' y" and p': "set p' \<subseteq> set p" and distinct: "distinct (x # p')"
[PROOF STATE]
proof (prove)
using this:
(\<And>xs'. \<lbrakk>path \<Gamma> x xs' y; distinct (x # xs'); set xs' \<subseteq> set p\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>path \<Gamma> x p' y; set p' \<subseteq> set p; distinct (x # p')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p' y
set p' \<subseteq> set p
distinct (x # p')

goal (2 subgoals):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<in> SINK (f \<frown> g)
[PROOF STEP]
from RF_f
[PROOF STATE]
proof (chain)
picking this:
x \<notin> RF\<^sup>\<circ> (TER f)
[PROOF STEP]
have "x \<in> SINK f"
[PROOF STATE]
proof (prove)
using this:
x \<notin> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. x \<in> SINK f
[PROOF STEP]
by(auto simp add: roofed_circ_def SINK.simps dest: waveD_OUT[OF w])
[PROOF STATE]
proof (state)
this:
x \<in> SINK f

goal (2 subgoals):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<in> SINK (f \<frown> g)
[PROOF STEP]
thus "x \<in> SINK (f \<frown> g)"
[PROOF STATE]
proof (prove)
using this:
x \<in> SINK f

goal (1 subgoal):
 1. x \<in> SINK (f \<frown> g)
[PROOF STEP]
using SINK
[PROOF STATE]
proof (prove)
using this:
x \<in> SINK f
x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)

goal (1 subgoal):
 1. x \<in> SINK (f \<frown> g)
[PROOF STEP]
by(simp add: SINK.simps d_OUT_plus_web)
[PROOF STATE]
proof (state)
this:
x \<in> SINK (f \<frown> g)

goal (1 subgoal):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
show "x \<in> SAT \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
proof(cases "x \<in> TER f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> TER f

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
hence "x \<in> SAT \<Gamma> f"
[PROOF STATE]
proof (prove)
using this:
x \<in> TER f

goal (1 subgoal):
 1. x \<in> SAT \<Gamma> f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> SAT \<Gamma> f

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> SAT \<Gamma> f

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
have "\<dots> \<subseteq> SAT \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAT \<Gamma> f \<subseteq> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
by(rule SAT_mono plus_web_greater)+
[PROOF STATE]
proof (state)
this:
SAT \<Gamma> f \<subseteq> SAT \<Gamma> (f \<frown> g)

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
 2. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> SAT \<Gamma> f
SAT \<Gamma> f \<subseteq> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> SAT \<Gamma> f
SAT \<Gamma> f \<subseteq> SAT \<Gamma> (f \<frown> g)

goal (1 subgoal):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> SAT \<Gamma> (f \<frown> g)

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> TER f

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f \<union> TER g)
x \<notin> TER f
[PROOF STEP]
have "x \<in> TER g"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f \<union> TER g)
x \<notin> TER f

goal (1 subgoal):
 1. x \<in> TER g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> TER g

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
from False RF_f
[PROOF STATE]
proof (chain)
picking this:
x \<notin> TER f
x \<notin> RF\<^sup>\<circ> (TER f)
[PROOF STEP]
have "x \<notin> RF (TER f)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> TER f
x \<notin> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. x \<notin> RF (TER f)
[PROOF STEP]
by(auto simp add: roofed_circ_def)
[PROOF STATE]
proof (state)
this:
x \<notin> RF (TER f)

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> RF (TER f)

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<notin> RF (TER f)

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
assume z: "z \<in> RF\<^sup>\<circ> (TER f)"
[PROOF STATE]
proof (state)
this:
z \<in> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
have "(z, x) \<notin> \<^bold>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z, x) \<notin> \<^bold>E
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z, x) \<in> \<^bold>E \<Longrightarrow> False
[PROOF STEP]
assume "(z, x) \<in> \<^bold>E"
[PROOF STATE]
proof (state)
this:
(z, x) \<in> \<^bold>E

goal (1 subgoal):
 1. (z, x) \<in> \<^bold>E \<Longrightarrow> False
[PROOF STEP]
hence path': "path \<Gamma> z (x # p') y"
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> \<^bold>E

goal (1 subgoal):
 1. path \<Gamma> z (x # p') y
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> \<^bold>E
path \<Gamma> x p' y

goal (1 subgoal):
 1. path \<Gamma> z (x # p') y
[PROOF STEP]
by(simp add: rtrancl_path.step)
[PROOF STATE]
proof (state)
this:
path \<Gamma> z (x # p') y

goal (1 subgoal):
 1. (z, x) \<in> \<^bold>E \<Longrightarrow> False
[PROOF STEP]
from z
[PROOF STATE]
proof (chain)
picking this:
z \<in> RF\<^sup>\<circ> (TER f)
[PROOF STEP]
have "z \<in> RF (TER f)"
[PROOF STATE]
proof (prove)
using this:
z \<in> RF\<^sup>\<circ> (TER f)

goal (1 subgoal):
 1. z \<in> RF (TER f)
[PROOF STEP]
by(simp add: roofed_circ_def)
[PROOF STATE]
proof (state)
this:
z \<in> RF (TER f)

goal (1 subgoal):
 1. (z, x) \<in> \<^bold>E \<Longrightarrow> False
[PROOF STEP]
from roofedD[OF this path' y] False
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set (x # p'). z \<in> TER f) \<or> z \<in> TER f
x \<notin> TER f
[PROOF STEP]
consider (path) z' where  "z' \<in> set p'" "z' \<in> TER f" | (TER) "z \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set (x # p'). z \<in> TER f) \<or> z \<in> TER f
x \<notin> TER f

goal (1 subgoal):
 1. \<lbrakk>\<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> thesis; z \<in> TER f \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> ?thesis; z \<in> TER f \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (z, x) \<in> \<^bold>E \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> ?thesis; z \<in> TER f \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> ?thesis; z \<in> TER f \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> False
 2. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> False
 2. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
case (path z')
[PROOF STATE]
proof (state)
this:
z' \<in> set p'
z' \<in> TER f

goal (2 subgoals):
 1. \<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> False
 2. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
with p distinct
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p' y
distinct (x # p')
z' \<in> set p'
z' \<in> TER f
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p' y
distinct (x # p')
z' \<in> set p'
z' \<in> TER f

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by(auto 4 3 intro: last_in_set elim: rtrancl_path.cases dest: rtrancl_path_last[symmetric])
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (2 subgoals):
 1. \<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> False
 2. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
from bypass[OF this, of z'] path False p'
[PROOF STATE]
proof (chain)
picking this:
z' \<in> set p \<Longrightarrow> z' = x \<or> z' \<notin> TER f \<union> TER g
z' \<in> set p'
z' \<in> TER f
x \<notin> TER f
set p' \<subseteq> set p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
z' \<in> set p \<Longrightarrow> z' = x \<or> z' \<notin> TER f \<union> TER g
z' \<in> set p'
z' \<in> TER f
x \<notin> TER f
set p' \<subseteq> set p

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

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z'2 \<in> set p'; ?z'2 \<in> TER f\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
note that = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z'2 \<in> set p'; ?z'2 \<in> TER f\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
case TER
[PROOF STATE]
proof (state)
this:
z \<in> TER f

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> RF\<^sup>\<circ> (TER f)
z \<in> TER f
[PROOF STEP]
have "\<not> essential \<Gamma> (B \<Gamma>) (TER f) z"
[PROOF STATE]
proof (prove)
using this:
z \<in> RF\<^sup>\<circ> (TER f)
z \<in> TER f

goal (1 subgoal):
 1. \<not> essential \<Gamma> (B \<Gamma>) (TER f) z
[PROOF STEP]
by(simp add: roofed_circ_def)
[PROOF STATE]
proof (state)
this:
\<not> essential \<Gamma> (B \<Gamma>) (TER f) z

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
from not_essentialD[OF this path' y] False
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> y \<and> (\<exists>za\<in>set (x # p'). za \<noteq> z \<and> za \<in> TER f)
x \<notin> TER f
[PROOF STEP]
obtain z' where "z' \<in> set p'" "z' \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> y \<and> (\<exists>za\<in>set (x # p'). za \<noteq> z \<and> za \<in> TER f)
x \<notin> TER f

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z' \<in> set p'; z' \<in> TER f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' \<in> set p'
z' \<in> TER f

goal (1 subgoal):
 1. z \<in> TER f \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
z' \<in> set p'
z' \<in> TER f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(z, x) \<notin> \<^bold>E

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?z2 \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> (?z2, x) \<notin> \<^bold>E

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> RF (TER f)
?z2 \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> (?z2, x) \<notin> \<^bold>E
[PROOF STEP]
have "d_IN ?g x = d_IN g x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> RF (TER f)
?z2 \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> (?z2, x) \<notin> \<^bold>E

goal (1 subgoal):
 1. d_IN (g \<upharpoonleft> \<Gamma> / f) x = d_IN g x
[PROOF STEP]
unfolding d_IN_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> RF (TER f)
?z2 \<in> RF\<^sup>\<circ> (TER f) \<Longrightarrow> (?z2, x) \<notin> \<^bold>E

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ xa. (g \<upharpoonleft> \<Gamma> / f) (xa, x)) = (\<Sum>\<^sup>+ xa. g (xa, x))
[PROOF STEP]
by(intro nn_integral_cong)(clarsimp split: split_indicator simp add: currentD_outside[OF g])
[PROOF STATE]
proof (state)
this:
d_IN (g \<upharpoonleft> \<Gamma> / f) x = d_IN g x

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
hence "d_IN (f \<frown> g) x \<ge> d_IN g x"
[PROOF STATE]
proof (prove)
using this:
d_IN (g \<upharpoonleft> \<Gamma> / f) x = d_IN g x

goal (1 subgoal):
 1. d_IN g x \<le> d_IN (f \<frown> g) x
[PROOF STEP]
by(simp add: d_IN_plus_web)
[PROOF STATE]
proof (state)
this:
d_IN g x \<le> d_IN (f \<frown> g) x

goal (1 subgoal):
 1. x \<notin> TER f \<Longrightarrow> x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
with \<open>x \<in> TER g\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> TER g
d_IN g x \<le> d_IN (f \<frown> g) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> TER g
d_IN g x \<le> d_IN (f \<frown> g) x

goal (1 subgoal):
 1. x \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
by(auto elim!: SAT.cases intro: SAT.intros)
[PROOF STATE]
proof (state)
this:
x \<in> SAT \<Gamma> (f \<frown> g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> SAT \<Gamma> (f \<frown> g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SINK_TER_in'':
  assumes "\<And>x. x \<notin> RF (TER g) \<Longrightarrow> d_OUT g x = 0"
  shows "x \<in> SINK g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> SINK g
[PROOF STEP]
using RF_g
[PROOF STATE]
proof (prove)
using this:
x \<notin> RF\<^sup>\<circ> (TER g)

goal (1 subgoal):
 1. x \<in> SINK g
[PROOF STEP]
by(auto simp add: roofed_circ_def SINK.simps assms)


[STATEMENT]
lemma wave_plus: "wave (quotient_web \<Gamma> f) (g \<upharpoonleft> \<Gamma> / f) \<Longrightarrow> wave \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave (quotient_web \<Gamma> f) (g \<upharpoonleft> \<Gamma> / f) \<Longrightarrow> wave \<Gamma> (f \<frown> g)
[PROOF STEP]
using f w
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
wave \<Gamma> f

goal (1 subgoal):
 1. wave (quotient_web \<Gamma> f) (g \<upharpoonleft> \<Gamma> / f) \<Longrightarrow> wave \<Gamma> (f \<frown> g)
[PROOF STEP]
by(rule wave_plus_current)(rule current_restrict_current[OF w g])


[STATEMENT]
lemma TER_plus_web'':
  assumes "\<And>x. x \<notin> RF (TER g) \<Longrightarrow> d_OUT g x = 0"
  shows "\<E> (TER f \<union> TER g) \<subseteq> TER (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E> (TER f \<union> TER g) \<subseteq> TER (f \<frown> g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<E> (TER f \<union> TER g) \<Longrightarrow> x \<in> TER (f \<frown> g)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<E> (TER f \<union> TER g) \<Longrightarrow> x \<in> TER (f \<frown> g)
[PROOF STEP]
assume *: "x \<in> \<E> (TER f \<union> TER g)"
[PROOF STATE]
proof (state)
this:
x \<in> \<E> (TER f \<union> TER g)

goal (1 subgoal):
 1. \<And>x. x \<in> \<E> (TER f \<union> TER g) \<Longrightarrow> x \<in> TER (f \<frown> g)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> \<E> (TER f \<union> TER g)

goal (1 subgoal):
 1. \<And>x. x \<in> \<E> (TER f \<union> TER g) \<Longrightarrow> x \<in> TER (f \<frown> g)
[PROOF STEP]
have "x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)
[PROOF STEP]
by(rule in_SINK_restrict_current)(rule MFMC_Unbounded.SINK_TER_in''[OF f w g * assms])
[PROOF STATE]
proof (state)
this:
x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)

goal (1 subgoal):
 1. \<And>x. x \<in> \<E> (TER f \<union> TER g) \<Longrightarrow> x \<in> TER (f \<frown> g)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f \<union> TER g)
x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)
[PROOF STEP]
show "x \<in> TER (f \<frown> g)"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f \<union> TER g)
x \<in> SINK (g \<upharpoonleft> \<Gamma> / f)

goal (1 subgoal):
 1. x \<in> TER (f \<frown> g)
[PROOF STEP]
by(rule TER_plus_web_aux)
[PROOF STATE]
proof (state)
this:
x \<in> TER (f \<frown> g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TER_plus_web': "wave \<Gamma> g \<Longrightarrow> \<E> (TER f \<union> TER g) \<subseteq> TER (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave \<Gamma> g \<Longrightarrow> \<E> (TER f \<union> TER g) \<subseteq> TER (f \<frown> g)
[PROOF STEP]
by(rule TER_plus_web'')(rule waveD_OUT)


[STATEMENT]
lemma wave_plus': "wave \<Gamma> g \<Longrightarrow> wave \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave \<Gamma> g \<Longrightarrow> wave \<Gamma> (f \<frown> g)
[PROOF STEP]
by(rule wave_plus)(rule wave_restrict_current[OF f w g])


[STATEMENT]
lemma RF_TER_plus_web:
  fixes \<Gamma> (structure)
  assumes f: "current \<Gamma> f"
  and w: "wave \<Gamma> f"
  and g: "current \<Gamma> g"
  and w': "wave \<Gamma> g"
  shows "RF (TER (f \<frown> g)) = RF (TER f \<union> TER g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RF (TER (f \<frown> g)) = RF (TER f \<union> TER g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
 2. RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
have "RF (\<E> (TER f \<union> TER g)) \<subseteq> RF (TER (f \<frown> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RF (\<E> (TER f \<union> TER g)) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
by(rule roofed_mono)(rule TER_plus_web'[OF f w g w'])
[PROOF STATE]
proof (state)
this:
RF (\<E> (TER f \<union> TER g)) \<subseteq> RF (TER (f \<frown> g))

goal (2 subgoals):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
 2. RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RF (\<E> (TER f \<union> TER g)) \<subseteq> RF (TER (f \<frown> g))

goal (2 subgoals):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
 2. RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
have "RF (\<E> (TER f \<union> TER g)) = RF (TER f \<union> TER g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RF (\<E> (TER f \<union> TER g)) = RF (TER f \<union> TER g)
[PROOF STEP]
by(rule RF_essential)
[PROOF STATE]
proof (state)
this:
RF (\<E> (TER f \<union> TER g)) = RF (TER f \<union> TER g)

goal (2 subgoals):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
 2. RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
show "\<dots> \<subseteq> RF (TER (f \<frown> g))"
[PROOF STATE]
proof (prove)
using this:
RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))

goal (1 subgoal):
 1. RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
RF (TER f \<union> TER g) \<subseteq> RF (TER (f \<frown> g))

goal (1 subgoal):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
[PROOF STEP]
have fg: "current \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (f \<frown> g)
[PROOF STEP]
using f w g
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
wave \<Gamma> f
current \<Gamma> g

goal (1 subgoal):
 1. current \<Gamma> (f \<frown> g)
[PROOF STEP]
by(rule current_plus_web)
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f \<frown> g)

goal (1 subgoal):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
[PROOF STEP]
show "RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)
[PROOF STEP]
proof(intro subsetI roofedI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
fix x p y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
assume RF: "x \<in> RF (TER (f \<frown> g))" and p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
[PROOF STATE]
proof (state)
this:
x \<in> RF (TER (f \<frown> g))
path \<Gamma> x p y
y \<in> B \<Gamma>

goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
from roofedD[OF RF p y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p. z \<in> TER (f \<frown> g)) \<or> x \<in> TER (f \<frown> g)
[PROOF STEP]
obtain z where z: "z \<in> set (x # p)" and TER: "z \<in> TER (f \<frown> g)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p. z \<in> TER (f \<frown> g)) \<or> x \<in> TER (f \<frown> g)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> set (x # p); z \<in> TER (f \<frown> g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> set (x # p)
z \<in> TER (f \<frown> g)

goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
from TER
[PROOF STATE]
proof (chain)
picking this:
z \<in> TER (f \<frown> g)
[PROOF STEP]
have SINK: "z \<in> SINK f"
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (f \<frown> g)

goal (1 subgoal):
 1. z \<in> SINK f
[PROOF STEP]
by(auto simp add: SINK.simps d_OUT_plus_web add_eq_0_iff_both_eq_0)
[PROOF STATE]
proof (state)
this:
z \<in> SINK f

goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
from TER
[PROOF STATE]
proof (chain)
picking this:
z \<in> TER (f \<frown> g)
[PROOF STEP]
have "z \<in> SAT \<Gamma> (f \<frown> g)"
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (f \<frown> g)

goal (1 subgoal):
 1. z \<in> SAT \<Gamma> (f \<frown> g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> SAT \<Gamma> (f \<frown> g)

goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
hence SAT: "z \<in> SAT \<Gamma> f \<union> SAT \<Gamma> g"
[PROOF STATE]
proof (prove)
using this:
z \<in> SAT \<Gamma> (f \<frown> g)

goal (1 subgoal):
 1. z \<in> SAT \<Gamma> f \<union> SAT \<Gamma> g
[PROOF STEP]
by(cases "z \<in> RF (TER f)")(auto simp add: currentD_SAT[OF f] currentD_SAT[OF g] currentD_SAT[OF fg] d_IN_plus_web d_IN_restrict_current_outside restrict_current_IN_not_RF[OF g] wave_not_RF_IN_zero[OF f w])
[PROOF STATE]
proof (state)
this:
z \<in> SAT \<Gamma> f \<union> SAT \<Gamma> g

goal (1 subgoal):
 1. \<And>x p y. \<lbrakk>x \<in> RF (TER (f \<frown> g)); path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
show "(\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
proof(cases "z \<in> RF (TER g)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
 2. z \<notin> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<notin> RF (TER g)

goal (2 subgoals):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
 2. z \<notin> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
hence "z \<in> SINK g"
[PROOF STATE]
proof (prove)
using this:
z \<notin> RF (TER g)

goal (1 subgoal):
 1. z \<in> SINK g
[PROOF STEP]
by(simp add: SINK.simps waveD_OUT[OF w'])
[PROOF STATE]
proof (state)
this:
z \<in> SINK g

goal (2 subgoals):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
 2. z \<notin> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
with SINK SAT
[PROOF STATE]
proof (chain)
picking this:
z \<in> SINK f
z \<in> SAT \<Gamma> f \<union> SAT \<Gamma> g
z \<in> SINK g
[PROOF STEP]
have "z \<in> TER f \<union> TER g"
[PROOF STATE]
proof (prove)
using this:
z \<in> SINK f
z \<in> SAT \<Gamma> f \<union> SAT \<Gamma> g
z \<in> SINK g

goal (1 subgoal):
 1. z \<in> TER f \<union> TER g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> TER f \<union> TER g

goal (2 subgoals):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
 2. z \<notin> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> TER f \<union> TER g

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z \<in> TER f \<union> TER g
z \<in> set (x # p)

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g

goal (1 subgoal):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z \<in> RF (TER g)

goal (1 subgoal):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
from split_list[OF z]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys zs. x # p = ys @ z # zs
[PROOF STEP]
obtain ys zs where split: "x # p = ys @ z # zs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys zs. x # p = ys @ z # zs

goal (1 subgoal):
 1. (\<And>ys zs. x # p = ys @ z # zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x # p = ys @ z # zs

goal (1 subgoal):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p y
x # p = ys @ z # zs
[PROOF STEP]
have "path \<Gamma> z zs y"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p y
x # p = ys @ z # zs

goal (1 subgoal):
 1. path \<Gamma> z zs y
[PROOF STEP]
by(auto elim: rtrancl_path_appendE simp add: Cons_eq_append_conv)
[PROOF STATE]
proof (state)
this:
path \<Gamma> z zs y

goal (1 subgoal):
 1. z \<in> RF (TER g) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
from roofedD[OF True this y] split
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set zs. z \<in> TER g) \<or> z \<in> TER g
x # p = ys @ z # zs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set zs. z \<in> TER g) \<or> z \<in> TER g
x # p = ys @ z # zs

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g
[PROOF STEP]
by(auto simp add: Cons_eq_append_conv)
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER f \<union> TER g) \<or> x \<in> TER f \<union> TER g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RF (TER (f \<frown> g)) \<subseteq> RF (TER f \<union> TER g)

goal:
No subgoals!
[PROOF STEP]
qed