[STATEMENT]
lemma checkNet3_correct: "checkNet3 el s t \<le> checkNet2 el s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. checkNet3 el s t \<le> checkNet2 el s t
[PROOF STEP]
unfolding checkNet3_def checkNet2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if s = t then return None else let rd = read' el s t in case rd of None \<Rightarrow> return None | Some x \<Rightarrow> if pn_s_node' x \<and> pn_t_node' x then assert (finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})) \<bind> (\<lambda>_. assert (finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u)) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u)) \<bind> (\<lambda>_. let succ_s = reachable_impl (graph_of_impl x s); pred_t = reachable_impl (rev_graph_of_impl x t) in if sets_eq_impl (pn_V' x) succ_s \<and> sets_eq_impl (pn_V' x) pred_t then return (Some (net_\<alpha> (pn_c' x, pn_adjmap' x))) else return None)))) else return None) \<le> (if s = t then return None else let rd = read el s t in case rd of None \<Rightarrow> return None | Some x \<Rightarrow> if pn_s_node x \<and> pn_t_node x then assert (finite ((Graph.E (pn_c x))\<^sup>* `` {s})) \<bind> (\<lambda>_. assert (finite (((Graph.E (pn_c x))\<inverse>)\<^sup>* `` {t})) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_succ x u) = Graph.E (pn_c x) `` {u} \<and> distinct (pn_succ x u)) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_pred x u) = (Graph.E (pn_c x))\<inverse> `` {u} \<and> distinct (pn_pred x u)) \<bind> (\<lambda>_. let succ_s = op_reachable (graph_of x s); pred_t = op_reachable (rev_graph_of x t) in if pn_V x = succ_s \<and> pn_V x = pred_t then return (Some (pn_c x, pn_adjmap x)) else return None)))) else return None)
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if s = t then return None else let rd = read' el s t in case rd of None \<Rightarrow> return None | Some x \<Rightarrow> if pn_s_node' x \<and> pn_t_node' x then assert (finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})) \<bind> (\<lambda>_. assert (finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u)) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u)) \<bind> (\<lambda>_. let succ_s = reachable_impl (graph_of_impl x s); pred_t = reachable_impl (rev_graph_of_impl x t) in if sets_eq_impl (pn_V' x) succ_s \<and> sets_eq_impl (pn_V' x) pred_t then return (Some (net_\<alpha> (pn_c' x, pn_adjmap' x))) else return None)))) else return None) \<le> \<Down> Id (if s = t then return None else let rd = read el s t in case rd of None \<Rightarrow> return None | Some x \<Rightarrow> if pn_s_node x \<and> pn_t_node x then assert (finite ((Graph.E (pn_c x))\<^sup>* `` {s})) \<bind> (\<lambda>_. assert (finite (((Graph.E (pn_c x))\<inverse>)\<^sup>* `` {t})) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_succ x u) = Graph.E (pn_c x) `` {u} \<and> distinct (pn_succ x u)) \<bind> (\<lambda>_. assert (\<forall>u. set (pn_pred x u) = (Graph.E (pn_c x))\<inverse> `` {u} \<and> distinct (pn_pred x u)) \<bind> (\<lambda>_. let succ_s = op_reachable (graph_of x s); pred_t = op_reachable (rev_graph_of x t) in if pn_V x = succ_s \<and> pn_V x = pred_t then return (Some (pn_c x, pn_adjmap x)) else return None)))) else return None)
[PROOF STEP]
apply (refine_rcg)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. (s = t) = (s = t)
 2. \<lbrakk>s \<noteq> t; s \<noteq> t\<rbrakk> \<Longrightarrow> (read' el s t, read el s t) \<in> \<langle>?Ra5\<rangle>option_rel
 3. \<And>x x'. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5\<rbrakk> \<Longrightarrow> (pn_s_node' x \<and> pn_t_node' x) = (pn_s_node x' \<and> pn_t_node x')
 4. \<And>x x'. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u)\<rbrakk> \<Longrightarrow> finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})
 5. \<And>x x'. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})\<rbrakk> \<Longrightarrow> finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})
 6. \<And>x x' u. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})\<rbrakk> \<Longrightarrow> set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u}
 7. \<And>x x' u. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})\<rbrakk> \<Longrightarrow> distinct (pn_succ (pnet_\<alpha> x) u)
 8. \<And>x x' u. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u)\<rbrakk> \<Longrightarrow> set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u}
 9. \<And>x x' u. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u)\<rbrakk> \<Longrightarrow> distinct (pn_pred (pnet_\<alpha> x) u)
 10. \<And>x x'. \<lbrakk>s \<noteq> t; s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; pn_s_node' x \<and> pn_t_node' x; pn_s_node x' \<and> pn_t_node x'; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u)\<rbrakk> \<Longrightarrow> (sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = op_reachable (graph_of x' s) \<and> pn_V x' = op_reachable (rev_graph_of x' t))
A total of 11 subgoals...
[PROOF STEP]
apply clarsimp_all
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. s \<noteq> t \<Longrightarrow> (read' el s t, read el s t) \<in> \<langle>?Ra5\<rangle>option_rel
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5\<rbrakk> \<Longrightarrow> (pn_s_node' x \<and> pn_t_node' x) = (pn_s_node x' \<and> pn_t_node x')
 3. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})
 4. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})
 5. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u}
 6. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_succ (pnet_\<alpha> x) u)
 7. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u}
 8. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_pred (pnet_\<alpha> x) u)
 9. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 10. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> ?Ra5; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (rule introR[where R="\<langle>pnet_rel\<rangle>option_rel"])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. s \<noteq> t \<Longrightarrow> (read' el s t, read el s t) \<in> \<langle>pnet_rel\<rangle>option_rel
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel\<rbrakk> \<Longrightarrow> (pn_s_node' x \<and> pn_t_node' x) = (pn_s_node x' \<and> pn_t_node x')
 3. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})
 4. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})
 5. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u}
 6. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_succ (pnet_\<alpha> x) u)
 7. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u}
 8. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_pred (pnet_\<alpha> x) u)
 9. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 10. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (simp add: read'_correct_alt; fail)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel\<rbrakk> \<Longrightarrow> (pn_s_node' x \<and> pn_t_node' x) = (pn_s_node x' \<and> pn_t_node x')
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s})
 3. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t})
 4. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u}
 5. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_succ (pnet_\<alpha> x) u)
 6. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u}
 7. \<And>x x' u. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> distinct (pn_pred (pnet_\<alpha> x) u)
 8. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 9. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply ((simp add: pnet_rel_def br_def pnet_\<alpha>_def)+) [7]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (subst sets_eq_impl_correct_aux1; assumption?)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> well_formed_pn x'
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 3. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (simp add: well_formed_pn_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t))) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (subst sets_eq_impl_correct_aux2; assumption?)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> rev_well_formed_pn x'
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t)) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 3. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (simp add: rev_well_formed_pn_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'\<rbrakk> \<Longrightarrow> (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t)) = (pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s) \<and> pn_V x' = (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t))
 2. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x'. \<lbrakk>s \<noteq> t; read' el s t = Some x; read el s t = Some x'; (x, x') \<in> pnet_rel; finite ((Graph.E (pn_c x'))\<^sup>* `` {s}); finite (((Graph.E (pn_c x'))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ x' u) = Graph.E (pn_c x') `` {u} \<and> distinct (pn_succ x' u); \<forall>u. set (pn_pred x' u) = (Graph.E (pn_c x'))\<inverse> `` {u} \<and> distinct (pn_pred x' u); finite ((Graph.E (pn_c (pnet_\<alpha> x)))\<^sup>* `` {s}); finite (((Graph.E (pn_c (pnet_\<alpha> x)))\<inverse>)\<^sup>* `` {t}); \<forall>u. set (pn_succ (pnet_\<alpha> x) u) = Graph.E (pn_c (pnet_\<alpha> x)) `` {u} \<and> distinct (pn_succ (pnet_\<alpha> x) u); \<forall>u. set (pn_pred (pnet_\<alpha> x) u) = (Graph.E (pn_c (pnet_\<alpha> x)))\<inverse> `` {u} \<and> distinct (pn_pred (pnet_\<alpha> x) u); pn_s_node' x; pn_t_node' x; pn_s_node x'; pn_t_node x'; sets_eq_impl (pn_V' x) (reachable_impl (graph_of_impl x s)); sets_eq_impl (pn_V' x) (reachable_impl (rev_graph_of_impl x t)); (g_E (rev_graph_of x' t))\<^sup>* `` g_V0 (rev_graph_of x' t) = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s); pn_V x' = (g_E (graph_of x' s))\<^sup>* `` g_V0 (graph_of x' s)\<rbrakk> \<Longrightarrow> net_\<alpha> (pn_c' x, pn_adjmap' x) = (pn_c x', pn_adjmap x')
[PROOF STEP]
apply (simp add: net_\<alpha>_def o_def pnet_\<alpha>_def pnet_rel_def br_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma enat_of_option_inj[simp]: "enat_of_option x = enat_of_option y \<longleftrightarrow> x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (enat_of_option x = enat_of_option y) = (x = y)
[PROOF STEP]
by (cases x; cases y; simp)


[STATEMENT]
lemma Field_set_code: "Field (set rel) = set (exefield rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (set rel) = set (exefield rel)
[PROOF STEP]
by (induction rel) fastforce+


[STATEMENT]
lemma pF3: "Fr_2 \<F> \<Longrightarrow> \<forall>A. \<F> A \<^bold>\<approx> \<B> A \<^bold>\<or> \<B>(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<F> A w = (\<B> A \<^bold>\<or> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
using Br_fr_def Fr_2_def conn
[PROOF STATE]
proof (prove)
using this:
\<B>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<and> ?\<F> A
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<^bold>\<midarrow>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

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. \<F> A w = (\<B> A \<^bold>\<or> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
by auto


[STATEMENT]
lemma IC_imp: "Fr_1 \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> \<forall>A B. \<I>(A \<^bold>\<rightarrow> B) \<^bold>\<preceq> \<C> A \<^bold>\<rightarrow> \<C> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
assume fr1: "Fr_1 \<F>" and fr2: "Fr_2 \<F>" and fr3: "Fr_3 \<F>"
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Fr_1 \<F>
Fr_2 \<F>
Fr_3 \<F>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
have "(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>b \<^bold>\<rightarrow> \<^bold>\<midarrow>a = \<^bold>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a = \<^bold>\<top>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. \<not> a w \<longleftarrow> (b w \<longleftarrow> a w) \<and> \<not> b w) = (\<lambda>w. True)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a = \<^bold>\<top>

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
hence "\<I>((a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) \<^bold>\<approx> \<I>(\<^bold>\<top>)"
[PROOF STATE]
proof (prove)
using this:
((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a = \<^bold>\<top>

goal (1 subgoal):
 1. \<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<I> \<^bold>\<top> w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<I> \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
hence "\<I>((a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<I> \<^bold>\<top> w

goal (1 subgoal):
 1. \<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w
[PROOF STEP]
using fr3 IF3 dNOR_def fr2
[PROOF STATE]
proof (prove)
using this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<I> \<^bold>\<top> w
Fr_3 \<F>
\<lbrakk>Fr_2 ?\<phi>; Fr_3 ?\<phi>\<rbrakk> \<Longrightarrow> Cl_5 (\<I>\<^sub>F ?\<phi>)
Cl_5 ?\<phi> \<equiv> \<forall>w. ?\<phi> \<^bold>\<top> w = \<^bold>\<top> w
Fr_2 \<F>

goal (1 subgoal):
 1. \<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
have "let A=(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>b; B=\<^bold>\<midarrow>a in \<I>(A \<^bold>\<rightarrow> B) \<^bold>\<preceq> \<I>(A) \<^bold>\<rightarrow> \<I>(B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let A = ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b; B = \<^bold>\<midarrow>a in contains (\<I> A \<^bold>\<rightarrow> \<I> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
using fr1 IF1 PI7 Int_7_def
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_1 ?\<phi> \<Longrightarrow> Int_1 (\<I>\<^sub>F ?\<phi>)
Int_1 ?\<phi> \<Longrightarrow> Int_7 ?\<phi>
Int_7 ?\<phi> \<equiv> \<forall>A B. contains (?\<phi> A \<^bold>\<rightarrow> ?\<phi> B) (?\<phi> (A \<^bold>\<rightarrow> B))

goal (1 subgoal):
 1. let A = ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b; B = \<^bold>\<midarrow>a in contains (\<I> A \<^bold>\<rightarrow> \<I> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
let A = ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b; B = \<^bold>\<midarrow>a in contains (\<I> A \<^bold>\<rightarrow> \<I> B) (\<I> (A \<^bold>\<rightarrow> B))

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w
let A = ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b; B = \<^bold>\<midarrow>a in contains (\<I> A \<^bold>\<rightarrow> \<I> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
have "\<I>((a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I>(\<^bold>\<midarrow>a) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. \<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b \<^bold>\<rightarrow> \<^bold>\<midarrow>a) w = \<^bold>\<top> w
let A = ((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b; B = \<^bold>\<midarrow>a in contains (\<I> A \<^bold>\<rightarrow> \<I> B) (\<I> (A \<^bold>\<rightarrow> B))

goal (1 subgoal):
 1. \<forall>w. (\<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<forall>w. \<I> (\<lambda>w. \<not> a w \<longleftarrow> (b w \<longleftarrow> a w) \<and> \<not> b w) w = True
let A = \<lambda>w. (b w \<longleftarrow> a w) \<and> \<not> b w; B = \<lambda>w. \<not> a w in contains (\<lambda>w. \<I> B w \<longleftarrow> \<I> A w) (\<I> (\<lambda>w. B w \<longleftarrow> A w))

goal (1 subgoal):
 1. \<forall>w. (\<I> (\<lambda>w. \<not> a w) w \<longleftarrow> \<I> (\<lambda>w. (b w \<longleftarrow> a w) \<and> \<not> b w) w) = True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
have "let A=a \<^bold>\<rightarrow> b; B=\<^bold>\<midarrow>b in \<I>(A \<^bold>\<and> B) \<^bold>\<approx> \<I>(A) \<^bold>\<and> \<I>(B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<midarrow>b in \<forall>w. \<I> (A \<^bold>\<and> B) w = (\<I> A \<^bold>\<and> \<I> B) w
[PROOF STEP]
using fr1 IF1 MULT_def
[PROOF STATE]
proof (prove)
using this:
Fr_1 \<F>
Fr_1 ?\<phi> \<Longrightarrow> Int_1 (\<I>\<^sub>F ?\<phi>)
Int_1 ?\<phi> \<equiv> \<forall>A B w. ?\<phi> (A \<^bold>\<and> B) w = (?\<phi> A \<^bold>\<and> ?\<phi> B) w

goal (1 subgoal):
 1. let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<midarrow>b in \<forall>w. \<I> (A \<^bold>\<and> B) w = (\<I> A \<^bold>\<and> \<I> B) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<midarrow>b in \<forall>w. \<I> (A \<^bold>\<and> B) w = (\<I> A \<^bold>\<and> \<I> B) w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. (\<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<midarrow>b in \<forall>w. \<I> (A \<^bold>\<and> B) w = (\<I> A \<^bold>\<and> \<I> B) w
[PROOF STEP]
have "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I>(\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I>(\<^bold>\<midarrow>a) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<I> (((\<^bold>\<rightarrow>) a \<^bold>\<sqinter> compl) b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
let A = a \<^bold>\<rightarrow> b; B = \<^bold>\<midarrow>b in \<forall>w. \<I> (A \<^bold>\<and> B) w = (\<I> A \<^bold>\<and> \<I> B) w

goal (1 subgoal):
 1. \<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I> (\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<I> (\<lambda>w. \<not> a w) w \<longleftarrow> \<I> (\<lambda>w. (b w \<longleftarrow> a w) \<and> \<not> b w) w) = True
let A = \<lambda>w. b w \<longleftarrow> a w; B = \<lambda>w. \<not> b w in \<forall>w. \<I> (\<lambda>w. A w \<and> B w) w = (\<I> A w \<and> \<I> B w)

goal (1 subgoal):
 1. \<forall>w. (\<I> (\<lambda>w. \<not> a w) w \<longleftarrow> \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<I> (\<lambda>w. \<not> b w) w) = True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I> (\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I> (\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
have "\<forall>A. \<I>(\<^bold>\<midarrow>A) \<^bold>\<approx> \<^bold>\<midarrow>\<C>(A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. \<I> (\<^bold>\<midarrow>A) w = \<C>\<^sup>c A w
[PROOF STEP]
using Cl_fr_def Fr_2_def Int_fr_def fr2
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<or> ?\<F> A
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<^bold>\<midarrow>A) w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A. A \<^bold>\<leftharpoonup> ?\<F> A
Fr_2 \<F>

goal (1 subgoal):
 1. \<forall>A w. \<I> (\<^bold>\<midarrow>A) w = \<C>\<^sup>c A w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<or> ?\<F> A w
Fr_2 ?\<phi> \<equiv> \<forall>A w. ?\<phi> A w = ?\<phi> (\<lambda>w. \<not> A w) w
\<I>\<^sub>F ?\<F> \<equiv> \<lambda>A w. A w \<and> \<not> ?\<F> A w
Fr_2 \<F>

goal (1 subgoal):
 1. \<forall>A w. \<I> (\<lambda>w. \<not> A w) w = (\<not> \<C> A w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A w. \<I> (\<^bold>\<midarrow>A) w = \<C>\<^sup>c A w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I> (\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
\<forall>A w. \<I> (\<^bold>\<midarrow>A) w = \<C>\<^sup>c A w
[PROOF STEP]
have "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>\<C>(b) \<^bold>\<rightarrow> \<^bold>\<midarrow>\<C>(a) \<^bold>\<approx> \<^bold>\<top>"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<I> (\<^bold>\<midarrow>b) \<^bold>\<rightarrow> \<I> (\<^bold>\<midarrow>a)) w = \<^bold>\<top> w
\<forall>A w. \<I> (\<^bold>\<midarrow>A) w = \<C>\<^sup>c A w

goal (1 subgoal):
 1. \<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b \<^bold>\<rightarrow> \<C>\<^sup>c a) w = \<^bold>\<top> w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<I> (\<lambda>w. \<not> a w) w \<longleftarrow> \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<I> (\<lambda>w. \<not> b w) w) = True
\<forall>A w. \<I> (\<lambda>w. \<not> A w) w = (\<not> \<C> A w)

goal (1 subgoal):
 1. \<forall>w. (\<not> \<C> a w \<longleftarrow> \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<not> \<C> b w) = True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b \<^bold>\<rightarrow> \<C>\<^sup>c a) w = \<^bold>\<top> w

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
hence "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<^bold>\<midarrow>\<C>(b) \<^bold>\<preceq> \<^bold>\<midarrow>\<C>(a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b \<^bold>\<rightarrow> \<C>\<^sup>c a) w = \<^bold>\<top> w

goal (1 subgoal):
 1. contains (\<C>\<^sup>c a) (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<forall>w. (\<not> \<C> a w \<longleftarrow> \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<not> \<C> b w) = True

goal (1 subgoal):
 1. contains (\<lambda>w. \<not> \<C> a w) (\<lambda>w. \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<not> \<C> b w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<C>\<^sup>c a) (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
hence "\<I>(a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C> a \<^bold>\<preceq> \<C> b"
[PROOF STATE]
proof (prove)
using this:
contains (\<C>\<^sup>c a) (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C>\<^sup>c b)

goal (1 subgoal):
 1. contains (\<C> b) (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C> a)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
contains (\<lambda>w. \<not> \<C> a w) (\<lambda>w. \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<not> \<C> b w)

goal (1 subgoal):
 1. contains (\<C> b) (\<lambda>w. \<I> (\<lambda>w. b w \<longleftarrow> a w) w \<and> \<C> a w)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
contains (\<C> b) (\<I> (a \<^bold>\<rightarrow> b) \<^bold>\<and> \<C> a)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<C> ?b2) (\<I> (?a2 \<^bold>\<rightarrow> ?b2) \<^bold>\<and> \<C> ?a2)

goal (1 subgoal):
 1. \<lbrakk>Fr_1 \<F>; Fr_2 \<F>; Fr_3 \<F>\<rbrakk> \<Longrightarrow> \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<C> ?b2) (\<I> (?a2 \<^bold>\<rightarrow> ?b2) \<^bold>\<and> \<C> ?a2)

goal (1 subgoal):
 1. \<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
contains (\<C> ?b2) (\<lambda>w. \<I> (\<lambda>w. ?b2 w \<longleftarrow> ?a2 w) w \<and> \<C> ?a2 w)

goal (1 subgoal):
 1. \<forall>A B. contains (\<lambda>w. \<C> B w \<longleftarrow> \<C> A w) (\<I> (\<lambda>w. B w \<longleftarrow> A w))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>A B. contains (\<C> A \<^bold>\<rightarrow> \<C> B) (\<I> (A \<^bold>\<rightarrow> B))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c_list_prepend_h_disjunct:
  assumes "distinct (ys@xs)"
  shows "c_list f cf (create_h_list h (ys@xs)) r xs = c_list f cf (create_h_list h xs) r xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (ys @ xs)

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
[PROOF STEP]
proof(induction xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
distinct (?ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (?ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct (ys @ x # xs)

goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (?ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (?ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct (ys @ x # xs)
[PROOF STEP]
have 0: "distinct (ys @ [x] @ xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (?ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (?ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct (ys @ x # xs)

goal (1 subgoal):
 1. distinct (ys @ [x] @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (ys @ [x] @ xs)

goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (ys @ [x] @ xs)
[PROOF STEP]
have 1: "distinct ([x] @ xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (ys @ [x] @ xs)

goal (1 subgoal):
 1. distinct ([x] @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct ([x] @ xs)

goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
let ?h = "create_h_list h (ys @ x # xs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
let ?h' = "create_h_list h xs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
let ?h'' = "create_h_list h (x#xs)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
have 2: "x \<notin> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set ys
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
distinct (ys @ x # xs)

goal (1 subgoal):
 1. x \<notin> set ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set ys

goal (2 subgoals):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. distinct (ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs; distinct (ys @ a # xs)\<rbrakk> \<Longrightarrow> c_list f cf (create_h_list h (ys @ a # xs)) r (a # xs) = c_list f cf (create_h_list h (a # xs)) r (a # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
proof(cases "xs=[]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
 2. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
using Cons distinct_create_eq_app in_multiset_in_set
[PROOF STATE]
proof (prove)
using this:
xs = []
distinct (?ys @ xs) \<Longrightarrow> c_list f cf (create_h_list h (?ys @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct (ys @ x # xs)
\<lbrakk>distinct (?ys @ ?xs); ?x \<in># mset ?xs\<rbrakk> \<Longrightarrow> create_h_list ?h ?xs ?x = create_h_list ?h (?ys @ ?xs) ?x
(?x \<in># mset ?xs) = (?x \<in> set ?xs)

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
by (metis CostFunctions.c_list.simps(2) List.list.set_intros(1))
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
obtain x' xs' where x'_def[simp]: "xs = x'#xs'"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>x' xs'. xs = x' # xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using List.list.exhaust_sel
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
\<lbrakk>?list = [] \<Longrightarrow> ?P; ?list = hd ?list # tl ?list \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x' xs'. xs = x' # xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs = x' # xs'

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = x' # xs'
[PROOF STEP]
have "c_list f cf ?h r (x # xs)
        = c_list f cf ?h r xs + ldeep_T f cf xs * c_list f cf ?h r [x]"
[PROOF STATE]
proof (prove)
using this:
xs = x' # xs'

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
have "\<dots> = c_list f cf ?h' r xs + ldeep_T f cf xs * c_list f cf ?h r [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]
[PROOF STEP]
using Cons.IH[of "ys@[x]"] 0
[PROOF STATE]
proof (prove)
using this:
distinct ((ys @ [x]) @ xs) \<Longrightarrow> c_list f cf (create_h_list h ((ys @ [x]) @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct (ys @ [x] @ xs)

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
have "\<dots> = c_list f cf ?h'' r xs + ldeep_T f cf xs * c_list f cf ?h r [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]
[PROOF STEP]
using Cons.IH[of "[x]"] 1
[PROOF STATE]
proof (prove)
using this:
distinct ([x] @ xs) \<Longrightarrow> c_list f cf (create_h_list h ([x] @ xs)) r xs = c_list f cf (create_h_list h xs) r xs
distinct ([x] @ xs)

goal (1 subgoal):
 1. c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h xs) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
have "\<dots> = c_list f cf ?h'' r xs + ldeep_T f cf xs * c_list f cf ?h'' r [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (x # xs)) r [x]
[PROOF STEP]
using c_list_single_h_list_not_elem_prepend 2
[PROOF STATE]
proof (prove)
using this:
?x \<notin> set ?ys \<Longrightarrow> c_list ?f ?cf (create_h_list ?h (?ys @ ?x # ?xs)) ?r [?x] = c_list ?f ?cf (create_h_list ?h (?x # ?xs)) ?r [?x]
x \<notin> set ys

goal (1 subgoal):
 1. c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (x # xs)) r [x]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (ys @ x # xs)) r [x] = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (x # xs)) r [x]

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (x # xs)) r [x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r xs + ldeep_T f cf xs * c_list f cf (create_h_list h (x # xs)) r [x]

goal (1 subgoal):
 1. c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c_list f cf (create_h_list h (ys @ x # xs)) r (x # xs) = c_list f cf (create_h_list h (x # xs)) r (x # xs)

goal (1 subgoal):
 1. \<And>ys. distinct (ys @ []) \<Longrightarrow> c_list f cf (create_h_list h (ys @ [])) r [] = c_list f cf (create_h_list h []) r []
[PROOF STEP]
qed(simp)


[STATEMENT]
theorem c_out_eq_c_list_hlist:
  fixes f cf t
  defines "h \<equiv> (\<lambda>xs x. (list_sel_aux' f xs x) * cf x)"
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs = c_out cf f t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs = c_out cf f t
[PROOF STEP]
using c_IKKBZ_eq_c_list_cout_hlist c_out_IKKBZ assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct_relations ?t; reasonable_cards ?cf ?f ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_IKKBZ (\<lambda>a. (*) (ldeep_s ?f (revorder ?t) a)) ?cf ?f ?t = c_list (ldeep_s ?f (revorder ?t)) ?cf (create_h_list (\<lambda>xs x. list_sel_aux' ?f xs x * ?cf x) (revorder ?t)) (first_node ?t) (revorder ?t)
\<lbrakk>distinct_relations ?t; reasonable_cards ?cf ?f ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_IKKBZ (\<lambda>a. (*) (ldeep_s ?f (revorder ?t) a)) ?cf ?f ?t = c_out ?cf ?f ?t
h \<equiv> \<lambda>xs x. list_sel_aux' f xs x * cf x
xs \<equiv> revorder t
distinct_relations t
reasonable_cards cf f t
left_deep t

goal (1 subgoal):
 1. c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs = c_out cf f t
[PROOF STEP]
by fastforce


[STATEMENT]
lemma prfx_reflexive:
    assumes "arr t"
    shows "t \<lesssim> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<lesssim> t
[PROOF STEP]
by (simp add: assms resid_arr_self)


[STATEMENT]
lemma preserves_joins:
    assumes "A.join_of t u v"
    shows "B.join_of (F t) (F u) (F v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.join_of (F t) (F u) (F v)
[PROOF STEP]
using assms A.join_of_def B.join_of_def A.joinable_def
[PROOF STATE]
proof (prove)
using this:
A.join_of t u v
A.join_of ?t ?u ?v \<equiv> A.composite_of ?t (?u \\<^sub>A ?t) ?v \<and> A.composite_of ?u (?t \\<^sub>A ?u) ?v
B.join_of ?t ?u ?v \<equiv> B.composite_of ?t (?u \\<^sub>B ?t) ?v \<and> B.composite_of ?u (?t \\<^sub>B ?u) ?v
A.joinable ?t ?u \<equiv> \<exists>v. A.join_of ?t ?u v

goal (1 subgoal):
 1. B.join_of (F t) (F u) (F v)
[PROOF STEP]
by (metis A.joinable_implies_con preserves_composites preserves_resid)


[STATEMENT]
lemma red_lcl_incr: "P \<turnstile> \<langle>e,(h\<^sub>0,l\<^sub>0,sh\<^sub>0),b\<rangle> \<rightarrow> \<langle>e',(h\<^sub>1,l\<^sub>1,sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
and reds_lcl_incr: "P \<turnstile> \<langle>es,(h\<^sub>0,l\<^sub>0,sh\<^sub>0),b\<rangle> [\<rightarrow>] \<langle>es',(h\<^sub>1,l\<^sub>1,sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile> \<langle>e,(h\<^sub>0, l\<^sub>0, sh\<^sub>0),b\<rangle> \<rightarrow> \<langle>e',(h\<^sub>1, l\<^sub>1, sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1) &&& (P \<turnstile> \<langle>es,(h\<^sub>0, l\<^sub>0, sh\<^sub>0),b\<rangle> [\<rightarrow>] \<langle>es',(h\<^sub>1, l\<^sub>1, sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile> \<langle>e,(h\<^sub>0, l\<^sub>0, sh\<^sub>0),b\<rangle> \<rightarrow> \<langle>e',(h\<^sub>1, l\<^sub>1, sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1) &&& (P \<turnstile> \<langle>es,(h\<^sub>0, l\<^sub>0, sh\<^sub>0),b\<rangle> [\<rightarrow>] \<langle>es',(h\<^sub>1, l\<^sub>1, sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1)
[PROOF STEP]
by(induct rule: red_reds_inducts)(auto simp del:fun_upd_apply)


[STATEMENT]
lemma PO_m3_observation_consistent [iff]:
  "obs_consistent R23 med32 m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R23 med32 m2 m3
[PROOF STEP]
by (auto simp add: obs_consistent_def R23_def med32_def m3_defs)


[STATEMENT]
lemma angular_component_ord_zero:
  assumes "ord x = 0"
  assumes "x \<in> nonzero Q\<^sub>p"
  shows "\<iota> (angular_component x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
have 0: "ord x \<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> ord x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ord x = 0
x \<in> nonzero Q\<^sub>p

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

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
have 1: "x \<in> nonzero Q\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> nonzero Q\<^sub>p
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> nonzero Q\<^sub>p
[PROOF STEP]
have "x \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<zero>
[PROOF STEP]
using nonzero_def assms(2)  Qp.nonzero_memE(2)
[PROOF STATE]
proof (prove)
using this:
nonzero ?R = {a \<in> carrier ?R. a \<noteq> \<zero>\<^bsub>?R\<^esub>}
x \<in> nonzero Q\<^sub>p
?a \<in> nonzero Q\<^sub>p \<Longrightarrow> ?a \<noteq> \<zero>

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

goal (1 subgoal):
 1. x \<in> nonzero Q\<^sub>p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<zero>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<zero>

goal (1 subgoal):
 1. x \<in> nonzero Q\<^sub>p
[PROOF STEP]
by (simp add: assms(2))
[PROOF STATE]
proof (state)
this:
x \<in> nonzero Q\<^sub>p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> nonzero Q\<^sub>p

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
obtain a where a_def: "a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 0 1 assms Qp_inc_id[of x]
[PROOF STATE]
proof (prove)
using this:
0 \<le> ord x
x \<in> nonzero Q\<^sub>p
ord x = 0
x \<in> nonzero Q\<^sub>p
\<lbrakk>x \<in> nonzero Q\<^sub>p; 0 \<le> ord x; \<And>b. \<lbrakk>b \<in> nonzero Z\<^sub>p; x = \<iota> b\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>a. a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x
[PROOF STEP]
have "x = frac a \<one>\<^bsub>Z\<^sub>p\<^esub>"
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x

goal (1 subgoal):
 1. x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
using local.inc_def Zp.nonzero_closed
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x
?a \<in> carrier Z\<^sub>p \<Longrightarrow> \<iota> ?a = fraction Z\<^sub>p ?a \<one>\<^bsub>Z\<^sub>p\<^esub>
?a \<in> nonzero Z\<^sub>p \<Longrightarrow> ?a \<in> carrier Z\<^sub>p

goal (1 subgoal):
 1. x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
have "angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> (ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
using ac_fract[of x a ]  "1" nonzero_memE Q\<^sub>p_def Zp.nonzero_closed Zp.nonzero_one_closed Z\<^sub>p_def a_def
      local.frac_closed padic_fields.ac_fract padic_fields_axioms
[PROOF STATE]
proof (prove)
using this:
x = fraction Z\<^sub>p a \<one>\<^bsub>Z\<^sub>p\<^esub>
\<lbrakk>x \<in> carrier Q\<^sub>p; a \<in> nonzero Z\<^sub>p; ?b \<in> nonzero Z\<^sub>p; x = fraction Z\<^sub>p a ?b\<rbrakk> \<Longrightarrow> angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp ?b
x \<in> nonzero Q\<^sub>p
?a \<in> nonzero Q\<^sub>p \<Longrightarrow> ?a \<in> carrier Q\<^sub>p
?a \<in> nonzero Q\<^sub>p \<Longrightarrow> ?a \<noteq> \<zero>
Q\<^sub>p \<equiv> Frac Z\<^sub>p
?a \<in> nonzero Z\<^sub>p \<Longrightarrow> ?a \<in> carrier Z\<^sub>p
\<one>\<^bsub>Z\<^sub>p\<^esub> \<in> nonzero Z\<^sub>p
Z\<^sub>p \<equiv> padic_int p
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x
\<lbrakk>?a \<in> carrier Z\<^sub>p; ?b \<in> nonzero Z\<^sub>p\<rbrakk> \<Longrightarrow> fraction Z\<^sub>p ?a ?b \<in> carrier Q\<^sub>p
\<lbrakk>padic_fields ?p; ?c \<in> carrier (Frac (padic_int ?p)); ?a \<in> nonzero (padic_int ?p); ?b \<in> nonzero (padic_int ?p); ?c = fraction (padic_int ?p) ?a ?b\<rbrakk> \<Longrightarrow> padic_fields.angular_component ?p ?c = padic_integers.ac_Zp ?p ?a \<otimes>\<^bsub>padic_int ?p\<^esub> inv\<^bsub>padic_int ?p\<^esub> padic_integers.ac_Zp ?p ?b
padic_fields p

goal (1 subgoal):
 1. angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
have "angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>"
[PROOF STATE]
proof (prove)
using this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> ac_Zp \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
by (simp add: ac_Zp_one)
[PROOF STATE]
proof (state)
this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
have 0: "angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>"
[PROOF STATE]
proof (prove)
using this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> inv\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
have "ac_Zp a \<in> nonzero Z\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ac_Zp a \<in> nonzero Z\<^sub>p
[PROOF STEP]
using Zp.Units_nonzero Zp.nonzero_closed Zp.not_nonzero_memI a_def ac_Zp_is_Unit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> Units Z\<^sub>p; \<one>\<^bsub>Z\<^sub>p\<^esub> \<noteq> \<zero>\<^bsub>Z\<^sub>p\<^esub>\<rbrakk> \<Longrightarrow> ?u \<in> nonzero Z\<^sub>p
?a \<in> nonzero Z\<^sub>p \<Longrightarrow> ?a \<in> carrier Z\<^sub>p
?a = \<zero>\<^bsub>Z\<^sub>p\<^esub> \<Longrightarrow> ?a \<notin> nonzero Z\<^sub>p
a \<in> nonzero Z\<^sub>p \<and> \<iota> a = x
\<lbrakk>?x \<in> carrier Z\<^sub>p; ?x \<noteq> \<zero>\<^bsub>Z\<^sub>p\<^esub>\<rbrakk> \<Longrightarrow> ac_Zp ?x \<in> Units Z\<^sub>p

goal (1 subgoal):
 1. ac_Zp a \<in> nonzero Z\<^sub>p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ac_Zp a \<in> nonzero Z\<^sub>p

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ac_Zp a \<in> nonzero Z\<^sub>p

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
ac_Zp a \<in> nonzero Z\<^sub>p
angular_component x = ac_Zp a \<otimes>\<^bsub>Z\<^sub>p\<^esub> \<one>\<^bsub>Z\<^sub>p\<^esub>

goal (1 subgoal):
 1. \<iota> (angular_component x) = x
[PROOF STEP]
by (metis Zp.l_one Zp.nonzero_closed Zp_defs(1) Zp_defs(4) a_def ac_Zp_factors'
        assms(1) int_pow_0 mult_comm ord_of_inc)
[PROOF STATE]
proof (state)
this:
\<iota> (angular_component x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_term_compD4:
  assumes "nat_term_comp cmp" and "fst (rep_nat_term u) = fst (rep_nat_term a)"
    and "fst (rep_nat_term v) = fst (rep_nat_term b)" and "snd (rep_nat_term u) = snd (rep_nat_term v)"
    and "snd (rep_nat_term a) = snd (rep_nat_term b)" and "cmp a b = Lt"
  shows "cmp u v = Lt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp u v = Lt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nat_term_comp cmp
fst (rep_nat_term u) = fst (rep_nat_term a)
fst (rep_nat_term v) = fst (rep_nat_term b)
snd (rep_nat_term u) = snd (rep_nat_term v)
snd (rep_nat_term a) = snd (rep_nat_term b)
cmp a b = Lt

goal (1 subgoal):
 1. cmp u v = Lt
[PROOF STEP]
unfolding nat_term_comp_def snd_conv
[PROOF STATE]
proof (prove)
using this:
(\<forall>u v. snd (rep_nat_term u) = snd (rep_nat_term v) \<longrightarrow> fst (rep_nat_term u) = 0 \<longrightarrow> cmp u v \<noteq> Gt) \<and> (\<forall>u v. fst (rep_nat_term u) = fst (rep_nat_term v) \<longrightarrow> snd (rep_nat_term u) < snd (rep_nat_term v) \<longrightarrow> cmp u v = Lt) \<and> (\<forall>t u v. cmp u v = Lt \<longrightarrow> cmp (splus t u) (splus t v) = Lt) \<and> (\<forall>u v a b. fst (rep_nat_term u) = fst (rep_nat_term a) \<longrightarrow> fst (rep_nat_term v) = fst (rep_nat_term b) \<longrightarrow> snd (rep_nat_term u) = snd (rep_nat_term v) \<longrightarrow> snd (rep_nat_term a) = snd (rep_nat_term b) \<longrightarrow> cmp a b = Lt \<longrightarrow> cmp u v = Lt)
fst (rep_nat_term u) = fst (rep_nat_term a)
fst (rep_nat_term v) = fst (rep_nat_term b)
snd (rep_nat_term u) = snd (rep_nat_term v)
snd (rep_nat_term a) = snd (rep_nat_term b)
cmp a b = Lt

goal (1 subgoal):
 1. cmp u v = Lt
[PROOF STEP]
by blast


[STATEMENT]
lemma  "eupdate (PLUS (E.INT 8 250) (UINT 8 500))
      = PLUS (E.INT 8 (- 6)) (UINT 8 244)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eupdate (PLUS (INT 8 250) (UINT 8 500)) = PLUS (INT 8 (- 6)) (UINT 8 244)
[PROOF STEP]
by(simp)