adapted examples to changes in SMT triggers
authorblanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 572328cecd655eef4
parent 57231 dca8d06ecbba
child 57233 8fcbfce2a2a9
adapted examples to changes in SMT triggers
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/SMT_Examples/VCC_Max.certs2
src/HOL/SMT_Examples/boogie.ML
     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -357,7 +357,9 @@
     1.4  lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt2
     1.5  lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt2
     1.6  lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt2
     1.7 -lemma "\<forall>x::int. SMT2.trigger [[SMT2.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt2
     1.8 +lemma "\<forall>x::int.
     1.9 +  SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat x) SMT2.Symb_Nil) SMT2.Symb_Nil)
    1.10 +    (x < a \<longrightarrow> 2 * x < 2 * a)" by smt2
    1.11  lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt2
    1.12  
    1.13  
     2.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jun 12 01:00:49 2014 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jun 12 01:00:49 2014 +0200
     2.3 @@ -18,28 +18,28 @@
     2.4  
     2.5  lemma
     2.6    "True"
     2.7 -  "\<not>False"
     2.8 -  "\<not>\<not>True"
     2.9 +  "\<not> False"
    2.10 +  "\<not> \<not> True"
    2.11    "True \<and> True"
    2.12    "True \<or> False"
    2.13    "False \<longrightarrow> True"
    2.14 -  "\<not>(False \<longleftrightarrow> True)"
    2.15 +  "\<not> (False \<longleftrightarrow> True)"
    2.16    by smt2+
    2.17  
    2.18  lemma
    2.19 -  "P \<or> \<not>P"
    2.20 -  "\<not>(P \<and> \<not>P)"
    2.21 -  "(True \<and> P) \<or> \<not>P \<or> (False \<and> P) \<or> P"
    2.22 +  "P \<or> \<not> P"
    2.23 +  "\<not> (P \<and> \<not> P)"
    2.24 +  "(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P"
    2.25    "P \<longrightarrow> P"
    2.26    "P \<and> \<not> P \<longrightarrow> False"
    2.27    "P \<and> Q \<longrightarrow> Q \<and> P"
    2.28    "P \<or> Q \<longrightarrow> Q \<or> P"
    2.29    "P \<and> Q \<longrightarrow> P \<or> Q"
    2.30 -  "\<not>(P \<or> Q) \<longrightarrow> \<not>P"
    2.31 -  "\<not>(P \<or> Q) \<longrightarrow> \<not>Q"
    2.32 -  "\<not>P \<longrightarrow> \<not>(P \<and> Q)"
    2.33 -  "\<not>Q \<longrightarrow> \<not>(P \<and> Q)"
    2.34 -  "(P \<and> Q) \<longleftrightarrow> (\<not>(\<not>P \<or> \<not>Q))"
    2.35 +  "\<not> (P \<or> Q) \<longrightarrow> \<not> P"
    2.36 +  "\<not> (P \<or> Q) \<longrightarrow> \<not> Q"
    2.37 +  "\<not> P \<longrightarrow> \<not> (P \<and> Q)"
    2.38 +  "\<not> Q \<longrightarrow> \<not> (P \<and> Q)"
    2.39 +  "(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))"
    2.40    "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
    2.41    "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
    2.42    "(P \<and> Q) \<or> R  \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
    2.43 @@ -50,23 +50,23 @@
    2.44    "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
    2.45    "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
    2.46    "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow>  ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
    2.47 -  "\<not>(P \<longrightarrow> R) \<longrightarrow>  \<not>(Q \<longrightarrow> R) \<longrightarrow> \<not>(P \<and> Q \<longrightarrow> R)"
    2.48 +  "\<not> (P \<longrightarrow> R) \<longrightarrow>  \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
    2.49    "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
    2.50    "P \<longrightarrow> (Q \<longrightarrow> P)"
    2.51    "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)"
    2.52    "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
    2.53    "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
    2.54 -  "(P \<longrightarrow> Q) \<longrightarrow> (\<not>Q \<longrightarrow> \<not>P)"
    2.55 +  "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
    2.56    "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
    2.57    "(P \<longrightarrow> Q) \<and> (Q  \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)"
    2.58    "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
    2.59 -  "\<not>(P \<longleftrightarrow> \<not>P)"
    2.60 -  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not>Q \<longrightarrow> \<not>P)"
    2.61 +  "\<not> (P \<longleftrightarrow> \<not> P)"
    2.62 +  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
    2.63    "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"
    2.64    by smt2+
    2.65  
    2.66  lemma
    2.67 -  "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not>P \<longrightarrow> Q2))"
    2.68 +  "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))"
    2.69    "if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)"
    2.70    "(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)"
    2.71    "(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)"
    2.72 @@ -75,9 +75,9 @@
    2.73    by smt2+
    2.74  
    2.75  lemma
    2.76 -  "case P of True \<Rightarrow> P | False \<Rightarrow> \<not>P"
    2.77 -  "case P of False \<Rightarrow> \<not>P | True \<Rightarrow> P"
    2.78 -  "case \<not>P of True \<Rightarrow> \<not>P | False \<Rightarrow> P"
    2.79 +  "case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P"
    2.80 +  "case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P"
    2.81 +  "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P"
    2.82    "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
    2.83    by smt2+
    2.84  
    2.85 @@ -104,7 +104,7 @@
    2.86    "(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x"
    2.87    "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))"
    2.88    "(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a"
    2.89 -  "(\<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"
    2.90 +  "(\<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"
    2.91    by smt2+
    2.92  
    2.93  lemma
    2.94 @@ -117,7 +117,7 @@
    2.95    "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
    2.96    "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)"
    2.97    "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)"
    2.98 -  "\<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))"
    2.99 +  "\<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))"
   2.100    by smt2+
   2.101  
   2.102  lemma
   2.103 @@ -130,16 +130,16 @@
   2.104    by smt2+
   2.105  
   2.106  lemma
   2.107 -  "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   2.108 +  "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   2.109    "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   2.110    "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   2.111 -  "(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y"
   2.112 +  "(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y"
   2.113    "(\<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"
   2.114    by smt2+
   2.115  
   2.116  lemma
   2.117    "\<forall>x. \<exists>y. f x y = f x (g x)"
   2.118 -  "(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))"
   2.119 +  "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   2.120    "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   2.121    "\<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))"
   2.122    "\<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))"
   2.123 @@ -150,7 +150,7 @@
   2.124  
   2.125  lemma
   2.126    "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
   2.127 -  "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))"
   2.128 +  "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))"
   2.129    "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   2.130    "(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)"
   2.131    "(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R"
   2.132 @@ -158,18 +158,18 @@
   2.133  
   2.134  lemma
   2.135    "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
   2.136 -  "(\<exists>x\<in>M. P x) \<or> \<not>(P c \<and> c \<in> M)"
   2.137 +  "(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)"
   2.138    by smt2+
   2.139  
   2.140  lemma
   2.141    "let P = True in P"
   2.142 -  "let P = P1 \<or> P2 in P \<or> \<not>P"
   2.143 +  "let P = P1 \<or> P2 in P \<or> \<not> P"
   2.144    "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"
   2.145    "(let x = y in x) = y"
   2.146    "(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)"
   2.147    "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)"
   2.148    "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)"
   2.149 -  "let P = (\<forall>x. Q x) in if P then P else \<not>P"
   2.150 +  "let P = (\<forall>x. Q x) in if P then P else \<not> P"
   2.151    by smt2+
   2.152  
   2.153  lemma
   2.154 @@ -185,35 +185,19 @@
   2.155  section {* Guidance for quantifier heuristics: patterns *}
   2.156  
   2.157  lemma
   2.158 -  assumes "\<forall>x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)"
   2.159 +  assumes "\<forall>x.
   2.160 +    SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x)) SMT2.Symb_Nil) SMT2.Symb_Nil)
   2.161 +    (f x = x)"
   2.162    shows "f 1 = 1"
   2.163    using assms using [[smt2_trace]] by smt2
   2.164  
   2.165  lemma
   2.166 -  assumes "\<forall>x y. SMT2.trigger [[SMT2.pat (f x), SMT2.pat (g y)]] (f x = g y)"
   2.167 +  assumes "\<forall>x y.
   2.168 +    SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x))
   2.169 +      (SMT2.Symb_Cons (SMT2.pat (g y)) SMT2.Symb_Nil)) SMT2.Symb_Nil) (f x = g y)"
   2.170    shows "f a = g b"
   2.171    using assms by smt2
   2.172  
   2.173 -lemma
   2.174 -  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (P x --> Q x)"
   2.175 -  and "P t"
   2.176 -  shows "Q t"
   2.177 -  using assms by smt2
   2.178 -
   2.179 -lemma
   2.180 -  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x), SMT2.pat (Q x)]]
   2.181 -    (P x & Q x --> R x)"
   2.182 -  and "P t" and "Q t"
   2.183 -  shows "R t"
   2.184 -  using assms by smt2
   2.185 -
   2.186 -lemma
   2.187 -  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)], [SMT2.pat (Q x)]]
   2.188 -    ((P x --> R x) & (Q x --> R x))"
   2.189 -  and "P t | Q t"
   2.190 -  shows "R t"
   2.191 -  using assms by smt2
   2.192 -
   2.193  
   2.194  section {* Meta-logical connectives *}
   2.195  
   2.196 @@ -224,9 +208,9 @@
   2.197    "P' x \<Longrightarrow> P' x"
   2.198    "P \<Longrightarrow> P \<or> Q"
   2.199    "Q \<Longrightarrow> P \<or> Q"
   2.200 -  "\<not>P \<Longrightarrow> P \<longrightarrow> Q"
   2.201 +  "\<not> P \<Longrightarrow> P \<longrightarrow> Q"
   2.202    "Q \<Longrightarrow> P \<longrightarrow> Q"
   2.203 -  "\<lbrakk>P; \<not>Q\<rbrakk> \<Longrightarrow> \<not>(P \<longrightarrow> Q)"
   2.204 +  "\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)"
   2.205    "P' x \<equiv> P' x"
   2.206    "P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x"
   2.207    "P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x"
   2.208 @@ -234,7 +218,7 @@
   2.209    "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   2.210    "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   2.211    "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
   2.212 -  "(p \<or> q) \<and> \<not>p \<Longrightarrow> q"
   2.213 +  "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   2.214    "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   2.215    by smt2+
   2.216  
   2.217 @@ -343,12 +327,12 @@
   2.218    "x < y \<longrightarrow> 3 * x < 3 * y"
   2.219    "x < y \<longrightarrow> x \<le> y"
   2.220    "(x < y) = (x + 1 \<le> y)"
   2.221 -  "\<not>(x < x)"
   2.222 +  "\<not> (x < x)"
   2.223    "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.224    "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.225    "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   2.226    "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   2.227 -  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
   2.228 +  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   2.229    by smt2+
   2.230  
   2.231  
   2.232 @@ -358,7 +342,7 @@
   2.233    "(0::int) = 0"
   2.234    "(0::int) = (- 0)"
   2.235    "(1::int) = 1"
   2.236 -  "\<not>(-1 = (1::int))"
   2.237 +  "\<not> (-1 = (1::int))"
   2.238    "(0::int) < 1"
   2.239    "(0::int) \<le> 1"
   2.240    "-123 + 345 < (567::int)"
   2.241 @@ -498,12 +482,12 @@
   2.242    "x < y \<longrightarrow> 3 * x < 3 * y"
   2.243    "x < y \<longrightarrow> x \<le> y"
   2.244    "(x < y) = (x + 1 \<le> y)"
   2.245 -  "\<not>(x < x)"
   2.246 +  "\<not> (x < x)"
   2.247    "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.248    "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.249    "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   2.250    "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   2.251 -  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
   2.252 +  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   2.253    by smt2+
   2.254  
   2.255  
   2.256 @@ -514,7 +498,7 @@
   2.257    "(0::real) = -0"
   2.258    "(0::real) = (- 0)"
   2.259    "(1::real) = 1"
   2.260 -  "\<not>(-1 = (1::real))"
   2.261 +  "\<not> (-1 = (1::real))"
   2.262    "(0::real) < 1"
   2.263    "(0::real) \<le> 1"
   2.264    "-123 + 345 < (567::real)"
   2.265 @@ -608,12 +592,12 @@
   2.266    "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   2.267    "x < y \<longrightarrow> 3 * x < 3 * y"
   2.268    "x < y \<longrightarrow> x \<le> y"
   2.269 -  "\<not>(x < x)"
   2.270 +  "\<not> (x < x)"
   2.271    "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.272    "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   2.273    "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   2.274    "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   2.275 -  "x < y \<and> y < z \<longrightarrow> \<not>(z < x)"
   2.276 +  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   2.277    by smt2+
   2.278  
   2.279  
     3.1 --- a/src/HOL/SMT_Examples/VCC_Max.certs2	Thu Jun 12 01:00:49 2014 +0200
     3.2 +++ b/src/HOL/SMT_Examples/VCC_Max.certs2	Thu Jun 12 01:00:49 2014 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -57921b560a136ca1a710a5f3b5e4e77c40b33980 2972 0
     3.5 +05a761f33f246f0fee720bec6f015ca5aba01c4d 2972 0
     3.6  unsat
     3.7  ((set-logic <null>)
     3.8  (declare-fun ?v0!14 () Int)
     3.9 @@ -114,10 +114,10 @@
    3.10  (let (($x19992 (or $x15590 $x15599 $x19474 $x19501 $x19989)))
    3.11  (let (($x19995 (not $x19992)))
    3.12  (let ((?x23404 (b_S_ref$ ?x10320)))
    3.13 -(let ((?x23225 (b_S_ptr$ b_T_T_u1$ ?x23404)))
    3.14 -(let ((?x24099 (b_S_typ$ ?x23225)))
    3.15 -(let ((?x24100 (b_S_kind_n_of$ ?x24099)))
    3.16 -(let (($x23805 (= ?x24100 b_S_kind_n_primitive$)))
    3.17 +(let ((?x23228 (b_S_ptr$ b_T_T_u1$ ?x23404)))
    3.18 +(let ((?x23728 (b_S_typ$ ?x23228)))
    3.19 +(let ((?x23730 (b_S_kind_n_of$ ?x23728)))
    3.20 +(let (($x24098 (= ?x23730 b_S_kind_n_primitive$)))
    3.21  (let ((?x21472 (b_S_kind_n_of$ b_T_T_u1$)))
    3.22  (let (($x21473 (= ?x21472 b_S_kind_n_primitive$)))
    3.23  (let (($x9768 (b_S_is_n_primitive$ b_T_T_u1$)))
    3.24 @@ -221,7 +221,7 @@
    3.25  (let ((@x24344 (unit-resolution (unit-resolution @x24337 (unit-resolution @x23870 @x19833 $x23270) $x23889) @x24343 false)))
    3.26  (let ((@x24345 (lemma @x24344 $x10321)))
    3.27  (let ((@x25031 (unit-resolution (def-axiom (or (not $x23270) $x15590 $x23242)) @x24345 (or (not $x23270) $x23242))))
    3.28 -(let (($x23227 (= ?x10320 ?x23225)))
    3.29 +(let (($x23306 (= ?x10320 ?x23228)))
    3.30  (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) )))
    3.31  ))
    3.32  (let (($x9604 (or (not $x9596) (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1))))))
    3.33 @@ -231,24 +231,24 @@
    3.34  (let ((@x9606 (rewrite (= (=> $x9596 (= ?1 (b_S_ptr$ ?0 (b_S_ref$ ?1)))) $x9604))))
    3.35  (let ((@x15336 (mp~ (mp (asserted $x9601) (quant-intro @x9606 (= $x9601 $x9607)) $x9607) (nnf-pos (refl (~ $x9604 $x9604)) (~ $x9607 $x9607)) $x9607)))
    3.36  (let (($x21994 (not $x9607)))
    3.37 -(let (($x24289 (or $x21994 $x15590 $x23227)))
    3.38 -(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)))
    3.39 -(let ((@x25262 (symm (unit-resolution @x24294 @x15336 @x24345 $x23227) (= ?x23225 ?x10320))))
    3.40 -(let ((@x24694 (trans (monotonicity @x25262 (= ?x24099 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x24099 b_T_T_u1$))))
    3.41 -(let ((@x24696 (trans (monotonicity @x24694 (= ?x24100 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x23805)))
    3.42 +(let (($x24294 (or $x21994 $x15590 $x23306)))
    3.43 +(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)))
    3.44 +(let ((@x25262 (symm (unit-resolution @x24335 @x15336 @x24345 $x23306) (= ?x23228 ?x10320))))
    3.45 +(let ((@x24694 (trans (monotonicity @x25262 (= ?x23728 ?x23241)) (unit-resolution @x25031 (unit-resolution @x23870 @x19833 $x23270) $x23242) (= ?x23728 b_T_T_u1$))))
    3.46 +(let ((@x24696 (trans (monotonicity @x24694 (= ?x23730 ?x21472)) (unit-resolution @x23544 (unit-resolution @x21484 @x15456 $x21480) $x21473) $x24098)))
    3.47  (let ((?x10272 (b_S_typemap$ v_b_S_s$)))
    3.48 -(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23225)))
    3.49 +(let ((?x24217 (b_S_select_o_tm$ ?x10272 ?x23228)))
    3.50  (let ((?x24218 (b_S_ts_n_emb$ ?x24217)))
    3.51 -(let (($x23797 (b_S_closed$ v_b_S_s$ ?x24218)))
    3.52 -(let (($x23803 (not $x23797)))
    3.53 -(let (($x23775 (b_S_ts_n_is_n_volatile$ ?x24217)))
    3.54 +(let (($x23775 (b_S_closed$ v_b_S_s$ ?x24218)))
    3.55  (let (($x23784 (not $x23775)))
    3.56 -(let (($x23804 (or $x23784 $x23803)))
    3.57 -(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))))))
    3.58 -(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23775))))
    3.59 -(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23784))))
    3.60 -(let ((?x23101 (b_S_select_o_tm$ ?x10272 ?x10320)))
    3.61 -(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23101)))
    3.62 +(let (($x23805 (b_S_ts_n_is_n_volatile$ ?x24217)))
    3.63 +(let (($x23770 (not $x23805)))
    3.64 +(let (($x23797 (or $x23770 $x23784)))
    3.65 +(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))))))
    3.66 +(let ((@x24702 (symm @x24686 (= (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320)) $x23805))))
    3.67 +(let ((@x24701 (monotonicity @x24702 (= (not (b_S_ts_n_is_n_volatile$ (b_S_select_o_tm$ ?x10272 ?x10320))) $x23770))))
    3.68 +(let ((?x23124 (b_S_select_o_tm$ ?x10272 ?x10320)))
    3.69 +(let (($x23361 (b_S_ts_n_is_n_volatile$ ?x23124)))
    3.70  (let (($x23297 (not $x23361)))
    3.71  (let (($x23362 (or $x15593 $x23361)))
    3.72  (let (($x23363 (not $x23362)))
    3.73 @@ -399,7 +399,7 @@
    3.74  (let (($x19313 (or $x19297 $x19298 $x15525 $x15533)))
    3.75  (let (($x20589 (not $x15533)))
    3.76  (let (($x19318 (not $x19313)))
    3.77 -(let ((@x24016 (hypothesis $x19318)))
    3.78 +(let ((@x23991 (hypothesis $x19318)))
    3.79  (let (($x10141 (b_S_thread_n_local$ v_b_S_s$ ?x10137)))
    3.80  (let ((?x21175 (b_S_typ$ ?x10078)))
    3.81  (let ((?x22803 (b_S_kind_n_of$ ?x21175)))
    3.82 @@ -439,7 +439,7 @@
    3.83  (let ((@x22576 (trans (monotonicity @x22567 (= (or $x22568 $x22543) $x22569)) (rewrite (= $x22569 $x22569)) (= (or $x22568 $x22543) $x22569))))
    3.84  (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)))
    3.85  (let ((@x22581 (def-axiom (or $x22562 $x22556))))
    3.86 -(let ((@x24124 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556)))
    3.87 +(let ((@x24189 (unit-resolution @x22581 (lemma (unit-resolution @x22577 @x18183 (hypothesis $x22562) false) $x22565) $x22556)))
    3.88  (let (($x21179 (= ?x10079 v_b_P_H_arr$)))
    3.89  (let (($x19835 (forall ((?v0 B_S_ctype$) (?v1 Int) )(!(= (b_S_ref$ (b_S_ptr$ ?v0 ?v1)) ?v1) :pattern ( (b_S_ptr$ ?v0 ?v1) )))
    3.90  ))
    3.91 @@ -453,12 +453,12 @@
    3.92  (let ((@x21185 ((_ quant-inst b_T_T_u1$ v_b_P_H_arr$) $x21184)))
    3.93  (let ((@x24511 (unit-resolution @x21185 @x19840 $x21179)))
    3.94  (let ((@x22852 (monotonicity @x24511 (= ?x22553 ?x10078))))
    3.95 -(let ((@x24070 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079))))
    3.96 -(let ((@x22338 (symm (monotonicity (trans @x24070 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505))))
    3.97 +(let ((@x24073 (monotonicity (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) (= ?x22485 ?x10079))))
    3.98 +(let ((@x22338 (symm (monotonicity (trans @x24073 @x24511 (= ?x22485 v_b_P_H_arr$)) (= ?x22505 ?x10078)) (= ?x10078 ?x22505))))
    3.99  (let ((@x22340 (unit-resolution (hypothesis (not $x22506)) (trans (trans (hypothesis $x22556) @x22852 (= ?x10137 ?x10078)) @x22338 $x22506) false)))
   3.100 -(let ((@x23350 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24124 $x22506)))
   3.101 -(let ((@x23663 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x10078 ?x10137))))
   3.102 -(let ((@x22940 (trans (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23350 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478))))
   3.103 +(let ((@x23667 (unit-resolution (lemma @x22340 (or $x22559 $x22506)) @x24189 $x22506)))
   3.104 +(let ((@x23699 (trans (symm @x22852 (= ?x10078 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x10078 ?x10137))))
   3.105 +(let ((@x22940 (trans (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (symm (monotonicity @x23667 (= ?x22478 ?x22655)) (= ?x22655 ?x22478)) (= ?x22818 ?x22478))))
   3.106  (let ((@x23082 (symm (monotonicity @x22940 (= $x22902 (b_S_ts_n_is_n_volatile$ ?x22478))) (= (b_S_ts_n_is_n_volatile$ ?x22478) $x22902))))
   3.107  (let (($x22602 (b_S_ts_n_is_n_volatile$ ?x22478)))
   3.108  (let (($x22641 (not $x22602)))
   3.109 @@ -1364,7 +1364,7 @@
   3.110  (let ((@x22613 ((_ quant-inst v_b_S_s$ (b_S_ptr$ ?x10076 ?x21014) (b_S_ptr$ ?x10076 ?x21014) b_l_H_public$) $x22612)))
   3.111  (let (($x35 (= b_S_kind_n_primitive$ b_S_kind_n_array$)))
   3.112  (let (($x36 (not $x35)))
   3.113 -(let (($x22500 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$)))))
   3.114 +(let (($x22488 (= $x36 (not (= (b_S_kind_n_of$ (b_S_typ$ ?x21983)) b_S_kind_n_primitive$)))))
   3.115  (let ((?x22234 (b_S_typ$ ?x21983)))
   3.116  (let ((?x22387 (b_S_kind_n_of$ ?x22234)))
   3.117  (let (($x22388 (= ?x22387 b_S_kind_n_primitive$)))
   3.118 @@ -1404,7 +1404,7 @@
   3.119  (let ((@x22414 (trans (monotonicity @x24520 (= ?x22234 ?x21180)) (unit-resolution @x21189 @x19846 $x21183) (= ?x22234 ?x10076))))
   3.120  (let ((@x22418 (trans (monotonicity @x22414 (= ?x22387 ?x10086)) (unit-resolution @x22406 (unit-resolution @x22160 @x15446 $x22149) $x22148) (= ?x22387 b_S_kind_n_array$))))
   3.121  (let ((@x22857 (monotonicity @x22418 (= $x22388 (= b_S_kind_n_array$ b_S_kind_n_primitive$)))))
   3.122 -(let ((@x22934 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35))))
   3.123 +(let ((@x22500 (trans @x22857 (commutativity (= (= b_S_kind_n_array$ b_S_kind_n_primitive$) $x35)) (= $x22388 $x35))))
   3.124  (let (($x41 (= b_S_kind_n_thread$ b_S_kind_n_array$)))
   3.125  (let (($x42 (not $x41)))
   3.126  (let (($x39 (= b_S_kind_n_composite$ b_S_kind_n_array$)))
   3.127 @@ -1431,10 +1431,10 @@
   3.128  (let ((@x22935 (monotonicity (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) (= $x11221 $x22336))))
   3.129  (let ((@x22938 (unit-resolution (def-axiom (or (not $x22326) $x22317 $x22333)) (mp (hypothesis $x11221) @x22935 $x22336) (unit-resolution @x22613 @x15021 $x22326) $x22333)))
   3.130  (let (($x22368 (b_S_is$ ?x21983 ?x22234)))
   3.131 -(let ((@x22898 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368)))
   3.132 +(let ((@x22885 (mp @x12044 (symm (monotonicity @x24520 @x22414 (= $x22368 $x10084)) (= $x10084 $x22368)) $x22368)))
   3.133  (let (($x22385 (b_S_typed$ v_b_S_s$ ?x21983)))
   3.134  (let ((@x12045 (and-elim @x12033 $x10085)))
   3.135 -(let ((@x22886 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385)))
   3.136 +(let ((@x22517 (mp @x12045 (symm (monotonicity @x24520 (= $x22385 $x10085)) (= $x10085 $x22385)) $x22385)))
   3.137  (let ((?x22243 (b_S_owner$ v_b_S_s$ ?x21983)))
   3.138  (let (($x22259 (= ?x22243 b_S_me$)))
   3.139  (let ((@x12043 (and-elim @x12033 $x10083)))
   3.140 @@ -1540,11 +1540,11 @@
   3.141  (let (($x22386 (not $x22385)))
   3.142  (let (($x22384 (not $x22368)))
   3.143  (let (($x24309 (or (not $x18905) $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)))
   3.144 -(let (($x24492 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309)))
   3.145 +(let (($x22614 (= (or (not $x18905) (or $x19677 $x22272 (not $x22259) $x22384 $x22386 $x22388 $x22242 $x22318)) $x24309)))
   3.146  (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)))))
   3.147 -(let ((@x24084 (mp @x24028 (rewrite $x24492) $x24309)))
   3.148 -(let ((@x22410 (unit-resolution @x24084 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318))))
   3.149 -(let ((@x22411 (unit-resolution @x22410 @x22886 @x22898 @x22938 (mp @x75 (monotonicity (symm @x22934 (= $x35 $x22388)) $x22500) (not $x22388)) false)))
   3.150 +(let ((@x24070 (mp @x24028 (rewrite $x22614) $x24309)))
   3.151 +(let ((@x22410 (unit-resolution @x24070 @x18908 @x12050 @x22409 @x22429 (trans (monotonicity @x24520 (= ?x22243 ?x10082)) @x12043 $x22259) (or $x22384 $x22386 $x22388 $x22318))))
   3.152 +(let ((@x22411 (unit-resolution @x22410 @x22517 @x22885 @x22938 (mp @x75 (monotonicity (symm @x22500 (= $x35 $x22388)) $x22488) (not $x22388)) false)))
   3.153  (let ((@x22434 (lemma @x22411 $x10136)))
   3.154  (let ((@x22687 (mp @x22434 (symm (monotonicity @x24520 @x24520 (= $x22317 $x10136)) (= $x10136 $x22317)) $x22317)))
   3.155  (let ((@x22688 (unit-resolution (def-axiom (or (not $x22326) $x22336 $x22318)) @x22687 (unit-resolution @x22613 @x15021 $x22326) $x22318)))
   3.156 @@ -1894,10 +1894,10 @@
   3.157  (let (($x23521 (or (not $x19072) $x22944)))
   3.158  (let ((@x23524 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$)) $x23521)))
   3.159  (let (($x23055 (not $x22801)))
   3.160 -(let ((@x23295 (monotonicity (symm (monotonicity @x23663 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055))))
   3.161 +(let ((@x23295 (monotonicity (symm (monotonicity @x23699 (= $x22801 $x10141)) (= $x10141 $x22801)) (= (not $x10141) $x23055))))
   3.162  (let ((@x23090 (unit-resolution (def-axiom (or (not $x22944) $x22801 $x22939)) (mp (hypothesis (not $x10141)) @x23295 $x23055) (unit-resolution @x23524 @x19075 $x22944) $x22939)))
   3.163 -(let ((@x23670 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23663 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799)))
   3.164 -(let ((@x23233 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23670 @x23090 $x22923) $x22900)))
   3.165 +(let ((@x23706 (mp (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) (symm (monotonicity @x23699 (= $x22799 $x10139)) (= $x10139 $x22799)) $x22799)))
   3.166 +(let ((@x23222 (unit-resolution (def-axiom (or $x22921 $x22900)) (unit-resolution (def-axiom (or $x22943 $x22802 $x22923)) @x23706 @x23090 $x22923) $x22900)))
   3.167  (let ((?x24419 (b_S_ref$ ?x21983)))
   3.168  (let ((?x24433 (b_S_ptr$ b_T_T_u1$ ?x24419)))
   3.169  (let ((?x24410 (b_S_idx$ ?x21983 0 b_T_T_u1$)))
   3.170 @@ -2016,13 +2016,13 @@
   3.171  (let ((@x14355 (mp~ (mp (asserted $x6917) @x6947 $x6943) (nnf-pos (refl (~ $x6940 $x6940)) (~ $x6943 $x6943)) $x6943)))
   3.172  (let ((@x17967 (mp @x14355 @x17966 $x17964)))
   3.173  (let (($x24241 (not $x24240)))
   3.174 -(let (($x23110 (not $x17964)))
   3.175 -(let (($x24183 (or $x23110 $x24241 $x11259 $x23791)))
   3.176 +(let (($x23252 (not $x17964)))
   3.177 +(let (($x23749 (or $x23252 $x24241 $x11259 $x23791)))
   3.178  (let (($x23792 (or $x24241 $x22599 $x22601 $x23791)))
   3.179 -(let (($x24184 (or $x23110 $x23792)))
   3.180 -(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)))))
   3.181 -(let ((@x23705 (trans (monotonicity @x23271 (= $x24184 (or $x23110 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23110 (or $x24241 $x11259 $x23791)) $x24183)) (= $x24184 $x24183))))
   3.182 -(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)))
   3.183 +(let (($x23750 (or $x23252 $x23792)))
   3.184 +(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)))))
   3.185 +(let ((@x23352 (trans (monotonicity @x23251 (= $x23750 (or $x23252 (or $x24241 $x11259 $x23791)))) (rewrite (= (or $x23252 (or $x24241 $x11259 $x23791)) $x23749)) (= $x23750 $x23749))))
   3.186 +(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)))
   3.187  (let (($x21186 (= ?x21014 ?x10079)))
   3.188  (let (($x21191 (or $x21152 $x21186)))
   3.189  (let ((@x21192 ((_ quant-inst (b_S_array$ b_T_T_u1$ v_b_P_H_len$) (b_S_ref$ ?x10078)) $x21191)))
   3.190 @@ -2030,19 +2030,19 @@
   3.191  (let ((@x24532 (trans @x24530 (unit-resolution @x22000 @x15336 @x12044 $x21990) (= ?x22595 ?x21983))))
   3.192  (let ((@x23632 (trans (monotonicity @x24532 (= ?x24245 ?x24410)) (hypothesis $x24436) (= ?x24245 ?x24433))))
   3.193  (let ((@x23628 (trans @x23632 (monotonicity (trans @x24524 @x24511 (= ?x24419 v_b_P_H_arr$)) (= ?x24433 ?x10078)) (= ?x24245 ?x10078))))
   3.194 -(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24124 (= ?x22553 ?x10137)) (= ?x24245 ?x10137))))
   3.195 -(let ((@x23636 (symm (monotonicity (trans @x23622 @x23350 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246))))
   3.196 -(let ((@x23256 (monotonicity (monotonicity (trans @x23663 @x23350 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655)))))
   3.197 -(let ((@x23678 (trans @x23256 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247))))
   3.198 -(let ((@x23865 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23755 $x23791) $x24248) (= ?x22903 ?x22595))))
   3.199 -(let ((@x23912 (trans (monotonicity (trans @x23865 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888)))
   3.200 +(let ((@x23622 (trans (trans @x23628 (symm @x22852 (= ?x10078 ?x22553)) (= ?x24245 ?x22553)) (symm @x24189 (= ?x22553 ?x10137)) (= ?x24245 ?x10137))))
   3.201 +(let ((@x23636 (symm (monotonicity (trans @x23622 @x23667 (= ?x24245 ?x22505)) (= ?x24246 ?x22655)) (= ?x22655 ?x24246))))
   3.202 +(let ((@x23746 (monotonicity (monotonicity (trans @x23699 @x23667 (= ?x10078 ?x22505)) (= ?x22818 ?x22655)) (= ?x22903 (b_S_ts_n_emb$ ?x22655)))))
   3.203 +(let ((@x23678 (trans @x23746 (monotonicity @x23636 (= (b_S_ts_n_emb$ ?x22655) ?x24247)) (= ?x22903 ?x24247))))
   3.204 +(let ((@x23867 (trans @x23678 (unit-resolution (def-axiom (or $x23737 $x24248)) (lemma @x23658 $x23791) $x24248) (= ?x22903 ?x22595))))
   3.205 +(let ((@x23912 (trans (monotonicity (trans @x23867 @x24530 (= ?x22903 ?x10080)) (= ?x22893 ?x10082)) @x12043 $x22888)))
   3.206  (let ((@x24132 (lemma (unit-resolution (hypothesis (not $x22888)) @x23912 false) (or $x24439 $x22888))))
   3.207  (let ((@x23115 (unit-resolution @x24132 (unit-resolution @x24460 (lemma @x24133 $x24445) $x24436) $x22888)))
   3.208  (let ((?x22658 (b_S_ts_n_emb$ ?x22655)))
   3.209  (let ((?x22663 (b_S_typ$ ?x22658)))
   3.210  (let ((?x22664 (b_S_kind_n_of$ ?x22663)))
   3.211  (let (($x22665 (= ?x22664 b_S_kind_n_primitive$)))
   3.212 -(let ((@x23071 (monotonicity (monotonicity (symm @x23256 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891))))
   3.213 +(let ((@x23071 (monotonicity (monotonicity (symm @x23746 (= ?x22658 ?x22903)) (= ?x22663 ?x22890)) (= ?x22664 ?x22891))))
   3.214  (let (($x22946 (b_S_is_n_non_n_primitive$ ?x22663)))
   3.215  (let (($x23237 (not $x22946)))
   3.216  (let (($x23503 (or $x22665 $x23237)))
   3.217 @@ -2063,8 +2063,8 @@
   3.218  (let ((@x23058 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x22505)) $x23057)))
   3.219  (let ((@x23584 (unit-resolution (def-axiom (or $x23503 (not $x22665))) (unit-resolution @x23058 @x19237 $x23504) (not $x22665))))
   3.220  (let ((@x23060 (lemma (unit-resolution @x23584 (trans @x23071 (hypothesis $x22892) $x22665) false) (not $x22892))))
   3.221 -(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))))
   3.222 -(let ((@x23406 (unit-resolution @x23231 @x23233 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false)))
   3.223 +(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))))
   3.224 +(let ((@x23406 (unit-resolution @x23221 @x23222 (unit-resolution (def-axiom (or $x22906 $x22902)) @x23294 $x22906) @x23076 false)))
   3.225  (let ((@x23403 (lemma @x23406 $x10141)))
   3.226  (let (($x20092 (or $x19318 $x20089)))
   3.227  (let (($x20095 (not $x20092)))
   3.228 @@ -2618,19 +2618,19 @@
   3.229  (let ((@x13510 (monotonicity (monotonicity @x13504 (= $x12021 (and $x10136 $x13502))) (= (not $x12021) $x13508))))
   3.230  (let ((@x13511 (mp (not-or-elim (mp (asserted $x10434) @x12031 $x12027) (not $x12021)) @x13510 $x13508)))
   3.231  (let ((@x20143 (mp (mp (mp (mp~ @x13511 @x15835 $x15833) @x16117 $x16115) @x19763 $x19761) (monotonicity @x20139 (= $x19761 $x20140)) $x20140)))
   3.232 -(let ((@x24002 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128)))
   3.233 +(let ((@x24008 (unit-resolution (def-axiom (or $x20134 $x20128)) (unit-resolution @x20143 @x22434 $x20137) $x20128)))
   3.234  (let ((?x22514 (b_S_typ$ ?x10137)))
   3.235  (let (($x22515 (= ?x22514 b_T_T_u1$)))
   3.236  (let ((@x22856 (trans (unit-resolution @x22581 (unit-resolution @x22577 @x18183 $x22565) $x22556) @x22852 (= ?x10137 ?x10078))))
   3.237  (let ((@x22875 (trans (monotonicity @x22856 (= ?x22514 ?x21175)) (unit-resolution @x21182 @x19846 $x21176) $x22515)))
   3.238 -(let (($x22507 (not $x22515)))
   3.239 +(let (($x22932 (not $x22515)))
   3.240  (let (($x22522 (= $x10138 $x22515)))
   3.241 -(let (($x22949 (or $x22002 $x22522)))
   3.242 -(let ((@x22487 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22949)))
   3.243 -(let ((@x22509 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22507)) (hypothesis $x15502) (or (not $x22522) $x22507))))
   3.244 -(let ((@x22873 (unit-resolution (unit-resolution @x22509 (unit-resolution @x22487 @x19833 $x22522) $x22507) @x22875 false)))
   3.245 +(let (($x22487 (or $x22002 $x22522)))
   3.246 +(let ((@x22492 ((_ quant-inst (b_S_idx$ ?x10078 0 b_T_T_u1$) b_T_T_u1$) $x22487)))
   3.247 +(let ((@x22511 (unit-resolution (def-axiom (or (not $x22522) $x10138 $x22932)) (hypothesis $x15502) (or (not $x22522) $x22932))))
   3.248 +(let ((@x22873 (unit-resolution (unit-resolution @x22511 (unit-resolution @x22492 @x19833 $x22522) $x22932) @x22875 false)))
   3.249  (let ((@x22876 (lemma @x22873 $x10138)))
   3.250 -(let ((@x23964 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24002 $x20125)))
   3.251 +(let ((@x24016 (unit-resolution (def-axiom (or $x20131 $x15502 $x15505 $x20125)) (unit-resolution (def-axiom (or $x22603 $x10139)) @x22760 $x10139) @x22876 @x24008 $x20125)))
   3.252  (let ((?x22963 (* (- 1) ?x10144)))
   3.253  (let ((?x22964 (+ v_b_L_H_max_G_0$ ?x22963)))
   3.254  (let (($x22965 (>= ?x22964 0)))
   3.255 @@ -2652,9 +2652,9 @@
   3.256  (let ((@x23011 (symm (unit-resolution @x22447 @x15336 (hypothesis $x10138) $x22506) (= ?x22505 ?x10137))))
   3.257  (let ((@x23020 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x22834) $x22839)) (symm (monotonicity @x23011 (= ?x22685 ?x10144)) $x22834) $x22839)))
   3.258  (let ((@x23023 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) @x23020 @x23010 (hypothesis $x20589) @x23016 false) (or $x15502 $x15533 $x19297 $x15525 $x15511 $x20119))))
   3.259 -(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15533 $x19297 $x15525 $x15511))))
   3.260 -(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)))
   3.261 -(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x23964 $x20116) (or $x15511 $x20113))))
   3.262 +(let ((@x24012 (unit-resolution @x23023 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15533 $x19297 $x15525 $x15511))))
   3.263 +(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)))
   3.264 +(let ((@x24417 (unit-resolution @x20962 @x22876 (unit-resolution (def-axiom (or $x20122 $x20116)) @x24016 $x20116) (or $x15511 $x20113))))
   3.265  (let ((@x24506 (unit-resolution (def-axiom (or $x20110 $x20104)) (unit-resolution @x24417 @x23403 $x20113) $x20104)))
   3.266  (let ((@x24507 (unit-resolution (def-axiom (or $x20107 $x11385 $x20101)) (lemma ((_ th-lemma arith farkas 1 1) @x12041 (hypothesis $x11385) false) $x11382) @x24506 $x20101)))
   3.267  (let ((@x24462 (unit-resolution (def-axiom (or $x20095 $x19318 $x20089)) (unit-resolution (def-axiom (or $x20098 $x20092)) @x24507 $x20092) $x20092)))
   3.268 @@ -2710,8 +2710,8 @@
   3.269  (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)))
   3.270  (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)))
   3.271  (let ((@x24502 (unit-resolution (def-axiom (or $x20071 $x20019 $x20065)) (unit-resolution (def-axiom (or $x20074 $x20068)) @x24583 $x20068) @x24500 $x20019)))
   3.272 -(let ((@x24684 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487)))
   3.273 -(let ((@x24741 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596)))
   3.274 +(let ((@x24656 (unit-resolution (def-axiom (or $x20016 $x11487)) @x24502 $x11487)))
   3.275 +(let ((@x24896 (mp @x22691 (symm (monotonicity @x24532 (= $x22596 $x22344)) (= $x22344 $x22596)) $x22596)))
   3.276  (let ((@x23420 (hypothesis $x11487)))
   3.277  (let (($x23378 (or $x22629 $x19677 $x21489 $x22597 $x19670 $x11486 $x23363)))
   3.278  (let (($x23360 (>= (+ v_b_L_H_p_G_0$ (* (- 1) v_b_P_H_len$)) 0)))
   3.279 @@ -2725,42 +2725,42 @@
   3.280  (let ((@x23387 (trans @x23383 (rewrite (= (or $x22629 (or $x19677 $x21489 $x22597 $x19670 $x11486 $x23363)) $x23378)) (= $x23379 $x23378))))
   3.281  (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)))
   3.282  (let ((@x23422 (unit-resolution @x23388 @x18670 @x9769 @x12050 (hypothesis $x11901) @x23420 (hypothesis $x22596) (hypothesis $x23362) false)))
   3.283 -(let ((@x24788 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24741 (or $x23363 $x19670 $x11486))))
   3.284 -(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x23297)))
   3.285 +(let ((@x24759 (unit-resolution (lemma @x23422 (or $x23363 $x19670 $x11486 $x22597)) @x24896 (or $x23363 $x19670 $x11486))))
   3.286 +(let ((@x24697 (unit-resolution (def-axiom (or $x23362 $x23297)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x23297)))
   3.287  (let (($x23782 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x24218)))
   3.288  (let ((?x23727 (b_S_owner$ v_b_S_s$ ?x24218)))
   3.289  (let (($x23776 (= ?x23727 b_S_me$)))
   3.290  (let (($x23785 (or $x23776 $x23782)))
   3.291  (let (($x24475 (not $x23785)))
   3.292 -(let ((?x23730 (b_S_typ$ ?x24218)))
   3.293 -(let ((?x23768 (b_S_kind_n_of$ ?x23730)))
   3.294 +(let ((?x23804 (b_S_typ$ ?x24218)))
   3.295 +(let ((?x23768 (b_S_kind_n_of$ ?x23804)))
   3.296  (let (($x23769 (= ?x23768 b_S_kind_n_primitive$)))
   3.297 -(let (($x23728 (not $x23804)))
   3.298 -(let (($x23770 (not $x23805)))
   3.299 -(let (($x24476 (or $x23770 $x23728 $x23769 $x24475)))
   3.300 -(let (($x24627 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23225)))
   3.301 -(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23225) b_S_me$)))
   3.302 -(let (($x24943 (or $x24478 $x24627)))
   3.303 -(let (($x25004 (not $x24943)))
   3.304 -(let (($x24820 (or $x23805 $x25004)))
   3.305 -(let (($x24623 (not $x24820)))
   3.306 +(let (($x23803 (not $x23797)))
   3.307 +(let (($x24099 (not $x24098)))
   3.308 +(let (($x24476 (or $x24099 $x23803 $x23769 $x24475)))
   3.309 +(let (($x24604 (b_S_in_n_wrapped_n_domain$ v_b_S_s$ ?x23228)))
   3.310 +(let (($x24478 (= (b_S_owner$ v_b_S_s$ ?x23228) b_S_me$)))
   3.311 +(let (($x24602 (or $x24478 $x24604)))
   3.312 +(let (($x24797 (not $x24602)))
   3.313 +(let (($x24820 (or $x24098 $x24797)))
   3.314 +(let (($x24655 (not $x24820)))
   3.315  (let (($x24474 (not $x24476)))
   3.316 -(let (($x24809 (or $x24474 $x24623)))
   3.317 -(let (($x24810 (not $x24809)))
   3.318 -(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23225)))
   3.319 +(let (($x24912 (or $x24474 $x24655)))
   3.320 +(let (($x24913 (not $x24912)))
   3.321 +(let (($x24209 (b_S_typed$ v_b_S_s$ ?x23228)))
   3.322  (let (($x24210 (not $x24209)))
   3.323 -(let (($x24817 (or $x24210 $x24810)))
   3.324 -(let (($x24818 (not $x24817)))
   3.325 -(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23225)))
   3.326 -(let (($x24819 (= $x23783 $x24818)))
   3.327 -(let (($x24622 (or (not $x19072) $x24819)))
   3.328 -(let ((@x24633 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622)))
   3.329 +(let (($x24931 (or $x24210 $x24913)))
   3.330 +(let (($x24932 (not $x24931)))
   3.331 +(let (($x23783 (b_S_thread_n_local$ v_b_S_s$ ?x23228)))
   3.332 +(let (($x24934 (= $x23783 $x24932)))
   3.333 +(let (($x24622 (or (not $x19072) $x24934)))
   3.334 +(let ((@x24172 ((_ quant-inst v_b_S_s$ (b_S_ptr$ b_T_T_u1$ ?x23404)) $x24622)))
   3.335  (let (($x24628 (not $x23783)))
   3.336  (let ((@x24670 (monotonicity (symm (monotonicity @x25262 (= $x23783 $x10324)) (= $x10324 $x23783)) (= $x15599 $x24628))))
   3.337 -(let ((@x24708 (unit-resolution (def-axiom (or (not $x24819) $x23783 $x24817)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24633 @x19075 $x24819) $x24817)))
   3.338 -(let ((@x24998 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24788 @x24684 @x24576 $x23363) $x10322)))
   3.339 -(let ((@x24710 (mp @x24998 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209)))
   3.340 -(let ((@x24724 (unit-resolution (def-axiom (or $x24809 $x24476)) (unit-resolution (def-axiom (or $x24818 $x24210 $x24810)) @x24710 @x24708 $x24810) $x24476)))
   3.341 +(let ((@x24708 (unit-resolution (def-axiom (or (not $x24934) $x23783 $x24931)) (mp (hypothesis $x15599) @x24670 $x24628) (unit-resolution @x24172 @x19075 $x24934) $x24931)))
   3.342 +(let ((@x24785 (unit-resolution (def-axiom (or $x23362 $x10322)) (unit-resolution @x24759 @x24656 @x24576 $x23363) $x10322)))
   3.343 +(let ((@x24710 (mp @x24785 (symm (monotonicity @x25262 (= $x24209 $x10322)) (= $x10322 $x24209)) $x24209)))
   3.344 +(let ((@x24724 (unit-resolution (def-axiom (or $x24912 $x24476)) (unit-resolution (def-axiom (or $x24932 $x24210 $x24913)) @x24710 @x24708 $x24913) $x24476)))
   3.345  (let ((?x24320 (b_S_idx$ ?x22595 v_b_L_H_p_G_0$ b_T_T_u1$)))
   3.346  (let ((?x24321 (b_S_select_o_tm$ ?x10272 ?x24320)))
   3.347  (let ((?x24322 (b_S_ts_n_emb$ ?x24321)))
   3.348 @@ -2771,12 +2771,12 @@
   3.349  (let (($x24324 (not $x24323)))
   3.350  (let (($x24330 (or $x24324 $x24325 (not (b_S_ts_n_is_n_array_n_elt$ ?x24321)) $x24329)))
   3.351  (let (($x24331 (not $x24330)))
   3.352 -(let (($x25071 (or $x23110 $x24241 $x19670 $x11486 $x24331)))
   3.353 +(let (($x25071 (or $x23252 $x24241 $x19670 $x11486 $x24331)))
   3.354  (let (($x24332 (or $x24241 $x19670 $x23360 $x24331)))
   3.355 -(let (($x25072 (or $x23110 $x24332)))
   3.356 +(let (($x25072 (or $x23252 $x24332)))
   3.357  (let ((@x25070 (monotonicity (trans @x23370 @x23372 (= $x23360 $x11486)) (= $x24332 (or $x24241 $x19670 $x11486 $x24331)))))
   3.358 -(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23110 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23110 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071))))
   3.359 -(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)))
   3.360 +(let ((@x25080 (trans (monotonicity @x25070 (= $x25072 (or $x23252 (or $x24241 $x19670 $x11486 $x24331)))) (rewrite (= (or $x23252 (or $x24241 $x19670 $x11486 $x24331)) $x25071)) (= $x25072 $x25071))))
   3.361 +(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)))
   3.362  (let ((@x25083 (def-axiom (or $x24330 $x24323))))
   3.363  (let ((?x24315 (b_S_ref$ ?x24198)))
   3.364  (let ((?x24367 (* (- 1) ?x24315)))
   3.365 @@ -2795,15 +2795,15 @@
   3.366  (let ((?x25227 (* (- 1) ?x24925)))
   3.367  (let ((?x25228 (+ ?x24174 ?x25227)))
   3.368  (let (($x25229 (<= ?x25228 0)))
   3.369 -(let ((?x23747 (* (- 1) ?x21014)))
   3.370 -(let ((?x23641 (+ ?x10079 ?x23747)))
   3.371 -(let (($x24296 (<= ?x23641 0)))
   3.372 -(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24296)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24296)))
   3.373 +(let ((?x24127 (* (- 1) ?x21014)))
   3.374 +(let ((?x23641 (+ ?x10079 ?x24127)))
   3.375 +(let (($x24104 (<= ?x23641 0)))
   3.376 +(let ((@x25085 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x24104)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x24104)))
   3.377  (let ((?x25173 (* (- 1) ?x24419)))
   3.378  (let ((?x25174 (+ ?x21014 ?x25173)))
   3.379  (let (($x25175 (<= ?x25174 0)))
   3.380  (let ((@x25090 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x21014 ?x24419)) $x25175)) (symm (monotonicity @x24520 (= ?x24419 ?x21014)) (= ?x21014 ?x24419)) $x25175)))
   3.381 -(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24296) (not $x25175))) @x25090 @x25085 $x25229)))
   3.382 +(let ((@x25103 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x25229 (not $x24104) (not $x25175))) @x25090 @x25085 $x25229)))
   3.383  (let (($x25230 (>= ?x25228 0)))
   3.384  (let (($x23809 (>= ?x23641 0)))
   3.385  (let ((@x25106 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x10079 ?x21014)) $x23809)) (symm (unit-resolution @x21192 @x19840 $x21186) (= ?x10079 ?x21014)) $x23809)))
   3.386 @@ -2829,54 +2829,54 @@
   3.387  (let ((@x25162 (monotonicity (monotonicity @x25154 (= $x24471 $x25155)) (= (or $x22568 $x24471) $x25158))))
   3.388  (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)))
   3.389  (let ((@x25257 (unit-resolution (def-axiom (or $x25152 $x25146)) (unit-resolution @x25166 @x18183 $x25155) $x25146)))
   3.390 -(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23225)) (= ?x24320 ?x23225))))
   3.391 -(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23101)) (= ?x23101 ?x24321))))
   3.392 -(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23101)) (= ?x24218 (b_S_ts_n_emb$ ?x23101)))))
   3.393 -(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23101) ?x24322)) (= ?x24218 ?x24322))))
   3.394 +(let ((@x25185 (trans (trans (monotonicity @x24532 (= ?x24320 ?x24463)) @x25257 (= ?x24320 ?x24930)) (monotonicity @x25183 (= ?x24930 ?x23228)) (= ?x24320 ?x23228))))
   3.395 +(let ((@x25217 (symm (monotonicity (trans @x25185 @x25262 (= ?x24320 ?x10320)) (= ?x24321 ?x23124)) (= ?x23124 ?x24321))))
   3.396 +(let ((@x25274 (monotonicity (monotonicity @x25262 (= ?x24217 ?x23124)) (= ?x24218 (b_S_ts_n_emb$ ?x23124)))))
   3.397 +(let ((@x25219 (trans @x25274 (monotonicity @x25217 (= (b_S_ts_n_emb$ ?x23124) ?x24322)) (= ?x24218 ?x24322))))
   3.398  (let ((@x25221 (trans (trans @x25219 (hypothesis $x24323) (= ?x24218 ?x22595)) @x24530 (= ?x24218 ?x10080))))
   3.399  (let ((@x25293 (unit-resolution (hypothesis (not $x23776)) (trans (monotonicity @x25221 (= ?x23727 ?x10082)) @x12043 $x23776) false)))
   3.400 -(let ((@x23976 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776)))
   3.401 -(let ((?x23443 (b_S_ts_n_emb$ ?x23101)))
   3.402 +(let ((@x24057 (unit-resolution (lemma @x25293 (or $x24324 $x23776)) (unit-resolution @x25083 (lemma @x25137 $x24331) $x24323) $x23776)))
   3.403 +(let ((?x23443 (b_S_ts_n_emb$ ?x23124)))
   3.404  (let ((?x23448 (b_S_typ$ ?x23443)))
   3.405  (let ((?x23449 (b_S_kind_n_of$ ?x23448)))
   3.406  (let (($x23450 (= ?x23449 b_S_kind_n_primitive$)))
   3.407 -(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23730)) (= ?x23449 ?x23768))))
   3.408 +(let ((@x24651 (monotonicity (monotonicity (symm @x25274 (= ?x23443 ?x24218)) (= ?x23448 ?x23804)) (= ?x23449 ?x23768))))
   3.409  (let (($x23598 (b_S_is_n_non_n_primitive$ ?x23448)))
   3.410  (let (($x23599 (not $x23598)))
   3.411  (let (($x23602 (or $x23450 $x23599)))
   3.412  (let (($x23603 (not $x23602)))
   3.413  (let (($x24666 (or (not $x19234) $x23603)))
   3.414 -(let ((@x24631 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666)))
   3.415 -(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24631 @x19237 $x23603) (not $x23450))))
   3.416 +(let ((@x24626 ((_ quant-inst (b_S_select_o_tm$ ?x10272 ?x10320)) $x24666)))
   3.417 +(let ((@x24965 (unit-resolution (def-axiom (or $x23602 (not $x23450))) (unit-resolution @x24626 @x19237 $x23603) (not $x23450))))
   3.418  (let ((@x24645 (lemma (unit-resolution @x24965 (trans @x24651 (hypothesis $x23769) $x23450) false) (not $x23769))))
   3.419 -(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))))
   3.420 -(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23804 $x23775)) (mp @x24697 @x24701 $x23784) $x23804) @x24696 false)))
   3.421 +(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))))
   3.422 +(let ((@x24717 (unit-resolution @x24718 @x24724 (unit-resolution (def-axiom (or $x23797 $x23805)) (mp @x24697 @x24701 $x23770) $x23797) @x24696 false)))
   3.423  (let ((@x20784 (def-axiom (or $x20013 $x15590 $x15593 $x20007))))
   3.424 -(let ((@x24650 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24998 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007)))
   3.425 +(let ((@x24630 (unit-resolution (unit-resolution @x20784 @x24345 (or $x20013 $x15593 $x20007)) @x24785 (unit-resolution (def-axiom (or $x20016 $x20010)) @x24502 $x20010) $x20007)))
   3.426  (let ((@x20774 (def-axiom (or $x20004 $x19998))))
   3.427  (let ((@x20768 (def-axiom (or $x20001 $x15590 $x15599 $x19995))))
   3.428 -(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24650 $x19998) (or $x15599 $x19995))))
   3.429 +(let ((@x25020 (unit-resolution (unit-resolution @x20768 @x24345 (or $x20001 $x15599 $x19995)) (unit-resolution @x20774 @x24630 $x19998) (or $x15599 $x19995))))
   3.430  (let ((@x23989 (hypothesis $x19980)))
   3.431 -(let ((@x24787 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953))))
   3.432 -(let ((@x24655 (unit-resolution @x24787 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959)))
   3.433 +(let ((@x25004 (unit-resolution (def-axiom (or $x19959 $x15590 $x15599 $x19953)) @x24345 (or $x19959 $x15599 $x19953))))
   3.434 +(let ((@x24684 (unit-resolution @x25004 (unit-resolution (def-axiom (or $x19992 $x10324)) (hypothesis $x19995) $x10324) (hypothesis $x19950) $x19959)))
   3.435  (let ((@x20748 (def-axiom (or $x19989 $x19977 $x19983))))
   3.436 -(let ((@x24904 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977)))
   3.437 +(let ((@x24916 (unit-resolution @x20748 (unit-resolution (def-axiom (or $x19992 $x19986)) (hypothesis $x19995) $x19986) @x23989 $x19977)))
   3.438  (let ((@x20716 (def-axiom (or $x19974 $x19968))))
   3.439 -(let ((@x24602 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965))))
   3.440 -(let ((@x24657 (unit-resolution @x24602 (unit-resolution @x20716 @x24904 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24655 $x19962) @x24998 false)))
   3.441 -(let ((@x24972 (unit-resolution (lemma @x24657 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953)))
   3.442 +(let ((@x24762 (unit-resolution (def-axiom (or $x19971 $x15590 $x15593 $x19965)) @x24345 (or $x19971 $x15593 $x19965))))
   3.443 +(let ((@x24920 (unit-resolution @x24762 (unit-resolution @x20716 @x24916 $x19968) (unit-resolution (def-axiom (or $x19962 $x19956)) @x24684 $x19962) @x24785 false)))
   3.444 +(let ((@x24972 (unit-resolution (lemma @x24920 (or $x19992 $x19983 $x19953)) @x23989 (unit-resolution @x25020 (lemma @x24717 $x10324) $x19995) $x19953)))
   3.445  (let (($x13277 (<= v_b_P_H_len$ 4294967295)))
   3.446  (let (($x13272 (= (+ b_S_max_o_u4$ (* (- 1) v_b_P_H_len$)) (+ 4294967295 (* (- 1) v_b_P_H_len$)))))
   3.447  (let ((@x13276 (monotonicity (monotonicity @x6446 $x13272) (= $x11245 (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0)))))
   3.448  (let ((@x13281 (trans @x13276 (rewrite (= (>= (+ 4294967295 (* (- 1) v_b_P_H_len$)) 0) $x13277)) (= $x11245 $x13277))))
   3.449  (let ((@x13282 (mp (and-elim @x12033 $x11245) @x13281 $x13277)))
   3.450  (let ((@x25068 (unit-resolution ((_ th-lemma arith assign-bounds 1 -1) (or $x13353 (not $x13277) $x11486)) @x13282 (or $x13353 $x11486))))
   3.451 -(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))))
   3.452 +(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))))
   3.453  (let ((@x25021 (unit-resolution @x25023 (unit-resolution (def-axiom (or $x19950 $x19944)) @x24972 $x19944) $x19941)))
   3.454  (let ((@x20652 (def-axiom (or $x19938 $x19932))))
   3.455  (let (($x20596 (>= ?x11582 (- 1))))
   3.456  (let ((@x25129 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x19452 $x20596)) (unit-resolution (def-axiom (or $x19938 $x11580)) @x25021 $x11580) $x20596)))
   3.457 -(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24684 (or $x11608 (not $x20596)))))
   3.458 +(let ((@x25134 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x11608 $x11486 (not $x20596))) @x24656 (or $x11608 (not $x20596)))))
   3.459  (let ((@x20638 (def-axiom (or $x19935 $x11612 $x19929))))
   3.460  (let ((@x25133 (unit-resolution @x20638 (unit-resolution @x25134 @x25129 $x11608) (unit-resolution @x20652 @x25021 $x19932) $x19929)))
   3.461  (let ((@x20630 (def-axiom (or $x19926 $x19920))))
   3.462 @@ -2888,12 +2888,12 @@
   3.463  (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$))))
   3.464  (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)))
   3.465  (let ((@x20614 (def-axiom (or $x19413 $x11647 (not $x10374)))))
   3.466 -(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)))
   3.467 +(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)))
   3.468  (let ((@x20618 (def-axiom (or $x19914 $x19412))))
   3.469  (let ((@x20626 (def-axiom (or $x19923 $x19386 $x19917))))
   3.470  (let ((@x25210 (unit-resolution @x20626 (unit-resolution @x20618 @x25206 $x19914) (unit-resolution @x20630 @x25133 $x19920) $x19386)))
   3.471 -(let (($x24182 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0)))
   3.472 -(let (($x24206 (not $x24182)))
   3.473 +(let (($x24195 (>= (+ v_b_L_H_max_G_1$ ?x15891) 0)))
   3.474 +(let (($x24206 (not $x24195)))
   3.475  (let ((?x11631 (* (- 1) v_b_L_H_max_G_3$)))
   3.476  (let ((?x20720 (+ v_b_L_H_max_G_1$ ?x11631)))
   3.477  (let (($x20721 (<= ?x20720 0)))
   3.478 @@ -2905,30 +2905,30 @@
   3.479  (let ((@x24170 (hypothesis $x20721)))
   3.480  (let (($x20603 (not $x15893)))
   3.481  (let ((@x24171 (hypothesis $x20603)))
   3.482 -(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24182) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721)))))
   3.483 +(let ((@x24211 (lemma ((_ th-lemma arith farkas -1 1 1) (hypothesis $x24195) @x24171 @x24170 false) (or $x24206 $x15893 (not $x20721)))))
   3.484  (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)))
   3.485  (let ((?x15869 (* (- 1) ?v0!14)))
   3.486  (let ((?x23656 (+ v_b_L_H_p_G_0$ ?x15869)))
   3.487 -(let (($x24586 (>= ?x23656 0)))
   3.488 +(let (($x24926 (>= ?x23656 0)))
   3.489  (let ((@x24735 (hypothesis $x20596)))
   3.490 -(let ((@x24001 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24586 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24586)))
   3.491 +(let ((@x24918 (unit-resolution ((_ th-lemma arith assign-bounds -1 -1) (or $x24926 $x15871 (not $x20596))) (hypothesis $x15876) @x24735 $x24926)))
   3.492  (let (($x23657 (<= ?x23656 0)))
   3.493 -(let (($x24913 (or $x19903 $x19365 $x19366 $x23657 $x24182)))
   3.494 +(let (($x24882 (or $x19903 $x19365 $x19366 $x23657 $x24195)))
   3.495  (let (($x23648 (<= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) 0)))
   3.496  (let (($x23640 (>= (+ ?v0!14 ?x11484) 0)))
   3.497  (let (($x23649 (or $x19365 $x19366 $x23640 $x23648)))
   3.498 -(let (($x24853 (or $x19903 $x23649)))
   3.499 -(let (($x24880 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634))))
   3.500 -(let ((@x24024 (monotonicity (rewrite $x24880) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0)))))
   3.501 -(let ((@x24867 (trans @x24024 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24182)) (= $x23648 $x24182))))
   3.502 -(let ((@x24020 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0)))))
   3.503 -(let ((@x24881 (trans @x24020 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657))))
   3.504 -(let ((@x24935 (monotonicity (monotonicity @x24881 @x24867 (= $x23649 (or $x19365 $x19366 $x23657 $x24182))) (= $x24853 (or $x19903 (or $x19365 $x19366 $x23657 $x24182))))))
   3.505 -(let ((@x24917 (trans @x24935 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24182)) $x24913)) (= $x24853 $x24913))))
   3.506 -(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)))
   3.507 -(let ((@x24757 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24586))) @x24941 @x24001 (hypothesis (not $x25035)) false)))
   3.508 -(let ((@x24761 (lemma @x24757 (or $x19381 $x25035 $x19903 $x24182 $x15871 (not $x20596)))))
   3.509 -(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)))
   3.510 +(let (($x24880 (or $x19903 $x23649)))
   3.511 +(let (($x24587 (= (+ ?x15634 (* (- 1) v_b_L_H_max_G_1$)) (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634))))
   3.512 +(let ((@x24936 (monotonicity (rewrite $x24587) (= $x23648 (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0)))))
   3.513 +(let ((@x24841 (trans @x24936 (rewrite (= (<= (+ (* (- 1) v_b_L_H_max_G_1$) ?x15634) 0) $x24195)) (= $x23648 $x24195))))
   3.514 +(let ((@x24943 (monotonicity (rewrite (= (+ ?v0!14 ?x11484) (+ ?x11484 ?v0!14))) (= $x23640 (>= (+ ?x11484 ?v0!14) 0)))))
   3.515 +(let ((@x24623 (trans @x24943 (rewrite (= (>= (+ ?x11484 ?v0!14) 0) $x23657)) (= $x23640 $x23657))))
   3.516 +(let ((@x24818 (monotonicity (monotonicity @x24623 @x24841 (= $x23649 (or $x19365 $x19366 $x23657 $x24195))) (= $x24880 (or $x19903 (or $x19365 $x19366 $x23657 $x24195))))))
   3.517 +(let ((@x24597 (trans @x24818 (rewrite (= (or $x19903 (or $x19365 $x19366 $x23657 $x24195)) $x24882)) (= $x24880 $x24882))))
   3.518 +(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)))
   3.519 +(let ((@x24984 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x25035 (not $x23657) (not $x24926))) @x24900 @x24918 (hypothesis (not $x25035)) false)))
   3.520 +(let ((@x24787 (lemma @x24984 (or $x19381 $x25035 $x19903 $x24195 $x15871 (not $x20596)))))
   3.521 +(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)))
   3.522  (let ((@x25060 (monotonicity (symm (hypothesis $x25035) (= ?v0!14 v_b_L_H_p_G_0$)) (= ?x15633 ?x10320))))
   3.523  (let ((@x25064 (unit-resolution (hypothesis (not $x25038)) (symm (monotonicity @x25060 (= ?x15634 ?x10327)) $x25038) false)))
   3.524  (let ((@x25067 (lemma @x25064 (or (not $x25035) $x25038))))
   3.525 @@ -2944,30 +2944,30 @@
   3.526  (let (($x25044 (not $x25038)))
   3.527  (let (($x25049 (not $x25041)))
   3.528  (let ((@x25051 (lemma ((_ th-lemma arith farkas 1 -1 -1 1) (hypothesis $x25041) @x24170 @x24171 (hypothesis $x11516) false) (or $x25049 (not $x20721) $x15893 $x11515))))
   3.529 -(let ((@x24891 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049)))
   3.530 -(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)))
   3.531 -(let ((@x24892 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719)))
   3.532 -(let ((@x24061 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190))))
   3.533 -(let ((@x24887 (trans (monotonicity @x24061 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$))))
   3.534 +(let ((@x24047 (unit-resolution @x25051 (unit-resolution (def-axiom (or $x19980 $x11516)) (hypothesis $x19983) $x11516) @x24171 @x24170 $x25049)))
   3.535 +(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)))
   3.536 +(let ((@x24887 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) (hypothesis $x19983) $x10391) $x20719)))
   3.537 +(let ((@x24982 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (= ?x10372 ?x10190))))
   3.538 +(let ((@x24897 (trans (monotonicity @x24982 (= ?x10373 ?x10191)) @x23175 (= ?x10373 v_b_L_H_max_G_1$))))
   3.539  (let ((?x11645 (* (- 1) v_b_SL_H_witness_G_1$)))
   3.540  (let ((?x20724 (+ v_b_SL_H_witness_G_0$ ?x11645)))
   3.541  (let (($x20726 (>= ?x20724 0)))
   3.542  (let (($x20723 (= v_b_SL_H_witness_G_0$ v_b_SL_H_witness_G_1$)))
   3.543 -(let ((@x24982 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
   3.544 -(let ((@x24888 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867))))
   3.545 -(let ((@x24648 (unit-resolution @x24888 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24982 $x20726) @x23180 $x11648)))
   3.546 -(let ((@x24798 (unit-resolution @x20618 (unit-resolution @x20614 @x24648 (trans @x24887 @x24892 $x10374) $x19413) $x19914)))
   3.547 +(let ((@x24788 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) (hypothesis $x19983) $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
   3.548 +(let ((@x24909 (lemma ((_ th-lemma arith farkas 1 -1 1) (hypothesis $x20726) (hypothesis $x11647) @x23180 false) (or $x11648 (not $x20726) $x11867))))
   3.549 +(let ((@x24673 (unit-resolution @x24909 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x20723) $x20726)) @x24788 $x20726) @x23180 $x11648)))
   3.550 +(let ((@x24789 (unit-resolution @x20618 (unit-resolution @x20614 @x24673 (trans @x24897 @x24887 $x10374) $x19413) $x19914)))
   3.551  (let ((@x20602 (def-axiom (or $x19381 $x15876))))
   3.552 -(let ((@x25013 (unit-resolution @x20602 (unit-resolution @x20626 @x24798 (unit-resolution @x20630 @x24597 $x19920) $x19386) $x15876)))
   3.553 -(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)))
   3.554 -(let ((@x24056 (lemma @x25017 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674))))
   3.555 -(let ((@x24843 (unit-resolution @x24056 @x24499 @x24415 @x24684 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935))))
   3.556 +(let ((@x24914 (unit-resolution @x20602 (unit-resolution @x20626 @x24789 (unit-resolution @x20630 @x24884 $x19920) $x19386) $x15876)))
   3.557 +(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)))
   3.558 +(let ((@x24889 (lemma @x24915 (or $x19980 $x19903 (not $x20596) $x11867 $x15893 (not $x20721) $x19935 $x11486 $x19674))))
   3.559 +(let ((@x24843 (unit-resolution @x24889 @x24499 @x24415 @x24656 @x24314 (or $x19980 (not $x20596) $x15893 (not $x20721) $x19935))))
   3.560  (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)))
   3.561  (let ((@x20605 (def-axiom (or $x19381 $x20603))))
   3.562  (let ((@x25302 (monotonicity (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (= ?x10372 ?x10190))))
   3.563  (let ((@x25305 (trans (monotonicity @x25302 (= ?x10373 ?x10191)) @x24314 (= ?x10373 v_b_L_H_max_G_1$))))
   3.564  (let ((@x25306 (trans @x25305 (symm (unit-resolution (def-axiom (or $x19980 $x10391)) @x25299 $x10391) $x20719) $x10374)))
   3.565  (let ((@x25307 (mp (unit-resolution (def-axiom (or $x19980 $x10392)) @x25299 $x10392) (symm (commutativity (= $x20723 $x10392)) (= $x10392 $x20723)) $x20723)))
   3.566 -(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)))
   3.567 +(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)))
   3.568  (unit-resolution @x20626 (unit-resolution @x20618 (unit-resolution @x20614 @x25311 @x25306 $x19413) $x19914) (unit-resolution @x20605 @x24844 $x19381) (unit-resolution @x20630 @x24954 $x19920) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   3.569  
     4.1 --- a/src/HOL/SMT_Examples/boogie.ML	Thu Jun 12 01:00:49 2014 +0200
     4.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Thu Jun 12 01:00:49 2014 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  signature BOOGIE =
     4.5  sig
     4.6    val boogie_prove: theory -> string list -> unit
     4.7 -end
     4.8 +end;
     4.9  
    4.10  structure Boogie: BOOGIE =
    4.11  struct
    4.12 @@ -16,7 +16,6 @@
    4.13  
    4.14  val as_int = fst o read_int o raw_explode
    4.15  
    4.16 -
    4.17  val isabelle_name =
    4.18    let
    4.19      fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
    4.20 @@ -31,7 +30,6 @@
    4.21    in prefix "b_" o translate_string purge end
    4.22  
    4.23  
    4.24 -
    4.25  (* context *)
    4.26  
    4.27  type context =
    4.28 @@ -39,54 +37,44 @@
    4.29  
    4.30  val empty_context: context = (Symtab.empty, Symtab.empty, [], [])
    4.31  
    4.32 -
    4.33  fun add_type name (tds, fds, axs, vcs) =
    4.34    let
    4.35      val T = TFree (isabelle_name name, @{sort type})
    4.36      val tds' = Symtab.update (name, T) tds
    4.37    in (tds', fds, axs, vcs) end
    4.38  
    4.39 -
    4.40  fun add_func name Ts T unique (tds, fds, axs, vcs) =
    4.41    let
    4.42      val t = Free (isabelle_name name, Ts ---> T)
    4.43      val fds' = Symtab.update (name, (t, unique)) fds
    4.44    in (tds, fds', axs, vcs) end
    4.45  
    4.46 -
    4.47  fun add_axiom t (tds, fds, axs, vcs) = (tds, fds, t :: axs, vcs)
    4.48  
    4.49  fun add_vc t (tds, fds, axs, vcs) = (tds, fds, axs, t :: vcs)
    4.50  
    4.51 -
    4.52  fun lookup_type (tds, _, _, _) name =
    4.53    (case Symtab.lookup tds name of
    4.54      SOME T => T
    4.55    | NONE => error "Undeclared type")
    4.56  
    4.57 -
    4.58  fun lookup_func (_, fds, _, _) name =
    4.59    (case Symtab.lookup fds name of
    4.60      SOME t_unique => t_unique
    4.61    | NONE => error "Undeclared function")
    4.62  
    4.63  
    4.64 -
    4.65  (* constructors *)
    4.66  
    4.67  fun mk_var name T = Free ("V_" ^ isabelle_name name, T)
    4.68  
    4.69 -
    4.70  fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T])
    4.71  
    4.72 -
    4.73  fun mk_binary t (t1, t2) = t $ t1 $ t2
    4.74  
    4.75 -
    4.76  fun mk_nary _ t [] = t
    4.77    | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
    4.78  
    4.79 -
    4.80  fun mk_distinct [] = @{const HOL.True}
    4.81    | mk_distinct [_] = @{const HOL.True}
    4.82    | mk_distinct (t :: ts) =
    4.83 @@ -95,34 +83,27 @@
    4.84            HOLogic.mk_conj (HOLogic.mk_not (HOLogic.mk_eq (t, u)), u')
    4.85        in fold_rev mk_noteq ts (mk_distinct ts) end
    4.86  
    4.87 -
    4.88  fun mk_store m k v =
    4.89    let
    4.90      val mT = Term.fastype_of m and kT = Term.fastype_of k
    4.91      val vT = Term.fastype_of v
    4.92    in Const (@{const_name fun_upd}, mT --> kT --> vT --> mT) $ m $ k $ v end
    4.93  
    4.94 -
    4.95  fun mk_quant q (Free (x, T)) t = q T $ absfree (x, T) t
    4.96    | mk_quant _ t _ = raise TERM ("bad variable", [t])
    4.97  
    4.98 -
    4.99 -fun mk_list T = HOLogic.mk_list T
   4.100 -
   4.101 -
   4.102  val patternT = @{typ "SMT2.pattern"}
   4.103  
   4.104  fun mk_pat t =
   4.105    Const (@{const_name "SMT2.pat"}, Term.fastype_of t --> patternT) $ t
   4.106  
   4.107  fun mk_pattern [] = raise TERM ("mk_pattern", [])
   4.108 -  | mk_pattern ts = mk_list patternT (map mk_pat ts)
   4.109 -
   4.110 +  | mk_pattern ts = SMT2_Util.mk_symb_list patternT (map mk_pat ts)
   4.111  
   4.112  fun mk_trigger [] t = t
   4.113    | mk_trigger pss t =
   4.114        @{term "SMT2.trigger"} $
   4.115 -        mk_list @{typ "SMT2.pattern list"} (map mk_pattern pss) $ t
   4.116 +        SMT2_Util.mk_symb_list @{typ "SMT2.pattern SMT2.symb_list"} (map mk_pattern pss) $ t
   4.117  
   4.118  
   4.119  (* parser *)
   4.120 @@ -131,7 +112,6 @@
   4.121    let fun apply (xs, ls) = f ls |>> (fn x => x :: xs)
   4.122    in funpow (as_int n) apply ([], ls) |>> rev end
   4.123  
   4.124 -
   4.125  fun parse_type _ (["bool"] :: ls) = (@{typ bool}, ls)
   4.126    | parse_type _ (["int"] :: ls) = (@{typ int}, ls)
   4.127    | parse_type cx (["array", arity] :: ls) =
   4.128 @@ -139,42 +119,29 @@
   4.129    | parse_type cx (("type-con" :: name :: _) :: ls) = (lookup_type cx name, ls)
   4.130    | parse_type _ _ = error "Bad type"
   4.131  
   4.132 -
   4.133  fun parse_expr _ (["true"] :: ls) = (@{term True}, ls)
   4.134    | parse_expr _ (["false"] :: ls) = (@{term False}, ls)
   4.135    | parse_expr cx (["not"] :: ls) = parse_expr cx ls |>> HOLogic.mk_not
   4.136 -  | parse_expr cx (["and", n] :: ls) =
   4.137 -      parse_nary_expr cx n HOLogic.mk_conj @{term True} ls
   4.138 -  | parse_expr cx (["or", n] :: ls) =
   4.139 -      parse_nary_expr cx n HOLogic.mk_disj @{term False} ls
   4.140 -  | parse_expr cx (["implies"] :: ls) =
   4.141 -      parse_bin_expr cx (mk_binary @{term HOL.implies}) ls
   4.142 +  | parse_expr cx (["and", n] :: ls) = parse_nary_expr cx n HOLogic.mk_conj @{term True} ls
   4.143 +  | parse_expr cx (["or", n] :: ls) = parse_nary_expr cx n HOLogic.mk_disj @{term False} ls
   4.144 +  | parse_expr cx (["implies"] :: ls) = parse_bin_expr cx (mk_binary @{term HOL.implies}) ls
   4.145    | parse_expr cx (["="] :: ls) = parse_bin_expr cx HOLogic.mk_eq ls
   4.146    | parse_expr cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   4.147    | parse_expr cx (["fun", name, n] :: ls) =
   4.148        let val (t, _) = lookup_func cx name
   4.149        in repeat (parse_expr cx) n ls |>> curry Term.list_comb t end
   4.150    | parse_expr cx (("label" :: _) :: ls) = parse_expr cx ls
   4.151 -  | parse_expr _ (["int-num", n] :: ls) =
   4.152 -      (HOLogic.mk_number @{typ int} (as_int n), ls)
   4.153 -  | parse_expr cx (["<"] :: ls) =
   4.154 -      parse_bin_expr cx (mk_binary @{term "op < :: int => _"}) ls
   4.155 -  | parse_expr cx (["<="] :: ls) =
   4.156 -      parse_bin_expr cx (mk_binary @{term "op <= :: int => _"}) ls
   4.157 -  | parse_expr cx ([">"] :: ls) =
   4.158 -      parse_bin_expr cx (mk_binary @{term "op < :: int => _"}o swap) ls
   4.159 +  | parse_expr _ (["int-num", n] :: ls) = (HOLogic.mk_number @{typ int} (as_int n), ls)
   4.160 +  | parse_expr cx (["<"] :: ls) = parse_bin_expr cx (mk_binary @{term "op < :: int => _"}) ls
   4.161 +  | parse_expr cx (["<="] :: ls) = parse_bin_expr cx (mk_binary @{term "op <= :: int => _"}) ls
   4.162 +  | parse_expr cx ([">"] :: ls) = parse_bin_expr cx (mk_binary @{term "op < :: int => _"}o swap) ls
   4.163    | parse_expr cx ([">="] :: ls) =
   4.164        parse_bin_expr cx (mk_binary @{term "op <= :: int => _"} o swap) ls
   4.165 -  | parse_expr cx (["+"] :: ls) =
   4.166 -      parse_bin_expr cx (mk_binary @{term "op + :: int => _"}) ls
   4.167 -  | parse_expr cx (["-"] :: ls) =
   4.168 -      parse_bin_expr cx (mk_binary @{term "op - :: int => _"}) ls
   4.169 -  | parse_expr cx (["*"] :: ls) =
   4.170 -      parse_bin_expr cx (mk_binary @{term "op * :: int => _"}) ls
   4.171 -  | parse_expr cx (["/"] :: ls) =
   4.172 -      parse_bin_expr cx (mk_binary @{term boogie_div}) ls
   4.173 -  | parse_expr cx (["%"] :: ls) =
   4.174 -      parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
   4.175 +  | parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary @{term "op + :: int => _"}) ls
   4.176 +  | parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary @{term "op - :: int => _"}) ls
   4.177 +  | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "op * :: int => _"}) ls
   4.178 +  | parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_div}) ls
   4.179 +  | parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
   4.180    | parse_expr cx (["select", n] :: ls) =
   4.181        repeat (parse_expr cx) n ls
   4.182        |>> (fn ts => hd ts $ HOLogic.mk_tuple (tl ts))
   4.183 @@ -188,14 +155,11 @@
   4.184        parse_quant cx HOLogic.exists_const vars pats atts ls
   4.185    | parse_expr _ _ = error "Bad expression"
   4.186  
   4.187 -
   4.188  and parse_bin_expr cx f ls = ls |> parse_expr cx ||>> parse_expr cx |>> f
   4.189  
   4.190 -
   4.191  and parse_nary_expr cx n f c ls =
   4.192    repeat (parse_expr cx) n ls |>> mk_nary (curry f) c
   4.193  
   4.194 -
   4.195  and parse_quant cx q vars pats atts ls =
   4.196    let
   4.197      val ((((vs, pss), _), t), ls') =
   4.198 @@ -206,15 +170,12 @@
   4.199        ||>> parse_expr cx
   4.200    in (fold_rev (mk_quant q) vs (mk_trigger pss t), ls') end
   4.201  
   4.202 -
   4.203  and parse_var cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name
   4.204    | parse_var _ _ = error "Bad variable"
   4.205  
   4.206 -
   4.207  and parse_pat cx (["pat", n] :: ls) = repeat (parse_expr cx) n ls
   4.208    | parse_pat _ _ = error "Bad pattern"
   4.209  
   4.210 -
   4.211  and parse_attr cx (["attribute", name, n] :: ls) =
   4.212        let
   4.213          fun attr (["expr-attr"] :: ls) = parse_expr cx ls |>> K ()
   4.214 @@ -223,7 +184,6 @@
   4.215        in repeat attr n ls |>> K name end
   4.216    | parse_attr _ _ = error "Bad attribute"
   4.217  
   4.218 -
   4.219  fun parse_func cx arity n ls =
   4.220    let
   4.221      val ((Ts, atts), ls') =
   4.222 @@ -231,7 +191,6 @@
   4.223      val unique = member (op =) atts "unique"
   4.224    in ((split_last Ts, unique), ls') end
   4.225  
   4.226 -
   4.227  fun parse_decl (("type-decl" :: name :: _) :: ls) cx = (ls, add_type name cx)
   4.228    | parse_decl (["fun-decl", name, arity, n] :: ls) cx =
   4.229        let val (((Ts, T), unique), ls') = parse_func cx arity n ls
   4.230 @@ -246,12 +205,10 @@
   4.231        in (ls', add_vc t cx) end
   4.232    | parse_decl _ _ = error "Bad declaration"
   4.233  
   4.234 -
   4.235  fun parse_lines [] cx = cx
   4.236    | parse_lines ls cx = parse_decl ls cx |-> parse_lines
   4.237  
   4.238  
   4.239 -
   4.240  (* splitting of text lines into a lists of tokens *)
   4.241  
   4.242  fun is_blank c = (c = " " orelse c = "\t" orelse c = "\r" orelse c = "\n")
   4.243 @@ -261,7 +218,6 @@
   4.244    #> filter (fn [] => false | _ => true)
   4.245  
   4.246  
   4.247 -
   4.248  (* proving verification conditions *)
   4.249  
   4.250  fun add_unique_axioms (tds, fds, axs, vcs) =
   4.251 @@ -271,7 +227,6 @@
   4.252    |> map (fn (T, ns) => mk_distinct (map (Free o rpair T) ns))
   4.253    |> (fn axs' => (tds, fds, axs' @ axs, vcs))
   4.254  
   4.255 -
   4.256  fun build_proof_context thy (tds, fds, axs, vcs) =
   4.257    let
   4.258      val vc =
   4.259 @@ -287,16 +242,13 @@
   4.260      |> pair (map HOLogic.mk_Trueprop axs, HOLogic.mk_Trueprop vc)
   4.261    end
   4.262  
   4.263 -
   4.264  val boogie_rules =
   4.265    [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
   4.266    [@{thm fun_upd_same}, @{thm fun_upd_apply}]
   4.267  
   4.268 -
   4.269  fun boogie_tac ctxt axioms =
   4.270    ALLGOALS (SMT2_Solver.smt2_tac ctxt (boogie_rules @ axioms))
   4.271  
   4.272 -
   4.273  fun boogie_prove thy lines =
   4.274    let
   4.275      val ((axioms, vc), ctxt) =
   4.276 @@ -305,8 +257,7 @@
   4.277        |> add_unique_axioms
   4.278        |> build_proof_context thy
   4.279  
   4.280 -    val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
   4.281 -      boogie_tac context prems)
   4.282 +    val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} => boogie_tac context prems)
   4.283      val _ = writeln "Verification condition proved successfully"
   4.284  
   4.285    in () end
   4.286 @@ -324,4 +275,4 @@
   4.287            val _ = boogie_prove thy' lines;
   4.288          in thy' end)))
   4.289  
   4.290 -end
   4.291 +end;