src/HOL/SMT_Examples/SMT_Examples_Verit.thy
changeset 73391 f16f209f996c
parent 72908 6a26a955308e
child 74403 dbd69d287ec6
equal deleted inserted replaced
73390:3c5a7746ffa4 73391:f16f209f996c
   312 
   312 
   313 lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
   313 lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
   314          x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
   314          x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
   315          x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
   315          x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
   316  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
   316  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
   317   supply [[smt_timeout=360]]
       
   318   by (smt (verit))
   317   by (smt (verit))
   319 
   318 
   320 
   319 
   321 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by (smt (verit))
   320 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by (smt (verit))
   322 
   321