[STATEMENT]
lemma iptables_bigstep_undecided_to_undecided_in_doubt_allow_approx:
  assumes agree: "matcher_agree_on_exact_matches \<gamma> \<beta>"
      and good: "good_ruleset rs" and semantics: "\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided"
    shows "(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
from semantics good
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided
good_ruleset rs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided
good_ruleset rs

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
proof(induction rs Undecided Undecided rule: iptables_bigstep_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. good_ruleset [] \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 3. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Skip
[PROOF STATE]
proof (state)
this:
good_ruleset []

goal (6 subgoals):
 1. good_ruleset [] \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 3. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
good_ruleset []

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by(auto intro: approximating_bigstep.skip)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (5 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Log
[PROOF STATE]
proof (state)
this:
Semantics.matches \<gamma> m_ p
a_ = Log \<or> a_ = Empty
good_ruleset [Rule m_ a_]

goal (5 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Semantics.matches \<gamma> m_ p
a_ = Log \<or> a_ = Empty
good_ruleset [Rule m_ a_]

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by(auto intro: approximating_bigstep.empty approximating_bigstep.log approximating_bigstep.nomatch)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case (Nomatch m a)
[PROOF STATE]
proof (state)
this:
\<not> Semantics.matches \<gamma> m p
good_ruleset [Rule m a]

goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
with not_exact_match_in_doubt_allow_approx_match[OF agree]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a = action.Accept \<or> ?a = Reject \<or> ?a = action.Drop; \<not> Semantics.matches \<gamma> ?m ?p\<rbrakk> \<Longrightarrow> ?a = action.Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) ?m ?a ?p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) ?m ?a ?p
\<not> Semantics.matches \<gamma> m p
good_ruleset [Rule m a]
[PROOF STEP]
have
        "a \<noteq> Log \<Longrightarrow> a \<noteq> Empty \<Longrightarrow> a = Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a = action.Accept \<or> ?a = Reject \<or> ?a = action.Drop; \<not> Semantics.matches \<gamma> ?m ?p\<rbrakk> \<Longrightarrow> ?a = action.Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) ?m ?a ?p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) ?m ?a ?p
\<not> Semantics.matches \<gamma> m p
good_ruleset [Rule m a]

goal (1 subgoal):
 1. \<lbrakk>a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p
[PROOF STEP]
by(simp add: good_ruleset_alt) blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p

goal (4 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<noteq> Log; a \<noteq> Empty\<rbrakk> \<Longrightarrow> a = action.Accept \<and> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p \<or> \<not> Matching_Ternary.matches (\<beta>, in_doubt_allow) m a p

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by(cases a) (auto intro: approximating_bigstep.empty approximating_bigstep.log approximating_bigstep.accept approximating_bigstep.nomatch)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case (Seq rs rs1 rs2 t)
[PROOF STATE]
proof (state)
this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
from Seq
[PROOF STATE]
proof (chain)
picking this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
[PROOF STEP]
have "good_ruleset rs1" and "good_ruleset rs2"
[PROOF STATE]
proof (prove)
using this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs

goal (1 subgoal):
 1. good_ruleset rs1 &&& good_ruleset rs2
[PROOF STEP]
by(simp_all add: good_ruleset_append)
[PROOF STATE]
proof (state)
this:
good_ruleset rs1
good_ruleset rs2

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
good_ruleset rs1
good_ruleset rs2

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
from Seq iptables_bigstep_to_undecided
[PROOF STATE]
proof (chain)
picking this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> Undecided \<Longrightarrow> ?s = Undecided
[PROOF STEP]
have "t = Undecided"
[PROOF STATE]
proof (prove)
using this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> Undecided \<Longrightarrow> ?s = Undecided

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

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<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_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
good_ruleset rs1
good_ruleset rs2
t = Undecided
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
good_ruleset rs1
good_ruleset rs2
t = Undecided

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
using Seq
[PROOF STATE]
proof (prove)
using this:
good_ruleset rs1
good_ruleset rs2
t = Undecided
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Undecided; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Undecided
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by(fastforce intro: approximating_bigstep.decision Semantics_Ternary.seq')
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

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_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
qed(simp_all add: good_ruleset_def)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FinalAllow_approximating_in_doubt_allow:
   assumes agree: "matcher_agree_on_exact_matches \<gamma> \<beta>"
       and good: "good_ruleset rs" and semantics: "\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow"
     shows "(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
from semantics good
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
good_ruleset rs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
good_ruleset rs

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
proof(induction rs Undecided "Decision FinalAllow" rule: iptables_bigstep_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Accept; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Allow
[PROOF STATE]
proof (state)
this:
Semantics.matches \<gamma> m_ p
a_ = action.Accept
good_ruleset [Rule m_ a_]

goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Accept; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Semantics.matches \<gamma> m_ p
a_ = action.Accept
good_ruleset [Rule m_ a_]

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by (auto intro: agree approximating_bigstep.accept in_doubt_allow_allows_Accept)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case (Seq rs rs1 rs2 t)
[PROOF STATE]
proof (state)
this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs

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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
from Seq
[PROOF STATE]
proof (chain)
picking this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
[PROOF STEP]
have good1: "good_ruleset rs1" and good2: "good_ruleset rs2"
[PROOF STATE]
proof (prove)
using this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs

goal (1 subgoal):
 1. good_ruleset rs1 &&& good_ruleset rs2
[PROOF STEP]
by(simp_all add: good_ruleset_append)
[PROOF STATE]
proof (state)
this:
good_ruleset rs1
good_ruleset rs2

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 FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset rs\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
proof(cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>x2. t = Decision x2 \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Decision
[PROOF STATE]
proof (state)
this:
t = Decision x2_

goal (2 subgoals):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 2. \<And>x2. t = Decision x2 \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
with Seq good1 good2
[PROOF STATE]
proof (chain)
picking this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
good_ruleset rs1
good_ruleset rs2
t = Decision x2_
[PROOF STEP]
show "(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
good_ruleset rs1
good_ruleset rs2
t = Decision x2_

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by (auto intro: approximating_bigstep.decision approximating_bigstep.seq dest: Semantics.decisionD)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (1 subgoal):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Undecided
[PROOF STATE]
proof (state)
this:
t = Undecided

goal (1 subgoal):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
with iptables_bigstep_undecided_to_undecided_in_doubt_allow_approx[OF agree good1] Seq
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma>,\<gamma>,?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
t = Undecided
[PROOF STEP]
have
              "(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma>,\<gamma>,?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),?p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
t = Undecided

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (1 subgoal):
 1. t = Undecided \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
with Undecided Seq good1 good2
[PROOF STATE]
proof (chain)
picking this:
t = Undecided
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
good_ruleset rs1
good_ruleset rs2
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
show "(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
t = Undecided
rs = rs1 @ rs2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow> t
\<lbrakk>t = Decision FinalAllow; good_ruleset rs1\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs2, t\<rangle> \<Rightarrow> Decision FinalAllow
\<lbrakk>t = Undecided; good_ruleset rs2\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset rs
good_ruleset rs1
good_ruleset rs2
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<or> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by (auto intro: approximating_bigstep.seq Semantics_Ternary.seq' approximating_bigstep.decision)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
next
[PROOF STATE]
proof (state)
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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
case Call_result
[PROOF STATE]
proof (state)
this:
Semantics.matches \<gamma> m_ p
a_ = Call chain_
\<Gamma> chain_ = Some rs_
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs_, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
good_ruleset rs_ \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs_, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset [Rule m_ a_]

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 FinalAllow; good_ruleset rs \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Semantics.matches \<gamma> m_ p
a_ = Call chain_
\<Gamma> chain_ = Some rs_
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs_, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
good_ruleset rs_ \<Longrightarrow> (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs_, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
good_ruleset [Rule m_ a_]

goal (1 subgoal):
 1. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by(simp add: good_ruleset_alt)
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>[Rule m_ a_], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed