[STATEMENT]
lemma runFw_scheme: "runFw s d c rs = runFw_scheme s d c p rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runFw s d c rs = runFw_scheme s d c p rs
[PROOF STEP]
apply(simp add: runFw_def runFw_scheme_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs (p\<lparr>p_iiface := pc_iiface c, p_oiface := pc_oiface c, p_src := s, p_dst := d, p_proto := pc_proto c, p_sport := pc_sport c, p_dport := pc_dport c\<rparr>)
[PROOF STEP]
apply(case_tac p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p_iiface p_oiface p_src p_dst p_proto p_sport p_dport p_tcp_flags p_payload more. p = \<lparr>p_iiface = p_iiface, p_oiface = p_oiface, p_src = p_src, p_dst = p_dst, p_proto = p_proto, p_sport = p_sport, p_dport = p_dport, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<Longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs (p\<lparr>p_iiface := pc_iiface c, p_oiface := pc_oiface c, p_src := s, p_dst := d, p_proto := pc_proto c, p_sport := pc_sport c, p_dport := pc_dport c\<rparr>)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p_iiface p_oiface p_src p_dst p_proto p_sport p_dport p_tcp_flags p_payload more. p = \<lparr>p_iiface = p_iiface, p_oiface = p_oiface, p_src = p_src, p_dst = p_dst, p_proto = p_proto, p_sport = p_sport, p_dport = p_dport, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<Longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
apply(thin_tac _, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p_tcp_flags p_payload more. simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
 2. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p_tcp_flags p_payload more. simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
 2. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
by(simp; fail)
[PROOF STATE]
proof (state)
this:
simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>

goal (1 subgoal):
 1. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
case(Cons r rs)
[PROOF STATE]
proof (state)
this:
simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = ?p_tcp_flags, p_payload = ?p_payload, \<dots> = ?more\<rparr>

goal (1 subgoal):
 1. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
obtain m a where r: "r = SimpleRule m a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m a. r = SimpleRule m a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases r) simp
[PROOF STATE]
proof (state)
this:
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
from simple_matches_extended_packet[symmetric, of _ "pc_iiface c" "pc_oiface c"
                                      s d "pc_proto c" "pc_sport c" "pc_dport c" _ _ _ "{TCP_SYN}" "[]"]
[PROOF STATE]
proof (chain)
picking this:
simple_matches ?m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = ?tcp_flags2.0, p_payload = ?payload2.0, \<dots> = ?aux\<rparr> = simple_matches ?m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
[PROOF STEP]
have pext: "simple_matches m
   \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
      p_tcp_flags = tcp_flags2, p_payload = payload2, \<dots> = aux\<rparr> =
  simple_matches m
   \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
      p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>" for tcp_flags2 payload2 and aux::'c
[PROOF STATE]
proof (prove)
using this:
simple_matches ?m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = ?tcp_flags2.0, p_payload = ?payload2.0, \<dots> = ?aux\<rparr> = simple_matches ?m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>

goal (1 subgoal):
 1. simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = tcp_flags2, p_payload = payload2, \<dots> = aux\<rparr> = simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = ?tcp_flags2.0, p_payload = ?payload2.0, \<dots> = ?aux\<rparr> = simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>

goal (1 subgoal):
 1. \<And>a rs p_tcp_flags p_payload more. (\<And>p_tcp_flags p_payload more. simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<Longrightarrow> simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw (r # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (r # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
apply(simp add: r, cases a, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a = Accept \<Longrightarrow> (simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<longrightarrow> \<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> Decision FinalAllow = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<and> (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<longrightarrow> (simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = Decision FinalAllow) \<and> (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>))
 2. a = Drop \<Longrightarrow> simple_fw (SimpleRule m a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (SimpleRule m a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = ?p_tcp_flags, p_payload = ?p_payload, \<dots> = ?more\<rparr>

goal (2 subgoals):
 1. a = Accept \<Longrightarrow> (simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<longrightarrow> \<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> Decision FinalAllow = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>) \<and> (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<longrightarrow> (simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = Decision FinalAllow) \<and> (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr> \<longrightarrow> simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>))
 2. a = Drop \<Longrightarrow> simple_fw (SimpleRule m a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (SimpleRule m a # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>
[PROOF STEP]
by(simp add: pext)+
[PROOF STATE]
proof (state)
this:
simple_fw (r # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (r # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = p_tcp_flags, p_payload = p_payload, \<dots> = more\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_default_policy_runFw: "has_default_policy rs \<Longrightarrow> runFw s d c rs = Decision FinalAllow \<or> runFw s d c rs = Decision FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> runFw s d c rs = Decision FinalAllow \<or> runFw s d c rs = Decision FinalDeny
[PROOF STEP]
by(simp add: runFw_def has_default_policy)


[STATEMENT]
lemma same_fw_behaviour_one_equi:
  "same_fw_behaviour_one x x c rs"
  "same_fw_behaviour_one x y c rs = same_fw_behaviour_one y x c rs"
  "same_fw_behaviour_one x y c rs \<and> same_fw_behaviour_one y z c rs \<Longrightarrow> same_fw_behaviour_one x z c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_fw_behaviour_one x x c rs &&& same_fw_behaviour_one x y c rs = same_fw_behaviour_one y x c rs &&& (same_fw_behaviour_one x y c rs \<and> same_fw_behaviour_one y z c rs \<Longrightarrow> same_fw_behaviour_one x z c rs)
[PROOF STEP]
unfolding same_fw_behaviour_one_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d s. runFw x d c rs = runFw x d c rs \<and> runFw s x c rs = runFw s x c rs &&& (\<forall>d s. runFw x d c rs = runFw y d c rs \<and> runFw s x c rs = runFw s y c rs) = (\<forall>d s. runFw y d c rs = runFw x d c rs \<and> runFw s y c rs = runFw s x c rs) &&& ((\<forall>d s. runFw x d c rs = runFw y d c rs \<and> runFw s x c rs = runFw s y c rs) \<and> (\<forall>d s. runFw y d c rs = runFw z d c rs \<and> runFw s y c rs = runFw s z c rs) \<Longrightarrow> \<forall>d s. runFw x d c rs = runFw z d c rs \<and> runFw s x c rs = runFw s z c rs)
[PROOF STEP]
by metis+


[STATEMENT]
lemma same_fw_behaviour_equi:
  "same_fw_behaviour x x rs"
  "same_fw_behaviour x y rs = same_fw_behaviour y x rs"
  "same_fw_behaviour x y rs \<and> same_fw_behaviour y z rs \<Longrightarrow> same_fw_behaviour x z rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_fw_behaviour x x rs &&& same_fw_behaviour x y rs = same_fw_behaviour y x rs &&& (same_fw_behaviour x y rs \<and> same_fw_behaviour y z rs \<Longrightarrow> same_fw_behaviour x z rs)
[PROOF STEP]
unfolding same_fw_behaviour_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. simple_fw rs (p\<lparr>p_src := x\<rparr>) = simple_fw rs (p\<lparr>p_src := x\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := x\<rparr>) = simple_fw rs (p\<lparr>p_dst := x\<rparr>) &&& (\<forall>p. simple_fw rs (p\<lparr>p_src := x\<rparr>) = simple_fw rs (p\<lparr>p_src := y\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := x\<rparr>) = simple_fw rs (p\<lparr>p_dst := y\<rparr>)) = (\<forall>p. simple_fw rs (p\<lparr>p_src := y\<rparr>) = simple_fw rs (p\<lparr>p_src := x\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := y\<rparr>) = simple_fw rs (p\<lparr>p_dst := x\<rparr>)) &&& ((\<forall>p. simple_fw rs (p\<lparr>p_src := x\<rparr>) = simple_fw rs (p\<lparr>p_src := y\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := x\<rparr>) = simple_fw rs (p\<lparr>p_dst := y\<rparr>)) \<and> (\<forall>p. simple_fw rs (p\<lparr>p_src := y\<rparr>) = simple_fw rs (p\<lparr>p_src := z\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := y\<rparr>) = simple_fw rs (p\<lparr>p_dst := z\<rparr>)) \<Longrightarrow> \<forall>p. simple_fw rs (p\<lparr>p_src := x\<rparr>) = simple_fw rs (p\<lparr>p_src := z\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := x\<rparr>) = simple_fw rs (p\<lparr>p_dst := z\<rparr>))
[PROOF STEP]
by auto


[STATEMENT]
lemma runFw_sameFw_behave:
       fixes W :: "'i::len word set set"
       shows
       "\<forall>A \<in> W. \<forall>a1 \<in> A. \<forall>a2 \<in> A. same_fw_behaviour_one a1 a2 c rs \<Longrightarrow> \<Union> W = UNIV \<Longrightarrow>
       \<forall>B \<in> W. \<exists>b \<in> B. runFw ip1 b c rs = runFw ip2 b c rs \<Longrightarrow>
       \<forall>B \<in> W. \<exists>b \<in> B. runFw b ip1 c rs = runFw b ip2 c rs \<Longrightarrow>
       same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
assume a1: "\<forall>A \<in> W. \<forall>a1 \<in> A. \<forall>a2 \<in> A. same_fw_behaviour_one a1 a2 c rs"
   and a2: "\<Union> W = UNIV "
   and a3: "\<forall>B \<in> W. \<exists>b \<in> B. runFw ip1 b c rs = runFw ip2 b c rs"
   and a4: "\<forall>B \<in> W. \<exists>b \<in> B. runFw b ip1 c rs = runFw b ip2 c rs"
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
\<Union> W = UNIV
\<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs
\<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
have relation_lem: "\<forall>D \<in> W. \<forall>d1 \<in> D. \<forall>d2 \<in> D. \<forall>s. f s d1 = f s d2 \<Longrightarrow> \<Union> W = UNIV \<Longrightarrow>
                     \<forall>B \<in> W. \<exists>b \<in> B. f s1 b = f s2 b \<Longrightarrow>
                     f s1 d = f s2 d" for W and f::"'c \<Rightarrow> 'b \<Rightarrow> 'd" and s1 d s2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>D\<in>W. \<forall>d1\<in>D. \<forall>d2\<in>D. \<forall>s. f s d1 = f s d2; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. f s1 b = f s2 b\<rbrakk> \<Longrightarrow> f s1 d = f s2 d
[PROOF STEP]
by (metis UNIV_I Union_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>D\<in>?W1. \<forall>d1\<in>D. \<forall>d2\<in>D. \<forall>s. ?f1 s d1 = ?f1 s d2; \<Union> ?W1 = UNIV; \<forall>B\<in>?W1. \<exists>b\<in>B. ?f1 ?s1.1 b = ?f1 ?s2.1 b\<rbrakk> \<Longrightarrow> ?f1 ?s1.1 ?d1 = ?f1 ?s2.1 ?d1

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
from a1
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
have a1':"\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>s. runFw s a1 c rs = runFw s a2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>s. runFw s a1 c rs = runFw s a2 c rs
[PROOF STEP]
unfolding same_fw_behaviour_one_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d s. runFw a1 d c rs = runFw a2 d c rs \<and> runFw s a1 c rs = runFw s a2 c rs

goal (1 subgoal):
 1. \<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>s. runFw s a1 c rs = runFw s a2 c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>s. runFw s a1 c rs = runFw s a2 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
from relation_lem[OF a1' a2 a3]
[PROOF STATE]
proof (chain)
picking this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs
[PROOF STEP]
have s1: "\<And> d. runFw ip1 d c rs = runFw ip2 d c rs"
[PROOF STATE]
proof (prove)
using this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs

goal (1 subgoal):
 1. \<And>d. runFw ip1 d c rs = runFw ip2 d c rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
from a1
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
have a1'':"\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d. runFw a1 d c rs = runFw a2 d c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d. runFw a1 d c rs = runFw a2 d c rs
[PROOF STEP]
unfolding same_fw_behaviour_one_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d s. runFw a1 d c rs = runFw a2 d c rs \<and> runFw s a1 c rs = runFw s a2 c rs

goal (1 subgoal):
 1. \<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d. runFw a1 d c rs = runFw a2 d c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. \<forall>d. runFw a1 d c rs = runFw a2 d c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
from relation_lem[OF a1'' a2 a4]
[PROOF STATE]
proof (chain)
picking this:
runFw ?d1 ip1 c rs = runFw ?d1 ip2 c rs
[PROOF STEP]
have s2: "\<And> s. runFw s ip1 c rs = runFw s ip2 c rs"
[PROOF STATE]
proof (prove)
using this:
runFw ?d1 ip1 c rs = runFw ?d1 ip2 c rs

goal (1 subgoal):
 1. \<And>s. runFw s ip1 c rs = runFw s ip2 c rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
runFw ?s1 ip1 c rs = runFw ?s1 ip2 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>A\<in>W. \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; \<Union> W = UNIV; \<forall>B\<in>W. \<exists>b\<in>B. runFw ip1 b c rs = runFw ip2 b c rs; \<forall>B\<in>W. \<exists>b\<in>B. runFw b ip1 c rs = runFw b ip2 c rs\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
from s1 s2
[PROOF STATE]
proof (chain)
picking this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs
runFw ?s1 ip1 c rs = runFw ?s1 ip2 c rs
[PROOF STEP]
show "same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
using this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs
runFw ?s1 ip1 c rs = runFw ?s1 ip2 c rs

goal (1 subgoal):
 1. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
unfolding same_fw_behaviour_one_def
[PROOF STATE]
proof (prove)
using this:
runFw ip1 ?d1 c rs = runFw ip2 ?d1 c rs
runFw ?s1 ip1 c rs = runFw ?s1 ip2 c rs

goal (1 subgoal):
 1. \<forall>d s. runFw ip1 d c rs = runFw ip2 d c rs \<and> runFw s ip1 c rs = runFw s ip2 c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
same_fw_behaviour_one ip1 ip2 c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sameFw_behave_sets:
  "\<forall>w\<in>set A. \<forall>a1 \<in> w. \<forall>a2 \<in> w. same_fw_behaviour_one a1 a2 c rs \<Longrightarrow>
   \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs \<Longrightarrow>
   \<forall>w1\<in>set A. \<forall>w2\<in>set A.
     \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs; \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs\<rbrakk> \<Longrightarrow> \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs; \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs\<rbrakk> \<Longrightarrow> \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
assume a1: "\<forall>w\<in>set A. \<forall>a1 \<in> w. \<forall>a2 \<in> w. same_fw_behaviour_one a1 a2 c rs" and
         "\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2.  same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs; \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs\<rbrakk> \<Longrightarrow> \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
have "\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2.  same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
using same_fw_behaviour_one_equi(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
same_fw_behaviour_one ?x ?y ?c ?rs \<and> same_fw_behaviour_one ?y ?z ?c ?rs \<Longrightarrow> same_fw_behaviour_one ?x ?z ?c ?rs

goal (1 subgoal):
 1. \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs; \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<exists>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs\<rbrakk> \<Longrightarrow> \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from a1 this
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
show "\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
using same_fw_behaviour_one_equi(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set A. \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<exists>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
same_fw_behaviour_one ?x ?y ?c ?rs \<and> same_fw_behaviour_one ?y ?z ?c ?rs \<Longrightarrow> same_fw_behaviour_one ?x ?z ?c ?rs

goal (1 subgoal):
 1. \<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>w1\<in>set A. \<forall>w2\<in>set A. \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs_not_empty: "groupWIs c rs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs c rs \<noteq> []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs c rs \<noteq> []
[PROOF STEP]
have "getParts rs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getParts rs \<noteq> []
[PROOF STEP]
by(simp add: getParts_def partitioningIps_nonempty)
[PROOF STATE]
proof (state)
this:
getParts rs \<noteq> []

goal (1 subgoal):
 1. groupWIs c rs \<noteq> []
[PROOF STEP]
with groupF_empty
[PROOF STATE]
proof (chain)
picking this:
(groupF ?f ?xs \<noteq> []) = (?xs \<noteq> [])
getParts rs \<noteq> []
[PROOF STEP]
have "\<And>f. groupF f (getParts rs) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(groupF ?f ?xs \<noteq> []) = (?xs \<noteq> [])
getParts rs \<noteq> []

goal (1 subgoal):
 1. \<And>f. groupF f (getParts rs) \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
groupF ?f (getParts rs) \<noteq> []

goal (1 subgoal):
 1. groupWIs c rs \<noteq> []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
groupF ?f (getParts rs) \<noteq> []

goal (1 subgoal):
 1. groupWIs c rs \<noteq> []
[PROOF STEP]
by(simp add: groupWIs_def Let_def) blast
[PROOF STATE]
proof (state)
this:
groupWIs c rs \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs_not_empty_elem: "V \<in> set (groupWIs c rs) \<Longrightarrow> V \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> V \<noteq> []
[PROOF STEP]
by(simp add: groupWIs_def Let_def groupF_empty_elem)


[STATEMENT]
lemma groupWIs_not_empty_elems:
  assumes V: "V \<in> set (groupWIs c rs)" and w: "w \<in> set V"
  shows "\<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> wordinterval_empty w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wordinterval_empty w
[PROOF STEP]
have "\<forall>w\<in>set (concat (groupWIs c rs)). \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (concat (groupWIs c rs)). \<not> wordinterval_empty w
[PROOF STEP]
apply(subst groupWIs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (concat (let W = getParts rs; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W)) in groupF f W)). \<not> wordinterval_empty w
[PROOF STEP]
apply(subst Let_def)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (concat (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs))). \<not> wordinterval_empty w
[PROOF STEP]
apply(subst groupF_concat_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w
[PROOF STEP]
using getParts_nonempty_elems
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w

goal (1 subgoal):
 1. \<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (concat (groupWIs c rs)). \<not> wordinterval_empty w

goal (1 subgoal):
 1. \<not> wordinterval_empty w
[PROOF STEP]
from this V w
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set (concat (groupWIs c rs)). \<not> wordinterval_empty w
V \<in> set (groupWIs c rs)
w \<in> set V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set (concat (groupWIs c rs)). \<not> wordinterval_empty w
V \<in> set (groupWIs c rs)
w \<in> set V

goal (1 subgoal):
 1. \<not> wordinterval_empty w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_empty w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupParts_same_fw_wi0:
    assumes "V \<in> set (groupWIs c rs)"
    shows "\<forall>w \<in> set (map wordinterval_to_set V). \<forall>a1 \<in> w. \<forall>a2 \<in> w. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>w\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
have "\<forall>A\<in>set (map wordinterval_to_set (concat (groupWIs c rs))).
        \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>set (map wordinterval_to_set (concat (groupWIs c rs))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
apply(subst groupWIs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>set (map wordinterval_to_set (concat (let W = getParts rs; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W)) in groupF f W))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
apply(subst Let_def)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>set (map wordinterval_to_set (concat (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
apply(subst set_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>wordinterval_to_set ` set (concat (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
apply(subst groupF_concat_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>wordinterval_to_set ` set (getParts rs). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
using getParts_same_fw_behaviour same_fw_spec
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (map wordinterval_to_set (getParts ?rs)); ?s1.0 \<in> ?A; ?s2.0 \<in> ?A\<rbrakk> \<Longrightarrow> same_fw_behaviour ?s1.0 ?s2.0 ?rs
same_fw_behaviour ?ip1.0 ?ip2.0 ?rs \<Longrightarrow> same_fw_behaviour_one ?ip1.0 ?ip2.0 ?c ?rs

goal (1 subgoal):
 1. \<forall>A\<in>wordinterval_to_set ` set (getParts rs). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>set (map wordinterval_to_set (concat (groupWIs c rs))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>w\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>set (map wordinterval_to_set (concat (groupWIs c rs))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
V \<in> set (groupWIs c rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>set (map wordinterval_to_set (concat (groupWIs c rs))). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
V \<in> set (groupWIs c rs)

goal (1 subgoal):
 1. \<forall>w\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs_same_fw_not: "A \<in> set (groupWIs c rs) \<Longrightarrow> B \<in> set (groupWIs c rs) \<Longrightarrow>
                            A \<noteq> B \<Longrightarrow>
                             \<forall>aw \<in> set (map wordinterval_to_set A).
                             \<forall>bw \<in> set (map wordinterval_to_set B).
                             \<forall>a \<in> aw. \<forall>b \<in> bw. \<not> same_fw_behaviour_one a b c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
assume asm: "A \<in> set (groupWIs c rs)" "B \<in> set (groupWIs c rs)" "A \<noteq> B"
[PROOF STATE]
proof (state)
this:
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B
[PROOF STEP]
have b1: "\<forall>aw \<in> set A. \<forall>bw \<in> set B.
                  (map (\<lambda>d. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)),
                   map (\<lambda>s. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) \<noteq>
                  (map (\<lambda>d. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)),
                   map (\<lambda>s. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))"
[PROOF STATE]
proof (prove)
using this:
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<forall>aw\<in>set A. \<forall>bw\<in>set B. (map (\<lambda>d. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))
[PROOF STEP]
apply(simp add: groupWIs_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)); B \<in> set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. (\<exists>x\<in>set (getParts rs). runFw (getOneIp aw) (getOneIp x) c rs \<noteq> runFw (getOneIp bw) (getOneIp x) c rs) \<or> (\<exists>x\<in>set (getParts rs). runFw (getOneIp x) (getOneIp aw) c rs \<noteq> runFw (getOneIp x) (getOneIp bw) c rs)
[PROOF STEP]
using groupF_nequality
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (groupF ?f ?xs); ?B \<in> set (groupF ?f ?xs); ?A \<noteq> ?B\<rbrakk> \<Longrightarrow> \<forall>a\<in>set ?A. \<forall>b\<in>set ?B. ?f a \<noteq> ?f b

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)); B \<in> set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. (\<exists>x\<in>set (getParts rs). runFw (getOneIp aw) (getOneIp x) c rs \<noteq> runFw (getOneIp bw) (getOneIp x) c rs) \<or> (\<exists>x\<in>set (getParts rs). runFw (getOneIp x) (getOneIp aw) c rs \<noteq> runFw (getOneIp x) (getOneIp bw) c rs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>aw\<in>set A. \<forall>bw\<in>set B. (map (\<lambda>d. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
have same_behave_runFw_not:
        "(map (\<lambda>d. runFw x1 d c rs) W, map (\<lambda>s. runFw s x1 c rs) W) \<noteq>
         (map (\<lambda>d. runFw x2 d c rs) W, map (\<lambda>s. runFw s x2 c rs) W) \<Longrightarrow>
         \<not> same_fw_behaviour_one x1 x2 c rs" for x1 x2 W
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map (\<lambda>d. runFw x1 d c rs) W, map (\<lambda>s. runFw s x1 c rs) W) \<noteq> (map (\<lambda>d. runFw x2 d c rs) W, map (\<lambda>s. runFw s x2 c rs) W) \<Longrightarrow> \<not> same_fw_behaviour_one x1 x2 c rs
[PROOF STEP]
by (simp add: same_fw_behaviour_one_def) (blast)
[PROOF STATE]
proof (state)
this:
(map (\<lambda>d. runFw ?x1.0 d c rs) ?W, map (\<lambda>s. runFw s ?x1.0 c rs) ?W) \<noteq> (map (\<lambda>d. runFw ?x2.0 d c rs) ?W, map (\<lambda>s. runFw s ?x2.0 c rs) ?W) \<Longrightarrow> \<not> same_fw_behaviour_one ?x1.0 ?x2.0 c rs

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
have "\<forall>C \<in> set (groupWIs c rs). \<forall>c \<in> set C. getOneIp c \<in> wordinterval_to_set c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>set (groupWIs c rs). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c
[PROOF STEP]
apply(simp add: groupWIs_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c
[PROOF STEP]
using getParts_nonempty_elems groupF_set getOneIp_elem
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w
\<forall>X\<in>set (groupF ?f ?xs). \<forall>x\<in>set X. x \<in> set ?xs
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W

goal (1 subgoal):
 1. \<forall>C\<in>set (groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c rs) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c rs) \<circ> getOneIp) (getParts rs))) (getParts rs)). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>set (groupWIs c rs). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
from this b1 asm
[PROOF STATE]
proof (chain)
picking this:
\<forall>C\<in>set (groupWIs c rs). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c
\<forall>aw\<in>set A. \<forall>bw\<in>set B. (map (\<lambda>d. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B
[PROOF STEP]
have
  "\<forall>aw \<in> set (map wordinterval_to_set A). \<forall>bw \<in> set (map wordinterval_to_set B).
   \<exists>a \<in> aw. \<exists>b \<in> bw. (map (\<lambda>d. runFw a d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s a c rs) (map getOneIp (getParts rs))) \<noteq>
    (map (\<lambda>d. runFw b d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s b c rs) (map getOneIp (getParts rs)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>set (groupWIs c rs). \<forall>c\<in>set C. getOneIp c \<in> wordinterval_to_set c
\<forall>aw\<in>set A. \<forall>bw\<in>set B. (map (\<lambda>d. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. (map (\<lambda>d. runFw a d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s a c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw b d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s b c rs) (map getOneIp (getParts rs)))
[PROOF STEP]
by (simp) (blast)
[PROOF STATE]
proof (state)
this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. (map (\<lambda>d. runFw a d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s a c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw b d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s b c rs) (map getOneIp (getParts rs)))

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
from this same_behave_runFw_not asm
[PROOF STATE]
proof (chain)
picking this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. (map (\<lambda>d. runFw a d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s a c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw b d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s b c rs) (map getOneIp (getParts rs)))
(map (\<lambda>d. runFw ?x1.0 d c rs) ?W, map (\<lambda>s. runFw s ?x1.0 c rs) ?W) \<noteq> (map (\<lambda>d. runFw ?x2.0 d c rs) ?W, map (\<lambda>s. runFw s ?x2.0 c rs) ?W) \<Longrightarrow> \<not> same_fw_behaviour_one ?x1.0 ?x2.0 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B
[PROOF STEP]
have " \<forall>aw \<in> set (map wordinterval_to_set A). \<forall>bw \<in> set (map wordinterval_to_set B).
         \<exists>a \<in> aw. \<exists>b \<in> bw. \<not> same_fw_behaviour_one a b c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. (map (\<lambda>d. runFw a d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s a c rs) (map getOneIp (getParts rs))) \<noteq> (map (\<lambda>d. runFw b d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s b c rs) (map getOneIp (getParts rs)))
(map (\<lambda>d. runFw ?x1.0 d c rs) ?W, map (\<lambda>s. runFw s ?x1.0 c rs) ?W) \<noteq> (map (\<lambda>d. runFw ?x2.0 d c rs) ?W, map (\<lambda>s. runFw s ?x2.0 c rs) ?W) \<Longrightarrow> \<not> same_fw_behaviour_one ?x1.0 ?x2.0 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
[PROOF STATE]
proof (chain)
picking this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
A \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set A). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
B \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set B). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B
[PROOF STEP]
have "\<forall>aw \<in> set (map wordinterval_to_set A).
        \<forall>bw \<in> set (map wordinterval_to_set B).
        \<forall>a \<in> aw. \<exists>b \<in> bw. \<not> same_fw_behaviour_one a b c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<exists>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
A \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set A). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
B \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set B). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>aw\<in>set A. \<forall>bw\<in>set B. \<exists>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs; \<forall>w\<in>set A. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; \<forall>w\<in>set B. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
using same_fw_behaviour_one_equi(3)
[PROOF STATE]
proof (prove)
using this:
same_fw_behaviour_one ?x ?y ?c ?rs \<and> same_fw_behaviour_one ?y ?z ?c ?rs \<Longrightarrow> same_fw_behaviour_one ?x ?z ?c ?rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>aw\<in>set A. \<forall>bw\<in>set B. \<exists>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs; \<forall>w\<in>set A. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; \<forall>w\<in>set B. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
[PROOF STATE]
proof (chain)
picking this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
A \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set A). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
B \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set B). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B
[PROOF STEP]
show "\<forall>aw \<in> set (map wordinterval_to_set A).
        \<forall>bw \<in> set (map wordinterval_to_set B).
        \<forall>a \<in> aw. \<forall>b \<in> bw. \<not> same_fw_behaviour_one a b c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<exists>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
A \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set A). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
B \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set B). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 c rs
A \<in> set (groupWIs c rs)
B \<in> set (groupWIs c rs)
A \<noteq> B

goal (1 subgoal):
 1. \<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs; \<forall>w\<in>set A. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; \<forall>w\<in>set B. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<forall>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
using same_fw_behaviour_one_equi(3)
[PROOF STATE]
proof (prove)
using this:
same_fw_behaviour_one ?x ?y ?c ?rs \<and> same_fw_behaviour_one ?y ?z ?c ?rs \<Longrightarrow> same_fw_behaviour_one ?x ?z ?c ?rs

goal (1 subgoal):
 1. \<lbrakk>\<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<exists>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs; \<forall>w\<in>set A. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; \<forall>w\<in>set B. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set A. \<forall>bw\<in>set B. \<forall>a\<in>wordinterval_to_set aw. \<forall>b\<in>wordinterval_to_set bw. \<not> same_fw_behaviour_one a b c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>aw\<in>set (map wordinterval_to_set A). \<forall>bw\<in>set (map wordinterval_to_set B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupParts_same_fw_wi1:
  "V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1 \<in> set V. \<forall>w2 \<in> set V.
     \<forall>a1 \<in> wordinterval_to_set w1. \<forall>a2 \<in> wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
assume asm: "V \<in> set (groupWIs c rs)"
[PROOF STATE]
proof (state)
this:
V \<in> set (groupWIs c rs)

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from getParts_same_fw_behaviour same_fw_spec
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?A \<in> set (map wordinterval_to_set (getParts ?rs)); ?s1.0 \<in> ?A; ?s2.0 \<in> ?A\<rbrakk> \<Longrightarrow> same_fw_behaviour ?s1.0 ?s2.0 ?rs
same_fw_behaviour ?ip1.0 ?ip2.0 ?rs \<Longrightarrow> same_fw_behaviour_one ?ip1.0 ?ip2.0 ?c ?rs
[PROOF STEP]
have b1: "\<forall>A \<in> set (map wordinterval_to_set (getParts rs)) . \<forall>a1 \<in> A. \<forall>a2 \<in> A.
              same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (map wordinterval_to_set (getParts ?rs)); ?s1.0 \<in> ?A; ?s2.0 \<in> ?A\<rbrakk> \<Longrightarrow> same_fw_behaviour ?s1.0 ?s2.0 ?rs
same_fw_behaviour ?ip1.0 ?ip2.0 ?rs \<Longrightarrow> same_fw_behaviour_one ?ip1.0 ?ip2.0 ?c ?rs

goal (1 subgoal):
 1. \<forall>A\<in>set (map wordinterval_to_set (getParts rs)). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>set (map wordinterval_to_set (getParts rs)). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from getParts_complete
[PROOF STATE]
proof (chain)
picking this:
wordinterval_list_to_set (getParts ?rs) = UNIV
[PROOF STEP]
have complete: "\<Union>(set (map wordinterval_to_set (getParts rs))) = UNIV"
[PROOF STATE]
proof (prove)
using this:
wordinterval_list_to_set (getParts ?rs) = UNIV

goal (1 subgoal):
 1. \<Union> (set (map wordinterval_to_set (getParts rs))) = UNIV
[PROOF STEP]
by(simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
\<Union> (set (map wordinterval_to_set (getParts rs))) = UNIV

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from getParts_nonempty_elems
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w
[PROOF STEP]
have nonempty: "\<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w

goal (1 subgoal):
 1. \<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
fix W x1 x2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
assume a1: "\<forall>A \<in> set (map wordinterval_to_set W). \<forall>a1 \<in> A. \<forall>a2 \<in> A. same_fw_behaviour_one a1 a2 c rs"
    and a2: "wordinterval_list_to_set W = UNIV"
    and a3: "\<forall>w \<in> set W. \<not> wordinterval_empty w"
    and a4: "(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) =
             (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))"
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>set (map wordinterval_to_set W). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
wordinterval_list_to_set W = UNIV
\<forall>w\<in>set W. \<not> wordinterval_empty w
(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from a3 a4 getOneIp_elem
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set W. \<not> wordinterval_empty w
(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
[PROOF STEP]
have b1: "\<forall>B \<in> set (map wordinterval_to_set W). \<exists>b \<in> B. runFw x1 b c rs = runFw x2 b c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set W. \<not> wordinterval_empty w
(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W

goal (1 subgoal):
 1. \<forall>B\<in>set (map wordinterval_to_set W). \<exists>b\<in>B. runFw x1 b c rs = runFw x2 b c rs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>B\<in>set (map wordinterval_to_set W). \<exists>b\<in>B. runFw x1 b c rs = runFw x2 b c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from a3 a4 getOneIp_elem
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set W. \<not> wordinterval_empty w
(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
[PROOF STEP]
have b2: "\<forall>B \<in> set (map wordinterval_to_set W). \<exists>b \<in> B. runFw b x1 c rs = runFw b x2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set W. \<not> wordinterval_empty w
(map (\<lambda>d. runFw x1 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x1 c rs) (map getOneIp W)) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp W), map (\<lambda>s. runFw s x2 c rs) (map getOneIp W))
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W

goal (1 subgoal):
 1. \<forall>B\<in>set (map wordinterval_to_set W). \<exists>b\<in>B. runFw b x1 c rs = runFw b x2 c rs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>B\<in>set (map wordinterval_to_set W). \<exists>b\<in>B. runFw b x1 c rs = runFw b x2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from runFw_sameFw_behave[OF a1 _ b1 b2] a2[unfolded wordinterval_list_to_set_def]
[PROOF STATE]
proof (chain)
picking this:
\<Union> (set (map wordinterval_to_set W)) = UNIV \<Longrightarrow> same_fw_behaviour_one x1 x2 c rs
\<Union> (set (map wordinterval_to_set W)) = UNIV
[PROOF STEP]
have
        "same_fw_behaviour_one x1 x2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<Union> (set (map wordinterval_to_set W)) = UNIV \<Longrightarrow> same_fw_behaviour_one x1 x2 c rs
\<Union> (set (map wordinterval_to_set W)) = UNIV

goal (1 subgoal):
 1. same_fw_behaviour_one x1 x2 c rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
same_fw_behaviour_one x1 x2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>A\<in>set (map wordinterval_to_set ?W2). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; wordinterval_list_to_set ?W2 = UNIV; \<forall>w\<in>set ?W2. \<not> wordinterval_empty w; (map (\<lambda>d. runFw ?x1.2 d c rs) (map getOneIp ?W2), map (\<lambda>s. runFw s ?x1.2 c rs) (map getOneIp ?W2)) = (map (\<lambda>d. runFw ?x2.2 d c rs) (map getOneIp ?W2), map (\<lambda>s. runFw s ?x2.2 c rs) (map getOneIp ?W2))\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ?x1.2 ?x2.2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
note same_behave_runFw=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>A\<in>set (map wordinterval_to_set ?W2). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs; wordinterval_list_to_set ?W2 = UNIV; \<forall>w\<in>set ?W2. \<not> wordinterval_empty w; (map (\<lambda>d. runFw ?x1.2 d c rs) (map getOneIp ?W2), map (\<lambda>s. runFw s ?x1.2 c rs) (map getOneIp ?W2)) = (map (\<lambda>d. runFw ?x2.2 d c rs) (map getOneIp ?W2), map (\<lambda>s. runFw s ?x2.2 c rs) (map getOneIp ?W2))\<rbrakk> \<Longrightarrow> same_fw_behaviour_one ?x1.2 ?x2.2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from same_behave_runFw[OF b1 getParts_complete nonempty]
       groupF_equality[of "(\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)),
                             map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs))))"
                     "(getParts rs)"] asm
[PROOF STATE]
proof (chain)
picking this:
(map (\<lambda>d. runFw ?x1.2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s ?x1.2 c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw ?x2.2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s ?x2.2 c rs) (map getOneIp (getParts rs))) \<Longrightarrow> same_fw_behaviour_one ?x1.2 ?x2.2 c rs
\<forall>A\<in>set (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)). \<forall>a1\<in>set A. \<forall>a2\<in>set A. (map (\<lambda>d. runFw (getOneIp a1) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a1) c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw (getOneIp a2) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a2) c rs) (map getOneIp (getParts rs)))
V \<in> set (groupWIs c rs)
[PROOF STEP]
have b2: "\<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs"
[PROOF STATE]
proof (prove)
using this:
(map (\<lambda>d. runFw ?x1.2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s ?x1.2 c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw ?x2.2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s ?x2.2 c rs) (map getOneIp (getParts rs))) \<Longrightarrow> same_fw_behaviour_one ?x1.2 ?x2.2 c rs
\<forall>A\<in>set (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)). \<forall>a1\<in>set A. \<forall>a2\<in>set A. (map (\<lambda>d. runFw (getOneIp a1) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a1) c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw (getOneIp a2) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a2) c rs) (map getOneIp (getParts rs)))
V \<in> set (groupWIs c rs)

goal (1 subgoal):
 1. \<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs
[PROOF STEP]
apply(subst (asm) groupWIs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x1 x2. (map (\<lambda>d. runFw x1 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s x1 c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s x2 c rs) (map getOneIp (getParts rs))) \<Longrightarrow> same_fw_behaviour_one x1 x2 c rs; \<forall>A\<in>set (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)). \<forall>a1\<in>set A. \<forall>a2\<in>set A. (map (\<lambda>d. runFw (getOneIp a1) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a1) c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw (getOneIp a2) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a2) c rs) (map getOneIp (getParts rs))); V \<in> set (let W = getParts rs; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W)) in groupF f W)\<rbrakk> \<Longrightarrow> \<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs
[PROOF STEP]
apply(subst (asm) Let_def)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x1 x2. (map (\<lambda>d. runFw x1 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s x1 c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw x2 d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s x2 c rs) (map getOneIp (getParts rs))) \<Longrightarrow> same_fw_behaviour_one x1 x2 c rs; \<forall>A\<in>set (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)). \<forall>a1\<in>set A. \<forall>a2\<in>set A. (map (\<lambda>d. runFw (getOneIp a1) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a1) c rs) (map getOneIp (getParts rs))) = (map (\<lambda>d. runFw (getOneIp a2) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp a2) c rs) (map getOneIp (getParts rs))); V \<in> set (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs))\<rbrakk> \<Longrightarrow> \<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from groupWIs_not_empty_elems asm
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?V \<in> set (groupWIs ?c ?rs); ?w \<in> set ?V\<rbrakk> \<Longrightarrow> \<not> wordinterval_empty ?w
V \<in> set (groupWIs c rs)
[PROOF STEP]
have "\<forall>w \<in> set V. \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?V \<in> set (groupWIs ?c ?rs); ?w \<in> set ?V\<rbrakk> \<Longrightarrow> \<not> wordinterval_empty ?w
V \<in> set (groupWIs c rs)

goal (1 subgoal):
 1. \<forall>w\<in>set V. \<not> wordinterval_empty w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set V. \<not> wordinterval_empty w

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from this b2 getOneIp_elem
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set V. \<not> wordinterval_empty w
\<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
[PROOF STEP]
have b3: "\<forall>w1\<in>set (map wordinterval_to_set V). \<forall>w2\<in>set (map wordinterval_to_set V).
           \<exists>ip1\<in> w1. \<exists>ip2\<in>w2.
           same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set V. \<not> wordinterval_empty w
\<forall>a1\<in>set V. \<forall>a2\<in>set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W

goal (1 subgoal):
 1. \<forall>w1\<in>set (map wordinterval_to_set V). \<forall>w2\<in>set (map wordinterval_to_set V). \<exists>ip1\<in>w1. \<exists>ip2\<in>w2. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
by (simp) (blast)
[PROOF STATE]
proof (state)
this:
\<forall>w1\<in>set (map wordinterval_to_set V). \<forall>w2\<in>set (map wordinterval_to_set V). \<exists>ip1\<in>w1. \<exists>ip2\<in>w2. same_fw_behaviour_one ip1 ip2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from groupParts_same_fw_wi0 asm
[PROOF STATE]
proof (chain)
picking this:
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set ?V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 ?c ?rs
V \<in> set (groupWIs c rs)
[PROOF STEP]
have "\<forall>A\<in>set (map wordinterval_to_set V). \<forall>a1\<in> A. \<forall>a2\<in> A. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
using this:
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set ?V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 ?c ?rs
V \<in> set (groupWIs c rs)

goal (1 subgoal):
 1. \<forall>A\<in>set (map wordinterval_to_set V). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>set (map wordinterval_to_set V). \<forall>a1\<in>A. \<forall>a2\<in>A. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
from sameFw_behave_sets[OF this b3]
[PROOF STATE]
proof (chain)
picking this:
\<forall>w1\<in>set (map wordinterval_to_set V). \<forall>w2\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
show "\<forall>w1 \<in> set V. \<forall>w2 \<in> set V.
   \<forall>a1 \<in> wordinterval_to_set w1. \<forall>a2 \<in> wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>w1\<in>set (map wordinterval_to_set V). \<forall>w2\<in>set (map wordinterval_to_set V). \<forall>a1\<in>w1. \<forall>a2\<in>w2. same_fw_behaviour_one a1 a2 c rs

goal (1 subgoal):
 1. \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupParts_same_fw_wi2: "V \<in> set (groupWIs c rs) \<Longrightarrow>
                               \<forall>ip1 \<in> wordinterval_list_to_set V.
                               \<forall>ip2 \<in> wordinterval_list_to_set V.
                               same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set V. \<forall>ip2\<in>wordinterval_list_to_set V. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
using groupParts_same_fw_wi0 groupParts_same_fw_wi1
[PROOF STATE]
proof (prove)
using this:
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> \<forall>w\<in>set (map wordinterval_to_set ?V). \<forall>a1\<in>w. \<forall>a2\<in>w. same_fw_behaviour_one a1 a2 ?c ?rs
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> \<forall>w1\<in>set ?V. \<forall>w2\<in>set ?V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 ?c ?rs

goal (1 subgoal):
 1. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set V. \<forall>ip2\<in>wordinterval_list_to_set V. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
apply (simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>V \<in> set (groupWIs c rs); \<And>V c rs. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w\<in>set V. \<forall>a1\<in>wordinterval_to_set w. \<forall>a2\<in>wordinterval_to_set w. same_fw_behaviour_one a1 a2 c rs; \<And>V c rs. V \<in> set (groupWIs c rs) \<Longrightarrow> \<forall>w1\<in>set V. \<forall>w2\<in>set V. \<forall>a1\<in>wordinterval_to_set w1. \<forall>a2\<in>wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs\<rbrakk> \<Longrightarrow> \<forall>y\<in>set V. \<forall>ip1\<in>wordinterval_to_set y. \<forall>y\<in>set V. \<forall>ip2\<in>wordinterval_to_set y. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
by fast


[STATEMENT]
lemma groupWIs_same_fw_not2: "A \<in> set (groupWIs c rs) \<Longrightarrow> B \<in> set (groupWIs c rs) \<Longrightarrow>
                                A \<noteq> B \<Longrightarrow>
                                \<forall>ip1 \<in> wordinterval_list_to_set A.
                                \<forall>ip2 \<in> wordinterval_list_to_set B.
                                \<not> same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set A. \<forall>ip2\<in>wordinterval_list_to_set B. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
apply(simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>y\<in>set A. \<forall>ip1\<in>wordinterval_to_set y. \<forall>y\<in>set B. \<forall>ip2\<in>wordinterval_to_set y. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
using groupWIs_same_fw_not
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (groupWIs ?c ?rs); ?B \<in> set (groupWIs ?c ?rs); ?A \<noteq> ?B\<rbrakk> \<Longrightarrow> \<forall>aw\<in>set (map wordinterval_to_set ?A). \<forall>bw\<in>set (map wordinterval_to_set ?B). \<forall>a\<in>aw. \<forall>b\<in>bw. \<not> same_fw_behaviour_one a b ?c ?rs

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>y\<in>set A. \<forall>ip1\<in>wordinterval_to_set y. \<forall>y\<in>set B. \<forall>ip2\<in>wordinterval_to_set y. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma "A \<in> set (groupWIs c rs) \<Longrightarrow> B \<in> set (groupWIs c rs) \<Longrightarrow>
                \<exists>ip1 \<in> wordinterval_list_to_set A.
                \<exists>ip2 \<in> wordinterval_list_to_set B. same_fw_behaviour_one ip1 ip2 c rs
                \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); \<exists>ip1\<in>wordinterval_list_to_set A. \<exists>ip2\<in>wordinterval_list_to_set B. same_fw_behaviour_one ip1 ip2 c rs\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
using groupWIs_same_fw_not2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (groupWIs ?c ?rs); ?B \<in> set (groupWIs ?c ?rs); ?A \<noteq> ?B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set ?A. \<forall>ip2\<in>wordinterval_list_to_set ?B. \<not> same_fw_behaviour_one ip1 ip2 ?c ?rs

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (groupWIs c rs); B \<in> set (groupWIs c rs); \<exists>ip1\<in>wordinterval_list_to_set A. \<exists>ip2\<in>wordinterval_list_to_set B. same_fw_behaviour_one ip1 ip2 c rs\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by blast


[STATEMENT]
lemma groupWIs_complete: "(\<Union>x\<in> set (groupWIs c rs). wordinterval_list_to_set x) = (UNIV::'i::len word set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (wordinterval_list_to_set ` set (groupWIs c rs)) = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (wordinterval_list_to_set ` set (groupWIs c rs)) = UNIV
[PROOF STEP]
have "(\<Union> y \<in> (\<Union>x\<in> set (groupWIs c rs). set x). wordinterval_to_set y) = (UNIV::'i word set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` \<Union> (set ` set (groupWIs c rs))) = UNIV
[PROOF STEP]
apply(simp add: groupWIs_def Let_def groupF_Union_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (getParts rs)) = UNIV
[PROOF STEP]
using getParts_complete wordinterval_list_to_set_def
[PROOF STATE]
proof (prove)
using this:
wordinterval_list_to_set (getParts ?rs) = UNIV
wordinterval_list_to_set ?ws = \<Union> (set (map wordinterval_to_set ?ws))

goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (getParts rs)) = UNIV
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<Union> (wordinterval_to_set ` \<Union> (set ` set (groupWIs c rs))) = UNIV

goal (1 subgoal):
 1. \<Union> (wordinterval_list_to_set ` set (groupWIs c rs)) = UNIV
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> (wordinterval_to_set ` \<Union> (set ` set (groupWIs c rs))) = UNIV

goal (1 subgoal):
 1. \<Union> (wordinterval_list_to_set ` set (groupWIs c rs)) = UNIV
[PROOF STEP]
by(simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
\<Union> (wordinterval_list_to_set ` set (groupWIs c rs)) = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs_groupWIs1_equi: "groupWIs1 c rs = groupWIs c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs1 c rs = groupWIs c rs
[PROOF STEP]
apply(subst groupWIs1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let P = getParts rs; W = map getOneIp P; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) W, map (\<lambda>s. runFw s (getOneIp wi) c rs) W) in map (map fst) (groupF snd (map (\<lambda>x. (x, f x)) P))) = groupWIs c rs
[PROOF STEP]
apply(subst groupWIs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let P = getParts rs; W = map getOneIp P; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) W, map (\<lambda>s. runFw s (getOneIp wi) c rs) W) in map (map fst) (groupF snd (map (\<lambda>x. (x, f x)) P))) = (let W = getParts rs; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W)) in groupF f W)
[PROOF STEP]
using groupF_tuple
[PROOF STATE]
proof (prove)
using this:
groupF ?f ?xs = map (map fst) (groupF snd (map (\<lambda>x. (x, ?f x)) ?xs))

goal (1 subgoal):
 1. (let P = getParts rs; W = map getOneIp P; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) W, map (\<lambda>s. runFw s (getOneIp wi) c rs) W) in map (map fst) (groupF snd (map (\<lambda>x. (x, f x)) P))) = (let W = getParts rs; f = \<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W)) in groupF f W)
[PROOF STEP]
by metis