# HG changeset patch
# User blanchet
# Date 1402527649 -7200
# Node ID 8cecd655eef4fd0554c35d9b7fd6feb3b28fa5a9
# Parent  dca8d06ecbbaa6096ab5041126dc7777f11114b8
adapted examples to changes in SMT triggers

diff -r dca8d06ecbba -r 8cecd655eef4 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -357,7 +357,9 @@
 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt2
 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt2
 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt2
-lemma "\<forall>x::int. SMT2.trigger [[SMT2.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt2
+lemma "\<forall>x::int.
+  SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat x) SMT2.Symb_Nil) SMT2.Symb_Nil)
+    (x < a \<longrightarrow> 2 * x < 2 * a)" by smt2
 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt2
 
 
diff -r dca8d06ecbba -r 8cecd655eef4 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -18,28 +18,28 @@
 
 lemma
   "True"
-  "\<not>False"
-  "\<not>\<not>True"
+  "\<not> False"
+  "\<not> \<not> True"
   "True \<and> True"
   "True \<or> False"
   "False \<longrightarrow> True"
-  "\<not>(False \<longleftrightarrow> True)"
+  "\<not> (False \<longleftrightarrow> True)"
   by smt2+
 
 lemma
-  "P \<or> \<not>P"
-  "\<not>(P \<and> \<not>P)"
-  "(True \<and> P) \<or> \<not>P \<or> (False \<and> P) \<or> P"
+  "P \<or> \<not> P"
+  "\<not> (P \<and> \<not> P)"
+  "(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P"
   "P \<longrightarrow> P"
   "P \<and> \<not> P \<longrightarrow> False"
   "P \<and> Q \<longrightarrow> Q \<and> P"
   "P \<or> Q \<longrightarrow> Q \<or> P"
   "P \<and> Q \<longrightarrow> P \<or> Q"
-  "\<not>(P \<or> Q) \<longrightarrow> \<not>P"
-  "\<not>(P \<or> Q) \<longrightarrow> \<not>Q"
-  "\<not>P \<longrightarrow> \<not>(P \<and> Q)"
-  "\<not>Q \<longrightarrow> \<not>(P \<and> Q)"
-  "(P \<and> Q) \<longleftrightarrow> (\<not>(\<not>P \<or> \<not>Q))"
+  "\<not> (P \<or> Q) \<longrightarrow> \<not> P"
+  "\<not> (P \<or> Q) \<longrightarrow> \<not> Q"
+  "\<not> P \<longrightarrow> \<not> (P \<and> Q)"
+  "\<not> Q \<longrightarrow> \<not> (P \<and> Q)"
+  "(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))"
   "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
   "(P \<and> Q) \<or> R  \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
@@ -50,23 +50,23 @@
   "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
   "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow>  ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
-  "\<not>(P \<longrightarrow> R) \<longrightarrow>  \<not>(Q \<longrightarrow> R) \<longrightarrow> \<not>(P \<and> Q \<longrightarrow> R)"
+  "\<not> (P \<longrightarrow> R) \<longrightarrow>  \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
   "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   "P \<longrightarrow> (Q \<longrightarrow> P)"
   "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)"
   "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
-  "(P \<longrightarrow> Q) \<longrightarrow> (\<not>Q \<longrightarrow> \<not>P)"
+  "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
   "(P \<longrightarrow> Q) \<and> (Q  \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)"
   "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
-  "\<not>(P \<longleftrightarrow> \<not>P)"
-  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not>Q \<longrightarrow> \<not>P)"
+  "\<not> (P \<longleftrightarrow> \<not> P)"
+  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"
   by smt2+
 
 lemma
-  "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not>P \<longrightarrow> Q2))"
+  "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))"
   "if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)"
   "(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)"
   "(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)"
@@ -75,9 +75,9 @@
   by smt2+
 
 lemma
-  "case P of True \<Rightarrow> P | False \<Rightarrow> \<not>P"
-  "case P of False \<Rightarrow> \<not>P | True \<Rightarrow> P"
-  "case \<not>P of True \<Rightarrow> \<not>P | False \<Rightarrow> P"
+  "case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P"
+  "case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P"
+  "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P"
   "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
   by smt2+
 
@@ -104,7 +104,7 @@
   "(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x"
   "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))"
   "(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a"
-  "(\<forall>s. q s \<longrightarrow> r s) \<and> \<not>r s \<and> (\<forall>s. \<not>r s \<and> \<not>q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t"
+  "(\<forall>s. q s \<longrightarrow> r s) \<and> \<not> r s \<and> (\<forall>s. \<not> r s \<and> \<not> q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t"
   by smt2+
 
 lemma
@@ -117,7 +117,7 @@
   "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
   "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)"
   "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)"
-  "\<not>((\<exists>x. \<not>P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not>(\<exists>x. P x))"
+  "\<not> ((\<exists>x. \<not> P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not> (\<exists>x. P x))"
   by smt2+
 
 lemma
@@ -130,16 +130,16 @@
   by smt2+
 
 lemma
-  "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
+  "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
-  "(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y"
+  "(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y"
   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   by smt2+
 
 lemma
   "\<forall>x. \<exists>y. f x y = f x (g x)"
-  "(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))"
+  "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
@@ -150,7 +150,7 @@
 
 lemma
   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
-  "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))"
+  "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))"
   "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   "(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)"
   "(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R"
@@ -158,18 +158,18 @@
 
 lemma
   "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
-  "(\<exists>x\<in>M. P x) \<or> \<not>(P c \<and> c \<in> M)"
+  "(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)"
   by smt2+
 
 lemma
   "let P = True in P"
-  "let P = P1 \<or> P2 in P \<or> \<not>P"
+  "let P = P1 \<or> P2 in P \<or> \<not> P"
   "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"
   "(let x = y in x) = y"
   "(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)"
   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)"
   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)"
-  "let P = (\<forall>x. Q x) in if P then P else \<not>P"
+  "let P = (\<forall>x. Q x) in if P then P else \<not> P"
   by smt2+
 
 lemma
@@ -185,35 +185,19 @@
 section {* Guidance for quantifier heuristics: patterns *}
 
 lemma
-  assumes "\<forall>x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)"
+  assumes "\<forall>x.
+    SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x)) SMT2.Symb_Nil) SMT2.Symb_Nil)
+    (f x = x)"
   shows "f 1 = 1"
   using assms using [[smt2_trace]] by smt2
 
 lemma
-  assumes "\<forall>x y. SMT2.trigger [[SMT2.pat (f x), SMT2.pat (g y)]] (f x = g y)"
+  assumes "\<forall>x y.
+    SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x))
+      (SMT2.Symb_Cons (SMT2.pat (g y)) SMT2.Symb_Nil)) SMT2.Symb_Nil) (f x = g y)"
   shows "f a = g b"
   using assms by smt2
 
-lemma
-  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (P x --> Q x)"
-  and "P t"
-  shows "Q t"
-  using assms by smt2
-
-lemma
-  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x), SMT2.pat (Q x)]]
-    (P x & Q x --> R x)"
-  and "P t" and "Q t"
-  shows "R t"
-  using assms by smt2
-
-lemma
-  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)], [SMT2.pat (Q x)]]
-    ((P x --> R x) & (Q x --> R x))"
-  and "P t | Q t"
-  shows "R t"
-  using assms by smt2
-
 
 section {* Meta-logical connectives *}
 
@@ -224,9 +208,9 @@
   "P' x \<Longrightarrow> P' x"
   "P \<Longrightarrow> P \<or> Q"
   "Q \<Longrightarrow> P \<or> Q"
-  "\<not>P \<Longrightarrow> P \<longrightarrow> Q"
+  "\<not> P \<Longrightarrow> P \<longrightarrow> Q"
   "Q \<Longrightarrow> P \<longrightarrow> Q"
-  "\<lbrakk>P; \<not>Q\<rbrakk> \<Longrightarrow> \<not>(P \<longrightarrow> Q)"
+  "\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)"
   "P' x \<equiv> P' x"
   "P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x"
   "P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x"
@@ -234,7 +218,7 @@
   "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
-  "(p \<or> q) \<and> \<not>p \<Longrightarrow> q"
+  "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   by smt2+
 
@@ -343,12 +327,12 @@
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
   "(x < y) = (x + 1 \<le> y)"
-  "\<not>(x < x)"
+  "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
-  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
+  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt2+
 
 
@@ -358,7 +342,7 @@
   "(0::int) = 0"
   "(0::int) = (- 0)"
   "(1::int) = 1"
-  "\<not>(-1 = (1::int))"
+  "\<not> (-1 = (1::int))"
   "(0::int) < 1"
   "(0::int) \<le> 1"
   "-123 + 345 < (567::int)"
@@ -498,12 +482,12 @@
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
   "(x < y) = (x + 1 \<le> y)"
-  "\<not>(x < x)"
+  "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
-  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
+  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt2+
 
 
@@ -514,7 +498,7 @@
   "(0::real) = -0"
   "(0::real) = (- 0)"
   "(1::real) = 1"
-  "\<not>(-1 = (1::real))"
+  "\<not> (-1 = (1::real))"
   "(0::real) < 1"
   "(0::real) \<le> 1"
   "-123 + 345 < (567::real)"
@@ -608,12 +592,12 @@
   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
-  "\<not>(x < x)"
+  "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
-  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
+  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt2+
 
 
diff -r dca8d06ecbba -r 8cecd655eef4 src/HOL/SMT_Examples/VCC_Max.certs2
--- a/src/HOL/SMT_Examples/VCC_Max.certs2	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT_Examples/VCC_Max.certs2	Thu Jun 12 01:00:49 2014 +0200
@@ -1,4 +1,4 @@
-57921b560a136ca1a710a5f3b5e4e77c40b33980 2972 0
+05a761f33f246f0fee720bec6f015ca5aba01c4d 2972 0
 unsat
 ((set-logic <null>)
 (declare-fun ?v0!14 () Int)
@@ -114,10 +114,10 @@
 (let (($x19992 (or $x15590 $x15599 $x19474 $x19501 $x19989)))
 (let (($x19995 (not $x19992)))
 (let ((?x23404 (b_S_ref$ ?x10320)))
-(let ((?x23225 (b_S_ptr$ b_T_T_u1$ ?x23404)))
-(let ((?x24099 (b_S_typ$ ?x23225)))
-(let ((?x24100 (b_S_kind_n_of$ ?x24099)))
-(let (($x23805 (= ?x24100 b_S_kind_n_primitive$)))
+(let ((?x23228 (b_S_ptr$ b_T_T_u1$ ?x23404)))
+(let ((?x23728 (b_S_typ$ ?x23228)))
+(let ((?x23730 (b_S_kind_n_of$ ?x23728)))
+(let (($x24098 (= ?x23730 b_S_kind_n_primitive$)))
 (let ((?x21472 (b_S_kind_n_of$ b_T_T_u1$)))
 (let (($x21473 (= ?x21472 b_S_kind_n_primitive$)))
 (let (($x9768 (b_S_is_n_primitive$ b_T_T_u1$)))
@@ -221,7 +221,7 @@
 (let ((@x24344 (unit-resolution (unit-resolution @x24337 (unit-resolution @x23870 @x19833 $x23270) $x23889) @x24343 false)))
 (let ((@x24345 (lemma @x24344 $x10321)))
 (let ((@x25031 (unit-resolution (def-axiom (or (not $x23270) $x15590 $x23242)) @x24345 (or (not $x23270) $x23242))))
-(let (($x23227 (= ?x10320 ?x23225)))
+(let (($x23306 (= ?x10320 ?x23228)))
 (let (($x9607 (forall ((?v0 B_S_ptr$) (?v1 B_S_ctype$) )(!(or (not (b_S_is$ ?v0 ?v1)) (= ?v0 (b_S_ptr$ ?v1 (b_S_ref$ ?v0)))) :pattern ( (b_S_is$ ?v0 ?v1) )))
 ))
 (let (($x9604 (or (not $x9596) (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1))))))
@@ -231,24 +231,24 @@
 (let ((@x9606 (rewrite (= (=> $x9596 (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1)))) $x9604))))
 (let ((@x15336 (mp~ (mp (asserted $x9601) (quant-intro @x9606 (= $x9601 $x9607)) $x9607) (nnf-pos (refl (~ $x9604 $x9604)) (~ $x9607 $x9607)) $x9607)))
 (let (($x21994 (not $x9607)))
-(let (($x24289 (or $x21994 $x15590 $x23227)))
-(let ((@x24294 (mp ((_ quant-inst (b_S_idx$ ?x10078 v_b_L_H_p_G_0$ b_T_T_u1$) b_T_T_u1$) (or $x21994 (or $x15590 $x23227))) (rewrite (= (or $x21994 (or $x15590 $x23227)) $x24289)) $x24289)))
-(let ((@x25262 (symm (unit-resolution @x24294 @x15336 @x24345 $x23227) (= ?x23225 ?x10320))))
-(let ((@x24694 (trans (monotonicity @x25262 (= ?x24099 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x24099 b_T_T_u1$))))
-(let ((@x24696 (trans (monotonicity @x24694 (= ?x24100 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x23805)))
+(let (($x24294 (or $x21994 $x15590 $x23306)))
+(let ((@x24335 (mp ((_ quant-inst (b_S_idx$ ?x10078 v_b_L_H_p_G_0$ b_T_T_u1$) b_T_T_u1$) (or $x21994 (or $x15590 $x23306))) (rewrite (= (or $x21994 (or $x15590 $x23306)) $x24294)) $x24294)))
+(let ((@x25262 (symm (unit-resolution @x24335 @x15336 @x24345 $x23306) (= ?x23228 ?x10320))))
+(let ((@x24694 (trans (monotonicity @x25262 (= ?x23728 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x23728 b_T_T_u1$))))
+(let ((@x24696 (trans (monotonicity @x24694 (= ?x23730 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x24098)))
 (let ((?x10272 (b_S_typemap$ v_b_S_s$)))
-(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23225)))
+(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23228)))
 (let ((?x24218 (b_S_ts_n_emb$ ?x24217)))
-(let (($x23797 (b_S_closed$ v_b_S_s$ ?x24218)))
-(let (($x23803 (not $x23797)))
-(let (($x23775 (b_S_ts_n_is_n_volatile$ ?x24217)))
+(let (($x23775 (b_S_closed$ v_b_S_s$ ?x24218)))
 (let (($x23784 (not $x23775)))
-(let (($x23804 (or $x23784 $x23803)))
-(let ((@x24686 (monotonicity (monotonicity @x25262 (= ?x24217 (b_S_select_o_tm$ ?x10272 ?x10320))) (= $x23775 (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))))))
-(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23775))))
-(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23784))))
-(let ((?x23101 (b_S_select_o_tm$ ?x10272 ?x10320)))
-(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23101)))
+(let (($x23805 (b_S_ts_n_is_n_volatile$ ?x24217)))
+(let (($x23770 (not $x23805)))
+(let (($x23797 (or $x23770 $x23784)))
+(let ((@x24686 (monotonicity (monotonicity @x25262 (= ?x24217 (b_S_select_o_tm$ ?x10272 ?x10320))) (= $x23805 (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))))))
+(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23805))))
+(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23770))))
+(let ((?x23124 (b_S_select_o_tm$ ?x10272 ?x10320)))
+(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23124)))
 (let (($x23297 (not $x23361)))
 (let (($x23362 (or $x15593 $x23361)))
 (let (($x23363 (not $x23362)))
@@ -399,7 +399,7 @@
 (let (($x19313 (or $x19297 $x19298 $x15525 $x15533)))
 (let (($x20589 (not $x15533)))
 (let (($x19318 (not $x19313)))
-(let ((@x24016 (hypothesis $x19318)))
+(let ((@x23991 (hypothesis $x19318)))
 (let (($x10141 (b_S_thread_n_local$ v_b_S_s$ ?x10137)))
 (let ((?x21175 (b_S_typ$ ?x10078)))
 (let ((?x22803 (b_S_kind_n_of$ ?x21175)))
@@ -439,7 +439,7 @@
 (let ((@x22576 (trans (monotonicity @x22567 (= (or $x22568 $x22543) $x22569)) (rewrite (= $x22569 $x22569)) (= (or $x22568 $x22543) $x22569))))
 (let ((@x22577 (mp ((_ quant-inst (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) 0 b_T_T_u1$) (or $x22568 $x22543)) @x22576 $x22569)))
 (let ((@x22581 (def-axiom (or $x22562 $x22556))))
-(let ((@x24124 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556)))
+(let ((@x24189 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556)))
 (let (($x21179 (= ?x10079 v_b_P_H_arr$)))
 (let (($x19835 (forall ((?v0 B_S_ctype$) (?v1 Int) )(!(= (b_S_ref$ (b_S_ptr$ ?v0 ?v1)) ?v1) :pattern ( (b_S_ptr$ ?v0 ?v1) )))
 ))
@@ -453,12 +453,12 @@
 (let ((@x21185 ((_ quant-inst b_T_T_u1$ v_b_P_H_arr$) $x21184)))
 (let ((@x24511 (unit-resolution @x21185 @x19840 $x21179)))
 (let ((@x22852 (monotonicity @x24511 (= ?x22553 ?x10078))))
-(let ((@x24070 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079))))
-(let ((@x22338 (symm (monotonicity (trans @x24070 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505))))
+(let ((@x24073 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079))))
+(let ((@x22338 (symm (monotonicity (trans @x24073 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505))))
 (let ((@x22340 (unit-resolution (hypothesis (not $x22506)) (trans (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) @x22338 $x22506) false)))
-(let ((@x23350 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24124 $x22506)))
-(let ((@x23663 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x10078 ?x10137))))
-(let ((@x22940 (trans (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23350 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478))))
+(let ((@x23667 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24189 $x22506)))
+(let ((@x23699 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x10078 ?x10137))))
+(let ((@x22940 (trans (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23667 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478))))
 (let ((@x23082 (symm (monotonicity @x22940 (= $x22902 (b_S_ts_n_is_n_volatile$ ?x22478))) (= (b_S_ts_n_is_n_volatile$ ?x22478) $x22902))))
 (let (($x22602 (b_S_ts_n_is_n_volatile$ ?x22478)))
 (let (($x22641 (not $x22602)))
@@ -1364,7 +1364,7 @@
 (let ((@x22613 ((_ quant-inst v_b_S_s$ (b_S_ptr$ ?x10076 ?x21014) (b_S_ptr$ ?x10076 ?x21014) b_l_H_public$) $x22612)))
 (let (($x35 (= b_S_kind_n_primitive$ b_S_kind_n_array$)))
 (let (($x36 (not $x35)))
-(let (($x22500 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$)))))
+(let (($x22488 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$)))))
 (let ((?x22234 (b_S_typ$ ?x21983)))
 (let ((?x22387 (b_S_kind_n_of$ ?x22234)))
 (let (($x22388 (= ?x22387 b_S_kind_n_primitive$)))
@@ -1404,7 +1404,7 @@
 (let ((@x22414 (trans (monotonicity @x24520 (= ?x22234 ?x21180)) (unit-resolution @x21189 @x19846 $x21183) (= ?x22234 ?x10076))))
 (let ((@x22418 (trans (monotonicity @x22414 (= ?x22387 ?x10086)) (unit-resolution @x22406 (unit-resolution @x22160 @x15446 $x22149) $x22148) (= ?x22387 b_S_kind_n_array$))))
 (let ((@x22857 (monotonicity @x22418 (= $x22388 (= b_S_kind_n_array$ b_S_kind_n_primitive$)))))
-(let ((@x22934 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35))))
+(let ((@x22500 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35))))
 (let (($x41 (= b_S_kind_n_thread$ b_S_kind_n_array$)))
 (let (($x42 (not $x41)))
 (let (($x39 (= b_S_kind_n_composite$ b_S_kind_n_array$)))
@@ -1431,10 +1431,10 @@
 (let ((@x22935 (monotonicity (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) (= $x11221 $x22336))))
 (let ((@x22938 (unit-resolution (def-axiom (or (not $x22326) $x22317 $x22333)) (mp (hypothesis $x11221) @x22935 $x22336) (unit-resolution @x22613 @x15021 $x22326) $x22333)))
 (let (($x22368 (b_S_is$ ?x21983 ?x22234)))
-(let ((@x22898 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368)))
+(let ((@x22885 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368)))
 (let (($x22385 (b_S_typed$ v_b_S_s$ ?x21983)))
 (let ((@x12045 (and-elim @x12033 $x10085)))
-(let ((@x22886 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385)))
+(let ((@x22517 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385)))
 (let ((?x22243 (b_S_owner$ v_b_S_s$ ?x21983)))
 (let (($x22259 (= ?x22243 b_S_me$)))
 (let ((@x12043 (and-elim @x12033 $x10083)))
@@ -1540,11 +1540,11 @@
 (let (($x22386 (not $x22385)))
 (let (($x22384 (not $x22368)))
 (let (($x24309 (or (not $x18905) $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)))
-(let (($x24492 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309)))
+(let (($x22614 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309)))
 (let ((@x24028 ((_ quant-inst v_b_S_s$ (b_S_ptr$ ?x10076 ?x21014)) (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)))))
-(let ((@x24084 (mp @x24028 (rewrite $x24492) $x24309)))
-(let ((@x22410 (unit-resolution @x24084 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318))))
-(let ((@x22411 (unit-resolution @x22410 @x22886 @x22898 @x22938 (mp @x75 (monotonicity (symm @x22934 (= $x35 $x22388)) $x22500) (not $x22388)) false)))
+(let ((@x24070 (mp @x24028 (rewrite $x22614) $x24309)))
+(let ((@x22410 (unit-resolution @x24070 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318))))
+(let ((@x22411 (unit-resolution @x22410 @x22517 @x22885 @x22938 (mp @x75 (monotonicity (symm @x22500 (= $x35 $x22388)) $x22488) (not $x22388)) false)))
 (let ((@x22434 (lemma @x22411 $x10136)))
 (let ((@x22687 (mp @x22434 (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) $x22317)))
 (let ((@x22688 (unit-resolution (def-axiom (or (not $x22326) $x22336 $x22318)) @x22687 (unit-resolution @x22613 @x15021 $x22326) $x22318)))
@@ -1894,10 +1894,10 @@
 (let (($x23521 (or (not $x19072) $x22944)))
 (let ((@x23524 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$)) $x23521)))
 (let (($x23055 (not $x22801)))
-(let ((@x23295 (monotonicity (symm (monotonicity @x23663 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055))))
+(let ((@x23295 (monotonicity (symm (monotonicity @x23699 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055))))
 (let ((@x23090 (unit-resolution (def-axiom (or (not $x22944) $x22801 $x22939)) (mp (hypothesis (not $x10141)) @x23295 $x23055) (unit-resolution @x23524 @x19075 $x22944) $x22939)))
-(let ((@x23670 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23663 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799)))
-(let ((@x23233 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23670 @x23090 $x22923) $x22900)))
+(let ((@x23706 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23699 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799)))
+(let ((@x23222 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23706 @x23090 $x22923) $x22900)))
 (let ((?x24419 (b_S_ref$ ?x21983)))
 (let ((?x24433 (b_S_ptr$ b_T_T_u1$ ?x24419)))
 (let ((?x24410 (b_S_idx$ ?x21983 0 b_T_T_u1$)))
@@ -2016,13 +2016,13 @@
 (let ((@x14355 (mp~ (mp (asserted $x6917) @x6947 $x6943) (nnf-pos (refl (~ $x6940 $x6940)) (~ $x6943 $x6943)) $x6943)))
 (let ((@x17967 (mp @x14355 @x17966 $x17964)))
 (let (($x24241 (not $x24240)))
-(let (($x23110 (not $x17964)))
-(let (($x24183 (or $x23110 $x24241 $x11259 $x23791)))
+(let (($x23252 (not $x17964)))
+(let (($x23749 (or $x23252 $x24241 $x11259 $x23791)))
 (let (($x23792 (or $x24241 $x22599 $x22601 $x23791)))
-(let (($x24184 (or $x23110 $x23792)))
-(let ((@x23271 (trans (monotonicity @x22715 @x22724 (= $x23792 (or $x24241 false $x11259 $x23791))) (rewrite (= (or $x24241 false $x11259 $x23791) (or $x24241 $x11259 $x23791))) (= $x23792 (or $x24241 $x11259 $x23791)))))
-(let ((@x23705 (trans (monotonicity @x23271 (= $x24184 (or $x23110 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23110 (or $x24241 $x11259 $x23791)) $x24183)) (= $x24184 $x24183))))
-(let ((@x23755 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ 0) $x24184) @x23705 $x24183) @x17967 @x12041 @x24355 (hypothesis $x23737) false)))
+(let (($x23750 (or $x23252 $x23792)))
+(let ((@x23251 (trans (monotonicity @x22715 @x22724 (= $x23792 (or $x24241 false $x11259 $x23791))) (rewrite (= (or $x24241 false $x11259 $x23791) (or $x24241 $x11259 $x23791))) (= $x23792 (or $x24241 $x11259 $x23791)))))
+(let ((@x23352 (trans (monotonicity @x23251 (= $x23750 (or $x23252 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23252 (or $x24241 $x11259 $x23791)) $x23749)) (= $x23750 $x23749))))
+(let ((@x23658 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ 0) $x23750) @x23352 $x23749) @x17967 @x12041 @x24355 (hypothesis $x23737) false)))
 (let (($x21186 (= ?x21014 ?x10079)))
 (let (($x21191 (or $x21152 $x21186)))
 (let ((@x21192 ((_ quant-inst (b_S_array$ b_T_T_u1$ v_b_P_H_len$) (b_S_ref$ ?x10078)) $x21191)))
@@ -2030,19 +2030,19 @@
 (let ((@x24532 (trans @x24530 (unit-resolution @x22000 @x15336 @x12044 $x21990) (= ?x22595 ?x21983))))
 (let ((@x23632 (trans (monotonicity @x24532 (= ?x24245 ?x24410)) (hypothesis $x24436) (= ?x24245 ?x24433))))
 (let ((@x23628 (trans @x23632 (monotonicity (trans @x24524 @x24511 (= ?x24419 v_b_P_H_arr$)) (= ?x24433 ?x10078)) (= ?x24245 ?x10078))))
-(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x24245 ?x10137))))
-(let ((@x23636 (symm (monotonicity (trans @x23622 @x23350 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246))))
-(let ((@x23256 (monotonicity (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655)))))
-(let ((@x23678 (trans @x23256 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247))))
-(let ((@x23865 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23755 $x23791) $x24248) (= ?x22903 ?x22595))))
-(let ((@x23912 (trans (monotonicity (trans @x23865 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888)))
+(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x24245 ?x10137))))
+(let ((@x23636 (symm (monotonicity (trans @x23622 @x23667 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246))))
+(let ((@x23746 (monotonicity (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655)))))
+(let ((@x23678 (trans @x23746 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247))))
+(let ((@x23867 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23658 $x23791) $x24248) (= ?x22903 ?x22595))))
+(let ((@x23912 (trans (monotonicity (trans @x23867 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888)))
 (let ((@x24132 (lemma (unit-resolution (hypothesis (not $x22888)) @x23912 false) (or $x24439 $x22888))))
 (let ((@x23115 (unit-resolution @x24132 (unit-resolution @x24460 (lemma @x24133 $x24445) $x24436) $x22888)))
 (let ((?x22658 (b_S_ts_n_emb$ ?x22655)))
 (let ((?x22663 (b_S_typ$ ?x22658)))
 (let ((?x22664 (b_S_kind_n_of$ ?x22663)))
 (let (($x22665 (= ?x22664 b_S_kind_n_primitive$)))
-(let ((@x23071 (monotonicity (monotonicity (symm @x23256 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891))))
+(let ((@x23071 (monotonicity (monotonicity (symm @x23746 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891))))
 (let (($x22946 (b_S_is_n_non_n_primitive$ ?x22663)))
 (let (($x23237 (not $x22946)))
 (let (($x23503 (or $x22665 $x23237)))
@@ -2063,8 +2063,8 @@
 (let ((@x23058 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x22505)) $x23057)))
 (let ((@x23584 (unit-resolution (def-axiom (or $x23503 (not $x22665))) (unit-resolution @x23058 @x19237 $x23504) (not $x22665))))
 (let ((@x23060 (lemma (unit-resolution @x23584 (trans @x23071 (hypothesis $x22892) $x22665) false) (not $x22892))))
-(let ((@x23231 (unit-resolution (def-axiom (or $x22901 $x22817 $x22889 $x22892 $x22896)) @x23060 (unit-resolution (def-axiom (or $x22895 (not $x22888))) @x23115 $x22895) (or $x22901 $x22817 $x22889))))
-(let ((@x23406 (unit-resolution @x23231 @x23233 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false)))
+(let ((@x23221 (unit-resolution (def-axiom (or $x22901 $x22817 $x22889 $x22892 $x22896)) @x23060 (unit-resolution (def-axiom (or $x22895 (not $x22888))) @x23115 $x22895) (or $x22901 $x22817 $x22889))))
+(let ((@x23406 (unit-resolution @x23221 @x23222 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false)))
 (let ((@x23403 (lemma @x23406 $x10141)))
 (let (($x20092 (or $x19318 $x20089)))
 (let (($x20095 (not $x20092)))
@@ -2618,19 +2618,19 @@
 (let ((@x13510 (monotonicity (monotonicity @x13504 (= $x12021 (and $x10136 $x13502))) (= (not $x12021) $x13508))))
 (let ((@x13511 (mp (not-or-elim (mp (asserted $x10434) @x12031 $x12027) (not $x12021)) @x13510 $x13508)))
 (let ((@x20143 (mp (mp (mp (mp~ @x13511 @x15835 $x15833) @x16117 $x16115) @x19763 $x19761) (monotonicity @x20139 (= $x19761 $x20140)) $x20140)))
-(let ((@x24002 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128)))
+(let ((@x24008 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128)))
 (let ((?x22514 (b_S_typ$ ?x10137)))
 (let (($x22515 (= ?x22514 b_T_T_u1$)))
 (let ((@x22856 (trans (unit-resolution @x22581 (unit-resolution @x22577 @x18183 $x22565) $x22556) @x22852 (= ?x10137 ?x10078))))
 (let ((@x22875 (trans (monotonicity @x22856 (= ?x22514 ?x21175)) (unit-resolution @x21182 @x19846 $x21176) $x22515)))
-(let (($x22507 (not $x22515)))
+(let (($x22932 (not $x22515)))
 (let (($x22522 (= $x10138 $x22515)))
-(let (($x22949 (or $x22002 $x22522)))
-(let ((@x22487 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22949)))
-(let ((@x22509 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22507)) (hypothesis $x15502) (or (not $x22522) $x22507))))
-(let ((@x22873 (unit-resolution (unit-resolution @x22509 (unit-resolution @x22487 @x19833 $x22522) $x22507) @x22875 false)))
+(let (($x22487 (or $x22002 $x22522)))
+(let ((@x22492 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22487)))
+(let ((@x22511 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22932)) (hypothesis $x15502) (or (not $x22522) $x22932))))
+(let ((@x22873 (unit-resolution (unit-resolution @x22511 (unit-resolution @x22492 @x19833 $x22522) $x22932) @x22875 false)))
 (let ((@x22876 (lemma @x22873 $x10138)))
-(let ((@x23964 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24002 $x20125)))
+(let ((@x24016 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24008 $x20125)))
 (let ((?x22963 (* (- 1) ?x10144)))
 (let ((?x22964 (+ v_b_L_H_max_G_0$ ?x22963)))
 (let (($x22965 (>= ?x22964 0)))
@@ -2652,9 +2652,9 @@
 (let ((@x23011 (symm (unit-resolution @x22447 @x15336 (hypothesis $x10138) $x22506) (= ?x22505 ?x10137))))
 (let ((@x23020 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x22834) $x22839)) (symm (monotonicity @x23011 (= ?x22685 ?x10144)) $x22834) $x22839)))
 (let ((@x23023 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) @x23020 @x23010 (hypothesis $x20589) @x23016 false) (or $x15502 $x15533 $x19297 $x15525 $x15511 $x20119))))
-(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15533 $x19297 $x15525 $x15511))))
-(let ((@x24203 (unit-resolution (unit-resolution @x24012 @x23403 (or $x15533 $x19297 $x15525)) (unit-resolution (def-axiom (or $x19313 (not $x15525))) @x24016 (not $x15525)) (unit-resolution (def-axiom (or $x19313 $x15523)) @x24016 $x15523) (unit-resolution (def-axiom (or $x19313 $x20589)) @x24016 $x20589) false)))
-(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15511 $x20113))))
+(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15533 $x19297 $x15525 $x15511))))
+(let ((@x24203 (unit-resolution (unit-resolution @x24012 @x23403 (or $x15533 $x19297 $x15525)) (unit-resolution (def-axiom (or $x19313 (not $x15525))) @x23991 (not $x15525)) (unit-resolution (def-axiom (or $x19313 $x15523)) @x23991 $x15523) (unit-resolution (def-axiom (or $x19313 $x20589)) @x23991 $x20589) false)))
+(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15511 $x20113))))
 (let ((@x24506 (unit-resolution (def-axiom (or $x20110 $x20104)) (unit-resolution @x24417 @x23403 $x20113) $x20104)))
 (let ((@x24507 (unit-resolution (def-axiom (or $x20107 $x11385 $x20101)) (lemma ((_ th-lemma arith farkas 1 1) @x12041 (hypothesis $x11385) false) $x11382) @x24506 $x20101)))
 (let ((@x24462 (unit-resolution (def-axiom (or $x20095 $x19318 $x20089)) (unit-resolution (def-axiom (or $x20098 $x20092)) @x24507 $x20092) $x20092)))
@@ -2710,8 +2710,8 @@
 (let ((@x23338 ((_ th-lemma arith farkas -1 1 1) (unit-resolution (def-axiom (or $x19575 $x16014)) @x23328 $x16014) (unit-resolution @x23335 @x23330 $x23168) (unit-resolution (def-axiom (or $x20062 $x11486)) (hypothesis $x20065) $x11486) false)))
 (let ((@x24500 (unit-resolution (lemma @x23338 (or $x20062 $x19903 $x11867 $x19501 $x19674 $x19669)) @x24499 @x24415 (unit-resolution (def-axiom (or $x20074 $x11432)) @x24583 $x11432) @x24314 (unit-resolution (def-axiom (or $x20074 $x13315)) @x24583 $x13315) $x20062)))
 (let ((@x24502 (unit-resolution (def-axiom (or $x20071 $x20019 $x20065)) (unit-resolution (def-axiom (or $x20074 $x20068)) @x24583 $x20068) @x24500 $x20019)))
-(let ((@x24684 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487)))
-(let ((@x24741 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596)))
+(let ((@x24656 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487)))
+(let ((@x24896 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596)))
 (let ((@x23420 (hypothesis $x11487)))
 (let (($x23378 (or $x22629 $x19677 $x21489 $x22597 $x19670 $x11486 $x23363)))
 (let (($x23360 (>= (+ v_b_L_H_p_G_0$ (* (- 1) v_b_P_H_len$)) 0)))
@@ -2725,42 +2725,42 @@
 (let ((@x23387 (trans @x23383 (rewrite (= (or $x22629 (or $x19677 $x21489 $x22597 $x19670 $x11486 $x23363)) $x23378)) (= $x23379 $x23378))))
 (let ((@x23388 (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ (b_S_ptr$ ?x10076 ?x21014) v_b_P_H_len$ v_b_L_H_p_G_0$ b_T_T_u1$) $x23379) @x23387 $x23378)))
 (let ((@x23422 (unit-resolution @x23388 @x18670 @x9769 @x12050 (hypothesis $x11901) @x23420 (hypothesis $x22596) (hypothesis $x23362) false)))
-(let ((@x24788 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24741 (or $x23363 $x19670 $x11486))))
-(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x23297)))
+(let ((@x24759 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24896 (or $x23363 $x19670 $x11486))))
+(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x23297)))
 (let (($x23782 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x24218)))
 (let ((?x23727 (b_S_owner$ v_b_S_s$ ?x24218)))
 (let (($x23776 (= ?x23727 b_S_me$)))
 (let (($x23785 (or $x23776 $x23782)))
 (let (($x24475 (not $x23785)))
-(let ((?x23730 (b_S_typ$ ?x24218)))
-(let ((?x23768 (b_S_kind_n_of$ ?x23730)))
+(let ((?x23804 (b_S_typ$ ?x24218)))
+(let ((?x23768 (b_S_kind_n_of$ ?x23804)))
 (let (($x23769 (= ?x23768 b_S_kind_n_primitive$)))
-(let (($x23728 (not $x23804)))
-(let (($x23770 (not $x23805)))
-(let (($x24476 (or $x23770 $x23728 $x23769 $x24475)))
-(let (($x24627 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23225)))
-(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23225) b_S_me$)))
-(let (($x24943 (or $x24478 $x24627)))
-(let (($x25004 (not $x24943)))
-(let (($x24820 (or $x23805 $x25004)))
-(let (($x24623 (not $x24820)))
+(let (($x23803 (not $x23797)))
+(let (($x24099 (not $x24098)))
+(let (($x24476 (or $x24099 $x23803 $x23769 $x24475)))
+(let (($x24604 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23228)))
+(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23228) b_S_me$)))
+(let (($x24602 (or $x24478 $x24604)))
+(let (($x24797 (not $x24602)))
+(let (($x24820 (or $x24098 $x24797)))
+(let (($x24655 (not $x24820)))
 (let (($x24474 (not $x24476)))
-(let (($x24809 (or $x24474 $x24623)))
-(let (($x24810 (not $x24809)))
-(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23225)))
+(let (($x24912 (or $x24474 $x24655)))
+(let (($x24913 (not $x24912)))
+(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23228)))
 (let (($x24210 (not $x24209)))
-(let (($x24817 (or $x24210 $x24810)))
-(let (($x24818 (not $x24817)))
-(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23225)))
-(let (($x24819 (= $x23783 $x24818)))
-(let (($x24622 (or (not $x19072) $x24819)))
-(let ((@x24633 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622)))
+(let (($x24931 (or $x24210 $x24913)))
+(let (($x24932 (not $x24931)))
+(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23228)))
+(let (($x24934 (= $x23783 $x24932)))
+(let (($x24622 (or (not $x19072) $x24934)))
+(let ((@x24172 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622)))
 (let (($x24628 (not $x23783)))
 (let ((@x24670 (monotonicity (symm (monotonicity @x25262 (= $x23783 $x10324)) (= $x10324 $x23783)) (= $x15599 $x24628))))
-(let ((@x24708 (unit-resolution (def-axiom (or (not $x24819) $x23783 $x24817)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24633 @x19075 $x24819) $x24817)))
-(let ((@x24998 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x10322)))
-(let ((@x24710 (mp @x24998 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209)))
-(let ((@x24724 (unit-resolution (def-axiom (or $x24809 $x24476)) (unit-resolution (def-axiom (or $x24818 $x24210 $x24810)) @x24710 @x24708 $x24810) $x24476)))
+(let ((@x24708 (unit-resolution (def-axiom (or (not $x24934) $x23783 $x24931)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24172 @x19075 $x24934) $x24931)))
+(let ((@x24785 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x10322)))
+(let ((@x24710 (mp @x24785 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209)))
+(let ((@x24724 (unit-resolution (def-axiom (or $x24912 $x24476)) (unit-resolution (def-axiom (or $x24932 $x24210 $x24913)) @x24710 @x24708 $x24913) $x24476)))
 (let ((?x24320 (b_S_idx$ ?x22595 v_b_L_H_p_G_0$ b_T_T_u1$)))
 (let ((?x24321 (b_S_select_o_tm$ ?x10272 ?x24320)))
 (let ((?x24322 (b_S_ts_n_emb$ ?x24321)))
@@ -2771,12 +2771,12 @@
 (let (($x24324 (not $x24323)))
 (let (($x24330 (or $x24324 $x24325 (not (b_S_ts_n_is_n_array_n_elt$ ?x24321)) $x24329)))
 (let (($x24331 (not $x24330)))
-(let (($x25071 (or $x23110 $x24241 $x19670 $x11486 $x24331)))
+(let (($x25071 (or $x23252 $x24241 $x19670 $x11486 $x24331)))
 (let (($x24332 (or $x24241 $x19670 $x23360 $x24331)))
-(let (($x25072 (or $x23110 $x24332)))
+(let (($x25072 (or $x23252 $x24332)))
 (let ((@x25070 (monotonicity (trans @x23370 @x23372 (= $x23360 $x11486)) (= $x24332 (or $x24241 $x19670 $x11486 $x24331)))))
-(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23110 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23110 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071))))
-(let ((@x25137 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ v_b_L_H_p_G_0$) $x25072) @x25080 $x25071) @x17967 @x24576 @x24684 @x24355 (hypothesis $x24330) false)))
+(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23252 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23252 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071))))
+(let ((@x25137 (unit-resolution (mp ((_ quant-inst v_b_S_s$ v_b_P_H_arr$ b_T_T_u1$ v_b_P_H_len$ v_b_L_H_p_G_0$) $x25072) @x25080 $x25071) @x17967 @x24576 @x24656 @x24355 (hypothesis $x24330) false)))
 (let ((@x25083 (def-axiom (or $x24330 $x24323))))
 (let ((?x24315 (b_S_ref$ ?x24198)))
 (let ((?x24367 (* (- 1) ?x24315)))
@@ -2795,15 +2795,15 @@
 (let ((?x25227 (* (- 1) ?x24925)))
 (let ((?x25228 (+ ?x24174 ?x25227)))
 (let (($x25229 (<= ?x25228 0)))
-(let ((?x23747 (* (- 1) ?x21014)))
-(let ((?x23641 (+ ?x10079 ?x23747)))
-(let (($x24296 (<= ?x23641 0)))
-(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24296)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24296)))
+(let ((?x24127 (* (- 1) ?x21014)))
+(let ((?x23641 (+ ?x10079 ?x24127)))
+(let (($x24104 (<= ?x23641 0)))
+(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24104)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24104)))
 (let ((?x25173 (* (- 1) ?x24419)))
 (let ((?x25174 (+ ?x21014 ?x25173)))
 (let (($x25175 (<= ?x25174 0)))
 (let ((@x25090 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x21014 ?x24419)) $x25175)) (symm (monotonicity @x24520 (= ?x24419 ?x21014)) (= ?x21014 ?x24419)) $x25175)))
-(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24296) (not $x25175))) @x25090 @x25085 $x25229)))
+(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24104) (not $x25175))) @x25090 @x25085 $x25229)))
 (let (($x25230 (>= ?x25228 0)))
 (let (($x23809 (>= ?x23641 0)))
 (let ((@x25106 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x23809)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x23809)))
@@ -2829,54 +2829,54 @@
 (let ((@x25162 (monotonicity (monotonicity @x25154 (= $x24471 $x25155)) (= (or $x22568 $x24471) $x25158))))
 (let ((@x25166 (mp ((_ quant-inst (b_S_ptr$ ?x10076 ?x21014) v_b_L_H_p_G_0$ b_T_T_u1$) (or $x22568 $x24471)) (trans @x25162 (rewrite (= $x25158 $x25158)) (= (or $x22568 $x24471) $x25158)) $x25158)))
 (let ((@x25257 (unit-resolution (def-axiom (or $x25152 $x25146)) (unit-resolution @x25166 @x18183 $x25155) $x25146)))
-(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23225)) (= ?x24320 ?x23225))))
-(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23101)) (= ?x23101 ?x24321))))
-(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23101)) (= ?x24218 (b_S_ts_n_emb$ ?x23101)))))
-(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23101) ?x24322)) (= ?x24218 ?x24322))))
+(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23228)) (= ?x24320 ?x23228))))
+(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23124)) (= ?x23124 ?x24321))))
+(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23124)) (= ?x24218 (b_S_ts_n_emb$ ?x23124)))))
+(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23124) ?x24322)) (= ?x24218 ?x24322))))
 (let ((@x25221 (trans (trans @x25219 (hypothesis $x24323) (= ?x24218 ?x22595)) @x24530 (= ?x24218 ?x10080))))
 (let ((@x25293 (unit-resolution (hypothesis (not $x23776)) (trans (monotonicity @x25221 (= ?x23727 ?x10082)) @x12043 $x23776) false)))
-(let ((@x23976 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776)))
-(let ((?x23443 (b_S_ts_n_emb$ ?x23101)))
+(let ((@x24057 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776)))
+(let ((?x23443 (b_S_ts_n_emb$ ?x23124)))
 (let ((?x23448 (b_S_typ$ ?x23443)))
 (let ((?x23449 (b_S_kind_n_of$ ?x23448)))
 (let (($x23450 (= ?x23449 b_S_kind_n_primitive$)))
-(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23730)) (= ?x23449 ?x23768))))
+(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23804)) (= ?x23449 ?x23768))))
 (let (($x23598 (b_S_is_n_non_n_primitive$ ?x23448)))
 (let (($x23599 (not $x23598)))
 (let (($x23602 (or $x23450 $x23599)))
 (let (($x23603 (not $x23602)))
 (let (($x24666 (or (not $x19234) $x23603)))
-(let ((@x24631 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666)))
-(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24631 @x19237 $x23603) (not $x23450))))
+(let ((@x24626 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666)))
+(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24626 @x19237 $x23603) (not $x23450))))
 (let ((@x24645 (lemma (unit-resolution @x24965 (trans @x24651 (hypothesis $x23769) $x23450) false) (not $x23769))))
-(let ((@x24718 (unit-resolution (def-axiom (or $x24474 $x23770 $x23728 $x23769 $x24475)) @x24645 (unit-resolution (def-axiom (or $x23785 (not $x23776))) @x23976 $x23785) (or $x24474 $x23770 $x23728))))
-(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23804 $x23775)) (mp @x24697 @x24701 $x23784) $x23804) @x24696 false)))
+(let ((@x24718 (unit-resolution (def-axiom (or $x24474 $x24099 $x23803 $x23769 $x24475)) @x24645 (unit-resolution (def-axiom (or $x23785 (not $x23776))) @x24057 $x23785) (or $x24474 $x24099 $x23803))))
+(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23797 $x23805)) (mp @x24697 @x24701 $x23770) $x23797) @x24696 false)))
 (let ((@x20784 (def-axiom (or $x20013 $x15590 $x15593 $x20007))))
-(let ((@x24650 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24998 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007)))
+(let ((@x24630 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24785 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007)))
 (let ((@x20774 (def-axiom (or $x20004 $x19998))))
 (let ((@x20768 (def-axiom (or $x20001 $x15590 $x15599 $x19995))))
-(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24650 $x19998) (or $x15599 $x19995))))
+(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24630 $x19998) (or $x15599 $x19995))))
 (let ((@x23989 (hypothesis $x19980)))
-(let ((@x24787 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953))))
-(let ((@x24655 (unit-resolution @x24787 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959)))
+(let ((@x25004 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953))))
+(let ((@x24684 (unit-resolution @x25004 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959)))
 (let ((@x20748 (def-axiom (or $x19989 $x19977 $x19983))))
-(let ((@x24904 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977)))
+(let ((@x24916 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977)))
 (let ((@x20716 (def-axiom (or $x19974 $x19968))))
-(let ((@x24602 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965))))
-(let ((@x24657 (unit-resolution @x24602 (unit-resolution @x20716 @x24904 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24655 $x19962) @x24998 false)))
-(let ((@x24972 (unit-resolution (lemma @x24657 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953)))
+(let ((@x24762 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965))))
+(let ((@x24920 (unit-resolution @x24762 (unit-resolution @x20716 @x24916 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24684 $x19962) @x24785 false)))
+(let ((@x24972 (unit-resolution (lemma @x24920 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953)))
 (let (($x13277 (<= v_b_P_H_len$ 4294967295)))
 (let (($x13272 (= (+ b_S_max_o_u4$ (* (- 1) v_b_P_H_len$)) (+ 4294967295 (* (- 1) v_b_P_H_len$)))))
 (let ((@x13276 (monotonicity (monotonicity @x6446 $x13272) (= $x11245 (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0)))))
 (let ((@x13281 (trans @x13276 (rewrite (= (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0) $x13277)) (= $x11245 $x13277))))
 (let ((@x13282 (mp (and-elim @x12033 $x11245) @x13281 $x13277)))
 (let ((@x25068 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1) (or $x13353 (not $x13277) $x11486)) @x13282 (or $x13353 $x11486))))
-(let ((@x25023 (unit-resolution (def-axiom (or $x19947 $x15611 $x15614 $x19941)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x19670 $x11570)) @x24576 $x11570) (unit-resolution @x25068 @x24684 $x13353) (or $x19947 $x19941))))
+(let ((@x25023 (unit-resolution (def-axiom (or $x19947 $x15611 $x15614 $x19941)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x19670 $x11570)) @x24576 $x11570) (unit-resolution @x25068 @x24656 $x13353) (or $x19947 $x19941))))
 (let ((@x25021 (unit-resolution @x25023 (unit-resolution (def-axiom (or $x19950 $x19944)) @x24972 $x19944) $x19941)))
 (let ((@x20652 (def-axiom (or $x19938 $x19932))))
 (let (($x20596 (>= ?x11582 (- 1))))
 (let ((@x25129 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x19452 $x20596)) (unit-resolution (def-axiom (or $x19938 $x11580)) @x25021 $x11580) $x20596)))
-(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24684 (or $x11608 (not $x20596)))))
+(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24656 (or $x11608 (not $x20596)))))
 (let ((@x20638 (def-axiom (or $x19935 $x11612 $x19929))))
 (let ((@x25133 (unit-resolution @x20638 (unit-resolution @x25134 @x25129 $x11608) (unit-resolution @x20652 @x25021 $x19932) $x19929)))
 (let ((@x20630 (def-axiom (or $x19926 $x19920))))
@@ -2888,12 +2888,12 @@
 (let ((@x25188 (symm (unit-resolution (def-axiom (or $x19950 $x10340)) @x24972 $x10340) (= v_b_L_H_p_G_0$ v_b_SL_H_witness_G_1$))))
 (let ((@x25200 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= v_b_L_H_p_G_0$ v_b_SL_H_witness_G_1$)) $x24861)) @x25188 $x24861)))
 (let ((@x20614 (def-axiom (or $x19413 $x11647 (not $x10374)))))
-(let ((@x25206 (unit-resolution @x20614 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11648 (not $x24861) $x11486)) @x25200 @x24684 $x11648) (trans @x25190 @x25121 $x10374) $x19413)))
+(let ((@x25206 (unit-resolution @x20614 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11648 (not $x24861) $x11486)) @x25200 @x24656 $x11648) (trans @x25190 @x25121 $x10374) $x19413)))
 (let ((@x20618 (def-axiom (or $x19914 $x19412))))
 (let ((@x20626 (def-axiom (or $x19923 $x19386 $x19917))))
 (let ((@x25210 (unit-resolution @x20626 (unit-resolution @x20618 @x25206 $x19914) (unit-resolution @x20630 @x25133 $x19920) $x19386)))
-(let (($x24182 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0)))
-(let (($x24206 (not $x24182)))
+(let (($x24195 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0)))
+(let (($x24206 (not $x24195)))
 (let ((?x11631 (* (- 1) v_b_L_H_max_G_3$)))
 (let ((?x20720 (+ v_b_L_H_max_G_1$ ?x11631)))
 (let (($x20721 (<= ?x20720 0)))
@@ -2905,30 +2905,30 @@
 (let ((@x24170 (hypothesis $x20721)))
 (let (($x20603 (not $x15893)))
 (let ((@x24171 (hypothesis $x20603)))
-(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24182) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721)))))
+(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24195) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721)))))
 (let ((@x25131 (unit-resolution @x24211 (unit-resolution (def-axiom (or $x19381 $x20603)) @x25210 $x20603) (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x20721 (not $x24870) $x11516)) @x25214 @x25195 $x20721) $x24206)))
 (let ((?x15869 (* (- 1) ?v0!14)))
 (let ((?x23656 (+ v_b_L_H_p_G_0$ ?x15869)))
-(let (($x24586 (>= ?x23656 0)))
+(let (($x24926 (>= ?x23656 0)))
 (let ((@x24735 (hypothesis $x20596)))
-(let ((@x24001 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24586 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24586)))
+(let ((@x24918 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24926 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24926)))
 (let (($x23657 (<= ?x23656 0)))
-(let (($x24913 (or $x19903 $x19365 $x19366 $x23657 $x24182)))
+(let (($x24882 (or $x19903 $x19365 $x19366 $x23657 $x24195)))
 (let (($x23648 (<= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) 0)))
 (let (($x23640 (>= (+ ?v0!14 ?x11484) 0)))
 (let (($x23649 (or $x19365 $x19366 $x23640 $x23648)))
-(let (($x24853 (or $x19903 $x23649)))
-(let (($x24880 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634))))
-(let ((@x24024 (monotonicity (rewrite $x24880) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0)))))
-(let ((@x24867 (trans @x24024 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24182)) (= $x23648 $x24182))))
-(let ((@x24020 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0)))))
-(let ((@x24881 (trans @x24020 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657))))
-(let ((@x24935 (monotonicity (monotonicity @x24881 @x24867 (= $x23649 (or $x19365 $x19366 $x23657 $x24182))) (= $x24853 (or $x19903 (or $x19365 $x19366 $x23657 $x24182))))))
-(let ((@x24917 (trans @x24935 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24182)) $x24913)) (= $x24853 $x24913))))
-(let ((@x24941 (unit-resolution (mp ((_ quant-inst ?v0!14) $x24853) @x24917 $x24913) @x23333 (unit-resolution (def-axiom (or $x19381 $x15626)) (hypothesis $x19386) $x15626) (unit-resolution (def-axiom (or $x19381 $x15627)) (hypothesis $x19386) $x15627) (hypothesis $x24206) $x23657)))
-(let ((@x24757 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24586))) @x24941 @x24001 (hypothesis (not $x25035)) false)))
-(let ((@x24761 (lemma @x24757 (or $x19381 $x25035 $x19903 $x24182 $x15871 (not $x20596)))))
-(let ((@x25179 (unit-resolution (unit-resolution @x24761 @x24499 (or $x19381 $x25035 $x24182 $x15871 (not $x20596))) @x25131 @x25129 (unit-resolution (def-axiom (or $x19381 $x15876)) @x25210 $x15876) @x25210 $x25035)))
+(let (($x24880 (or $x19903 $x23649)))
+(let (($x24587 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634))))
+(let ((@x24936 (monotonicity (rewrite $x24587) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0)))))
+(let ((@x24841 (trans @x24936 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24195)) (= $x23648 $x24195))))
+(let ((@x24943 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0)))))
+(let ((@x24623 (trans @x24943 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657))))
+(let ((@x24818 (monotonicity (monotonicity @x24623 @x24841 (= $x23649 (or $x19365 $x19366 $x23657 $x24195))) (= $x24880 (or $x19903 (or $x19365 $x19366 $x23657 $x24195))))))
+(let ((@x24597 (trans @x24818 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24195)) $x24882)) (= $x24880 $x24882))))
+(let ((@x24900 (unit-resolution (mp ((_ quant-inst ?v0!14) $x24880) @x24597 $x24882) @x23333 (unit-resolution (def-axiom (or $x19381 $x15626)) (hypothesis $x19386) $x15626) (unit-resolution (def-axiom (or $x19381 $x15627)) (hypothesis $x19386) $x15627) (hypothesis $x24206) $x23657)))
+(let ((@x24984 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24926))) @x24900 @x24918 (hypothesis (not $x25035)) false)))
+(let ((@x24787 (lemma @x24984 (or $x19381 $x25035 $x19903 $x24195 $x15871 (not $x20596)))))
+(let ((@x25179 (unit-resolution (unit-resolution @x24787 @x24499 (or $x19381 $x25035 $x24195 $x15871 (not $x20596))) @x25131 @x25129 (unit-resolution (def-axiom (or $x19381 $x15876)) @x25210 $x15876) @x25210 $x25035)))
 (let ((@x25060 (monotonicity (symm (hypothesis $x25035) (= ?v0!14 v_b_L_H_p_G_0$)) (= ?x15633 ?x10320))))
 (let ((@x25064 (unit-resolution (hypothesis (not $x25038)) (symm (monotonicity @x25060 (= ?x15634 ?x10327)) $x25038) false)))
 (let ((@x25067 (lemma @x25064 (or (not $x25035) $x25038))))
@@ -2944,30 +2944,30 @@
 (let (($x25044 (not $x25038)))
 (let (($x25049 (not $x25041)))
 (let ((@x25051 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) (hypothesis $x25041) @x24170 @x24171 (hypothesis $x11516) false) (or $x25049 (not $x20721) $x15893 $x11515))))
-(let ((@x24891 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049)))
-(let ((@x24597 (unit-resolution @x20638 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24735 @x23420 $x11608) (hypothesis $x19932) $x19929)))
-(let ((@x24892 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719)))
-(let ((@x24061 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190))))
-(let ((@x24887 (trans (monotonicity @x24061 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$))))
+(let ((@x24047 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049)))
+(let ((@x24884 (unit-resolution @x20638 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24735 @x23420 $x11608) (hypothesis $x19932) $x19929)))
+(let ((@x24887 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719)))
+(let ((@x24982 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190))))
+(let ((@x24897 (trans (monotonicity @x24982 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$))))
 (let ((?x11645 (* (- 1) v_b_SL_H_witness_G_1$)))
 (let ((?x20724 (+ v_b_SL_H_witness_G_0$ ?x11645)))
 (let (($x20726 (>= ?x20724 0)))
 (let (($x20723 (= v_b_SL_H_witness_G_0$ v_b_SL_H_witness_G_1$)))
-(let ((@x24982 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
-(let ((@x24888 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867))))
-(let ((@x24648 (unit-resolution @x24888 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24982 $x20726) @x23180 $x11648)))
-(let ((@x24798 (unit-resolution @x20618 (unit-resolution @x20614 @x24648 (trans @x24887 @x24892 $x10374) $x19413) $x19914)))
+(let ((@x24788 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
+(let ((@x24909 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867))))
+(let ((@x24673 (unit-resolution @x24909 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24788 $x20726) @x23180 $x11648)))
+(let ((@x24789 (unit-resolution @x20618 (unit-resolution @x20614 @x24673 (trans @x24897 @x24887 $x10374) $x19413) $x19914)))
 (let ((@x20602 (def-axiom (or $x19381 $x15876))))
-(let ((@x25013 (unit-resolution @x20602 (unit-resolution @x20626 @x24798 (unit-resolution @x20630 @x24597 $x19920) $x19386) $x15876)))
-(let ((@x25017 (unit-resolution @x24761 @x25013 (unit-resolution @x20626 @x24798 (unit-resolution @x20630 @x24597 $x19920) $x19386) @x23333 (unit-resolution @x24211 @x24171 @x24170 $x24206) (unit-resolution @x25067 (unit-resolution @x25052 @x24891 $x25044) $x25065) @x24735 false)))
-(let ((@x24056 (lemma @x25017 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674))))
-(let ((@x24843 (unit-resolution @x24056 @x24499 @x24415 @x24684 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935))))
+(let ((@x24914 (unit-resolution @x20602 (unit-resolution @x20626 @x24789 (unit-resolution @x20630 @x24884 $x19920) $x19386) $x15876)))
+(let ((@x24915 (unit-resolution @x24787 @x24914 (unit-resolution @x20626 @x24789 (unit-resolution @x20630 @x24884 $x19920) $x19386) @x23333 (unit-resolution @x24211 @x24171 @x24170 $x24206) (unit-resolution @x25067 (unit-resolution @x25052 @x24047 $x25044) $x25065) @x24735 false)))
+(let ((@x24889 (lemma @x24915 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674))))
+(let ((@x24843 (unit-resolution @x24889 @x24499 @x24415 @x24656 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935))))
 (let ((@x24844 (unit-resolution @x24843 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20719) $x20721)) @x25006 $x20721) @x25299 @x24947 (unit-resolution @x20652 @x24908 $x19932) $x15893)))
 (let ((@x20605 (def-axiom (or $x19381 $x20603))))
 (let ((@x25302 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (= ?x10372 ?x10190))))
 (let ((@x25305 (trans (monotonicity @x25302 (= ?x10373 ?x10191)) @x24314 (= ?x10373 v_b_L_H_max_G_1$))))
 (let ((@x25306 (trans @x25305 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) @x25299 $x10391) $x20719) $x10374)))
 (let ((@x25307 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
-(let ((@x25311 (unit-resolution (unit-resolution @x24888 @x24415 (or $x11648 (not $x20726))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x25307 $x20726) $x11648)))
+(let ((@x25311 (unit-resolution (unit-resolution @x24909 @x24415 (or $x11648 (not $x20726))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x25307 $x20726) $x11648)))
 (unit-resolution @x20626 (unit-resolution @x20618 (unit-resolution @x20614 @x25311 @x25306 $x19413) $x19914) (unit-resolution @x20605 @x24844 $x19381) (unit-resolution @x20630 @x24954 $x19920) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
diff -r dca8d06ecbba -r 8cecd655eef4 src/HOL/SMT_Examples/boogie.ML
--- a/src/HOL/SMT_Examples/boogie.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -7,7 +7,7 @@
 signature BOOGIE =
 sig
   val boogie_prove: theory -> string list -> unit
-end
+end;
 
 structure Boogie: BOOGIE =
 struct
@@ -16,7 +16,6 @@
 
 val as_int = fst o read_int o raw_explode
 
-
 val isabelle_name =
   let
     fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
@@ -31,7 +30,6 @@
   in prefix "b_" o translate_string purge end
 
 
-
 (* context *)
 
 type context =
@@ -39,54 +37,44 @@
 
 val empty_context: context = (Symtab.empty, Symtab.empty, [], [])
 
-
 fun add_type name (tds, fds, axs, vcs) =
   let
     val T = TFree (isabelle_name name, @{sort type})
     val tds' = Symtab.update (name, T) tds
   in (tds', fds, axs, vcs) end
 
-
 fun add_func name Ts T unique (tds, fds, axs, vcs) =
   let
     val t = Free (isabelle_name name, Ts ---> T)
     val fds' = Symtab.update (name, (t, unique)) fds
   in (tds, fds', axs, vcs) end
 
-
 fun add_axiom t (tds, fds, axs, vcs) = (tds, fds, t :: axs, vcs)
 
 fun add_vc t (tds, fds, axs, vcs) = (tds, fds, axs, t :: vcs)
 
-
 fun lookup_type (tds, _, _, _) name =
   (case Symtab.lookup tds name of
     SOME T => T
   | NONE => error "Undeclared type")
 
-
 fun lookup_func (_, fds, _, _) name =
   (case Symtab.lookup fds name of
     SOME t_unique => t_unique
   | NONE => error "Undeclared function")
 
 
-
 (* constructors *)
 
 fun mk_var name T = Free ("V_" ^ isabelle_name name, T)
 
-
 fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T])
 
-
 fun mk_binary t (t1, t2) = t $ t1 $ t2
 
-
 fun mk_nary _ t [] = t
   | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
 
-
 fun mk_distinct [] = @{const HOL.True}
   | mk_distinct [_] = @{const HOL.True}
   | mk_distinct (t :: ts) =
@@ -95,34 +83,27 @@
           HOLogic.mk_conj (HOLogic.mk_not (HOLogic.mk_eq (t, u)), u')
       in fold_rev mk_noteq ts (mk_distinct ts) end
 
-
 fun mk_store m k v =
   let
     val mT = Term.fastype_of m and kT = Term.fastype_of k
     val vT = Term.fastype_of v
   in Const (@{const_name fun_upd}, mT --> kT --> vT --> mT) $ m $ k $ v end
 
-
 fun mk_quant q (Free (x, T)) t = q T $ absfree (x, T) t
   | mk_quant _ t _ = raise TERM ("bad variable", [t])
 
-
-fun mk_list T = HOLogic.mk_list T
-
-
 val patternT = @{typ "SMT2.pattern"}
 
 fun mk_pat t =
   Const (@{const_name "SMT2.pat"}, Term.fastype_of t --> patternT) $ t
 
 fun mk_pattern [] = raise TERM ("mk_pattern", [])
-  | mk_pattern ts = mk_list patternT (map mk_pat ts)
-
+  | mk_pattern ts = SMT2_Util.mk_symb_list patternT (map mk_pat ts)
 
 fun mk_trigger [] t = t
   | mk_trigger pss t =
       @{term "SMT2.trigger"} $
-        mk_list @{typ "SMT2.pattern list"} (map mk_pattern pss) $ t
+        SMT2_Util.mk_symb_list @{typ "SMT2.pattern SMT2.symb_list"} (map mk_pattern pss) $ t
 
 
 (* parser *)
@@ -131,7 +112,6 @@
   let fun apply (xs, ls) = f ls |>> (fn x => x :: xs)
   in funpow (as_int n) apply ([], ls) |>> rev end
 
-
 fun parse_type _ (["bool"] :: ls) = (@{typ bool}, ls)
   | parse_type _ (["int"] :: ls) = (@{typ int}, ls)
   | parse_type cx (["array", arity] :: ls) =
@@ -139,42 +119,29 @@
   | parse_type cx (("type-con" :: name :: _) :: ls) = (lookup_type cx name, ls)
   | parse_type _ _ = error "Bad type"
 
-
 fun parse_expr _ (["true"] :: ls) = (@{term True}, ls)
   | parse_expr _ (["false"] :: ls) = (@{term False}, ls)
   | parse_expr cx (["not"] :: ls) = parse_expr cx ls |>> HOLogic.mk_not
-  | parse_expr cx (["and", n] :: ls) =
-      parse_nary_expr cx n HOLogic.mk_conj @{term True} ls
-  | parse_expr cx (["or", n] :: ls) =
-      parse_nary_expr cx n HOLogic.mk_disj @{term False} ls
-  | parse_expr cx (["implies"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term HOL.implies}) ls
+  | parse_expr cx (["and", n] :: ls) = parse_nary_expr cx n HOLogic.mk_conj @{term True} ls
+  | parse_expr cx (["or", n] :: ls) = parse_nary_expr cx n HOLogic.mk_disj @{term False} ls
+  | parse_expr cx (["implies"] :: ls) = parse_bin_expr cx (mk_binary @{term HOL.implies}) ls
   | parse_expr cx (["="] :: ls) = parse_bin_expr cx HOLogic.mk_eq ls
   | parse_expr cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   | parse_expr cx (["fun", name, n] :: ls) =
       let val (t, _) = lookup_func cx name
       in repeat (parse_expr cx) n ls |>> curry Term.list_comb t end
   | parse_expr cx (("label" :: _) :: ls) = parse_expr cx ls
-  | parse_expr _ (["int-num", n] :: ls) =
-      (HOLogic.mk_number @{typ int} (as_int n), ls)
-  | parse_expr cx (["<"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op < :: int => _"}) ls
-  | parse_expr cx (["<="] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op <= :: int => _"}) ls
-  | parse_expr cx ([">"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op < :: int => _"}o swap) ls
+  | parse_expr _ (["int-num", n] :: ls) = (HOLogic.mk_number @{typ int} (as_int n), ls)
+  | parse_expr cx (["<"] :: ls) = parse_bin_expr cx (mk_binary @{term "op < :: int => _"}) ls
+  | parse_expr cx (["<="] :: ls) = parse_bin_expr cx (mk_binary @{term "op <= :: int => _"}) ls
+  | parse_expr cx ([">"] :: ls) = parse_bin_expr cx (mk_binary @{term "op < :: int => _"}o swap) ls
   | parse_expr cx ([">="] :: ls) =
       parse_bin_expr cx (mk_binary @{term "op <= :: int => _"} o swap) ls
-  | parse_expr cx (["+"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op + :: int => _"}) ls
-  | parse_expr cx (["-"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op - :: int => _"}) ls
-  | parse_expr cx (["*"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term "op * :: int => _"}) ls
-  | parse_expr cx (["/"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term boogie_div}) ls
-  | parse_expr cx (["%"] :: ls) =
-      parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
+  | parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary @{term "op + :: int => _"}) ls
+  | parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary @{term "op - :: int => _"}) ls
+  | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "op * :: int => _"}) ls
+  | parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_div}) ls
+  | parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
   | parse_expr cx (["select", n] :: ls) =
       repeat (parse_expr cx) n ls
       |>> (fn ts => hd ts $ HOLogic.mk_tuple (tl ts))
@@ -188,14 +155,11 @@
       parse_quant cx HOLogic.exists_const vars pats atts ls
   | parse_expr _ _ = error "Bad expression"
 
-
 and parse_bin_expr cx f ls = ls |> parse_expr cx ||>> parse_expr cx |>> f
 
-
 and parse_nary_expr cx n f c ls =
   repeat (parse_expr cx) n ls |>> mk_nary (curry f) c
 
-
 and parse_quant cx q vars pats atts ls =
   let
     val ((((vs, pss), _), t), ls') =
@@ -206,15 +170,12 @@
       ||>> parse_expr cx
   in (fold_rev (mk_quant q) vs (mk_trigger pss t), ls') end
 
-
 and parse_var cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   | parse_var _ _ = error "Bad variable"
 
-
 and parse_pat cx (["pat", n] :: ls) = repeat (parse_expr cx) n ls
   | parse_pat _ _ = error "Bad pattern"
 
-
 and parse_attr cx (["attribute", name, n] :: ls) =
       let
         fun attr (["expr-attr"] :: ls) = parse_expr cx ls |>> K ()
@@ -223,7 +184,6 @@
       in repeat attr n ls |>> K name end
   | parse_attr _ _ = error "Bad attribute"
 
-
 fun parse_func cx arity n ls =
   let
     val ((Ts, atts), ls') =
@@ -231,7 +191,6 @@
     val unique = member (op =) atts "unique"
   in ((split_last Ts, unique), ls') end
 
-
 fun parse_decl (("type-decl" :: name :: _) :: ls) cx = (ls, add_type name cx)
   | parse_decl (["fun-decl", name, arity, n] :: ls) cx =
       let val (((Ts, T), unique), ls') = parse_func cx arity n ls
@@ -246,12 +205,10 @@
       in (ls', add_vc t cx) end
   | parse_decl _ _ = error "Bad declaration"
 
-
 fun parse_lines [] cx = cx
   | parse_lines ls cx = parse_decl ls cx |-> parse_lines
 
 
-
 (* splitting of text lines into a lists of tokens *)
 
 fun is_blank c = (c = " " orelse c = "\t" orelse c = "\r" orelse c = "\n")
@@ -261,7 +218,6 @@
   #> filter (fn [] => false | _ => true)
 
 
-
 (* proving verification conditions *)
 
 fun add_unique_axioms (tds, fds, axs, vcs) =
@@ -271,7 +227,6 @@
   |> map (fn (T, ns) => mk_distinct (map (Free o rpair T) ns))
   |> (fn axs' => (tds, fds, axs' @ axs, vcs))
 
-
 fun build_proof_context thy (tds, fds, axs, vcs) =
   let
     val vc =
@@ -287,16 +242,13 @@
     |> pair (map HOLogic.mk_Trueprop axs, HOLogic.mk_Trueprop vc)
   end
 
-
 val boogie_rules =
   [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
   [@{thm fun_upd_same}, @{thm fun_upd_apply}]
 
-
 fun boogie_tac ctxt axioms =
   ALLGOALS (SMT2_Solver.smt2_tac ctxt (boogie_rules @ axioms))
 
-
 fun boogie_prove thy lines =
   let
     val ((axioms, vc), ctxt) =
@@ -305,8 +257,7 @@
       |> add_unique_axioms
       |> build_proof_context thy
 
-    val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
-      boogie_tac context prems)
+    val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} => boogie_tac context prems)
     val _ = writeln "Verification condition proved successfully"
 
   in () end
@@ -324,4 +275,4 @@
           val _ = boogie_prove thy' lines;
         in thy' end)))
 
-end
+end;