| products/sources/formale sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: vertical.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(vertical
(nz_spz 0 (nz_spz-1 nil 3432031751 ("" (judgement-tcc) nil 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" vertical nil) (Spz type-eq-decl nil vertical nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (neg_spz 0 (neg_spz-1 nil 3432031751 ("" (skeep :preds? t) (("" (rewrite "abs_neg") nil nil)) nil) ((nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_neg formula-decl nil abs_lems "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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" vertical nil) (Spz type-eq-decl nil vertical nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (on_signed_H 0 (on_signed_H-1 nil 3432556510 ("" (skeep) (("" (typepred "eps") (("" (grind) nil nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (vertical_conflict_neg 0 (vertical_conflict_neg-1 nil 3451899803 ("" (grind) nil 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) (real_ge_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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (vertical_conflict? const-decl "bool" vertical nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (vertical_conflict_symm 0 (vertical_conflict_symm-1 nil 3451899824 ("" (skeep) (("" (split) (("1" (flatten) (("1" (lemma "vertical_conflict_neg") (("1" (inst -1 "sz" "vz") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "vertical_conflict_neg") (("2" (inst -1 "-sz" "-vz") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((vertical_conflict_neg formula-decl nil vertical nil) (minus_real_is_real application-judgement "real" reals 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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) shostak)) (Theta_H_symm 0 (Theta_H_symm-1 nil 3431282370 ("" (skeep) (("" (expand "Theta_H") (("" (rewrite "sign_neg") (("" (assert) nil nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Theta_H const-decl "real" vertical nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (sign_neg formula-decl nil sign "reals/")) shostak)) (Theta_H_lt 0 (Theta_H_lt-1 nil 3431451755 ("" (skeep) (("" (expand "Theta_H") (("" (case "nzvz > 0") (("1" (rewrite "sign_eq_1") (("1" (grind-reals) nil nil)) nil) ("2" (rewrite "sign_eq_neg1") (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil) ((nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Theta_H const-decl "real" vertical nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sign_eq_neg1 formula-decl nil sign "reals/") (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_div_neg_lt1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_eq_1 formula-decl nil sign "reals/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (both_sides_minus_le1 formula-decl nil real_props nil) (both_sides_minus_lt1 formula-decl nil real_props 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (Theta_H_on_H 0 (Theta_H_on_H-1 nil 3471111551 ("" (skeep) (("" (typepred "eps") (("" (grind) nil nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (sign_mult_clos application-judgement "Sign" sign "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign const-decl "Sign" sign "reals/") (Theta_H const-decl "real" vertical nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (Theta_H_eq_0 0 (Theta_H_eq_0-1 nil 3431455094 ("" (skeep) (("" (expand "Theta_H") (("" (cross-mult 1) (("" (case "nzvz > 0") (("1" (rewrite "sign_eq_1") (("1" (grind-reals) (("1" (neg-formula -3) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (rewrite "sign_eq_neg1") (("2" (grind-reals) (("2" (neg-formula -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Theta_H const-decl "real" vertical nil) (zero_times1 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_ge formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (mult_neg formula-decl nil extra_tegies nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sign_eq_1 formula-decl nil sign "reals/") (nnreal type-eq-decl nil real_types nil) (neg_ge formula-decl nil real_props nil) (sign_eq_neg1 formula-decl nil sign "reals/") (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (nzint nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (sign const-decl "Sign" sign "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" vertical nil) (div_cancel3 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (Theta_H_ge_0 0 (Theta_H_ge_0-1 nil 3431455829 ("" (skeep :preds? t) (("" (expand "Theta_H") (("" (case "nzvz > 0") (("1" (cross-mult 2) (("1" (rewrite "sign_eq_1") (("1" (grind-reals) (("1" (neg-formula -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 3) (("2" (grind) (("2" (neg-formula -3) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (Theta_H const-decl "real" vertical nil) (div_mult_neg_ge1 formula-decl nil real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (neg_neg formula-decl nil extra_tegies nil) (neg_one_times formula-decl nil extra_tegies nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (Spz type-eq-decl nil vertical nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (H formal-const-decl "posreal" vertical nil) (sign const-decl "Sign" sign "reals/") (Sign type-eq-decl nil sign "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nzvz skolem-const-decl "nzreal" vertical nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (zero_times1 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_ge formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (neg_spz application-judgement "Spz" vertical nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (mult_neg formula-decl nil extra_tegies nil) (sign_eq_1 formula-decl nil sign "reals/") (nnreal type-eq-decl nil real_types 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) shostak)) (Theta_H_exit_gt_0 0 (Theta_H_exit_gt_0-1 nil 3460649494 ("" (grind) (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)) nil) ((pos_div_gt formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (/= const-decl "boolean" notequal 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) (Theta_H const-decl "real" vertical nil) (sign const-decl "Sign" sign "reals/")) shostak)) (Theta_H_unique_eps 0 (Theta_H_unique_eps-1 nil 3463581492 ("" (skeep) (("" (split) (("1" (flatten) (("1" (inst-cp 1 "1") (("1" (inst 1 "-1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (grind) 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) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign const-decl "Sign" sign "reals/") (Theta_H const-decl "real" vertical nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (Theta_H_unique 0 (Theta_H_unique-1 nil 3463310423 ("" (grind) nil 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) (/= const-decl "boolean" notequal 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) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign const-decl "Sign" sign "reals/") (Theta_H const-decl "real" vertical nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (vertical_los_entry 0 (vertical_los_entry-1 nil 3460733943 ("" (grind) (("1" (neg-formula -2 :auto-step (grind-reals)) nil nil) ("2" (neg-formula -2 :auto-step (grind-reals)) nil nil) ("3" (neg-formula 3 :auto-step (grind-reals)) nil nil) ("4" (neg-formula 3 :auto-step (grind-reals)) nil nil)) nil) ((both_sides_times_neg_ge1 formula-decl nil real_props nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (neg_times_ge formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_neg formula-decl nil extra_tegies nil) (neg_one_times formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_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) (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) (/= const-decl "boolean" notequal 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) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sign const-decl "Sign" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (Theta_H_entry_lt_t 0 (Theta_H_entry_lt_t-1 nil 3460649413 ("" (grind) (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)) nil) ((div_mult_neg_lt1 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (real_gt_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_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (/= const-decl "boolean" notequal 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Theta_H const-decl "real" vertical nil) (sign const-decl "Sign" sign "reals/")) shostak)) (vertical_conflict 0 (vertical_conflict-2 nil 3431456578 ("" (skeep) (("" (split) (("1" (flatten) (("1" (assert) (("1" (expand "vertical_conflict?") (("1" (skeep -1) (("1" (neg-formula 2) (("1" (both-sides-f -1 "sq") (("1" (both-sides-f 1 "sq") (("1" (sq-simp) (("1" (mult-by 2 "2*nnt") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "sq_lt") nil nil)) nil) ("2" (rewrite "sq_lt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "vertical_conflict?") (("2" (split -1) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil) ("2" (name "t1" "Theta_H(sz,nzvz,-1)") (("2" (case "t1 >= 0") (("1" (name "t2" "Theta_H(sz,nzvz,1)") (("1" (lemma "Theta_H_lt") (("1" (inst?) (("1" (inst 1 "(t1+t2)/2") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "0") (("2" (assert) (("2" (lemma "Theta_H_ge_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_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) (H formal-const-decl "posreal" vertical nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (sq_lt formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_plus formula-decl nil sq "reals/") (sq_abs formula-decl nil sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnt skolem-const-decl "nnreal" vertical nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_times_neg_ge1 formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_neg formula-decl nil extra_tegies nil) (neg_one_times formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (vertical_conflict? const-decl "bool" vertical nil) (real_plus_real_is_real application-judgement "real" reals nil) (Theta_H const-decl "real" vertical nil) (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (= const-decl "[T, T -> boolean]" equalities nil) (Theta_H_ge_0 formula-decl nil vertical nil) (Spz type-eq-decl nil vertical nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (sign const-decl "Sign" sign "reals/") (t2 skolem-const-decl "real" vertical nil) (t1 skolem-const-decl "real" vertical nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Theta_H_lt formula-decl nil vertical nil)) nil) (vertical_conflict-1 nil 3431451389 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "vertical_conflict?") (("1" (skeep -1) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "abs(sz) < H") (("1" (hide -2) (("1" (expand "vertical_conflict?") (("1" (inst 1 "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "vertical_conflict?") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (vertical_los_inside_Theta 0 (vertical_los_inside_Theta-2 "" 3504843804 ("" (skeep) (("" (grind) (("1" (lemma "div_mult_pos_gt1") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil) ("4" (lemma "div_mult_neg_gt1") (("4" (inst?) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (grind-reals) nil nil) ("6" (grind-reals) nil nil) ("7" (grind-reals) nil nil) ("8" (grind-reals) nil nil) ("9" (lemma "div_mult_pos_gt1") (("9" (inst?) (("9" (inst?) (("9" (assert) nil nil)) nil)) nil)) nil) ("10" (lemma "div_mult_pos_gt1") (("10" (inst?) (("10" (inst?) (("10" (assert) nil nil)) nil)) nil)) nil) ("11" (lemma "div_mult_neg_gt1") (("11" (inst?) (("11" (inst?) (("11" (assert) nil nil)) nil)) nil)) nil) ("12" (lemma "div_mult_neg_gt1") (("12" (inst?) (("12" (inst?) (("12" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (Theta_H const-decl "real" vertical nil) (sign const-decl "Sign" sign "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_ge_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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (H formal-const-decl "posreal" vertical nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (div_mult_neg_lt2 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (div_mult_neg_gt1 formula-decl nil extra_real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak) (vertical_los_inside_Theta-1 nil 3448810512 ("" (skeep) (("" (grind) (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil) ("5" (grind-reals) nil nil) ("6" (grind-reals) nil nil) ("7" (grind-reals) nil nil) ("8" (grind-reals) nil nil) ("9" (grind-reals) nil nil) ("10" (grind-reals) nil nil) ("11" (grind-reals) nil nil) ("12" (grind-reals) nil nil)) nil)) nil) ((sign const-decl "Sign" sign "reals/")) nil)) (vertical_sep_outside_Theta 0 (vertical_sep_outside_Theta-1 nil 3463310676 ("" (skosimp*) (("" (lemma "vertical_los_inside_Theta") (("" (inst - "nzvz!1" "sz!1" "t!1") (("" (lemma "Theta_H_unique") (("" (inst - "nzvz!1" "sz!1" "t!1") (("" (lemma "Theta_H_lt") (("" (inst - "nzvz!1" "sz!1") (("" (name "myabs" "abs(sz!1 + t!1 * nzvz!1)") (("" (name "entryone" "Theta_H(sz!1, nzvz!1, Entry)") (("" (name "exitone" "Theta_H(sz!1, nzvz!1, Exit)") (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vertical_los_inside_Theta formula-decl nil vertical nil) (Theta_H_unique formula-decl nil vertical nil) (Theta_H_lt formula-decl nil vertical nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_H const-decl "real" vertical nil) (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (Theta_H_vertical_dir 0 (Theta_H_vertical_dir-1 nil 3463413902 ("" (skeep) (("" (expand "Theta_H") (("" (grind-reals) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil) ((nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (Theta_H const-decl "real" vertical nil) (neg_ge formula-decl nil real_props nil) (sign const-decl "Sign" sign "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (times_div2 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (neg_times_ge formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil)) nil)) (vertical_tau_entry_exit 0 (vertical_tau_entry_exit-3 "" 3504843925 ("" (skeep) (("" (grind) (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil) ("3" (lemma "both_sides_div_pos_gt1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil) ("4" (lemma "both_sides_div_neg_gt1") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((Theta_H const-decl "real" vertical nil) (sign const-decl "Sign" sign "reals/") (vertical_tau const-decl "real" definitions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_ge_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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (both_sides_div_neg_lt1 formula-decl nil real_props 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) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (H formal-const-decl "posreal" vertical nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_div_neg_gt1 formula-decl nil real_props nil)) shostak) (vertical_tau_entry_exit-2 nil 3465922252 ("" (skeep) (("" (grind) (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)) nil)) nil) ((sign const-decl "Sign" sign "reals/") (vertical_tau const-decl "real" definitions nil)) nil) (vertical_tau_entry_exit-1 nil 3465922232 ("" (skeep) (("" (postpone) nil nil)) nil) nil shostak)) (vertical_tau_midpoint 0 (vertical_tau_midpoint-1 nil 3448792694 ("" (grind) nil 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) (/= const-decl "boolean" notequal 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (vertical_tau const-decl "real" definitions nil) (sign const-decl "Sign" sign "reals/") (Theta_H const-decl "real" vertical nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (vertical_tau_pos 0 (vertical_tau_pos-1 nil 3448733819 ("" (skeep) (("" (lemma "Theta_H_ge_0") (("" (inst?) (("" (assert) (("" (lemma "vertical_tau_entry_exit") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Theta_H_ge_0 formula-decl nil vertical nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (vertical_tau_entry_exit formula-decl nil vertical nil) (Spz type-eq-decl nil vertical nil) (H formal-const-decl "posreal" vertical nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (vs_at_neg 0 (vs_at_neg-1 nil 3451839793 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (vs_at const-decl "real" vertical nil)) shostak)) (vs_at_H 0 (vs_at_H-1 nil 3451826874 ("" (grind) nil nil) ((nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (vs_at const-decl "real" vertical nil)) shostak)) (vs_at_complete 0 (vs_at_complete-1 nil 3466361851 ("" (grind) nil 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) (/= const-decl "boolean" notequal 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) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (vs_at const-decl "real" vertical nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (vertical_sep_dir 0 (vertical_sep_dir-1 nil 3466182457 ("" (skeep :preds? t) (("" (hide -3 1) (("" (split +) (("1" (flatten) (("1" (skeep) (("1" (both-sides-f 1 "sq") (("1" (assert) (("1" (sq-simp) (("1" (both-sides-f -4 "sq") (("1" (assert) (("1" (sub-formulas 1 -1) (("1" (mult-ineq -1 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "sq_ge") nil nil)) nil)) nil)) nil) ("2" (lemma "sq_ge") (("2" (inst -1 "abs(spz + t * vz)" "H") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "vz=0") (("1" (assert) nil nil) ("2" (inst -1 "-spz/vz") (("1" (assert) (("1" (field 2) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((neg_spz application-judgement "Spz" vertical nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (vz skolem-const-decl "real" vertical nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers 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) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_ge1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (FDX_46 skolem-const-decl "real" vertical nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (neg_times_ge formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" vertical nil) (Spz type-eq-decl nil vertical nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sq_times formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_plus formula-decl nil sq "reals/") (sq_ge formula-decl nil sq "reals/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (Sign type-eq-decl nil sign "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sign_mult_clos application-judgement "Sign" sign "reals/") (abs_0 formula-decl nil abs_lems "reals/") (ge_times_ge_any1 formula-decl nil extra_real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (mult_neg formula-decl nil extra_tegies nil) (add_neg formula-decl nil extra_tegies nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq_abs formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (vertical_sep_at_sign 0 (vertical_sep_at_sign-1 nil 3466182501 ("" (skeep) (("" (lemma "vertical_sep_dir") (("" (inst?) (("" (assert) (("" (inst -1 "t") (("" (assert) (("" (case-replace "vz=0") (("1" (assert) nil nil) ("2" (typepred "spz") (("2" (case "sign(spz+t*vz)=-sign(spz)") (("1" (hide 2) (("1" (rewrite "sign_abs") (("1" (rewrite "sign_abs") (("1" (replaces -1) (("1" (typepred "dir") (("1" (hide -1) (("1" (grind) (("1" (hide -1) (("1" (neg-formula -3) (("1" (cancel-by -4 "spz") (("1" (mult-by -1 "t") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (real-props -2 :simple? t) (("2" (cancel-by -3 "spz") (("2" (mult-by -1 "t") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -1) (("3" (real-props -3 :simple? t) (("3" (cancel-by -4 "spz") (("3" (mult-by -1 "-t") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide -1) (("4" (real-props -2 :simple? t) (("4" (cancel-by -3 "spz") (("4" (mult-by -1 "-t") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.125 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.Bot Zugriff |
