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