[STATEMENT]
lemma approximating_bigstep_undecided_to_undecided_in_doubt_allow_approx: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
       good_ruleset rs \<Longrightarrow>
       (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or>  \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(induction rs Undecided Undecided rule: approximating_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.skip)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.empty iptables_bigstep.log iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp split: ternaryvalue.split_asm add: matches_case_ternaryvalue_tuple)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryFalse\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis in_doubt_allow_allows_Accept iptables_bigstep.nomatch matches_casesE ternaryvalue.distinct(1) ternaryvalue.distinct(5))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = action.Accept\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = action.Drop\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 7. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 8. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 9. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_allow a p; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 10. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m action.Drop]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; a = action.Drop\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m action.Drop], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m action.Drop], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Log]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Reject]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 6. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 7. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 8. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 9. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.drop iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Log]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Reject]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 7. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 8. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.log iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Reject]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Reject], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 7. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.nomatch iptables_bigstep.reject)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 6. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 5. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.empty iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_append,clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; \<not> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided
[PROOF STEP]
by (metis approximating_bigstep_to_undecided iptables_bigstep.decision iptables_bigstep.seq)


[STATEMENT]
lemma FinalDeny_approximating_in_doubt_allow: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
   good_ruleset rs \<Longrightarrow>
   (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(induction rs Undecided "Decision FinalDeny" rule: approximating_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; a = action.Drop \<or> a = Reject; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p; a = action.Drop \<or> a = Reject; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis action.distinct(1) action.distinct(5) deny not_exact_match_in_doubt_allow_approx_match)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_append, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(case_tac t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(drule(2) approximating_bigstep_undecided_to_undecided_in_doubt_allow_approx[where \<Gamma>=\<Gamma>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.seq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
apply (metis iptables_bigstep.decision iptables_bigstep.seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalDeny \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny
[PROOF STEP]
by (metis Decision_approximating_bigstep_fun approximating_semantics_imp_fun iptables_bigstep.decision iptables_bigstep.seq)