[STATEMENT]
lemma directly_subsumes: "directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing
[PROOF STEP]
apply (rule direct_subsumption[of _ _ _ _ "\<lambda>c2. c2 $ 2 = Some (Num 0)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t c1 c2. \<lbrakk>obtains 1 c1 drinks2 0 <> t; obtains 1 c2 drinks 0 <> t\<rbrakk> \<Longrightarrow> c2 $ 2 = Some (Num 0)
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> subsumes vend_fail c vend_nothing
[PROOF STEP]
apply (simp add: obtains_1_c2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> subsumes vend_fail c vend_nothing
[PROOF STEP]
apply (rule subsumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> Label vend_nothing = Label vend_fail \<and> Arity vend_nothing = Arity vend_fail
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> can_take_transition vend_fail i c
 3. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 4. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> can_take_transition vend_fail i c
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 3. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
by (simp add: posterior_separate_def vend_fail_def vend_nothing_def)