[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


[STATEMENT]
lemma multiplicity_Lcm:
  fixes A :: "'a :: {semiring_Gcd, factorial_semiring_gcd} set"
  assumes "finite A" "A \<noteq> {}" "prime p" "0 \<notin> A"
  shows   "multiplicity p (Lcm A) = Max (multiplicity p ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (Lcm A) = Max (multiplicity p ` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
prime p
(0::'a) \<notin> A

goal (1 subgoal):
 1. multiplicity p (Lcm A) = Max (multiplicity p ` A)
[PROOF STEP]
proof (induction A rule: finite_ne_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
A \<noteq> {}
x \<notin> A
\<lbrakk>prime p; (0::'a) \<notin> A\<rbrakk> \<Longrightarrow> multiplicity p (Lcm A) = Max (multiplicity p ` A)
prime p
(0::'a) \<notin> insert x A

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
have "Lcm (insert x A) = lcm x (Lcm A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lcm (insert x A) = lcm x (Lcm A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Lcm (insert x A) = lcm x (Lcm A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Lcm (insert x A) = lcm x (Lcm A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
have "multiplicity p \<dots> = Max (multiplicity p ` insert x A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
x \<notin> A
\<lbrakk>prime p; (0::'a) \<notin> A\<rbrakk> \<Longrightarrow> multiplicity p (Lcm A) = Max (multiplicity p ` A)
prime p
(0::'a) \<notin> insert x A

goal (1 subgoal):
 1. multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
by (subst multiplicity_lcm) (auto simp: Lcm_0_iff)
[PROOF STATE]
proof (state)
this:
multiplicity p (lcm x (Lcm A)) = Max (multiplicity p ` insert x A)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<lbrakk>prime p; (0::'a) \<notin> F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm F) = Max (multiplicity p ` F); prime p; (0::'a) \<notin> insert x F\<rbrakk> \<Longrightarrow> multiplicity p (Lcm (insert x F)) = Max (multiplicity p ` insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)

goal (1 subgoal):
 1. multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity p (Lcm (insert x A)) = Max (multiplicity p ` insert x A)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>prime p; (0::'a) \<notin> {x}\<rbrakk> \<Longrightarrow> multiplicity p (Lcm {x}) = Max (multiplicity p ` {x})
[PROOF STEP]
qed auto


[STATEMENT]
lemma path_append_elim[elim!] :
  assumes "path M q (p1@p2)"
  obtains "path M q p1"
      and "path M (target q p1) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>path M q p1; path M (target q p1) p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms path_prefix path_suffix)


[STATEMENT]
lemma visited_states_length : "length (visited_states q p) = Suc (length p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (visited_states q p) = Suc (length p)
[PROOF STEP]
by auto


[STATEMENT]
lemma h_obs_distinguishes :
  assumes "observable M"
  and     "h_obs M q1 x y = Some q1'"
  and     "h_obs M q2 x y = None"
shows "distinguishes M q1 q2 [(x,y)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
using assms(2,3) LS_single_transition[of x y M]
[PROOF STATE]
proof (prove)
using this:
FSM.h_obs M q1 x y = Some q1'
FSM.h_obs M q2 x y = None
([(x, y)] \<in> LS M ?q) = (\<exists>t\<in>FSM.transitions M. t_source t = ?q \<and> t_input t = x \<and> t_output t = y)

goal (1 subgoal):
 1. distinguishes M q1 q2 [(x, y)]
[PROOF STEP]
unfolding distinguishes_def h_obs_Some[OF assms(1)] h_obs_None[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
{q'. (q1, x, y, q') \<in> FSM.transitions M} = {q1'}
\<nexists>q'. (q2, x, y, q') \<in> FSM.transitions M
([(x, y)] \<in> LS M ?q) = (\<exists>t\<in>FSM.transitions M. t_source t = ?q \<and> t_input t = x \<and> t_output t = y)

goal (1 subgoal):
 1. [(x, y)] \<in> LS M q1 \<union> LS M q2 \<and> [(x, y)] \<notin> LS M q1 \<inter> LS M q2
[PROOF STEP]
by (metis Int_iff UnI1 \<open>\<And>y x q. (h_obs M q x y = None) = (\<nexists>q'. (q, x, y, q') \<in> FSM.transitions M)\<close> assms(1) assms(2) fst_conv h_obs_language_iff option.distinct(1) snd_conv)


[STATEMENT]
lemma index_states_integer_observable :
  assumes "observable M"
  shows "observable (index_states_integer M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (index_states_integer M)
[PROOF STEP]
using rename_states_observable[of "integer_of_nat \<circ> assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms]
[PROOF STATE]
proof (prove)
using this:
observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))

goal (1 subgoal):
 1. observable (index_states_integer M)
[PROOF STEP]
unfolding index_states_integer.simps
[PROOF STATE]
proof (prove)
using this:
observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))

goal (1 subgoal):
 1. observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))
[PROOF STEP]
.


[STATEMENT]
lemma matrix_right_invertible_ker:
  fixes M :: "real^('m::finite)^'n"
  shows "(\<exists> M'. M ** M' = mat 1) \<longleftrightarrow> (\<forall> x. x v* M = 0 \<longrightarrow> x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>M'. M ** M' = mat 1) = (\<forall>x. x v* M = 0 \<longrightarrow> x = 0)
[PROOF STEP]
using left_invertible_transpose matrix_left_invertible_ker
[PROOF STATE]
proof (prove)
using this:
(\<exists>B. B ** Finite_Cartesian_Product.transpose ?A = mat (1::?'a)) = (\<exists>B. ?A ** B = mat (1::?'a))
(\<exists>B. B ** ?A = mat (1::?'a)) = (\<forall>x. ?A *v x = 0 \<longrightarrow> x = 0)

goal (1 subgoal):
 1. (\<exists>M'. M ** M' = mat 1) = (\<forall>x. x v* M = 0 \<longrightarrow> x = 0)
[PROOF STEP]
by force


[STATEMENT]
lemma f_values: "(f 0 = 0 \<or> f 0 = 1) \<and> (f 1 = 0 \<or> f 1 = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f 0 = 0 \<or> f 0 = 1) \<and> (f 1 = 0 \<or> f 1 = 1)
[PROOF STEP]
using dom
[PROOF STATE]
proof (prove)
using this:
f \<in> {0, 1} \<rightarrow>\<^sub>E {0, 1}

goal (1 subgoal):
 1. (f 0 = 0 \<or> f 0 = 1) \<and> (f 1 = 0 \<or> f 1 = 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma rt_fresher_single [intro]:
  assumes "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
    shows "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
.


[STATEMENT]
lemma vD_invalidate_rt_strictly_fresher [simp]:
  assumes "dip \<in> vD(invalidate rt1 dests)"
    shows "(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
proof (cases "dip \<in> dom(dests)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
assume "dip \<in> dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<in> dom dests

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
hence "dip \<notin> vD(invalidate rt1 dests)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<notin> vD (invalidate rt1 dests)
[PROOF STEP]
unfolding invalidate_def vD_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> dom dests

goal (1 subgoal):
 1. dip \<notin> {dip. map_option \<pi>\<^sub>4 (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some val}
[PROOF STEP]
by clarsimp (metis assms option.simps(3) vD_invalidate_vD_not_dests)
[PROOF STATE]
proof (state)
this:
dip \<notin> vD (invalidate rt1 dests)

goal (2 subgoals):
 1. dip \<in> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
 2. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
with \<open>dip \<in> vD(invalidate rt1 dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (invalidate rt1 dests)
dip \<notin> vD (invalidate rt1 dests)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (invalidate rt1 dests)
dip \<notin> vD (invalidate rt1 dests)

goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
assume "dip \<notin> dom(dests)"
[PROOF STATE]
proof (state)
this:
dip \<notin> dom dests

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
hence "dests dip = None"
[PROOF STATE]
proof (prove)
using this:
dip \<notin> dom dests

goal (1 subgoal):
 1. dests dip = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dests dip = None

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dests dip = None

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
with \<open>dip \<in> vD(invalidate rt1 dests)\<close>
[PROOF STATE]
proof (chain)
picking this:
dip \<in> vD (invalidate rt1 dests)
dests dip = None
[PROOF STEP]
have "dip \<in> vD(rt1)"
[PROOF STATE]
proof (prove)
using this:
dip \<in> vD (invalidate rt1 dests)
dests dip = None

goal (1 subgoal):
 1. dip \<in> vD rt1
[PROOF STEP]
unfolding invalidate_def vD_def
[PROOF STATE]
proof (prove)
using this:
dip \<in> {dip. map_option \<pi>\<^sub>4 (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) = Some val}
dests dip = None

goal (1 subgoal):
 1. dip \<in> {dip. flag rt1 dip = Some val}
[PROOF STEP]
by clarsimp (metis (opaque_lifting, no_types) assms vD_Some vD_invalidate_vD_not_dests)
[PROOF STATE]
proof (state)
this:
dip \<in> vD rt1

goal (1 subgoal):
 1. dip \<notin> dom dests \<Longrightarrow> (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dests dip = None
dip \<in> vD rt1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dests dip = None
dip \<in> vD rt1

goal (1 subgoal):
 1. (invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)
[PROOF STEP]
unfolding invalidate_def rt_strictly_fresher_def'
[PROOF STATE]
proof (prove)
using this:
dests dip = None
dip \<in> vD rt1

goal (1 subgoal):
 1. (nsqn\<^sub>r (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) < nsqn\<^sub>r (the (rt2 dip)) \<or> nsqn\<^sub>r (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba))) = nsqn\<^sub>r (the (rt2 dip)) \<and> \<pi>\<^sub>5 (the (rt2 dip)) < \<pi>\<^sub>5 (the (case (rt1 dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)))) = (nsqn\<^sub>r (the (rt1 dip)) < nsqn\<^sub>r (the (rt2 dip)) \<or> nsqn\<^sub>r (the (rt1 dip)) = nsqn\<^sub>r (the (rt2 dip)) \<and> \<pi>\<^sub>5 (the (rt2 dip)) < \<pi>\<^sub>5 (the (rt1 dip)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(invalidate rt1 dests \<sqsubset>\<^bsub>dip\<^esub> rt2) = (rt1 \<sqsubset>\<^bsub>dip\<^esub> rt2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pwd_owner_iv_rel_1:
 "\<lbrakk>n \<in> bad_prikey \<inter> bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\<rbrakk> \<Longrightarrow>
    s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)"
      (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<Turnstile> ?t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> bad_prikey \<inter> bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\<rbrakk> \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)
[PROOF STEP]
by (rule rtrancl_into_rtrancl, erule pwd_spy_iii_rel, drule pwd_spy_iii_msg,
 subgoal_tac "(s, ?t) \<in> rel_owner_iv", simp_all add: rel_def pwd_owner_iv_def
 Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B],
 rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto)


[STATEMENT]
lemma split_block_hermitian_4:
  assumes "hermitian A"
  and "n \<le> dim_row A"
and "(A1, A2, A3, A4) = split_block A n n"
shows "hermitian A4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hermitian A4
[PROOF STEP]
unfolding hermitian_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 = A4
[PROOF STEP]
proof (rule eq_matI, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_col A4 = dim_row A4
 3. dim_row A4 = dim_col A4
[PROOF STEP]
have arc: "dim_row A = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = dim_col A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_row A = dim_col A
[PROOF STEP]
by (metis carrier_matD(2) hermitian_square)
[PROOF STATE]
proof (state)
this:
dim_row A = dim_col A

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_col A4 = dim_row A4
 3. dim_row A4 = dim_col A4
[PROOF STEP]
thus "dim_col A4 = dim_row A4"
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col A4 = dim_row A4

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_row A4 = dim_col A4
[PROOF STEP]
thus "dim_row A4 = dim_col A4"
[PROOF STATE]
proof (prove)
using this:
dim_col A4 = dim_row A4

goal (1 subgoal):
 1. dim_row A4 = dim_col A4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row A4 = dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
show "\<And>i j. i < dim_row A4 \<Longrightarrow> j < dim_col A4 \<Longrightarrow>
    Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
assume "i < dim_row A4" and "j < dim_col A4"
[PROOF STATE]
proof (state)
this:
i < dim_row A4
j < dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
note ij = this
[PROOF STATE]
proof (state)
this:
i < dim_row A4
j < dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have r: "dim_row A4 = dim_row A - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A4 = dim_row A - n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_row A4 = dim_row A - n
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

goal (1 subgoal):
 1. dim_row A4 = dim_row A - n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row A4 = dim_row A - n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have c: "dim_col A4 = dim_col A - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j,i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
using ij r c arc
[PROOF STATE]
proof (prove)
using this:
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
unfolding Complex_Matrix.adjoint_def
[PROOF STATE]
proof (prove)
using this:
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. Matrix.mat (dim_col A4) (dim_row A4) (\<lambda>(i, j). conjugate (A4 $$ (j, i))) $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = conjugate (A $$ (j +n ,i+n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
using assms ij r c arc
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = A $$ (i+n,j+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
using assms ij r c arc
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
unfolding hermitian_def Complex_Matrix.adjoint_def
[PROOF STATE]
proof (prove)
using this:
Matrix.mat (dim_col A) (dim_row A) (\<lambda>(i, j). conjugate (A $$ (j, i))) = A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
by (metis index_mat(1) less_diff_conv split_conv)
[PROOF STATE]
proof (state)
this:
conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = A4 $$(i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
using assms ij r c
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $$ (i + n, j + n) = A4 $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
show "Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)

goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row A4; ?j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (?i, ?j) = A4 $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<alpha>_strict[simp]: "\<alpha> bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> bot = bot
[PROOF STEP]
using \<alpha>_dist[of "{}"]
[PROOF STATE]
proof (prove)
using this:
is_chain {} \<Longrightarrow> \<alpha> (Sup {}) = Sup (\<alpha> ` {})

goal (1 subgoal):
 1. \<alpha> bot = bot
[PROOF STEP]
by simp


[STATEMENT]
lemma d_delta_arctan_upper_31_pos: "x \<noteq> 0 \<Longrightarrow> diff_delta_arctan_upper_31 x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < diff_delta_arctan_upper_31 x
[PROOF STEP]
unfolding diff_delta_arctan_upper_31_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < 64 / (x\<^sup>2 * (15 + 70 * x\<^sup>2 + 63 * x ^ 4)\<^sup>2 * (1 + x\<^sup>2))
[PROOF STEP]
by (auto simp: divide_simps zero_less_mult_iff add_pos_pos add_nonneg_eq_0_iff)


[STATEMENT]
lemma power_poly_f_mod_i: assumes m: "(poly_rel ===> poly_rel) m (\<lambda> x'. x' mod m')"
  shows "poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
from m
[PROOF STATE]
proof (chain)
picking this:
(poly_rel ===> poly_rel) m (\<lambda>x'. x' mod m')
[PROOF STEP]
have m: "\<And> x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')"
[PROOF STATE]
proof (prove)
using this:
(poly_rel ===> poly_rel) m (\<lambda>x'. x' mod m')

goal (1 subgoal):
 1. \<And>x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. poly_rel x y \<longrightarrow> poly_rel (m x) (y mod m')

goal (1 subgoal):
 1. \<And>x x'. poly_rel x x' \<Longrightarrow> poly_rel (m x) (x' mod m')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_rel ?x ?x' \<Longrightarrow> poly_rel (m ?x) (?x' mod m')

goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show "poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof (induct n arbitrary: f f' rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
case (less n f f')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y < n; poly_rel ?f ?f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m ?f ?y) (power_poly_f_mod m' ?f' ?y)
poly_rel f f'

goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
note f[transfer_rule] = less(2)
[PROOF STATE]
proof (state)
this:
poly_rel f f'

goal (1 subgoal):
 1. \<And>x f f'. \<lbrakk>\<And>y f f'. \<lbrakk>y < x; poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f y) (power_poly_f_mod m' f' y); poly_rel f f'\<rbrakk> \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f x) (power_poly_f_mod m' f' x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
 2. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
 2. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
by (simp add: True power_poly_f_mod_i.simps power_poly_f_mod_binary,
          rule m[OF poly_rel_one])
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
hence n: "(n = 0) = False"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

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

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
obtain q r where div: "Euclidean_Division.divmod_nat n 2 = (q,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q r. Euclidean_Division.divmod_nat n 2 = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Euclidean_Division.divmod_nat n 2 = (q, r)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
from this[unfolded Euclidean_Division.divmod_nat_def] n
[PROOF STATE]
proof (chain)
picking this:
(n div 2, n mod 2) = (q, r)
(n = 0) = False
[PROOF STEP]
have "q < n"
[PROOF STATE]
proof (prove)
using this:
(n div 2, n mod 2) = (q, r)
(n = 0) = False

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

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
note IH = less(1)[OF this]
[PROOF STATE]
proof (state)
this:
poly_rel ?f ?f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m ?f q) (power_poly_f_mod m' ?f' q)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
have rec: "poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q)
        (power_poly_f_mod m' (f' * f' mod m') q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)
[PROOF STEP]
by (rule IH, rule m, transfer_prover)
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
have other: "poly_rel
        (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f))
        (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
by (rule m, rule poly_rel_times[unfolded rel_fun_def, rule_format, OF rec f])
[PROOF STATE]
proof (state)
this:
poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)
[PROOF STEP]
unfolding power_poly_f_mod_i.simps[of _ _ _ n] Let_def
        power_poly_f_mod_binary[of _ _ n] div split n if_False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_rel (if r = 0 then power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q else m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (if r = 0 then power_poly_f_mod m' (f' * f' mod m') q else power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
using rec other
[PROOF STATE]
proof (prove)
using this:
poly_rel (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) (power_poly_f_mod m' (f' * f' mod m') q)
poly_rel (m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (power_poly_f_mod m' (f' * f' mod m') q * f' mod m')

goal (1 subgoal):
 1. poly_rel (if r = 0 then power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q else m (times_poly_i ff_ops (power_poly_f_mod_i ff_ops m (m (times_poly_i ff_ops f f)) q) f)) (if r = 0 then power_poly_f_mod m' (f' * f' mod m') q else power_poly_f_mod m' (f' * f' mod m') q * f' mod m')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly_rel f f' \<Longrightarrow> poly_rel (power_poly_f_mod_i ff_ops m f n) (power_poly_f_mod m' f' n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aType_empty:
  assumes h1:"msg (Suc 0) a"
         and h2: "a t \<noteq> [sc_ack]"
  shows       "a t = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a t = []
[PROOF STEP]
proof (cases "a t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a t = [] \<Longrightarrow> a t = []
 2. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
assume a1:"a t = []"
[PROOF STATE]
proof (state)
this:
a t = []

goal (2 subgoals):
 1. a t = [] \<Longrightarrow> a t = []
 2. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
a t = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a t = []

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

goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
fix aa l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
assume a2:"a t = aa # l"
[PROOF STATE]
proof (state)
this:
a t = aa # l

goal (1 subgoal):
 1. \<And>aa list. a t = aa # list \<Longrightarrow> a t = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a t = []
[PROOF STEP]
proof (cases "aa")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
assume a3:"aa = sc_ack"
[PROOF STATE]
proof (state)
this:
aa = sc_ack

goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
from h1
[PROOF STATE]
proof (chain)
picking this:
msg (Suc 0) a
[PROOF STEP]
have sg1:"length (a t) \<le> Suc 0"
[PROOF STATE]
proof (prove)
using this:
msg (Suc 0) a

goal (1 subgoal):
 1. length (a t) \<le> Suc 0
[PROOF STEP]
by (simp add: msg_def)
[PROOF STATE]
proof (state)
this:
length (a t) \<le> Suc 0

goal (1 subgoal):
 1. aa = sc_ack \<Longrightarrow> a t = []
[PROOF STEP]
from this and assms and a2 and a3
[PROOF STATE]
proof (chain)
picking this:
length (a t) \<le> Suc 0
msg (Suc 0) a
a t \<noteq> [sc_ack]
a t = aa # l
aa = sc_ack
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (a t) \<le> Suc 0
msg (Suc 0) a
a t \<noteq> [sc_ack]
a t = aa # l
aa = sc_ack

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Delay_L3:
 assumes h1:"\<forall>t1 \<le> t. y t1 = []"
        and h2:"Delay y i1 d x i2"
        and h3:"t2 \<le> t + d"
   shows "x t2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x t2 = []
[PROOF STEP]
proof (cases "t2 < d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
assume a1:"t2 < d"
[PROOF STATE]
proof (state)
this:
t2 < d

goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
Delay y i1 d x i2
[PROOF STEP]
have sg1:"t2 < d \<longrightarrow> x t2 = []"
[PROOF STATE]
proof (prove)
using this:
Delay y i1 d x i2

goal (1 subgoal):
 1. t2 < d \<longrightarrow> x t2 = []
[PROOF STEP]
by (simp add: Delay_def)
[PROOF STATE]
proof (state)
this:
t2 < d \<longrightarrow> x t2 = []

goal (2 subgoals):
 1. t2 < d \<Longrightarrow> x t2 = []
 2. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from sg1 and a1
[PROOF STATE]
proof (chain)
picking this:
t2 < d \<longrightarrow> x t2 = []
t2 < d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t2 < d \<longrightarrow> x t2 = []
t2 < d

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

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
assume a2:"\<not> t2 < d"
[PROOF STATE]
proof (state)
this:
\<not> t2 < d

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h2
[PROOF STATE]
proof (chain)
picking this:
Delay y i1 d x i2
[PROOF STEP]
have sg2:"d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)"
[PROOF STATE]
proof (prove)
using this:
Delay y i1 d x i2

goal (1 subgoal):
 1. d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)
[PROOF STEP]
by (simp add: Delay_def)
[PROOF STATE]
proof (state)
this:
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from a2 and sg2
[PROOF STATE]
proof (chain)
picking this:
\<not> t2 < d
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)
[PROOF STEP]
have sg3:"x t2 = y (t2 - d)"
[PROOF STATE]
proof (prove)
using this:
\<not> t2 < d
d \<le> t2 \<longrightarrow> x t2 = y (t2 - d)

goal (1 subgoal):
 1. x t2 = y (t2 - d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x t2 = y (t2 - d)

goal (1 subgoal):
 1. \<not> t2 < d \<Longrightarrow> x t2 = []
[PROOF STEP]
from h1 and a2 and h3 and sg3
[PROOF STATE]
proof (chain)
picking this:
\<forall>t1\<le>t. y t1 = []
\<not> t2 < d
t2 \<le> t + d
x t2 = y (t2 - d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>t1\<le>t. y t1 = []
\<not> t2 < d
t2 \<le> t + d
x t2 = y (t2 - d)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma edgeSet_finite:
  "finite (edgeSet s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edgeSet s)
[PROOF STEP]
by (simp add: edgeSet_def)


[STATEMENT]
lemma relation_of_Ndet: "relation_of (P \<sqinter> Q) = ((relation_of P) \<or> (relation_of Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action.relation_of (P \<sqinter> Q) = (action.relation_of P \<or> action.relation_of Q)
[PROOF STEP]
by (simp add: Ndet_def action_of_inverse Ndet_is_CSP)


[STATEMENT]
lemma sorted_sublist_wrt_le: \<open>hi \<le> lo \<Longrightarrow> hi < length xs \<Longrightarrow> sorted_sublist_wrt R xs lo hi\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi \<le> lo; hi < length xs\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo hi
[PROOF STEP]
apply (auto simp add: nat_le_eq_or_lt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo lo
 2. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_sublist_wrt R xs lo hi
[PROOF STEP]
unfolding sorted_sublist_wrt_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo lo)
 2. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo lo)
[PROOF STEP]
apply (rewrite sublist_single)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> lo < length xs
 2. \<lbrakk>lo < length xs; hi = lo\<rbrakk> \<Longrightarrow> sorted_wrt R [xs ! lo]
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hi < length xs; hi < lo\<rbrakk> \<Longrightarrow> sorted_wrt R (WB_Sort.sublist xs lo hi)
[PROOF STEP]
by (auto simp add: sublist_lt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bindET_unitET [simp]:
  "bindET\<cdot>(unitET\<cdot>x)\<cdot>k = k\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bindET\<cdot>(unitET\<cdot>x)\<cdot>k = k\<cdot>x
[PROOF STEP]
by (rule errorT_eqI, simp)


[STATEMENT]
lemma subindex_permutation2:
  assumes "distinct ss" "set ss \<subseteq> {..<length ls}"
  obtains f where "f permutes {..<length ls}"
    "ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f permutes {..<length ls}; ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subindex_permutation
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?ss; set ?ss \<subseteq> {..<length ?ls}; \<And>f. \<lbrakk>f permutes {..<length ?ls}; permute_list f ?ls = map ((!) ?ls) (filter (\<lambda>i. i \<notin> set ?ss) [0..<length ?ls]) @ map ((!) ?ls) ?ss\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f permutes {..<length ls}; ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(1) assms(2) length_permute_list mset_eq_permutation mset_permute_list)


[STATEMENT]
lemma r_tl [simp]: "eval r_tl [e] \<down>= e_tl e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_tl [e] \<down>= e_tl e
[PROOF STEP]
unfolding r_tl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (let r = Cn 1 r_pdec1 [r_dec] in Cn 1 r_ifz [recf.Id 1 0, Z, Cn 1 r_ifz [r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]) [e] \<down>= e_tl e
[PROOF STEP]
using e_tl_elementary
[PROOF STATE]
proof (prove)
using this:
e_tl ?e = (if ?e = 0 then 0 else if pdec1 (?e - 1) = 0 then 0 else Suc (prod_encode (pdec1 (?e - 1) - 1, pdec22 (?e - 1))))

goal (1 subgoal):
 1. eval (let r = Cn 1 r_pdec1 [r_dec] in Cn 1 r_ifz [recf.Id 1 0, Z, Cn 1 r_ifz [r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]) [e] \<down>= e_tl e
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma e_append_zeros_length: "e_length (e_append_zeros b z) = e_length b + z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_length (e_append_zeros b z) = e_length b + z
[PROOF STEP]
using e_append_def e_append_zeros_def
[PROOF STATE]
proof (prove)
using this:
e_append ?xs ?ys \<equiv> Partial_Recursive.list_encode (Partial_Recursive.list_decode ?xs @ Partial_Recursive.list_decode ?ys)
e_append_zeros ?b ?z \<equiv> e_append ?b (Partial_Recursive.list_encode (replicate ?z 0))

goal (1 subgoal):
 1. e_length (e_append_zeros b z) = e_length b + z
[PROOF STEP]
by simp


[STATEMENT]
lemma aux: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or>  (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> a; y \<noteq> b; x \<noteq> y \<and> x \<noteq> b \<or> a \<noteq> b \<and> a \<noteq> y\<rbrakk> \<Longrightarrow> {x, a} \<noteq> {y, b}
[PROOF STEP]
by (auto)


[STATEMENT]
lemma iso_in_homI [intro]:
    assumes "\<guillemotleft>f : a \<rightarrow> b\<guillemotright>" and "iso f"
    shows "\<guillemotleft>f : a \<cong> b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : a \<cong> b\<guillemotright>
[PROOF STEP]
using assms iso_in_hom_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a \<rightarrow> b\<guillemotright>
local.iso f
\<guillemotleft>?f : ?a \<cong> ?b\<guillemotright> \<equiv> \<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> \<and> local.iso ?f

goal (1 subgoal):
 1. \<guillemotleft>f : a \<cong> b\<guillemotright>
[PROOF STEP]
by simp


[STATEMENT]
lemma YFtorObj:
  assumes "LSCategory C" and "X \<in> Obj C"
  shows "(YFtor C) @@ X = Hom\<^bsub>C \<^esub>[\<midarrow>,X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
have "CatDom (YFtor' C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CatDom (YFtor' C) = C
[PROOF STEP]
by (simp add: YFtor'_def)
[PROOF STATE]
proof (state)
this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
hence "(YFtor' C) @@ X = Hom\<^bsub>C \<^esub>[\<midarrow>,X]"
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
by(simp add: YFtor'Obj)
[PROOF STATE]
proof (state)
this:
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
have "PreFunctor (YFtor' C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PreFunctor (YFtor' C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. PreFunctor (YFtor' C)
[PROOF STEP]
by (simp add: YFtorPreFtor)
[PROOF STATE]
proof (state)
this:
PreFunctor (YFtor' C)

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
by (simp add: MakeFtorObj YFtor_def)
[PROOF STATE]
proof (state)
this:
YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_vector_derivative_divide[derivative_intros]:
  fixes a :: "'a::real_normed_field"
  shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative (x / a)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative x / a) F
[PROOF STEP]
unfolding divide_inverse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * inverse a) has_vector_derivative x * inverse a) F
[PROOF STEP]
by (fact has_vector_derivative_mult_left)


[STATEMENT]
lemma seq_Lam_Arr_implies:
    shows "\<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof (induct U arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam
 2. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "\<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>seq [t] []; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>seq [?t] []; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set [] \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
fix u U t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume ind: "\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (state)
this:
\<lbrakk>seq [?t] U; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume uU: "seq [t] (u # U)"
[PROOF STATE]
proof (state)
this:
seq [t] (u # U)

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume t: "\<Lambda>.is_Lam t"
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam t

goal (1 subgoal):
 1. \<And>a U t. \<lbrakk>\<And>t. \<lbrakk>seq [t] U; \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam; seq [t] (a # U); \<Lambda>.is_Lam t\<rbrakk> \<Longrightarrow> set (a # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "set (u # U) \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "\<Lambda>.is_Lam u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Lambda>.is_Lam u
[PROOF STEP]
by (metis Trg_last_Src_hd_eqI \<Lambda>.Src.simps(1-2,4-5) \<Lambda>.Trg.simps(2) \<Lambda>.is_App_def
            \<Lambda>.is_Beta_def \<Lambda>.is_Lam_def \<Lambda>.is_Var_def \<Lambda>.lambda.disc(9) \<Lambda>.lambda.exhaust_disc
            last_ConsL list.sel(1) t uU)
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "set U \<subseteq> Collect \<Lambda>.is_Lam"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
proof (cases "U = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
 2. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show "U = [] \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U = [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
assume U: "U \<noteq> []"
[PROOF STATE]
proof (state)
this:
U \<noteq> []

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
have "seq [u] U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq [u] U
[PROOF STEP]
by (metis U append_Cons arr_append_imp_seq not_Cons_self2 self_append_conv2
                seqE uU)
[PROOF STATE]
proof (state)
this:
seq [u] U

goal (1 subgoal):
 1. U \<noteq> [] \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
seq [u] U

goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
using ind calculation
[PROOF STATE]
proof (prove)
using this:
seq [u] U
\<lbrakk>seq [?t] U; \<Lambda>.is_Lam ?t\<rbrakk> \<Longrightarrow> set U \<subseteq> Collect \<Lambda>.is_Lam
\<Lambda>.is_Lam u

goal (1 subgoal):
 1. set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set U \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Lambda>.is_Lam u
set U \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Lambda>.is_Lam u
set U \<subseteq> Collect \<Lambda>.is_Lam

goal (1 subgoal):
 1. set (u # U) \<subseteq> Collect \<Lambda>.is_Lam
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (u # U) \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (u # U) \<subseteq> Collect \<Lambda>.is_Lam

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma second_summands_in_sums: "P y (x \<oplus> y) \<and> P v (z \<oplus> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P y (x \<oplus> y) \<and> P v (z \<oplus> v)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P y (x \<oplus> y)
 2. P v (z \<oplus> v)
[PROOF STEP]
show "P y (x \<oplus> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P y (x \<oplus> y)
[PROOF STEP]
using second_summand_in_sum
[PROOF STATE]
proof (prove)
using this:
P ?y (?x \<oplus> ?y)

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

goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
show "P v (z \<oplus> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
using second_summand_in_sum
[PROOF STATE]
proof (prove)
using this:
P ?y (?x \<oplus> ?y)

goal (1 subgoal):
 1. P v (z \<oplus> v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P v (z \<oplus> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "Fr_2 \<F> \<Longrightarrow> \<forall>A B. Cl(A) \<longrightarrow> CoP3\<^sup>A\<^sup>B \<^bold>\<not>\<^sup>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A. contains (\<lambda>B. contains A B \<longleftarrow> contains (\<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I A)) (\<lambda>B. \<forall>w. \<C> A w = A w)
[PROOF STEP]
by (metis Disj_I ICdual' compl_def dual_def eq_ext' meet_def neg_I_def)


[STATEMENT]
lemma "Fr_2 \<F> \<Longrightarrow> \<forall>A B. Cl(A) \<and> Cl(B) \<longrightarrow> DM1\<^sup>A\<^sup>B \<^bold>\<not>\<^sup>I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A. contains (\<lambda>B. contains (\<^bold>\<not>\<^sup>I A \<^bold>\<and> \<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I (A \<^bold>\<or> B))) (\<lambda>B. (\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<C> B w = B w))
[PROOF STEP]
using pF2 pI2 conn
[PROOF STATE]
proof (prove)
using this:
Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<F> A w = (\<C> A \<^bold>\<and> \<C> (\<^bold>\<midarrow>A)) w
\<forall>A w. \<I> A w = (A \<^bold>\<leftharpoonup> \<F> A) w
?A \<^bold>\<and> ?B \<equiv> \<lambda>w. ?A w \<and> ?B w
?A \<^bold>\<or> ?B \<equiv> \<lambda>w. ?A w \<or> ?B w
\<^bold>\<top> \<equiv> \<lambda>w. True
\<^bold>\<bottom> \<equiv> \<lambda>w. False
?A \<^bold>\<rightarrow> ?B \<equiv> \<lambda>w. ?B w \<longleftarrow> ?A w
?A \<^bold>\<leftrightarrow> ?B \<equiv> \<lambda>w. ?A w = ?B w
?A \<^bold>\<leftharpoonup> ?B \<equiv> \<lambda>w. ?A w \<and> \<not> ?B w
\<^bold>\<midarrow>?A \<equiv> \<lambda>w. \<not> ?A w
\<^bold>\<not>\<^sup>I ?\<phi> \<equiv> \<I> (\<^bold>\<midarrow>?\<phi>)
\<^bold>\<not>\<^sup>C ?\<phi> \<equiv> \<C> (\<^bold>\<midarrow>?\<phi>)

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A. contains (\<lambda>B. contains (\<^bold>\<not>\<^sup>I A \<^bold>\<and> \<^bold>\<not>\<^sup>I B) (\<^bold>\<not>\<^sup>I (A \<^bold>\<or> B))) (\<lambda>B. (\<forall>w. \<C> A w = A w) \<and> (\<forall>w. \<C> B w = B w))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma app_insf2_Seq: "Seq s k \<Longrightarrow> k' \<noteq> k \<Longrightarrow> app (insf s k y) k' = app s k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s k; k' \<noteq> k\<rbrakk> \<Longrightarrow> app (insf s k y) k' = app s k'
[PROOF STEP]
by (simp add: app_nonrestrict_Seq insf_def app_ins2)


[STATEMENT]
lemma Apps_Var_neq_Apps_beta[simp, THEN not_sym, simp]:
  "\<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<cdot> s \<bullet> ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<cdot> s \<bullet> ts
[PROOF STEP]
by (metis Apps_Var_neq_Apps_Abs Apps_append Apps_snoc eq_Apps_conv(9))


[STATEMENT]
lemma invarNT_K1exit: "invarNT (K1exit cid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invarNT (K1exit cid)
[PROOF STEP]
unfolding invarNT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K1exit cid s \<and> \<not> T (Trans s a ou s') \<and> step s a = (ou, s') \<longrightarrow> K1exit cid s'
[PROOF STEP]
apply (safe dest!: reachNT_reach)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reach s; K1exit cid s; \<not> T (Trans s a ou s'); step s a = (ou, s')\<rbrakk> \<Longrightarrow> K1exit cid s'
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_)\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConf x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPC x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cChair x41 x42 x43 x44\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPaper x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cAuthor x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConflict x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> K1exit cid s'_
 8. \<And>x81 x82 x83 x84 x85. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cReview x81 x82 x83 x84 x85\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: c_defs K1exit_def geq_noPH_confIDs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 6. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 5. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x61
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases "x61 = cid")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_; x61 = cid\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62_ x63_ x64_ x65_; x61 \<noteq> cid\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K1exit cid s'_
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> K1exit cid s'_
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: uu_defs K1exit_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K1exit cid s'_
 2. \<And>x5. \<lbrakk>reach s_; K1exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K1exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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