[STATEMENT]
lemma (in SecurityInvariant_withOffendingFlows) 
    fixes "default_node_properties" :: "'a" ("\<bottom>")
    shows "\<not> sinvar G nP \<Longrightarrow> sinvar_all_edges_normal_form P \<Longrightarrow>
    (\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> (P (nP e1) (nP e2)) \<longrightarrow>  \<not> (P \<bottom> (nP e2))) \<Longrightarrow>
    (\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> (P (nP e1) (nP e2)) \<longrightarrow> \<not> (P (nP e1) \<bottom>)) \<Longrightarrow>
    (\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> P \<bottom> \<bottom>)
    \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
assume a1: "\<not> sinvar G nP"
    and   a2d: "sinvar_all_edges_normal_form P"
    and    a3: "\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> (P (nP e1) (nP e2)) \<longrightarrow> \<not> (P \<bottom> (nP e2))"
    and    a4: "\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> (P (nP e1) (nP e2)) \<longrightarrow> \<not> (P (nP e1) \<bottom>)"
    and    a5: "\<forall> (nP::'v \<Rightarrow> 'a) e1 e2. \<not> P \<bottom> \<bottom>"
[PROOF STATE]
proof (state)
this:
\<not> sinvar G nP
sinvar_all_edges_normal_form P
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2)
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>
\<forall>nP e1 e2. \<not> P \<bottom> \<bottom>

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from a2d
[PROOF STATE]
proof (chain)
picking this:
sinvar_all_edges_normal_form P
[PROOF STEP]
have a2: "\<And> G nP. sinvar G nP  = (\<forall> (e1, e2) \<in> edges G. P (nP e1) (nP e2))"
[PROOF STATE]
proof (prove)
using this:
sinvar_all_edges_normal_form P

goal (1 subgoal):
 1. \<And>G nP. sinvar G nP = (\<forall>(e1, e2)\<in>edges G. P (nP e1) (nP e2))
[PROOF STEP]
using sinvar_all_edges_normal_form_def
[PROOF STATE]
proof (prove)
using this:
sinvar_all_edges_normal_form P
sinvar_all_edges_normal_form ?P \<equiv> \<forall>G nP. sinvar G nP = (\<forall>(e1, e2)\<in>edges G. ?P (nP e1) (nP e2))

goal (1 subgoal):
 1. \<And>G nP. sinvar G nP = (\<forall>(e1, e2)\<in>edges G. P (nP e1) (nP e2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sinvar ?G1 ?nP1 = (\<forall>(e1, e2)\<in>edges ?G1. P (?nP1 e1) (?nP1 e2))

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from ENF_default_update_fst[OF a1 a2d] a3
[PROOF STATE]
proof (chain)
picking this:
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P ?default_node_properties (nP e2) \<Longrightarrow> \<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(?i := ?default_node_properties)) e1) (nP e2))
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2)
[PROOF STEP]
have subgoal1: "\<not> (\<forall> (e1, e2) \<in> edges G. P ((nP(i := \<bottom>)) e1) (nP e2))"
[PROOF STATE]
proof (prove)
using this:
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P ?default_node_properties (nP e2) \<Longrightarrow> \<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(?i := ?default_node_properties)) e1) (nP e2))
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2)

goal (1 subgoal):
 1. \<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) (nP e2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) (nP e2))

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
let ?nP' = "(nP(i := \<bottom>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from subgoal1
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) (nP e2))
[PROOF STEP]
have "\<exists> (e1, e2) \<in> edges G. \<not> P (?nP' e1) (nP e2)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) (nP e2))

goal (1 subgoal):
 1. \<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) (nP e2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) (nP e2)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) (nP e2)
[PROOF STEP]
obtain e11 e21 where s1cond: "(e11, e21) \<in> edges G \<and> \<not> P (?nP' e11) (nP e21)"
[PROOF STATE]
proof (prove)
using this:
\<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) (nP e2)

goal (1 subgoal):
 1. (\<And>e11 e21. (e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from s1cond
[PROOF STATE]
proof (chain)
picking this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
[PROOF STEP]
have "i \<noteq> e11 \<Longrightarrow> \<not> P (nP e11) (nP e21)"
[PROOF STATE]
proof (prove)
using this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)

goal (1 subgoal):
 1. i \<noteq> e11 \<Longrightarrow> \<not> P (nP e11) (nP e21)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<noteq> e11 \<Longrightarrow> \<not> P (nP e11) (nP e21)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from s1cond
[PROOF STATE]
proof (chain)
picking this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
[PROOF STEP]
have "e11 \<noteq> e21 \<Longrightarrow> \<not> P (?nP' e11) (?nP' e21)"
[PROOF STATE]
proof (prove)
using this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)

goal (1 subgoal):
 1. e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e11 \<noteq> e21; (e11, e21) \<in> edges G \<and> \<not> P (if e11 = i then \<bottom> else nP e11) (nP e21)\<rbrakk> \<Longrightarrow> (e11 = i \<longrightarrow> e21 = i \<longrightarrow> \<not> P \<bottom> \<bottom>) \<and> (e11 \<noteq> i \<longrightarrow> e21 = i \<longrightarrow> \<not> P (nP e11) \<bottom>)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>e11 \<noteq> e21; (e11, e21) \<in> edges G \<and> \<not> P (if e11 = i then \<bottom> else nP e11) (nP e21)\<rbrakk> \<Longrightarrow> e11 = i \<longrightarrow> e21 = i \<longrightarrow> \<not> P \<bottom> \<bottom>
 2. \<lbrakk>e11 \<noteq> e21; (e11, e21) \<in> edges G \<and> \<not> P (if e11 = i then \<bottom> else nP e11) (nP e21)\<rbrakk> \<Longrightarrow> e11 \<noteq> i \<longrightarrow> e21 = i \<longrightarrow> \<not> P (nP e11) \<bottom>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e11 \<noteq> e21; (e11, e21) \<in> edges G \<and> \<not> P (if e11 = i then \<bottom> else nP e11) (nP e21)\<rbrakk> \<Longrightarrow> e11 \<noteq> i \<longrightarrow> e21 = i \<longrightarrow> \<not> P (nP e11) \<bottom>
[PROOF STEP]
apply(insert a4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e11 \<noteq> e21; (e11, e21) \<in> edges G \<and> \<not> P (if e11 = i then \<bottom> else nP e11) (nP e21); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>\<rbrakk> \<Longrightarrow> e11 \<noteq> i \<longrightarrow> e21 = i \<longrightarrow> \<not> P (nP e11) \<bottom>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from s1cond a4 fun_upd_apply
[PROOF STATE]
proof (chain)
picking this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)
[PROOF STEP]
have ex1: "e11 \<noteq> e21 \<Longrightarrow> \<not> P (?nP' e11) (?nP' e21)"
[PROOF STATE]
proof (prove)
using this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
\<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)

goal (1 subgoal):
 1. e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from s1cond a5
[PROOF STATE]
proof (chain)
picking this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
\<forall>nP e1 e2. \<not> P \<bottom> \<bottom>
[PROOF STEP]
have ex2: "e11 = e21 \<Longrightarrow> \<not> P (?nP' e11) (?nP' e21)"
[PROOF STATE]
proof (prove)
using this:
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
\<forall>nP e1 e2. \<not> P \<bottom> \<bottom>

goal (1 subgoal):
 1. e11 = e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e11 = e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from ex1 ex2 s1cond
[PROOF STATE]
proof (chain)
picking this:
e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
e11 = e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)
[PROOF STEP]
have "\<exists> (e1, e2) \<in> edges G. \<not> P (?nP' e1) (?nP' e2)"
[PROOF STATE]
proof (prove)
using this:
e11 \<noteq> e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
e11 = e21 \<Longrightarrow> \<not> P ((nP(i := \<bottom>)) e11) ((nP(i := \<bottom>)) e21)
(e11, e21) \<in> edges G \<and> \<not> P ((nP(i := \<bottom>)) e11) (nP e21)

goal (1 subgoal):
 1. \<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2)

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
hence "\<not> (\<forall> (e1, e2) \<in> edges G. P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2))"
[PROOF STATE]
proof (prove)
using this:
\<exists>(e1, e2)\<in>edges G. \<not> P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2)

goal (1 subgoal):
 1. \<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2))

goal (1 subgoal):
 1. \<lbrakk>\<not> sinvar G nP; sinvar_all_edges_normal_form P; \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P \<bottom> (nP e2); \<forall>nP e1 e2. \<not> P (nP e1) (nP e2) \<longrightarrow> \<not> P (nP e1) \<bottom>; \<forall>nP e1 e2. \<not> P \<bottom> \<bottom>\<rbrakk> \<Longrightarrow> \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
from this a2
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2))
sinvar ?G1 ?nP1 = (\<forall>(e1, e2)\<in>edges ?G1. P (?nP1 e1) (?nP1 e2))
[PROOF STEP]
show "\<not> sinvar G (nP(i := \<bottom>))"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>(e1, e2)\<in>edges G. P ((nP(i := \<bottom>)) e1) ((nP(i := \<bottom>)) e2))
sinvar ?G1 ?nP1 = (\<forall>(e1, e2)\<in>edges ?G1. P (?nP1 e1) (?nP1 e2))

goal (1 subgoal):
 1. \<not> sinvar G (nP(i := \<bottom>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<not> sinvar G (nP(i := \<bottom>))

goal:
No subgoals!
[PROOF STEP]
qed