[STATEMENT]
lemma check_tableau_normalized: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))
[PROOF STEP]
using check_tableau
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> \<U> ?s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s ?s; \<diamond> ?s; \<triangle> (\<T> ?s); \<nabla> ?s\<rbrakk> \<Longrightarrow> let s' = check ?s in ?v \<Turnstile>\<^sub>t \<T> ?s = ?v \<Turnstile>\<^sub>t \<T> s' \<and> \<triangle> (\<T> s') \<and> \<nabla> s' \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s'

goal (1 subgoal):
 1. \<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))
[PROOF STEP]
by (simp add: Let_def)