|
(vectors
(times_TCC1 0
(times_TCC1-1 nil 3254159790 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sqv_TCC1 0
(sqv_TCC1-1 nil 3254159790
("" (skosimp*)
(("" (expand "*") (("" (rewrite "sigma_nonneg") nil nil)) nil))
nil)
((* const-decl "real" vectors nil)
(below type-eq-decl nil naturalnumbers nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T_low type-eq-decl nil sigma "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_high type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Index type-eq-decl nil vectors nil)
(sigma_nonneg formula-decl nil sigma "reals/")
(int_minus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sqv_rew 0
(sqv_rew-1 nil 3440253127 ("" (grind) nil nil)
((* const-decl "real" vectors nil)
(sqv const-decl "nnreal" vectors nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(sqv_sos 0
(sqv_sos-1 nil 3602098415 ("" (grind) nil nil)
((* const-decl "real" vectors nil)
(sqv const-decl "nnreal" vectors nil)
(sq const-decl "nonneg_real" sq "reals/")
(sos const-decl "nnreal" vectors nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(unity_TCC1 0
(unity_TCC1-1 nil 3254159790
("" (skolem 1 "m")
(("" (expand "norm")
(("" (case "sqv(vectors.zero WITH [m := 1]) = 1")
(("1" (expand "zero")
(("1" (replace -1) (("1" (rewrite "sqrt_1") nil nil)) nil))
nil)
("2" (hide 2)
(("2" (expand "sqv")
(("2" (expand "*")
(("2" (typepred "m")
(("2" (case "m=n-1")
(("1" (replace -1 :dir rl)
(("1" (expand "sigma")
(("1" (assert)
(("1" (lemma "sigma_eq")
(("1"
(inst -1
"LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))"
"zero" "m-1" "0")
(("1" (split -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand "zero")
(("1"
(rewrite "sigma_zero")
nil
nil))
nil))
nil))
nil)
("2"
(skolem 1 "N")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sigma_split")
(("2"
(inst -1
"LAMBDA i: (zero WITH [m := 1](i)) * (zero WITH [m := 1](i))"
"n-1" "0" "m")
(("2" (assert)
(("2" (replace -1)
(("2" (hide -1)
(("2"
(case-replace "sigma(1 + m, n - 1,
LAMBDA i: (zero WITH [m := 1](i)) * (zero WITH [m := 1](i))) =0")
(("1"
(hide -1)
(("1"
(assert)
(("1"
(expand "sigma")
(("1"
(assert)
(("1"
(lemma "sigma_eq")
(("1"
(inst
-1
"LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))"
"zero"
"m-1"
"0")
(("1"
(split -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand "zero")
(("1"
(rewrite
"sigma_zero")
nil
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(skolem 1 "N")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(lemma "sigma_eq")
(("2"
(inst
-1
"LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))"
"zero"
"n-1"
"1+m")
(("2"
(split -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand "zero")
(("1"
(rewrite "sigma_zero")
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skolem 1 "N")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors nil)
(* const-decl "real" vectors nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sigma def-decl "real" sigma "reals/")
(sigma_eq formula-decl nil sigma "reals/")
(below type-eq-decl nil naturalnumbers nil)
(sigma_zero formula-decl nil sigma "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sigma_split formula-decl nil sigma "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors nil)
(zero const-decl "Vector" vectors nil))
nil))
(comp_distr_add 0
(comp_distr_add-1 nil 3254159790 ("" (grind) nil nil)
((+ const-decl "real" vectors nil)) nil))
(comp_distr_sub 0
(comp_distr_sub-1 nil 3254159790 ("" (grind) nil nil)
((- const-decl "real" vectors nil)) nil))
(comp_distr_scal 0
(comp_distr_scal-1 nil 3256995715
("" (skosimp*) (("" (grind) nil nil)) nil)
((real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors nil))
shostak))
(comp_distr_neg 0
(comp_distr_neg-1 nil 3467132784
("" (skeep) (("" (grind) nil nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(- const-decl "Vector" vectors nil))
shostak))
(comp_zero 0
(comp_zero-1 nil 3254159790 ("" (grind) nil nil)
((zero const-decl "Vector" vectors nil)) nil))
(comps_eq 0
(comps_eq-1 nil 3440253315
("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil))
nil))
(norm_comp_eq_0 0
(norm_comp_eq_0-2 nil 3428791579
("" (skeep)
(("" (expand "norm")
(("" (split)
(("1" (flatten)
(("1" (lemma "sqrt_eq_0")
(("1" (inst -1 "sqv(v)")
(("1" (split -1)
(("1" (hide -2)
(("1" (rewrite "sqv_sos")
(("1" (expand "sos")
(("1" (lemma "sigma_nonneg_eq_0")
(("1" (inst?)
(("1" (skeep)
(("1" (inst -1 "i")
(("1"
(assert)
(("1" (rewrite "sq_eq_0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (rewrite "sqv_sos")
(("2" (expand "sos")
(("2" (case-replace "(LAMBDA i:sq(v(i))) = (LAMBDA i:0)")
(("1" (hide -)
(("1" (rewrite "sigma_const")
(("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("2" (inst?) (("2" (rewrite "sq_eq_0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_const formula-decl nil sigma "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors nil)
(sos const-decl "nnreal" vectors nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(sq const-decl "nonneg_real" sq "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_low type-eq-decl nil sigma "reals/")
(sq_eq_0 formula-decl nil sq "reals/")
(sigma_nnreal application-judgement "nnreal" vectors nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
(sqv_sos formula-decl nil vectors nil)
(sqrt_eq_0 formula-decl nil sqrt "reals/"))
nil)
(norm_comp_eq_0-1 nil 3428791425
(";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0"
(skeep)
((";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0"
(expand "norm")
((";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0"
(split)
(("1" (flatten)
(("1" (lemma "sqrt_eq_0")
(("1" (inst -1 "sqv(v)")
(("1" (split -1)
(("1" (hide -2)
(("1" (rewrite "sqv_sq")
(("1" (rewrite "sq_plus_eq_0") nil)))))
("2" (propax) nil)))))))))
("2" (flatten)
(("2" (rewrite "sqv_sq")
(("2" (ground)
(("2" (replaces -) (("2" (assert) nil))))))))))))))
";;; developed with shostak decision procedures")
nil nil))
(norm_sqv_eq_0 0
(norm_sqv_eq_0-1 nil 3428791377
("" (skeep)
(("" (expand "norm")
(("" (ground) (("" (replaces -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((norm const-decl "nnreal" vectors nil)
(sqrt_0 formula-decl nil sqrt "reals/"))
nil))
(norm_eq_0 0
(norm_eq_0-1 nil 3430054299
("" (skeep)
(("" (lemma "norm_comp_eq_0")
(("" (inst?)
(("" (replaces -1)
(("" (split)
(("1" (flatten)
(("1" (decompose-equality)
(("1" (inst?)
(("1" (expand "zero") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skeep)
(("2" (decompose-equality -1)
(("2" (inst?)
(("2" (expand "zero") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_comp_eq_0 formula-decl nil vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(zero const-decl "Vector" vectors nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(norm_zero 0
(norm_zero-3 nil 3430834190
("" (lemma "norm_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(norm_eq_0 formula-decl nil vectors nil))
nil)
(norm_zero-2 nil 3428791139
("" (skeep)
(("" (lemma "norm_comp_eq_0")
(("" (inst?)
(("" (replaces -1)
(("" (split)
(("1" (flatten)
(("1" (decompose-equality)
(("1" (inst?)
(("1" (expand "zero") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skeep)
(("2" (decompose-equality -1)
(("2" (inst?)
(("2" (expand "zero") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil)
(norm_zero-1 nil 3254159790
("" (skosimp*)
(("" (expand "norm")
(("" (prop)
(("1" (lemma "sqv_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (replace -1)
(("2" (rewrite "sqv_zero") (("2" (rewrite "sqrt_0") nil nil))
nil))
nil))
nil))
nil))
nil)
((sqrt_0 formula-decl nil sqrt "reals/")) nil))
(sqv_zero 0
(sqv_zero-1 nil 3254159790
("" (expand "sqv")
(("" (expand "*")
(("" (expand "zero") (("" (rewrite "sigma_const") nil nil)) nil))
nil))
nil)
((* const-decl "real" vectors nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(sigma_const formula-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_low type-eq-decl nil sigma "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(below type-eq-decl nil naturalnumbers nil)
(zero const-decl "Vector" vectors nil)
(sqv const-decl "nnreal" vectors nil))
nil))
(sqv_eq_0 0
(sqv_eq_0-2 nil 3428790905
("" (skeep)
(("" (lemma "norm_sqv_eq_0")
(("" (inst?)
(("" (replaces -1 :dir rl)
(("" (lemma "norm_eq_0") (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_sqv_eq_0 formula-decl nil vectors nil)
(norm_eq_0 formula-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(sqv_eq_0-1 nil 3254159790
("" (skolem 1 "v")
(("" (prop)
(("1" (expand "sqv")
(("1" (expand "*")
(("1" (lemma "sigma_nonneg_eq_0")
(("1" (inst?)
(("1" (apply-extensionality 1 :hide? t)
(("1" (inst?)
(("1" (assert)
(("1" (hide -2)
(("1" (grind :theories "real_props") nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (rewrite "sqv_zero") nil nil)) nil))
nil))
nil)
((T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(sigma_nonneg_eq_0 formula-decl nil sigma "reals/"))
nil))
(v_neq_zero 0
(v_neq_zero-1 nil 3428790819
("" (skeep)
(("" (lemma "sqv_eq_0") (("" (inst?) (("" (ground) nil nil)) nil))
nil))
nil)
((sqv_eq_0 formula-decl nil vectors nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(v_neq_0 0
(v_neq_0-1 nil 3412514418
("" (skeep)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (assert)
(("" (expand "norm")
(("" (flatten)
(("" (split +)
(("1" (flatten)
(("1" (expand "sqv")
(("1" (case-replace "v*v = 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (assert)
(("2" (expand "*")
(("2" (lemma "sigma_Fnnr")
(("2"
(inst?)
(("2"
(assert)
(("2"
(expand "sq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -2)
(("2" (expand "zero")
(("2" (expand "sq")
(("2" (lemma "sigma_zero")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(sigma_nnreal application-judgement "nnreal" vectors nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero const-decl "Vector" vectors nil)
(sigma_zero formula-decl nil sigma "reals/")
(sigma_nat application-judgement "nat" vectors nil)
(* const-decl "real" vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(sigma_Fnnr formula-decl nil sigma "reals/")
(below type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_low type-eq-decl nil sigma "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors nil)
(norm const-decl "nnreal" vectors nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(sq_dot_eq_0 0
(sq_dot_eq_0-3 nil 3428790726
("" (skeep)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (replaces -1 :dir rl)
(("" (case-replace "norm(v)=0 IFF sq(norm(v))=0")
(("1" (hide -1)
(("1" (expand "norm")
(("1" (rewrite "sq_sqrt")
(("1" (expand "sqv") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "sq_eq_0") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors nil)
(sq_eq_0 formula-decl nil sq "reals/")
(sqv const-decl "nnreal" vectors nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(sq_dot_eq_0-2 nil 3428790700 nil nil nil)
(sq_dot_eq_0-1 nil 3428790692 ("" (postpone) nil nil) nil shostak))
(nzv_comp_neq_0 0
(nzv_comp_neq_0-1 nil 3430834221
("" (skeep)
(("" (expand "nz_vector?")
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (lemma "norm_comp_eq_0")
(("" (inst?)
(("" (replaces -1)
(("" (ground)
(("1" (skeep -1) (("1" (inst? -2) nil nil)) nil)
("2" (skeep 4)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors nil)
(norm_comp_eq_0 formula-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(nz_norm_gt_0 0
(nz_norm_gt_0-2 nil 3430834334
("" (skeep :preds? t)
(("" (expand "nz_vector?")
(("" (flatten)
(("" (lemma "norm_eq_0")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((norm_eq_0 formula-decl nil vectors nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(nz_norm_gt_0-1 nil 3430833347 ("" (judgement-tcc) nil nil) nil nil))
(nz_sqv_gt_0 0
(nz_sqv_gt_0-2 nil 3430834353
("" (skeep :preds? t)
(("" (lemma "v_neq_zero")
(("" (inst?)
(("" (expand "nz_vector?") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((v_neq_zero formula-decl nil vectors nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Nz_vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(nz_sqv_gt_0-1 nil 3430833347 ("" (judgement-tcc) nil nil) nil nil))
(normalized_nz 0
(normalized_nz-2 nil 3430834369
("" (skeep :preds? t)
(("" (assert)
(("" (lemma "norm_eq_0")
(("" (inst?)
(("" (expand "nz_vector?") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors nil)
(Normalized type-eq-decl nil vectors nil)
(norm_eq_0 formula-decl nil vectors nil))
nil)
(normalized_nz-1 nil 3430833347 ("" (judgement-tcc) nil nil) nil
nil))
(neg_nzv 0
(neg_nzv-1 nil 3431076704
("" (grind)
(("" (decompose-equality -1)
(("" (decompose-equality 1)
(("" (inst?) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "Vector" vectors nil)
(minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(Nz_vector type-eq-decl nil vectors nil)
(/= const-decl "boolean" notequal nil))
nil))
(nz_nzv 0
(nz_nzv-1 nil 3431179313
("" (grind)
(("" (decompose-equality 2)
(("" (decompose-equality -1)
(("" (inst?) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(Vector type-eq-decl nil vectors nil)
(zero const-decl "Vector" vectors nil)
(Nz_vector type-eq-decl nil vectors nil)
(/= const-decl "boolean" notequal nil))
nil))
(neg_zero 0
(neg_zero-1 nil 3462009511
("" (expand "zero")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(- const-decl "Vector" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(zero const-decl "Vector" vectors nil))
shostak))
(add_zero_left 0
(add_zero_left-1 nil 3254159790
("" (skolem 1 "v")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(zero const-decl "Vector" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_zero_right 0
(add_zero_right-1 nil 3254159790
("" (skolem 1 "v")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(zero const-decl "Vector" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_comm 0
(add_comm-1 nil 3254159790
("" (skolem 1 ("u" "v"))
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_assoc 0
(add_assoc-1 nil 3254159790
("" (skolem 1 ("u" "v" "w"))
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(add_move_left 0
(add_move_left-1 nil 3430835475
("" (skolem 1 ("u" "v" "w"))
(("" (ground)
(("1" (decompose-equality 1)
(("1" (decompose-equality -1)
(("1" (inst -1 "x!1") (("1" (grind) nil nil)) nil)) nil))
nil)
("2" (decompose-equality -1)
(("2" (decompose-equality 1)
(("2" (inst -1 "x!1") (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "real" vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(- const-decl "real" vectors nil)
(Vector type-eq-decl nil vectors nil))
nil))
(add_move_right 0
(add_move_right-1 nil 3254159790
("" (skolem 1 ("u" "v" "w"))
(("" (ground)
(("1" (decompose-equality 1)
(("1" (decompose-equality -1)
(("1" (inst -1 "x!1") (("1" (grind) nil nil)) nil)) nil))
nil)
("2" (decompose-equality -1)
(("2" (decompose-equality 1)
(("2" (inst -1 "x!1") (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "real" vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(- const-decl "real" vectors nil)
(Vector type-eq-decl nil vectors nil))
nil))
(add_move_both 0
(add_move_both-1 nil 3254159790
("" (skolem 1 ("u" "v" "w"))
(("" (ground)
(("1" (decompose-equality 1)
(("1" (decompose-equality -1)
(("1" (inst -1 "x!1") (("1" (grind) nil nil)) nil)) nil))
nil)
("2" (decompose-equality -1)
(("2" (decompose-equality 1)
(("2" (inst -1 "x!1") (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "real" vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil)
(- const-decl "real" vectors nil)
(Vector type-eq-decl nil vectors nil))
nil))
(add_neg_sub 0
(add_neg_sub-1 nil 3254159790
("" (skolem 1 ("u" "v"))
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(- const-decl "Vector" vectors nil)
(- const-decl "real" vectors nil)
(Index type-eq-decl nil vectors nil)
(n formal-const-decl "posnat" vectors nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(add_cancel 0
(add_cancel-1 nil 3254159790
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors nil)
(- const-decl "real" vectors nil) (+ const-decl "real" vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil))
nil))
(add_cancel_neg 0
(add_cancel_neg-1 nil 3254159790
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil)
(- const-decl "Vector" vectors nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil))
nil))
(add_cancel2 0
(add_cancel2-1 nil 3255196933
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors nil)
(+ const-decl "real" vectors nil) (- const-decl "real" vectors nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n formal-const-decl "posnat" vectors nil)
(Index type-eq-decl nil vectors nil))
shostak))
(add_cancel_neg2 0
(add_cancel_neg2-1 nil 3255196940
("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)
((Vector type-eq-decl nil vectors nil)
(- const-decl "real" vectors nil) (+ const-decl "real" vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.248 Sekunden
(vorverarbeitet)
¤
|
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
