equal
deleted
inserted
replaced
352 lemma "(if (ALL x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by smt |
352 lemma "(if (ALL x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by smt |
353 lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt |
353 lemma "~ (\<exists>x y z::int. 4 * x + -6 * y = (1::int))" by smt |
354 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt |
354 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt |
355 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt |
355 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt |
356 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt |
356 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt |
357 lemma "\<forall>x::int. |
|
358 SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat x) SMT.Symb_Nil) SMT.Symb_Nil) |
|
359 (x < a \<longrightarrow> 2 * x < 2 * a)" by smt |
|
360 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt |
357 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt |
361 |
358 |
362 |
359 |
363 subsection {* Non-linear arithmetic over integers and reals *} |
360 subsection {* Non-linear arithmetic over integers and reals *} |
364 |
361 |