src/HOL/SMT_Examples/SMT_Examples_Verit.thy
 changeset 73391 f16f209f996c parent 72908 6a26a955308e child 74403 dbd69d287ec6
equal 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)"`
`   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 `