[STATEMENT]
lemma iptables_bigstep_undecided_to_undecided_in_doubt_deny_approx: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
       good_ruleset rs \<Longrightarrow>
       \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<Longrightarrow>
       (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(induction rs Undecided Undecided rule: iptables_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ [Rule m' Return] @ rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 6. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 6. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.skip)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.empty approximating_bigstep.log approximating_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(case_tac "a = Log")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a = Log\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a \<noteq> Log\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.log approximating_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a \<noteq> Log\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(case_tac "a = Empty")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a \<noteq> Log; a = Empty\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.empty approximating_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(drule_tac a=a in not_exact_match_in_doubt_deny_approx_match)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<or> a = Reject \<or> a = action.Drop
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> \<not> Semantics.matches \<gamma> (?m21 m a) (?p21 m a)
 3. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty; (a = action.Drop \<or> a = Reject) \<and> Matching_Ternary.matches (\<beta>, in_doubt_deny) (?m21 m a) a (?p21 m a) \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) (?m21 m a) a (?p21 m a)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 6. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<or> a = Reject \<or> a = action.Drop
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty; (a = action.Drop \<or> a = Reject) \<and> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; a = action.Accept \<or> a = action.Drop \<or> a = Reject; a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<or> a = Reject \<or> a = action.Drop
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty; (a = action.Drop \<or> a = Reject) \<and> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 5. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]; a \<noteq> Log; a \<noteq> Empty; (a = action.Drop \<or> a = Reject) \<and> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.drop approximating_bigstep.nomatch approximating_bigstep.reject)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(frule iptables_bigstep_to_undecided)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>2 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_append)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1 \<and> good_ruleset rs\<^sub>2; t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis (opaque_lifting, no_types) approximating_bigstep.decision Semantics_Ternary.seq')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ Rule m' Return # rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs\<^sub>1 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma FinalDeny_approximating_in_doubt_deny: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
   good_ruleset rs \<Longrightarrow>
   \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(induction rs Undecided "Decision FinalDeny" rule: iptables_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Drop \<or> a = Reject; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Drop \<or> a = Reject; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.drop approximating_bigstep.reject in_doubt_deny_denies_DropReject)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(case_tac t)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<lbrakk>t = Decision FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalDeny; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Decision x2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>2 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision x2; \<lbrakk>x2 = FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Decision x2\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Decision x2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision x2; \<lbrakk>x2 = FinalDeny; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Decision x2\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Decision x2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>2 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_append)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision x2; x2 = FinalDeny \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Decision x2\<rangle> \<Rightarrow> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1 \<and> good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>2 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.decision approximating_bigstep.seq Semantics.decisionD state.inject)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs\<^sub>2 \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2); t = Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_append, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(drule(2) iptables_bigstep_undecided_to_undecided_in_doubt_deny_approx)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 3. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.seq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 2. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply (metis approximating_bigstep.decision Semantics_Ternary.seq')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a chain rs. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call chain)]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_deny),p\<turnstile> \<langle>[Rule m (Call chain)], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done