[STATEMENT]
lemma reduce_not_trap:
  assumes "\<lparr>s;vs;es\<rparr> \<leadsto>_i \<lparr>s';vs';es'\<rparr>"
  shows "es \<noteq> [Trap]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. es \<noteq> [Trap]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lparr>s;vs;es\<rparr> \<leadsto>_ i \<lparr>s';vs';es'\<rparr>

goal (1 subgoal):
 1. es \<noteq> [Trap]
[PROOF STEP]
proof (induction rule: reduce.induct)
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>e e' s vs i. \<lparr>e\<rparr> \<leadsto> \<lparr>e'\<rparr> \<Longrightarrow> e \<noteq> [Trap]
 2. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 3. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 5. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 8. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 9. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 10. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
A total of 24 subgoals...
[PROOF STEP]
case (basic e e' s vs i)
[PROOF STATE]
proof (state)
this:
\<lparr>e\<rparr> \<leadsto> \<lparr>e'\<rparr>

goal (24 subgoals):
 1. \<And>e e' s vs i. \<lparr>e\<rparr> \<leadsto> \<lparr>e'\<rparr> \<Longrightarrow> e \<noteq> [Trap]
 2. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 3. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 5. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 8. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 9. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 10. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
A total of 24 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lparr>e\<rparr> \<leadsto> \<lparr>e'\<rparr>

goal (1 subgoal):
 1. e \<noteq> [Trap]
[PROOF STEP]
using reduce_simple_not_trap
[PROOF STATE]
proof (prove)
using this:
\<lparr>e\<rparr> \<leadsto> \<lparr>e'\<rparr>
\<lparr>?es\<rparr> \<leadsto> \<lparr>?es'\<rparr> \<Longrightarrow> ?es \<noteq> [Trap]

goal (1 subgoal):
 1. e \<noteq> [Trap]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e \<noteq> [Trap]

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
case (label s vs es i s' vs' es' k lholed les les')
[PROOF STATE]
proof (state)
this:
\<lparr>s;vs;es\<rparr> \<leadsto>_ i \<lparr>s';vs';es'\<rparr>
Lfilled k lholed es les
Lfilled k lholed es' les'
es \<noteq> [Trap]

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lparr>s;vs;es\<rparr> \<leadsto>_ i \<lparr>s';vs';es'\<rparr>
Lfilled k lholed es les
Lfilled k lholed es' les'
es \<noteq> [Trap]

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
assume "les = [Trap]"
[PROOF STATE]
proof (state)
this:
les = [Trap]

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
hence "Lfilled k lholed es [Trap]"
[PROOF STATE]
proof (prove)
using this:
les = [Trap]

goal (1 subgoal):
 1. Lfilled k lholed es [Trap]
[PROOF STEP]
using label(2)
[PROOF STATE]
proof (prove)
using this:
les = [Trap]
Lfilled k lholed es les

goal (1 subgoal):
 1. Lfilled k lholed es [Trap]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Lfilled k lholed es [Trap]

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
Lfilled k lholed es [Trap]

goal (1 subgoal):
 1. False
[PROOF STEP]
using lfilled_single reduce_not_nil[OF label(1)] label(4)
[PROOF STATE]
proof (prove)
using this:
Lfilled k lholed es [Trap]
\<lbrakk>Lfilled ?k ?lholed ?es [?e]; \<And>a b c. ?e \<noteq> Label a b c\<rbrakk> \<Longrightarrow> ?es = [?e] \<and> ?lholed = LBase [] [] \<or> ?es = []
es \<noteq> []
es \<noteq> [Trap]

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
les = [Trap] \<Longrightarrow> False

goal (23 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 23 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
les = [Trap] \<Longrightarrow> False

goal (1 subgoal):
 1. les \<noteq> [Trap]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
les \<noteq> [Trap]

goal (22 subgoals):
 1. \<And>s vs j i. [$Call j] \<noteq> [Trap]
 2. \<And>s i c cl j tf vs. \<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 3. \<And>s i c cl j vs. stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl \<or> stab s i (nat_of_int c) = None \<Longrightarrow> [$C ConstInt32 c, $Call_indirect j] \<noteq> [Trap]
 4. \<And>cl j t1s t2s ts es ves vcs n k m zs s vs i. \<lbrakk>cl = Func_native j (t1s _> t2s) ts es; ves = $$* vcs; length vcs = n; length ts = k; length t1s = n; length t2s = m; n_zeros ts = zs\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 5. \<And>cl t1s t2s f ves vcs n m s hs s' vcs' vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 6. \<And>cl t1s t2s f ves vcs n m s vs i. \<lbrakk>cl = Func_host (t1s _> t2s) f; ves = $$* vcs; length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> ves @ [Callcl cl] \<noteq> [Trap]
 7. \<And>vi j s v vs i. length vi = j \<Longrightarrow> [$Get_local j] \<noteq> [Trap]
 8. \<And>vi j s v vs v' i. length vi = j \<Longrightarrow> [$C v', $Set_local j] \<noteq> [Trap]
 9. \<And>s vs j i. [$Get_global j] \<noteq> [Trap]
 10. \<And>s i j v s' vs. supdate_glob s i j v = s' \<Longrightarrow> [$C v, $Set_global j] \<noteq> [Trap]
A total of 22 subgoals...
[PROOF STEP]
qed auto


[STATEMENT]
lemma lens_equiv_via_bij:
  assumes "bij_lens Z" "X = Z ;\<^sub>L Y"
  shows "X \<approx>\<^sub>L Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<approx>\<^sub>L Y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij_lens Z
X = Z ;\<^sub>L Y

goal (1 subgoal):
 1. X \<approx>\<^sub>L Y
[PROOF STEP]
apply (auto simp add: lens_equiv_def sublens_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> \<exists>Za. vwb_lens Za \<and> Z ;\<^sub>L Y = Za ;\<^sub>L Y
 2. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> \<exists>Za. vwb_lens Za \<and> Y = Za ;\<^sub>L (Z ;\<^sub>L Y)
[PROOF STEP]
using bij_lens_vwb
[PROOF STATE]
proof (prove)
using this:
bij_lens ?x \<Longrightarrow> vwb_lens ?x

goal (2 subgoals):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> \<exists>Za. vwb_lens Za \<and> Z ;\<^sub>L Y = Za ;\<^sub>L Y
 2. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> \<exists>Za. vwb_lens Za \<and> Y = Za ;\<^sub>L (Z ;\<^sub>L Y)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> \<exists>Za. vwb_lens Za \<and> Y = Za ;\<^sub>L (Z ;\<^sub>L Y)
[PROOF STEP]
apply (rule_tac x="lens_inv Z" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> vwb_lens (inv\<^sub>L Z) \<and> Y = inv\<^sub>L Z ;\<^sub>L (Z ;\<^sub>L Y)
[PROOF STEP]
apply (auto simp add: lens_comp_assoc bij_lens_inv_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> vwb_lens (inv\<^sub>L Z)
[PROOF STEP]
using bij_lens_vwb lens_inv_bij
[PROOF STATE]
proof (prove)
using this:
bij_lens ?x \<Longrightarrow> vwb_lens ?x
bij_lens ?X \<Longrightarrow> bij_lens (inv\<^sub>L ?X)

goal (1 subgoal):
 1. \<lbrakk>bij_lens Z; X = Z ;\<^sub>L Y\<rbrakk> \<Longrightarrow> vwb_lens (inv\<^sub>L Z)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma poly_rel_poly_of_list[transfer_rule]: "(list_all2 R ===> poly_rel) (poly_of_list_i ops) poly_of_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_all2 R ===> poly_rel) (poly_of_list_i ops) poly_of_list
[PROOF STEP]
unfolding rel_fun_def poly_of_list_i_def poly_rel_def poly_of_list_impl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. list_all2 R x y \<longrightarrow> list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)
[PROOF STEP]
proof (intro allI impI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. list_all2 R x y \<Longrightarrow> list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)
[PROOF STEP]
case (1 x y)
[PROOF STATE]
proof (state)
this:
list_all2 R x y

goal (1 subgoal):
 1. \<And>x y. list_all2 R x y \<Longrightarrow> list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)
[PROOF STEP]
note [transfer_rule] = this
[PROOF STATE]
proof (state)
this:
list_all2 R x y

goal (1 subgoal):
 1. \<And>x y. list_all2 R x y \<Longrightarrow> list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
list_all2 R (strip_while ((=) (arith_ops_record.zero ops)) x) (strip_while ((=) (0::'a)) y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rt_fresh_as_refl [simp]: "\<And>rt dip. rt \<approx>\<^bsub>dip\<^esub> rt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. rt \<approx>\<^bsub>dip\<^esub> rt
[PROOF STEP]
unfolding rt_fresh_as_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dip. rt \<sqsubseteq>\<^bsub>dip\<^esub> rt \<and> rt \<sqsubseteq>\<^bsub>dip\<^esub> rt
[PROOF STEP]
by simp


[STATEMENT]
lemma preprocess:
  assumes id: "preprocess cs = (t, as, trans_v, ui)"
  shows "\<triangle> t"
  "fst ` set as \<union> set ui \<subseteq> fst ` set cs"
  "distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)"
  "I \<inter> set ui = {} \<Longrightarrow> (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow>
       \<langle>v\<rangle> \<Turnstile>\<^sub>t t \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs"
  "i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs"
  "\<exists> v. (I,v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set cs \<Longrightarrow> \<exists>v'. (I,v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<triangle> t &&& fst ` set as \<union> set ui \<subseteq> fst ` set cs &&& (distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as))) &&& (\<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs) &&& (i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs) &&& (\<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
define ncs where "ncs = map (map_prod id normalize_ns_constraint) cs"
[PROOF STATE]
proof (state)
this:
ncs = map (map_prod id normalize_ns_constraint) cs

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
have ncs: "fst ` set ncs = fst ` set cs" "\<And> Iv. Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set ncs \<longleftrightarrow> Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set ncs = fst ` set cs &&& (\<And>Iv. Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs = Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs)
[PROOF STEP]
unfolding ncs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (map (map_prod id normalize_ns_constraint) cs) = fst ` set cs &&& (\<And>Iv. Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set (map (map_prod id normalize_ns_constraint) cs) = Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs)
[PROOF STEP]
by force auto
[PROOF STATE]
proof (state)
this:
fst ` set ncs = fst ` set cs
?Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs = ?Iv \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
from id
[PROOF STATE]
proof (chain)
picking this:
preprocess cs = (t, as, trans_v, ui)
[PROOF STEP]
obtain t1 where part1: "preprocess_part_1 ncs = (t1,as,ui)"
[PROOF STATE]
proof (prove)
using this:
preprocess cs = (t, as, trans_v, ui)

goal (1 subgoal):
 1. (\<And>t1. preprocess_part_1 ncs = (t1, as, ui) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding preprocess_def
[PROOF STATE]
proof (prove)
using this:
(case preprocess_part_1 (map (map_prod id normalize_ns_constraint) cs) of (t, as, ui) \<Rightarrow> case preprocess_part_2 as t of (t, tv) \<Rightarrow> (t, as, tv, ui)) = (t, as, trans_v, ui)

goal (1 subgoal):
 1. (\<And>t1. preprocess_part_1 ncs = (t1, as, ui) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ncs_def split: prod.splits)
[PROOF STATE]
proof (state)
this:
preprocess_part_1 ncs = (t1, as, ui)

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
from id[unfolded preprocess_def part1 split ncs_def[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
(case preprocess_part_2 as t1 of (t, tv) \<Rightarrow> (t, as, tv, ui)) = (t, as, trans_v, ui)
[PROOF STEP]
have part_2: "preprocess_part_2 as t1 = (t,trans_v)"
[PROOF STATE]
proof (prove)
using this:
(case preprocess_part_2 as t1 of (t, tv) \<Rightarrow> (t, as, tv, ui)) = (t, as, trans_v, ui)

goal (1 subgoal):
 1. preprocess_part_2 as t1 = (t, trans_v)
[PROOF STEP]
by (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
preprocess_part_2 as t1 = (t, trans_v)

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
have norm: "\<triangle> t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<triangle> t1
[PROOF STEP]
using normalized_tableau_preprocess' part1
[PROOF STATE]
proof (prove)
using this:
\<triangle> (Tableau (preprocess' ?cs (start_fresh_variable ?cs)))
preprocess_part_1 ncs = (t1, as, ui)

goal (1 subgoal):
 1. \<triangle> t1
[PROOF STEP]
by (auto simp: preprocess_part_1_def Let_def)
[PROOF STATE]
proof (state)
this:
\<triangle> t1

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
note part_2 = preprocess_part_2[OF part_2 norm]
[PROOF STATE]
proof (state)
this:
\<triangle> t
\<langle>?w\<rangle> \<Turnstile>\<^sub>t t \<Longrightarrow> \<langle>trans_v ?w\<rangle> \<Turnstile>\<^sub>t t1
(?I, \<langle>?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow> (?I, \<langle>trans_v ?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as
?v \<Turnstile>\<^sub>t t1 \<Longrightarrow> ?v \<Turnstile>\<^sub>t t

goal (6 subgoals):
 1. \<triangle> t
 2. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 3. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 4. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 6. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
show "\<triangle> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<triangle> t
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<triangle> t

goal (5 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
have unsat: "(I,\<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow> \<langle>v\<rangle> \<Turnstile>\<^sub>t t1 \<Longrightarrow> I \<inter> set ui = {} \<Longrightarrow> (I,\<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set ncs" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t1; I \<inter> set ui = {}\<rbrakk> \<Longrightarrow> (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
[PROOF STEP]
using part1[unfolded preprocess_part_1_def Let_def, simplified] i_preprocess'_sat[of I]
[PROOF STATE]
proof (prove)
using this:
Tableau (preprocess' ncs (start_fresh_variable ncs)) = t1 \<and> Atoms (preprocess' ncs (start_fresh_variable ncs)) = as \<and> UnsatIndices (preprocess' ncs (start_fresh_variable ncs)) = ui
\<lbrakk>(I, ?v) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set (Atoms (preprocess' ?s ?start)); ?v \<Turnstile>\<^sub>t Tableau (preprocess' ?s ?start); I \<inter> set (UnsatIndices (preprocess' ?s ?start)) = {}\<rbrakk> \<Longrightarrow> (I, ?v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ?s

goal (1 subgoal):
 1. \<lbrakk>(I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t1; I \<inter> set ui = {}\<rbrakk> \<Longrightarrow> (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>(I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>?v\<rangle> \<Turnstile>\<^sub>t t1; I \<inter> set ui = {}\<rbrakk> \<Longrightarrow> (I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs

goal (5 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 5. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
with part_2(2,3)
[PROOF STATE]
proof (chain)
picking this:
\<langle>?w\<rangle> \<Turnstile>\<^sub>t t \<Longrightarrow> \<langle>trans_v ?w\<rangle> \<Turnstile>\<^sub>t t1
(?I, \<langle>?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow> (?I, \<langle>trans_v ?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as
\<lbrakk>(I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>?v\<rangle> \<Turnstile>\<^sub>t t1; I \<inter> set ui = {}\<rbrakk> \<Longrightarrow> (I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
[PROOF STEP]
show "I \<inter> set ui = {} \<Longrightarrow> (I,\<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow> \<langle>v\<rangle> \<Turnstile>\<^sub>t t \<Longrightarrow> (I,\<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set cs"
[PROOF STATE]
proof (prove)
using this:
\<langle>?w\<rangle> \<Turnstile>\<^sub>t t \<Longrightarrow> \<langle>trans_v ?w\<rangle> \<Turnstile>\<^sub>t t1
(?I, \<langle>?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<Longrightarrow> (?I, \<langle>trans_v ?w\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as
\<lbrakk>(I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>?v\<rangle> \<Turnstile>\<^sub>t t1; I \<inter> set ui = {}\<rbrakk> \<Longrightarrow> (I, \<langle>?v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs

goal (1 subgoal):
 1. \<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
by (auto simp: ncs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>I \<inter> set ui = {}; (I, \<langle>v\<rangle>) \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as; \<langle>v\<rangle> \<Turnstile>\<^sub>t t\<rbrakk> \<Longrightarrow> (I, \<langle>trans_v v\<rangle>) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (4 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
from part1[unfolded preprocess_part_1_def Let_def]
[PROOF STATE]
proof (chain)
picking this:
(Tableau (preprocess' ncs (start_fresh_variable ncs)), Atoms (preprocess' ncs (start_fresh_variable ncs)), UnsatIndices (preprocess' ncs (start_fresh_variable ncs))) = (t1, as, ui)
[PROOF STEP]
obtain var where
    as: "as = Atoms (preprocess' ncs var)" and ui: "ui = UnsatIndices (preprocess' ncs var)"
[PROOF STATE]
proof (prove)
using this:
(Tableau (preprocess' ncs (start_fresh_variable ncs)), Atoms (preprocess' ncs (start_fresh_variable ncs)), UnsatIndices (preprocess' ncs (start_fresh_variable ncs))) = (t1, as, ui)

goal (1 subgoal):
 1. (\<And>var. \<lbrakk>as = Atoms (preprocess' ncs var); ui = UnsatIndices (preprocess' ncs var)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as = Atoms (preprocess' ncs var)
ui = UnsatIndices (preprocess' ncs var)

goal (4 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
note min_defs = distinct_indices_atoms_def distinct_indices_ns_def
[PROOF STATE]
proof (state)
this:
distinct_indices_atoms ?as = (\<forall>i a b. (i, a) \<in> ?as \<longrightarrow> (i, b) \<in> ?as \<longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b)
distinct_indices_ns ?ns = (\<forall>n1 n2 i. (i, n1) \<in> ?ns \<longrightarrow> (i, n2) \<in> ?ns \<longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2)

goal (4 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
have min1: "(distinct_indices_ns (set ncs) \<longrightarrow> (\<forall> k a. (k,a) \<in> set as \<longrightarrow> (\<exists> v p. a = qdelta_constraint_to_atom p v \<and> (k,p) \<in> set ncs
    \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)  )))
    \<and> fst ` set as \<union> set ui \<subseteq> fst ` set ncs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct_indices_ns (set ncs) \<longrightarrow> (\<forall>k a. (k, a) \<in> set as \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)))) \<and> fst ` set as \<union> set ui \<subseteq> fst ` set ncs
[PROOF STEP]
unfolding as ui
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct_indices_ns (set ncs) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ncs var)) \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)))) \<and> fst ` set (Atoms (preprocess' ncs var)) \<union> set (UnsatIndices (preprocess' ncs var)) \<subseteq> fst ` set ncs
[PROOF STEP]
proof (induct ncs var rule: preprocess'.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. (distinct_indices_ns (set []) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' [] v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set [] \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' [] v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' [] v)) \<union> set (UnsatIndices (preprocess' [] v)) \<subseteq> fst ` set []
 2. \<And>i h t v. (distinct_indices_ns (set t) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' t v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t \<Longrightarrow> (distinct_indices_ns (set ((i, h) # t)) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
case (2 i h t v)
[PROOF STATE]
proof (state)
this:
(distinct_indices_ns (set t) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' t v)) \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some v)))) \<and> fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t

goal (2 subgoals):
 1. \<And>v. (distinct_indices_ns (set []) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' [] v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set [] \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' [] v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' [] v)) \<union> set (UnsatIndices (preprocess' [] v)) \<subseteq> fst ` set []
 2. \<And>i h t v. (distinct_indices_ns (set t) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' t v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t \<Longrightarrow> (distinct_indices_ns (set ((i, h) # t)) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
hence sub: "fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t"
[PROOF STATE]
proof (prove)
using this:
(distinct_indices_ns (set t) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' t v)) \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some v)))) \<and> fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t

goal (1 subgoal):
 1. fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t

goal (2 subgoals):
 1. \<And>v. (distinct_indices_ns (set []) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' [] v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set [] \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' [] v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' [] v)) \<union> set (UnsatIndices (preprocess' [] v)) \<subseteq> fst ` set []
 2. \<And>i h t v. (distinct_indices_ns (set t) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' t v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t \<Longrightarrow> (distinct_indices_ns (set ((i, h) # t)) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct_indices_ns (set ((i, h) # t)) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v)) \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)))) \<and> fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
proof (intro conjI impI allI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
 2. fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
show "fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i,h) #t) v)) \<subseteq> fst ` set ((i, h) # t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
using sub
[PROOF STATE]
proof (prove)
using this:
fst ` set (Atoms (preprocess' t v)) \<union> set (UnsatIndices (preprocess' t v)) \<subseteq> fst ` set t

goal (1 subgoal):
 1. fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)
[PROOF STEP]
by (auto simp: Let_def split: option.splits)
[PROOF STATE]
proof (state)
this:
fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)

goal (1 subgoal):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
case (1 k a)
[PROOF STATE]
proof (state)
this:
distinct_indices_ns (set ((i, h) # t))
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))

goal (1 subgoal):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
hence min': "distinct_indices_ns (set t)"
[PROOF STATE]
proof (prove)
using this:
distinct_indices_ns (set ((i, h) # t))
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))

goal (1 subgoal):
 1. distinct_indices_ns (set t)
[PROOF STEP]
unfolding min_defs list.simps
[PROOF STATE]
proof (prove)
using this:
\<forall>n1 n2 i. (i, n1) \<in> insert (i, h) (set t) \<longrightarrow> (i, n2) \<in> insert (i, h) (set t) \<longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))

goal (1 subgoal):
 1. \<forall>n1 n2 i. (i, n1) \<in> set t \<longrightarrow> (i, n2) \<in> set t \<longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct_indices_ns (set t)

goal (1 subgoal):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
note IH = 2[THEN conjunct1, rule_format, OF min']
[PROOF STATE]
proof (state)
this:
(?k, ?a) \<in> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. ?a = qdelta_constraint_to_atom p v \<and> (?k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some v)

goal (1 subgoal):
 1. \<And>k a. \<lbrakk>distinct_indices_ns (set ((i, h) # t)); (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))\<rbrakk> \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
proof (cases "(k,a) \<in> set (Atoms (preprocess' t v))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (k, a) \<in> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
 2. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(k, a) \<in> set (Atoms (preprocess' t v))

goal (2 subgoals):
 1. (k, a) \<in> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
 2. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set t \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' t v) (poly p) = Some v)

goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
by (force simp: Let_def split: option.splits if_split)
[PROOF STATE]
proof (state)
this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)

goal (1 subgoal):
 1. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
case new: False
[PROOF STATE]
proof (state)
this:
(k, a) \<notin> set (Atoms (preprocess' t v))

goal (1 subgoal):
 1. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
with 1(2)
[PROOF STATE]
proof (chain)
picking this:
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))
(k, a) \<notin> set (Atoms (preprocess' t v))
[PROOF STEP]
have ki: "k = i"
[PROOF STATE]
proof (prove)
using this:
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))
(k, a) \<notin> set (Atoms (preprocess' t v))

goal (1 subgoal):
 1. k = i
[PROOF STEP]
by (auto simp: Let_def split: if_splits option.splits)
[PROOF STATE]
proof (state)
this:
k = i

goal (1 subgoal):
 1. (k, a) \<notin> set (Atoms (preprocess' t v)) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
proof (cases "is_monom (poly h)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
 2. \<not> is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_monom (poly h)

goal (2 subgoals):
 1. is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
 2. \<not> is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_monom (poly h)

goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
using new 1(2)
[PROOF STATE]
proof (prove)
using this:
is_monom (poly h)
(k, a) \<notin> set (Atoms (preprocess' t v))
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))

goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
by (auto simp: Let_def True intro!: exI)
[PROOF STATE]
proof (state)
this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)

goal (1 subgoal):
 1. \<not> is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
case no_monom: False
[PROOF STATE]
proof (state)
this:
\<not> is_monom (poly h)

goal (1 subgoal):
 1. \<not> is_monom (poly h) \<Longrightarrow> \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_monom (poly h)

goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
using new 1(2)
[PROOF STATE]
proof (prove)
using this:
\<not> is_monom (poly h)
(k, a) \<notin> set (Atoms (preprocess' t v))
(k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v))

goal (1 subgoal):
 1. \<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)
[PROOF STEP]
by (auto simp: Let_def no_monom split: option.splits if_splits intro!: exI)
[PROOF STATE]
proof (state)
this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(distinct_indices_ns (set ((i, h) # t)) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' ((i, h) # t) v)) \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ((i, h) # t) \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ((i, h) # t) v) (poly p) = Some v)))) \<and> fst ` set (Atoms (preprocess' ((i, h) # t) v)) \<union> set (UnsatIndices (preprocess' ((i, h) # t) v)) \<subseteq> fst ` set ((i, h) # t)

goal (1 subgoal):
 1. \<And>v. (distinct_indices_ns (set []) \<longrightarrow> (\<forall>k a. (k, a) \<in> set (Atoms (preprocess' [] v)) \<longrightarrow> (\<exists>va p. a = qdelta_constraint_to_atom p va \<and> (k, p) \<in> set [] \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' [] v) (poly p) = Some va)))) \<and> fst ` set (Atoms (preprocess' [] v)) \<union> set (UnsatIndices (preprocess' [] v)) \<subseteq> fst ` set []
[PROOF STEP]
qed (auto simp: min_defs)
[PROOF STATE]
proof (state)
this:
(distinct_indices_ns (set ncs) \<longrightarrow> (\<forall>k a. (k, a) \<in> set as \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)))) \<and> fst ` set as \<union> set ui \<subseteq> fst ` set ncs

goal (4 subgoals):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
 2. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 3. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 4. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(distinct_indices_ns (set ncs) \<longrightarrow> (\<forall>k a. (k, a) \<in> set as \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)))) \<and> fst ` set as \<union> set ui \<subseteq> fst ` set ncs
[PROOF STEP]
show "fst ` set as \<union> set ui \<subseteq> fst ` set cs"
[PROOF STATE]
proof (prove)
using this:
(distinct_indices_ns (set ncs) \<longrightarrow> (\<forall>k a. (k, a) \<in> set as \<longrightarrow> (\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)))) \<and> fst ` set as \<union> set ui \<subseteq> fst ` set ncs

goal (1 subgoal):
 1. fst ` set as \<union> set ui \<subseteq> fst ` set cs
[PROOF STEP]
by (auto simp: ncs)
[PROOF STATE]
proof (state)
this:
fst ` set as \<union> set ui \<subseteq> fst ` set cs

goal (3 subgoals):
 1. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 2. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 3. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
fst ` set as \<union> set ui \<subseteq> fst ` set cs

goal (3 subgoals):
 1. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 2. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 3. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
assume mini: "distinct_indices_ns (set cs)"
[PROOF STATE]
proof (state)
this:
distinct_indices_ns (set cs)

goal (3 subgoals):
 1. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 2. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 3. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
have mini: "distinct_indices_ns (set ncs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_indices_ns (set ncs)
[PROOF STEP]
unfolding distinct_indices_ns_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n1 n2 i. (i, n1) \<in> set ncs \<longrightarrow> (i, n2) \<in> set ncs \<longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
proof (intro impI allI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n1 n2 i. \<lbrakk>(i, n1) \<in> set ncs; (i, n2) \<in> set ncs\<rbrakk> \<Longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
case (1 n1 n2 i)
[PROOF STATE]
proof (state)
this:
(i, n1) \<in> set ncs
(i, n2) \<in> set ncs

goal (1 subgoal):
 1. \<And>n1 n2 i. \<lbrakk>(i, n1) \<in> set ncs; (i, n2) \<in> set ncs\<rbrakk> \<Longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
(i, n1) \<in> set ncs
[PROOF STEP]
obtain c1 where c1: "(i,c1) \<in> set cs" and n1: "n1 = normalize_ns_constraint c1"
[PROOF STATE]
proof (prove)
using this:
(i, n1) \<in> set ncs

goal (1 subgoal):
 1. (\<And>c1. \<lbrakk>(i, c1) \<in> set cs; n1 = normalize_ns_constraint c1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ncs_def
[PROOF STATE]
proof (prove)
using this:
(i, n1) \<in> set (map (map_prod id normalize_ns_constraint) cs)

goal (1 subgoal):
 1. (\<And>c1. \<lbrakk>(i, c1) \<in> set cs; n1 = normalize_ns_constraint c1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, c1) \<in> set cs
n1 = normalize_ns_constraint c1

goal (1 subgoal):
 1. \<And>n1 n2 i. \<lbrakk>(i, n1) \<in> set ncs; (i, n2) \<in> set ncs\<rbrakk> \<Longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
from 1(2)
[PROOF STATE]
proof (chain)
picking this:
(i, n2) \<in> set ncs
[PROOF STEP]
obtain c2 where c2: "(i,c2) \<in> set cs" and n2: "n2 = normalize_ns_constraint c2"
[PROOF STATE]
proof (prove)
using this:
(i, n2) \<in> set ncs

goal (1 subgoal):
 1. (\<And>c2. \<lbrakk>(i, c2) \<in> set cs; n2 = normalize_ns_constraint c2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ncs_def
[PROOF STATE]
proof (prove)
using this:
(i, n2) \<in> set (map (map_prod id normalize_ns_constraint) cs)

goal (1 subgoal):
 1. (\<And>c2. \<lbrakk>(i, c2) \<in> set cs; n2 = normalize_ns_constraint c2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, c2) \<in> set cs
n2 = normalize_ns_constraint c2

goal (1 subgoal):
 1. \<And>n1 n2 i. \<lbrakk>(i, n1) \<in> set ncs; (i, n2) \<in> set ncs\<rbrakk> \<Longrightarrow> poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
from mini[unfolded distinct_indices_ns_def, rule_format, OF c1 c2]
[PROOF STATE]
proof (chain)
picking this:
poly c1 = poly c2 \<and> ns_constraint_const c1 = ns_constraint_const c2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
poly c1 = poly c2 \<and> ns_constraint_const c1 = ns_constraint_const c2

goal (1 subgoal):
 1. poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2
[PROOF STEP]
unfolding n1 n2
[PROOF STATE]
proof (prove)
using this:
poly c1 = poly c2 \<and> ns_constraint_const c1 = ns_constraint_const c2

goal (1 subgoal):
 1. poly (normalize_ns_constraint c1) = poly (normalize_ns_constraint c2) \<and> ns_constraint_const (normalize_ns_constraint c1) = ns_constraint_const (normalize_ns_constraint c2)
[PROOF STEP]
by (cases c1; cases c2; auto simp: normalize_ns_constraint.simps Let_def)
[PROOF STATE]
proof (state)
this:
poly n1 = poly n2 \<and> ns_constraint_const n1 = ns_constraint_const n2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct_indices_ns (set ncs)

goal (3 subgoals):
 1. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 2. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 3. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
note min = min1[THEN conjunct1, rule_format, OF this]
[PROOF STATE]
proof (state)
this:
(?k, ?a) \<in> set as \<Longrightarrow> \<exists>v p. ?a = qdelta_constraint_to_atom p v \<and> (?k, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)

goal (3 subgoals):
 1. distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)
 2. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 3. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
show "distinct_indices_atoms (set as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_indices_atoms (set as)
[PROOF STEP]
unfolding distinct_indices_atoms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i a b. (i, a) \<in> set as \<longrightarrow> (i, b) \<in> set as \<longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
fix i a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
assume a: "(i,a) \<in> set as" and b: "(i,b) \<in> set as"
[PROOF STATE]
proof (state)
this:
(i, a) \<in> set as
(i, b) \<in> set as

goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
from min[OF a]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (i, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)
[PROOF STEP]
obtain v p where aa: "a = qdelta_constraint_to_atom p v" "(i, p) \<in> set ncs"
        "\<not> is_monom (poly p) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v"
[PROOF STATE]
proof (prove)
using this:
\<exists>v p. a = qdelta_constraint_to_atom p v \<and> (i, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)

goal (1 subgoal):
 1. (\<And>p v. \<lbrakk>a = qdelta_constraint_to_atom p v; (i, p) \<in> set ncs; \<not> is_monom (poly p) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = qdelta_constraint_to_atom p v
(i, p) \<in> set ncs
\<not> is_monom (poly p) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v

goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
from min[OF b]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v p. b = qdelta_constraint_to_atom p v \<and> (i, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)
[PROOF STEP]
obtain w q where bb: "b = qdelta_constraint_to_atom q w" "(i, q) \<in> set ncs"
        "\<not> is_monom (poly q) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly q) = Some w"
[PROOF STATE]
proof (prove)
using this:
\<exists>v p. b = qdelta_constraint_to_atom p v \<and> (i, p) \<in> set ncs \<and> (\<not> is_monom (poly p) \<longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v)

goal (1 subgoal):
 1. (\<And>q w. \<lbrakk>b = qdelta_constraint_to_atom q w; (i, q) \<in> set ncs; \<not> is_monom (poly q) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly q) = Some w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b = qdelta_constraint_to_atom q w
(i, q) \<in> set ncs
\<not> is_monom (poly q) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly q) = Some w

goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
from mini[unfolded distinct_indices_ns_def, rule_format, OF aa(2) bb(2)]
[PROOF STATE]
proof (chain)
picking this:
poly p = poly q \<and> ns_constraint_const p = ns_constraint_const q
[PROOF STEP]
have *: "poly p = poly q" "ns_constraint_const p = ns_constraint_const q"
[PROOF STATE]
proof (prove)
using this:
poly p = poly q \<and> ns_constraint_const p = ns_constraint_const q

goal (1 subgoal):
 1. poly p = poly q &&& ns_constraint_const p = ns_constraint_const q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly p = poly q
ns_constraint_const p = ns_constraint_const q

goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>(i, a) \<in> set as; (i, b) \<in> set as\<rbrakk> \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
show "atom_var a = atom_var b \<and> atom_const a = atom_const b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
proof (cases "is_monom (poly q)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
 2. \<not> is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_monom (poly q)

goal (2 subgoals):
 1. is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
 2. \<not> is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_monom (poly q)

goal (1 subgoal):
 1. atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
unfolding aa(1) bb(1)
[PROOF STATE]
proof (prove)
using this:
is_monom (poly q)

goal (1 subgoal):
 1. atom_var (qdelta_constraint_to_atom p v) = atom_var (qdelta_constraint_to_atom q w) \<and> atom_const (qdelta_constraint_to_atom p v) = atom_const (qdelta_constraint_to_atom q w)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
is_monom (poly q)
poly p = poly q
ns_constraint_const p = ns_constraint_const q

goal (1 subgoal):
 1. atom_var (qdelta_constraint_to_atom p v) = atom_var (qdelta_constraint_to_atom q w) \<and> atom_const (qdelta_constraint_to_atom p v) = atom_const (qdelta_constraint_to_atom q w)
[PROOF STEP]
by (cases p; cases q, auto)
[PROOF STATE]
proof (state)
this:
atom_var a = atom_var b \<and> atom_const a = atom_const b

goal (1 subgoal):
 1. \<not> is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_monom (poly q)

goal (1 subgoal):
 1. \<not> is_monom (poly q) \<Longrightarrow> atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_monom (poly q)

goal (1 subgoal):
 1. atom_var a = atom_var b \<and> atom_const a = atom_const b
[PROOF STEP]
unfolding aa(1) bb(1)
[PROOF STATE]
proof (prove)
using this:
\<not> is_monom (poly q)

goal (1 subgoal):
 1. atom_var (qdelta_constraint_to_atom p v) = atom_var (qdelta_constraint_to_atom q w) \<and> atom_const (qdelta_constraint_to_atom p v) = atom_const (qdelta_constraint_to_atom q w)
[PROOF STEP]
using * aa(3) bb(3)
[PROOF STATE]
proof (prove)
using this:
\<not> is_monom (poly q)
poly p = poly q
ns_constraint_const p = ns_constraint_const q
\<not> is_monom (poly p) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly p) = Some v
\<not> is_monom (poly q) \<Longrightarrow> Poly_Mapping (preprocess' ncs var) (poly q) = Some w

goal (1 subgoal):
 1. atom_var (qdelta_constraint_to_atom p v) = atom_var (qdelta_constraint_to_atom q w) \<and> atom_const (qdelta_constraint_to_atom p v) = atom_const (qdelta_constraint_to_atom q w)
[PROOF STEP]
by (cases p; cases q, auto)
[PROOF STATE]
proof (state)
this:
atom_var a = atom_var b \<and> atom_const a = atom_const b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom_var a = atom_var b \<and> atom_const a = atom_const b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct_indices_atoms (set as)

goal (2 subgoals):
 1. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 2. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
distinct_indices_ns (set cs) \<Longrightarrow> distinct_indices_atoms (set as)

goal (2 subgoals):
 1. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
 2. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
show "i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
using preprocess'_unsat_indices[of i ncs] part1
[PROOF STATE]
proof (prove)
using this:
i \<in> set (UnsatIndices (preprocess' ncs ?start)) \<Longrightarrow> \<not> ({i}, ?v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
preprocess_part_1 ncs = (t1, as, ui)

goal (1 subgoal):
 1. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
unfolding preprocess_part_1_def Let_def
[PROOF STATE]
proof (prove)
using this:
i \<in> set (UnsatIndices (preprocess' ncs ?start)) \<Longrightarrow> \<not> ({i}, ?v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
(Tableau (preprocess' ncs (start_fresh_variable ncs)), Atoms (preprocess' ncs (start_fresh_variable ncs)), UnsatIndices (preprocess' ncs (start_fresh_variable ncs))) = (t1, as, ui)

goal (1 subgoal):
 1. i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
by (auto simp: ncs)
[PROOF STATE]
proof (state)
this:
i \<in> set ui \<Longrightarrow> \<nexists>v. ({i}, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
assume "\<exists> w. (I,w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set cs"
[PROOF STATE]
proof (state)
this:
\<exists>w. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>w. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
obtain w where "(I,w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set cs"
[PROOF STATE]
proof (prove)
using this:
\<exists>w. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. (\<And>w. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
hence "(I,w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s set ncs"
[PROOF STATE]
proof (prove)
using this:
(I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs
[PROOF STEP]
unfolding ncs
[PROOF STATE]
proof (prove)
using this:
(I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs

goal (1 subgoal):
 1. (I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(I, w) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set ncs

goal (1 subgoal):
 1. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
from preprocess'_unsat[OF this _  start_fresh_variable_fresh, of ncs]
[PROOF STATE]
proof (chain)
picking this:
vars_constraints (map snd ncs) \<subseteq> vars_constraints (map snd ncs) \<Longrightarrow> \<exists>v'. (\<forall>var\<in>vars_constraints (map snd ncs). w var = v' var) \<and> v' \<Turnstile>\<^sub>a\<^sub>s (snd ` (set (Atoms (preprocess' ncs (start_fresh_variable ncs))) \<inter> I \<times> UNIV)) \<and> v' \<Turnstile>\<^sub>t Tableau (preprocess' ncs (start_fresh_variable ncs))
[PROOF STEP]
have "\<exists>v'. (I,v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1"
[PROOF STATE]
proof (prove)
using this:
vars_constraints (map snd ncs) \<subseteq> vars_constraints (map snd ncs) \<Longrightarrow> \<exists>v'. (\<forall>var\<in>vars_constraints (map snd ncs). w var = v' var) \<and> v' \<Turnstile>\<^sub>a\<^sub>s (snd ` (set (Atoms (preprocess' ncs (start_fresh_variable ncs))) \<inter> I \<times> UNIV)) \<and> v' \<Turnstile>\<^sub>t Tableau (preprocess' ncs (start_fresh_variable ncs))

goal (1 subgoal):
 1. \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1
[PROOF STEP]
using part1
[PROOF STATE]
proof (prove)
using this:
vars_constraints (map snd ncs) \<subseteq> vars_constraints (map snd ncs) \<Longrightarrow> \<exists>v'. (\<forall>var\<in>vars_constraints (map snd ncs). w var = v' var) \<and> v' \<Turnstile>\<^sub>a\<^sub>s (snd ` (set (Atoms (preprocess' ncs (start_fresh_variable ncs))) \<inter> I \<times> UNIV)) \<and> v' \<Turnstile>\<^sub>t Tableau (preprocess' ncs (start_fresh_variable ncs))
preprocess_part_1 ncs = (t1, as, ui)

goal (1 subgoal):
 1. \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1
[PROOF STEP]
unfolding preprocess_part_1_def Let_def
[PROOF STATE]
proof (prove)
using this:
vars_constraints (map snd ncs) \<subseteq> vars_constraints (map snd ncs) \<Longrightarrow> \<exists>v'. (\<forall>var\<in>vars_constraints (map snd ncs). w var = v' var) \<and> v' \<Turnstile>\<^sub>a\<^sub>s (snd ` (set (Atoms (preprocess' ncs (start_fresh_variable ncs))) \<inter> I \<times> UNIV)) \<and> v' \<Turnstile>\<^sub>t Tableau (preprocess' ncs (start_fresh_variable ncs))
(Tableau (preprocess' ncs (start_fresh_variable ncs)), Atoms (preprocess' ncs (start_fresh_variable ncs)), UnsatIndices (preprocess' ncs (start_fresh_variable ncs))) = (t1, as, ui)

goal (1 subgoal):
 1. \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1

goal (1 subgoal):
 1. \<exists>v. (I, v) \<Turnstile>\<^sub>i\<^sub>n\<^sub>s\<^sub>s  set cs \<Longrightarrow> \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1
[PROOF STEP]
show "\<exists>v'. (I,v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t"
[PROOF STATE]
proof (prove)
using this:
\<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1

goal (1 subgoal):
 1. \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
using part_2(4)
[PROOF STATE]
proof (prove)
using this:
\<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t1
?v \<Turnstile>\<^sub>t t1 \<Longrightarrow> ?v \<Turnstile>\<^sub>t t

goal (1 subgoal):
 1. \<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v'. (I, v') \<Turnstile>\<^sub>i\<^sub>a\<^sub>s set as \<and> v' \<Turnstile>\<^sub>t t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coclop_dual_var:
  fixes f :: "'a::order_with_dual \<Rightarrow> 'a"
  shows "coclop f = clop (\<partial>\<^sub>F f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coclop f = clop (\<partial>\<^sub>F f)
[PROOF STEP]
by (simp add: coclop_dual)


[STATEMENT]
lemma coclop_coclosure_prop: "(coclop::('a::complete_lattice \<Rightarrow> 'a) \<Rightarrow> bool) (Sup \<circ> \<down>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coclop (Sup \<circ> \<down>)
[PROOF STEP]
by (simp add: coclop_def mono_def)


[STATEMENT]
lemma transpose_scalar: "transpose (k *k A) = k *k transpose A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose (k *k A) = k *k Finite_Cartesian_Product.transpose A
[PROOF STEP]
unfolding transpose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. (k *k A) $ j $ i) = k *k (\<chi>i j. A $ j $ i)
[PROOF STEP]
by (vector, simp add: matrix_scalar_mult_def)


[STATEMENT]
lemma sdescending_stuck:
    fixes w :: "'a :: wellorder stream"
    assumes "sdescending w"
    obtains k
    where "sdrop k w = sconst (w !! k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. sdrop k w = sconst (w !! k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sdescending w

goal (1 subgoal):
 1. (\<And>k. sdrop k w = sconst (w !! k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induct "w !! 0" arbitrary: w thesis rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w thesis. \<lbrakk>\<And>wa thesis. \<lbrakk>wa !! 0 < w !! 0; \<And>k. sdrop k wa = sconst (wa !! k) \<Longrightarrow> thesis; sdescending wa\<rbrakk> \<Longrightarrow> thesis; \<And>k. sdrop k w = sconst (w !! k) \<Longrightarrow> thesis; sdescending w\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w !! 0 < w !! 0; \<And>k. sdrop k ?w = sconst (?w !! k) \<Longrightarrow> ?thesis; sdescending ?w\<rbrakk> \<Longrightarrow> ?thesis
sdrop ?k w = sconst (w !! ?k) \<Longrightarrow> thesis
sdescending w

goal (1 subgoal):
 1. \<And>w thesis. \<lbrakk>\<And>wa thesis. \<lbrakk>wa !! 0 < w !! 0; \<And>k. sdrop k wa = sconst (wa !! k) \<Longrightarrow> thesis; sdescending wa\<rbrakk> \<Longrightarrow> thesis; \<And>k. sdrop k w = sconst (w !! k) \<Longrightarrow> thesis; sdescending w\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases "w = sconst (w !! 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w = sconst (w !! 0) \<Longrightarrow> thesis
 2. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w = sconst (w !! 0)

goal (2 subgoals):
 1. w = sconst (w !! 0) \<Longrightarrow> thesis
 2. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less(2)[of 0] True
[PROOF STATE]
proof (prove)
using this:
sdrop 0 w = sconst (w !! 0) \<Longrightarrow> thesis
w = sconst (w !! 0)

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

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
w \<noteq> sconst (w !! 0)

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
obtain k where 1: "w !! k \<noteq> w !! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. w !! k \<noteq> w !! 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
w \<noteq> sconst (w !! 0)

goal (1 subgoal):
 1. (\<And>k. w !! k \<noteq> w !! 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis empty_iff eqI_snth insert_iff snth_sset sset_sconst)
[PROOF STATE]
proof (state)
this:
w !! k \<noteq> w !! 0

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
have 2: "antimono (snth w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antimono ((!!) w)
[PROOF STEP]
using sdescending_snth_antimono less(3)
[PROOF STATE]
proof (prove)
using this:
sdescending ?w \<Longrightarrow> antimono ((!!) ?w)
sdescending w

goal (1 subgoal):
 1. antimono ((!!) w)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
antimono ((!!) w)

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
have 3: "w !! k \<le> w !! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w !! k \<le> w !! 0
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
w !! k \<noteq> w !! 0
antimono ((!!) w)

goal (1 subgoal):
 1. w !! k \<le> w !! 0
[PROOF STEP]
by (blast dest: antimonoD)
[PROOF STATE]
proof (state)
this:
w !! k \<le> w !! 0

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
have 4: "sdrop k w !! 0 < w !! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop k w !! 0 < w !! 0
[PROOF STEP]
using 1 3
[PROOF STATE]
proof (prove)
using this:
w !! k \<noteq> w !! 0
w !! k \<le> w !! 0

goal (1 subgoal):
 1. sdrop k w !! 0 < w !! 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sdrop k w !! 0 < w !! 0

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
have 5: "sdescending (sdrop k w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdescending (sdrop k w)
[PROOF STEP]
using sdescending_sdrop less(3)
[PROOF STATE]
proof (prove)
using this:
sdescending ?w \<Longrightarrow> sdescending (sdrop ?k ?w)
sdescending w

goal (1 subgoal):
 1. sdescending (sdrop k w)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
sdescending (sdrop k w)

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
obtain l where 5: "sdrop l (sdrop k w) = sconst (sdrop k w !! l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. sdrop l (sdrop k w) = sconst (sdrop k w !! l) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less(1)[OF 4 _ 5]
[PROOF STATE]
proof (prove)
using this:
(\<And>ka. sdrop ka (sdrop k w) = sconst (sdrop k w !! ka) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l. sdrop l (sdrop k w) = sconst (sdrop k w !! l) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
sdrop l (sdrop k w) = sconst (sdrop k w !! l)

goal (1 subgoal):
 1. w \<noteq> sconst (w !! 0) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less(2) 5
[PROOF STATE]
proof (prove)
using this:
sdrop ?k w = sconst (w !! ?k) \<Longrightarrow> thesis
sdrop l (sdrop k w) = sconst (sdrop k w !! l)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed