[STATEMENT]
lemma succ_valuation_satisfies:
  assumes "s \<succ> s'" "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s"
  shows "\<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
from \<open>s \<succ> s'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> s \<succ>\<^sub>x s' \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s
[PROOF STEP]
obtain x\<^sub>i x\<^sub>j b where
    "\<triangle> (\<T> s)" "\<nabla> s"
    "min_lvar_not_in_bounds s = Some x\<^sub>i"
    "min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j"
    "b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)"
    "s' = pivot_and_update x\<^sub>i x\<^sub>j b s"
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> s \<succ>\<^sub>x s' \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s

goal (1 subgoal):
 1. (\<And>x\<^sub>i x\<^sub>j b. \<lbrakk>\<triangle> (\<T> s); \<nabla> s; min_lvar_not_in_bounds s = Some x\<^sub>i; min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j; b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i); s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding gt_state_def
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> (\<exists>x\<^sub>i x\<^sub>j l\<^sub>i. let dir = if \<langle>\<V> s\<rangle> x\<^sub>i <\<^sub>l\<^sub>b \<B>\<^sub>l s x\<^sub>i then Positive else Negative in gt_state' dir s s' x\<^sub>i x\<^sub>j l\<^sub>i) \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s

goal (1 subgoal):
 1. (\<And>x\<^sub>i x\<^sub>j b. \<lbrakk>\<triangle> (\<T> s); \<nabla> s; min_lvar_not_in_bounds s = Some x\<^sub>i; min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j; b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i); s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
[PROOF STEP]
have
    "x\<^sub>i \<in> lvars (\<T> s)"
    "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_lvar_not_in_bounds_lvars[of s x\<^sub>i]
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_rvar_incdec_eq_Some_rvars[of Positive s "eq_for_lvar (\<T> s) x\<^sub>i" x\<^sub>j]
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_rvar_incdec_eq_Some_rvars[of Negative s "eq_for_lvar (\<T> s) x\<^sub>i" x\<^sub>j] \<open>\<triangle> (\<T> s)\<close>
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<triangle> (\<T> s)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
by (auto simp add: normalized_tableau_def)
[PROOF STATE]
proof (state)
this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using pivotandupdate_satisfies_tableau[of s x\<^sub>i x\<^sub>j b]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using pivotandupdate_tableau_equiv[of s x\<^sub>i x\<^sub>j ]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> ?v \<Turnstile>\<^sub>t \<T> s = ?v \<Turnstile>\<^sub>t \<T> (pivot_and_update x\<^sub>i x\<^sub>j ?c s)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using \<open>\<triangle> (\<T> s)\<close> \<open>\<nabla> s\<close> \<open>\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s\<close> \<open>s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<close>
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> ?v \<Turnstile>\<^sub>t \<T> s = ?v \<Turnstile>\<^sub>t \<T> (pivot_and_update x\<^sub>i x\<^sub>j ?c s)
\<triangle> (\<T> s)
\<nabla> s
\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'

goal:
No subgoals!
[PROOF STEP]
qed