[STATEMENT]
lemma one_before_two_2:
  "alw (\<lambda>x. statename (shd (stl x)) = Some 2 \<longrightarrow> statename (shd x) = Some 1) (make_full_observation drinks (Some 2) r [r $ 1] x2a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (make_full_observation drinks (Some 2) r [r $ 1] x2a)
[PROOF STEP]
proof(coinduction)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
case alw
[PROOF STATE]
proof (state)
this:


goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))
[PROOF STEP]
apply (simp add: drinks_step_2_none)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. make_full_observation drinks None r [] (stl x2a) = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (make_full_observation drinks None r [] (stl x2a))
[PROOF STEP]
by (metis (mono_tags, lifting) alw_mono nxt.simps once_none_nxt_always_none option.distinct(1))
[PROOF STATE]
proof (state)
this:
\<exists>xs. make_full_observation drinks (Some 2) r [r $ 1] x2a = xs \<and> (state_eq (Some 2) (stl xs) \<longrightarrow> state_eq (Some 1) xs) \<and> (stl xs = make_full_observation drinks (Some 2) r [r $ 1] x2a \<or> alw (\<lambda>x. state_eq (Some 2) (stl x) \<longrightarrow> state_eq (Some 1) x) (stl xs))

goal:
No subgoals!
[PROOF STEP]
qed