Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/SMT_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 39 kB

Quelle SMT_Examples_Verit.thy Sprache: Isabelle

(* Title: HOL/SMT_Examples/SMT_Examples_Verit.thy
 Author: Sascha Boehme, TU Muenchen
 Author: Mathias Fleury, JKU

Half of the examples come from the corresponding file for z3,
the others come from the Isabelle distribution or the AFP.
*)

section \<open>Examples for the (smt (verit)) binding\<close>

theory SMT_Examples_Verit
imports Complex_Main
begin

external_file \<open>SMT_Examples_Verit.certs\<close>

declare [[smt_certificates = "SMT_Examples_Verit.certs"]]
declare [[smt_read_only_certificates = true]]

section \<open>Propositional and first-order logic\<close>

lemma "True" by (smt (verit))
lemma "p \ \p" by (smt (verit))
lemma "(p \ True) = p" by (smt (verit))
lemma "(p \ q) \ \p \ q" by (smt (verit))
lemma "(a \ b) \ (c \ d) \ (a \ b) \ (c \ d)" by (smt (verit))
lemma "(p1 \ p2) \ p3 \ (p1 \ (p3 \ p2) \ (p1 \ p3)) \ p1" by (smt (verit))
lemma "P = P = P = P = P = P = P = P = P = P" by (smt (verit))

lemma
 assumes "a \ b \ c \ d"
 and "e \ f \ (a \ d)"
 and "\ (a \ (c \ ~c)) \ b"
 and "\ (b \ (x \ \ x)) \ c"
 and "\ (d \ False) \ c"
 and "\ (c \ (\ p \ (p \ (q \ \ q))))"
 shows False
 using assms by (smt (verit))

axiomatization symm_f :: "'a \ 'a \ 'a" where
 symm_f: "symm_f x y = symm_f y x"

lemma "a = a \ symm_f a b = symm_f b a"
 by (smt (verit) symm_f)

(*
Taken from ~~/src/HOL/ex/SAT_Examples.thy.
Translated from TPTP problem library: PUZ015-2.006.dimacs
*)
lemma
 assumes "~x0"
 and "~x30"
 and "~x29"
 and "~x59"
 and "x1 \ x31 \ x0"
 and "x2 \ x32 \ x1"
 and "x3 \ x33 \ x2"
 and "x4 \ x34 \ x3"
 and "x35 \ x4"
 and "x5 \ x36 \ x30"
 and "x6 \ x37 \ x5 \ x31"
 and "x7 \ x38 \ x6 \ x32"
 and "x8 \ x39 \ x7 \ x33"
 and "x9 \ x40 \ x8 \ x34"
 and "x41 \ x9 \ x35"
 and "x10 \ x42 \ x36"
 and "x11 \ x43 \ x10 \ x37"
 and "x12 \ x44 \ x11 \ x38"
 and "x13 \ x45 \ x12 \ x39"
 and "x14 \ x46 \ x13 \ x40"
 and "x47 \ x14 \ x41"
 and "x15 \ x48 \ x42"
 and "x16 \ x49 \ x15 \ x43"
 and "x17 \ x50 \ x16 \ x44"
 and "x18 \ x51 \ x17 \ x45"
 and "x19 \ x52 \ x18 \ x46"
 and "x53 \ x19 \ x47"
 and "x20 \ x54 \ x48"
 and "x21 \ x55 \ x20 \ x49"
 and "x22 \ x56 \ x21 \ x50"
 and "x23 \ x57 \ x22 \ x51"
 and "x24 \ x58 \ x23 \ x52"
 and "x59 \ x24 \ x53"
 and "x25 \ x54"
 and "x26 \ x25 \ x55"
 and "x27 \ x26 \ x56"
 and "x28 \ x27 \ x57"
 and "x29 \ x28 \ x58"
 and "~x1 \ ~x31"
 and "~x1 \ ~x0"
 and "~x31 \ ~x0"
 and "~x2 \ ~x32"
 and "~x2 \ ~x1"
 and "~x32 \ ~x1"
 and "~x3 \ ~x33"
 and "~x3 \ ~x2"
 and "~x33 \ ~x2"
 and "~x4 \ ~x34"
 and "~x4 \ ~x3"
 and "~x34 \ ~x3"
 and "~x35 \ ~x4"
 and "~x5 \ ~x36"
 and "~x5 \ ~x30"
 and "~x36 \ ~x30"
 and "~x6 \ ~x37"
 and "~x6 \ ~x5"
 and "~x6 \ ~x31"
 and "~x37 \ ~x5"
 and "~x37 \ ~x31"
 and "~x5 \ ~x31"
 and "~x7 \ ~x38"
 and "~x7 \ ~x6"
 and "~x7 \ ~x32"
 and "~x38 \ ~x6"
 and "~x38 \ ~x32"
 and "~x6 \ ~x32"
 and "~x8 \ ~x39"
 and "~x8 \ ~x7"
 and "~x8 \ ~x33"
 and "~x39 \ ~x7"
 and "~x39 \ ~x33"
 and "~x7 \ ~x33"
 and "~x9 \ ~x40"
 and "~x9 \ ~x8"
 and "~x9 \ ~x34"
 and "~x40 \ ~x8"
 and "~x40 \ ~x34"
 and "~x8 \ ~x34"
 and "~x41 \ ~x9"
 and "~x41 \ ~x35"
 and "~x9 \ ~x35"
 and "~x10 \ ~x42"
 and "~x10 \ ~x36"
 and "~x42 \ ~x36"
 and "~x11 \ ~x43"
 and "~x11 \ ~x10"
 and "~x11 \ ~x37"
 and "~x43 \ ~x10"
 and "~x43 \ ~x37"
 and "~x10 \ ~x37"
 and "~x12 \ ~x44"
 and "~x12 \ ~x11"
 and "~x12 \ ~x38"
 and "~x44 \ ~x11"
 and "~x44 \ ~x38"
 and "~x11 \ ~x38"
 and "~x13 \ ~x45"
 and "~x13 \ ~x12"
 and "~x13 \ ~x39"
 and "~x45 \ ~x12"
 and "~x45 \ ~x39"
 and "~x12 \ ~x39"
 and "~x14 \ ~x46"
 and "~x14 \ ~x13"
 and "~x14 \ ~x40"
 and "~x46 \ ~x13"
 and "~x46 \ ~x40"
 and "~x13 \ ~x40"
 and "~x47 \ ~x14"
 and "~x47 \ ~x41"
 and "~x14 \ ~x41"
 and "~x15 \ ~x48"
 and "~x15 \ ~x42"
 and "~x48 \ ~x42"
 and "~x16 \ ~x49"
 and "~x16 \ ~x15"
 and "~x16 \ ~x43"
 and "~x49 \ ~x15"
 and "~x49 \ ~x43"
 and "~x15 \ ~x43"
 and "~x17 \ ~x50"
 and "~x17 \ ~x16"
 and "~x17 \ ~x44"
 and "~x50 \ ~x16"
 and "~x50 \ ~x44"
 and "~x16 \ ~x44"
 and "~x18 \ ~x51"
 and "~x18 \ ~x17"
 and "~x18 \ ~x45"
 and "~x51 \ ~x17"
 and "~x51 \ ~x45"
 and "~x17 \ ~x45"
 and "~x19 \ ~x52"
 and "~x19 \ ~x18"
 and "~x19 \ ~x46"
 and "~x52 \ ~x18"
 and "~x52 \ ~x46"
 and "~x18 \ ~x46"
 and "~x53 \ ~x19"
 and "~x53 \ ~x47"
 and "~x19 \ ~x47"
 and "~x20 \ ~x54"
 and "~x20 \ ~x48"
 and "~x54 \ ~x48"
 and "~x21 \ ~x55"
 and "~x21 \ ~x20"
 and "~x21 \ ~x49"
 and "~x55 \ ~x20"
 and "~x55 \ ~x49"
 and "~x20 \ ~x49"
 and "~x22 \ ~x56"
 and "~x22 \ ~x21"
 and "~x22 \ ~x50"
 and "~x56 \ ~x21"
 and "~x56 \ ~x50"
 and "~x21 \ ~x50"
 and "~x23 \ ~x57"
 and "~x23 \ ~x22"
 and "~x23 \ ~x51"
 and "~x57 \ ~x22"
 and "~x57 \ ~x51"
 and "~x22 \ ~x51"
 and "~x24 \ ~x58"
 and "~x24 \ ~x23"
 and "~x24 \ ~x52"
 and "~x58 \ ~x23"
 and "~x58 \ ~x52"
 and "~x23 \ ~x52"
 and "~x59 \ ~x24"
 and "~x59 \ ~x53"
 and "~x24 \ ~x53"
 and "~x25 \ ~x54"
 and "~x26 \ ~x25"
 and "~x26 \ ~x55"
 and "~x25 \ ~x55"
 and "~x27 \ ~x26"
 and "~x27 \ ~x56"
 and "~x26 \ ~x56"
 and "~x28 \ ~x27"
 and "~x28 \ ~x57"
 and "~x27 \ ~x57"
 and "~x29 \ ~x28"
 and "~x29 \ ~x58"
 and "~x28 \ ~x58"
shows False
 using assms by (smt (verit))

lemma "\x::int. P x \ (\y::int. P x \ P y)"
 by (smt (verit))

lemma
 assumes "(\x y. P x y = x)"
 shows "(\y. P x y) = P x c"
 using assms by (smt (verit))

lemma
 assumes "(\x y. P x y = x)"
 and "(\x. \y. P x y) = (\x. P x c)"
 shows "(\y. P x y) = P x c"
 using assms by (smt (verit))

lemma
 assumes "if P x then \(\y. P y) else (\y. \P y)"
 shows "P x \ P y"
 using assms by (smt (verit))

section \<open>Arithmetic\<close>

subsection \<open>Linear arithmetic over integers and reals\<close>

lemma "(3::int) = 3" by (smt (verit))
lemma "(3::real) = 3" by (smt (verit))
lemma "(3 :: int) + 1 = 4" by (smt (verit))
lemma "x + (y + z) = y + (z + (x::int))" by (smt (verit))
lemma "max (3::int) 8 > 5" by (smt (verit))
lemma "\x :: real\ + \y\ \ \x + y\" by (smt (verit))
lemma "P ((2::int) < 3) = P True" supply[[smt_trace]] by (smt (verit))
lemma "x + 3 \ 4 \ x < (1::int)" by (smt (verit))

lemma
 assumes "x \ (3::int)" and "y = x + 4"
 shows "y - x > 0"
 using assms by (smt (verit))

lemma "let x = (2 :: int) in x + x \ 5" by (smt (verit))

lemma
 fixes x :: int
 assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
 shows "a < 0"
 using assms by (smt (verit))

lemma "(0 \ y + -1 * x \ \ 0 \ x \ 0 \ (x::int)) = (\ False)" by (smt (verit))

lemma "
 (n < m \<and> m < n') \<or> (n < m \<and> m = n') \<or> (n < n' \<and> n' < m) \<or>
 (n = n' \ n' < m) \ (n = m \ m < n') \
 (n' < m \ m < n) \ (n' < m \ m = n) \
 (n' < n \ n < m) \ (n' = n \ n < m) \ (n' = m \ m < n) \
 (m < n \<and> n < n') \<or> (m < n \<and> n' = n) \<or> (m < n' \<and> n' < n) \<or>
 (m = n \<and> n < n') \<or> (m = n' \<and> n' < n) \<or>
 (n' = m \ m = (n::int))"
 by (smt (verit))

text\<open>
The following example was taken from HOL/ex/PresburgerEx.thy, where it says:

 This following theorem proves that all solutions to the
 recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
 period 9. The example was brought to our attention by John
 Harrison. It does does not require Presburger arithmetic but merely
 quantifier-free linear arithmetic and holds for the rationals as well.

 Warning: it takes (in 2006) over 4.2 minutes!

There, it is proved by "arith". (smt (verit)) is able to prove this within a fraction
of one second. With proof reconstruction, it takes about 13 seconds on a Core2
processor.
\<close>

lemma "\ x3 = \x2\ - x1; x4 = \x3\ - x2; x5 = \x4\ - x3;
 x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
 x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
\<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
 by (smt (verit))

lemma "let P = 2 * x + 1 > x + (x::real) in P \ False \ P" by (smt (verit))

subsection \<open>Linear arithmetic with quantifiers\<close>

lemma "~ (\x::int. False)" by (smt (verit))
lemma "~ (\x::real. False)" by (smt (verit))

lemma "\x y::int. (x = 0 \ y = 1) \ x \ y" by (smt (verit))
lemma "\x y::int. x < y \ (2 * x + 1) < (2 * y)" by (smt (verit))
lemma "\x y::int. x + y > 2 \ x + y = 2 \ x + y < 2" by (smt (verit))
lemma "\x::int. if x > 0 then x + 1 > 0 else 1 > x" by (smt (verit))
lemma "(if (\x::int. x < 0 \ x > 0) then -1 else 3) > (0::int)" by (smt (verit))
lemma "\x::int. \x y. 0 < x \ 0 < y \ (0::int) < x + y" by (smt (verit))
lemma "\u::int. $x::int) y::real. 0 < x \ 0 < y \ -1 < x" by (smt (verit))
lemma "\(a::int) b::int. 0 Linear arithmetic for natural numbers\<close>

declare [[smt_nat_as_int]]

lemma "2 * (x::nat) \ 1" by (smt (verit))

lemma "a < 3 \ (7::nat) > 2 * a" by (smt (verit))

lemma "let x = (1::nat) + y in x - y > 0 * x" by (smt (verit))

lemma
 "let x = (1::nat) + y in
 let P = (if x > 0 then True else False) in
 False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
 by (smt (verit))

lemma "int (nat \x::int$ = \x\" by (smt (verit) int_nat_eq)

definition prime_nat :: "nat \ bool" where
 "prime_nat p = (1 m = 1 \ m = p))"

lemma "prime_nat (4*m + 1) \ m \ (1::nat)" by (smt (verit) prime_nat_def)

lemma "2 * (x::nat) \ 1"
 by (smt (verit))

lemma \<open>2*(x :: int) \<noteq> 1\<close>
 by (smt (verit))

declare [[smt_nat_as_int = false]]

section \<open>Pairs\<close>

lemma "fst (x, y) = a \ x = a"
 using fst_conv by (smt (verit))

lemma "p1 = (x, y) \ p2 = (y, x) \ fst p1 = snd p2"
 using fst_conv snd_conv by (smt (verit))

section \<open>Higher-order problems and recursion\<close>

lemma "i \ i1 \ i \ i2 \ (f (i1 := v1, i2 := v2)) i = f i"
 using fun_upd_same fun_upd_apply by (smt (verit))

lemma "(f g (x::'a::type) = (g x \ True)) \ (f g x = True) \ (g x = True)"
 by (smt (verit))

lemma "id x = x \ id True = True"
 by (smt (verit) id_def)

lemma "i \ i1 \ i \ i2 \ ((f (i1 := v1)) (i2 := v2)) i = f i"
 using fun_upd_same fun_upd_apply by (smt (verit))

lemma
 "f (\x. g x) \ True"
 "f (\x. g x) \ True"
 by (smt (verit))+

lemma True using let_rsp by (smt (verit))
lemma "le = (\) \ le (3::int) 42" by (smt (verit))
lemma "map (\i::int. i + 1) [0, 1] = [1, 2]" by (smt (verit) list.map)
lemma "(\x. P x) \ \ All P" by (smt (verit))

fun dec_10 :: "int \ int" where
 "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"

lemma "dec_10 (4 * dec_10 4) = 6" by (smt (verit) dec_10.simps)

context complete_lattice
begin

lemma
 assumes "Sup {a | i::bool. True} \ Sup {b | i::bool. True}"
 and "Sup {b | i::bool. True} \ Sup {a | i::bool. True}"
 shows "Sup {a | i::bool. True} \ Sup {a | i::bool. True}"
 using assms by (smt (verit) order_trans)

end

lemma
"eq_set (List.coset xs) (set ys) = rhs"
 if "\ys. subset' (List.coset xs) (set ys) = (let n = card (UNIV::'a set) in 0 < n \ card (set (xs @ ys)) = n)"
 and "\uu A. (uu::'a) \ - A \ uu \ A"
 and "\uu. card (set (uu::'a list)) = length (remdups uu)"
 and "\uu. finite (set (uu::'a list))"
 and "\uu. (uu::'a) \ UNIV"
 and "(UNIV::'a set) \ {}"
 and "\c A B P. \(c::'a) \ A \ B; c \ A \ P; c \ B \ P\ \ P"
 and "\a b. (a::nat) + b = b + a"
 and "\a b. ((a::nat) = a + b) = (b = 0)"
 and "card' (set xs) = length (remdups xs)"
 and "card' = (card :: 'a set \ nat)"
 and "\A B. \finite (A::'a set); finite B\ \ card A + card B = card (A \ B) + card (A \ B)"
 and "\A. (card (A::'a set) = 0) = (A = {} \ infinite A)"
 and "\A. \finite (UNIV::'a set); card (A::'a set) = card (UNIV::'a set)\ \ A = UNIV"
 and "\xs. - List.coset (xs::'a list) = set xs"
 and "\xs. - set (xs::'a list) = List.coset xs"
 and "\A B. (A \ B = {}) = (\x. (x::'a) \ A \ x \ B)"
 and "eq_set = (=)"
 and "\A. finite (A::'a set) \ finite (- A) = finite (UNIV::'a set)"
 and "rhs \ let n = card (UNIV::'a set) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n \ (\x\set xs'. x \ set ys') \ (\y\set ys'. y \ set xs')"
 and "\xs ys. set ((xs::'a list) @ ys) = set xs \ set ys"
 and "\A B. ((A::'a set) = B) = (A \ B \ B \ A)"
 and "\xs. set (remdups (xs::'a list)) = set xs"
 and "subset' = (\)"
 and "\A B. (\x. (x::'a) \ A \ x \ B) \ A \ B"
 and "\A B. \(A::'a set) \ B; B \ A\ \ A = B"
 and "\A ys. (A \ List.coset ys) = (\y\set ys. (y::'a) \ A)"
 using that by (smt (verit, default))

notepad
begin
 have "line_integral F {i, j} g = line_integral F {i} g + line_integral F {j} g"
 if \<open>(k, g) \<in> one_chain_typeI\<close>
 \<open>\<And>A b B. ({} = (A::(real \<times> real) set) \<inter> insert (b::real \<times> real) (B::(real \<times> real) set)) = (b \<notin> A \<and> {} = A \<inter> B)\<close>
 \<open>finite ({} :: (real \<times> real) set)\<close>
 \<open>\<And>a A. finite (A::(real \<times> real) set) \<Longrightarrow> finite (insert (a::real \<times> real) A)\<close>
 \<open>(i::real \<times> real) = (1::real, 0::real)\<close>
 \<open> \<And>a A. (a::real \<times> real) \<in> (A::(real \<times> real) set) \<Longrightarrow> insert a A = A\<close> \<open>j = (0, 1)\<close>
 \<open>\<And>x. (x::(real \<times> real) set) \<inter> {} = {}\<close>
 \<open>\<And>y x A. insert (x::real \<times> real) (insert (y::real \<times> real) (A::(real \<times> real) set)) = insert y (insert x A)\<close>
 \<open>\<And>a A. insert (a::real \<times> real) (A::(real \<times> real) set) = {a} \<union> A\<close>
 \<open>\<And>F u basis2 basis1 \<gamma>. finite (u :: (real \<times> real) set) \<Longrightarrow>
 line_integral_exists F basis1 \<gamma> \<Longrightarrow>
 line_integral_exists F basis2 \<gamma> \<Longrightarrow>
 basis1 \<union> basis2 = u \<Longrightarrow>
 basis1 \<inter> basis2 = {} \<Longrightarrow>
 line_integral F u \<gamma> = line_integral F basis1 \<gamma> + line_integral F basis2 \<gamma>\<close>
 \<open>one_chain_line_integral F {i} one_chain_typeI =
 one_chain_line_integral F {i} one_chain_typeII \<and>
 (\<forall>(k, \<gamma>)\<in>one_chain_typeI. line_integral_exists F {i} \<gamma>) \<and>
 (\<forall>(k, \<gamma>)\<in>one_chain_typeII. line_integral_exists F {i} \<gamma>)\<close>
 \<open> one_chain_line_integral (F::real \<times> real \<Rightarrow> real \<times> real) {j::real \<times> real}
 (one_chain_typeII::(int \<times> (real \<Rightarrow> real \<times> real)) set) =
 one_chain_line_integral F {j} (one_chain_typeI::(int \<times> (real \<Rightarrow> real \<times> real)) set) \<and>
 (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeII. line_integral_exists F {j} \<gamma>) \<and>
 (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeI. line_integral_exists F {j} \<gamma>)\<close>
 for F i j g one_chain_typeI one_chain_typeII and
 line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> real\<close> and
 line_integral_exists :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> bool\<close> and
 one_chain_line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real)) set \<Rightarrow> real\<close> and
 k
 using prod.case_eq_if singleton_inject snd_conv
 that
 by (smt (verit))
end

lemma
 fixes x y z :: real
 assumes \<open>x + 2 * y > 0\<close> and
 \<open>x - 2 * y > 0\<close> and
 \<open>x < 0\<close>
 shows False
 using assms by (smt (verit))

(*test for arith reconstruction*)
lemma
 fixes d :: real
 assumes \<open>0 < d\<close>
 \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
 \<open>\<And>a b c :: real. (a / c a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
 \<open>\<And>a b c :: real. (a / c a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
 \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
 \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
 \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
 (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
 (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
 (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
 False\<close>
 using assms
 by (smt (verit,del_insts))

lemma
 fixes d :: real
 assumes \<open>0 < d\<close>
 \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
 \<open>\<And>a b c :: real. (a / c a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
 \<open>\<And>a b c :: real. (a / c a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
 \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
 \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
 \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
 (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
 (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
 (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
 False\<close>
 using assms
 by (smt (verit,ccfv_threshold))

(*qnt_rm_unused example*)
lemma
 assumes \<open>\<forall>z y x. P z y\<close>
 \<open>P z y \<Longrightarrow> False\<close>
 shows False
 using assms
 by (smt (verit))

lemma
 "max (x::int) y \ y"
 supply [[smt_trace]]
 by (smt (verit))+

context
begin
abbreviation finite' :: "'a set \<Rightarrow> bool"
 where "finite' A \ finite A \ A \ {}"

lemma
 fixes f :: "'b \ 'c :: linorder"
 assumes
 \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
 \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
 \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
 finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
 \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
 finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
 \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
 b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
 b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
 b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
 b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
 inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
 \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
 \<open>inj_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set))\<close>
 \<open>finite (B::'a::type set)\<close>
 \<open>(B::'a::type set) \<noteq> {}\<close>
 \<open>arg_min_on ((f::'b::type \<Rightarrow> 'c::linorder) \<circ> (g::'a::type \<Rightarrow> 'b::type)) (B::'a::type set) \<in> B\<close>
 \<open>\<nexists>x::'a::type.
 x \<in> (B::'a::type set) \<and>
 ((f::'b::type \ 'c::linorder) \ (g::'a::type \ 'b::type)) x < (f \ g) (arg_min_on (f \ g) B)\
 \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (P::'b::type \<Rightarrow> bool) a::'b::type.
 inj_on f (Collect P) \<and> P a \<and> (\<forall>y::'b::type. P y \<longrightarrow> f a \<le> f y) \<longrightarrow> arg_min f P = a\<close>
 \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
 \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
 \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
 finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
 \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
 finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
 \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
 \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
 b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
 b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
 b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
 b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
 \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {}) \<close>
 \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {})\<close>
 \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
 inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
 \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
 \<open>arg_min_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set)) \<noteq>
 g (arg_min_on (f \<circ> g) B) \<close>
 shows False
 using assms
 by (smt (verit))
end

experiment
begin
private datatype abort =
 Rtype_error
 | Rtimeout_error
private datatype ('a) error_result =
 Rraise " 'a " \<comment> \<open>\<open> Should only be a value of type exn \<close>\<close>
 | Rabort " abort "

private datatype( 'a, 'b) result =
 Rval " 'a "
 | Rerr " ('b) error_result "

lemma
 fixes clock :: \<open>'astate \<Rightarrow> nat\<close> and
 fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
 'astate*((('v)list),('v))result\
 assumes
 "fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
 (st'::'astate, r::('v list, 'v) result)"
 "clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0])) \ clock st"
 "\(b::nat) (a::nat) c::nat. b \ a \ c \ b \ c \ a"
 "\(a::'astate) p::'astate \ ('v list, 'v) result. (a = fst p) = (\b::('v list, 'v) result. p = (a, b))"
 "\y::'v error_result. (\x1::'v. y = Rraise x1 \ False) \ (\x2::abort. y = Rabort x2 \ False) \ False"
 "\(f1::'v \ 'astate \ ('v list, 'v) result) (f2::abort \ 'astate \ ('v list, 'v) result) x1::'v.
 (case Rraise x1 of Rraise (x::'v) \ f1 x | Rabort (x::abort) \ f2 x) = f1 x1"
 "\(f1::'v \ 'astate \ ('v list, 'v) result) (f2::abort \ 'astate \ ('v list, 'v) result) x2::abort.
 (case Rabort x2 of Rraise (x::'v) \ f1 x | Rabort (x::abort) \ f2 x) = f2 x2"
 "\(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
 fix_clock s1 (s2, x) = (s, x) \<longrightarrow> clock s \<le> clock s2"
 "\(s::'astate) (s'::'astate) res::('v list, 'v) result.
 fix_clock s (s', res) =
 (update_clock (\<lambda>_::nat. if clock s' \<le> clock s then clock s' else clock s) s', res)"
 "\(x2::'v error_result) x1::'v.
 (r::('v list, 'v) result) = Rerr x2 \<and> x2 = Rraise x1 \<longrightarrow>
 clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat \<times> 'exp0) list) x1))
 \<le> clock st'"
 shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) \
 clock
 (fst (case x2 of
 Rraise (v2::'v) \
 fun_evaluate_match (st'::'astate) (env::'vsemv_env) v2 (pes::('pat \<times> 'exp0) list) v2
 | Rabort (abort::abort) \<Rightarrow> (st', Rerr (Rabort abort))))
 \<le> clock (st::'astate))"
 using assms by (smt (verit))
end

context
 fixes piecewise_C1 :: "('real :: {one,zero,ord} \ 'a :: {one,zero,ord}) \ 'real set \ bool" and
 joinpaths :: "('real \ 'a) \ ('real \ 'a) \ 'real \ 'a"
begin
notation piecewise_C1 (infixr \<open>piecewise'_C1'_differentiable'_on\<close> 50)
notation joinpaths (infixr \<open>+++\<close> 75)

lemma
 \<open>(\<And>v1. \<forall>v0. (rec_join v0 = v1 \<and>
 (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
 (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
 (\<forall>v2 v3 v4.
 v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
 False) =
 (rec_join v0 = rec_join v0 \<and>
 (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
 (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
 (\<forall>v2 v3 v4.
 v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
 False) \<longrightarrow>
 False)) \<Longrightarrow>
 (\<forall>v0 v1.
 rec_join v0 = v1 \<and>
 (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
 (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
 (\<forall>v2 v3 v4. v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
 False) =
 (\<forall>v0. rec_join v0 = rec_join v0 \<and>
 (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
 (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
 (\<forall>v2 v3 v4.
 v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
 False) \<longrightarrow>
 False)\<close>
 by (smt (verit))

end

section \<open>Monomorphization examples\<close>

definition Pred :: "'a \ bool" where
 "Pred x = True"

lemma poly_Pred: "Pred x \ (Pred [x] \ \ Pred [x])"
 by (simp add: Pred_def)

lemma "Pred (1::int)"
 by (smt (verit) poly_Pred)

axiomatization g :: "'a \ nat"
axiomatization where
 g1: "g (Some x) = g [x]" and
 g2: "g None = g []" and
 g3: "g xs = length xs"

lemma "g (Some (3::int)) = g (Some True)" by (smt (verit) g1 g2 g3 list.size)

experiment
begin

lemma duplicate_goal: \<open>A \<Longrightarrow> A \<Longrightarrow> A\<close>
 by auto

datatype 'a M_nres = is_fail: FAIL | SPEC "'a \<Rightarrow> bool"

definition "is_res m x \ case m of FAIL \ True | SPEC P \ P x"

datatype ('a,'s) M_state = M_STATE (run: "'s \ ('a\'s) M_nres")

(*Courtesy of Peter Lammich
https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20smt.20.28verit.29.3A.20exception.20THM.200.20raised.20.28line.20312.20.2E.2E.2E/near/290088165
*)
lemma "\\x y. (\xa s. is_fail (run (x xa) s) \
 is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
 (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
\<longrightarrow>
 (\<forall>s. is_fail (run (B x) s) \<or>
 is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
 (\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
 \<And>y. \<forall>x ya. (\<forall>xa s. is_fail (run (x xa) s) \<or>
 is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
 (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
\<longrightarrow>
 (\<forall>s. is_fail (run (C y x) s) \<or>
 is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
 (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a,
b)))\<rbrakk>
 \<Longrightarrow> \<forall>x y. (\<forall>xa s.
 is_fail (run (x xa) s) \<or>
 is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
 (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
\<longrightarrow>
 (\<forall>s. is_fail (run (B x) s) \<or>
 (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
 (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and>
is_fail (run (C a y) b))) =
 (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and>
is_fail (run (C a x) b))) \<and>
 (\<forall>a b. (is_fail (run (B y) s) \<or>
 (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y)
ba) (a, b))) =
 (is_fail (run (B x) s) \<or>
 (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x)
ba) (a, b)))))"
 apply (rule duplicate_goal)
 subgoal
 supply [[verit_compress_proofs=true]]
 by (smt (verit))
 subgoal
 supply [[verit_compress_proofs=false]]
 by (smt (verit))
 done

(*Example of Reordering in skolemization*)
lemma
 fixes Abs_ExpList :: "'freeExp_list \ 'exp_list" and
 Abs_Exp:: "'freeExp_set \ 'exp" and
 exprel:: "('freeExp \ 'freeExp) set" and
 map2 :: "('freeExp \ 'exp) \ 'freeExp_list \ 'exp_list"
 assumes "\Xs. Abs_ExpList Xs \ map2 (\U. Abs_Exp (myImage exprel {U})) Xs"
 "\P z. (\U. z = Abs_Exp (myImage exprel {U}) \ P) \ P"
 "\(ys::'exp_list) (f::'freeExp \ _). (\xs. ys = map2 f xs) = (\y\myset ys. \x. y = f x)"
 shows "\Us. z = Abs_ExpList Us"
 apply (rule duplicate_goal)
 subgoal
 supply [[verit_compress_proofs=true]]
 using assms
 by (smt (verit,del_insts))
 subgoal
 using assms
 supply [[verit_compress_proofs=false]]
 by (smt (verit,del_insts))
 done

end

context
 fixes
 L2_final :: "'afset \ 'afset \ 'afset \ bool" and
 L3_final :: "'afset \ 'afset \ 'afset \ bool" and
 ground_resolution :: "'a \ 'a \ 'a \ bool" and
 is_least_false_clause :: "'afset \ 'a \ bool" and
 fset :: "'afset \ 'a set" and
 union_fset :: "'afset \ 'afset \ 'afset" (infixr \|\|\ 50)
begin
term "a |\| b"

fun L2_matches_L3 where
 "L2_matches_L3 N2 (Ur2, Uff2) N3 (Urr3, Uff3) \
 N2 = N3 \<and> Uff2 = Uff3 \<and>
 (\<forall>Cr \<in> fset Ur2. \<exists>C \<in> fset (N3 |\<union>| Urr3 |\<union>| Uff3). \<exists>D \<in> fset (N3 |\<union>| Urr3 |\<union>| Uff3).
 (ground_resolution D)\<^sup>+\<^sup>+ C Cr \<and>
 (\<exists>Crr \<in> fset Urr3. (ground_resolution D)\<^sup>*\<^sup>* Cr Crr) \<or> (is_least_false_clause (N2 |\<union>| Ur2 |\<union>| Uff2) Cr))"

lemma
 assumes match: "L2_matches_L3 Const2 S2 Const3 S3"
 shows "L2_final Const2 S2 \ L2_final Const3 S3"
proof -
 from match obtain N Ur Uff Urr where
 state_simps:
 "Const2 = N"
 "Const3 = N"
 "S2 = (Ur, Uff)"
 "S3 = (Urr, Uff)" and
 Ur_spec: "
 \<forall>Cr \<in> fset Ur.
 \<exists>C \<in> fset (N |\<union>| Urr |\<union>| Uff).
 \<exists>D \<in> fset (N |\<union>| Urr |\<union>| Uff).
 (ground_resolution D)\<^sup>+\<^sup>+ C Cr \<and>
 (\<exists>Crr \<in> fset Urr. (ground_resolution D)\<^sup>*\<^sup>* Cr Crr) \<or>
 (is_least_false_clause (N |\<union>| Ur |\<union>| Uff) Cr)"
 by (smt (verit) L2_matches_L3.elims(2))
 oops
end

end

quality97%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.