| products/sources/formale sprachen/PVS/Bernstein/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: expt_rew.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(util
(le_realorder 0 (le_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil) ((realorder? const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (lt_realorder 0 (lt_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil) ((realorder? const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (ge_realorder 0 (ge_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil) ((realorder? const-decl "bool" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (gt_realorder 0 (gt_realorder-1 nil 3499875743 ("" (judgement-tcc) nil nil) ((realorder? const-decl "bool" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (relreal_scal 0 (relreal_scal-1 nil 3503403768 ("" (case "FORALL (relreal: RealOrder, x, y: real, pr: posreal): relreal(x, y) IMPLIES relreal(pr * x, pr * y)") (("1" (skeep) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst - "relreal" "pr*x" "pr*y" "1/pr") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred "relreal") (("2" (expand "realorder?") (("2" (split -) (("1" (replace -1) (("1" (assert) (("1" (mult-by -2 "pr") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (mult-by -2 "pr") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (assert) (("3" (mult-by -2 "pr") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (replace -1) (("4" (assert) (("4" (mult-by -2 "pr") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_times_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) (realorder? const-decl "bool" util nil) (RealOrder type-eq-decl nil util 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (edge_point?_TCC1 0 (edge_point?_TCC1-1 nil 3509968302 ("" (subtype-tcc) nil nil) nil nil)) (normalize_lambda_TCC1 0 (normalize_lambda_TCC1-1 nil 3500326686 ("" (subtype-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) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (lt_below? const-decl "bool" util nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util 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) (real_plus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil)) nil)) (normalize_lambda_TCC2 0 (normalize_lambda_TCC2-1 nil 3503397081 ("" (subtype-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) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (lt_below? const-decl "bool" util nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (normalize_lambda_TCC3 0 (normalize_lambda_TCC3-1 nil 3503397081 ("" (subtype-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) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Vars type-eq-decl nil util nil) (lt_below? const-decl "bool" util nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (gt_realorder name-judgement "RealOrder" util nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util 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) (/= const-decl "boolean" notequal nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (normalize_lambda_unitbox 0 (normalize_lambda_unitbox-2 nil 3509875526 ("" (skeep) (("" (hide -2) (("" (expand "normalize_lambda") (("" (expand "unitbox?") (("" (expand "boxbetween?") (("" (expand "interval_between?") (("" (skeep) (("" (inst - "j") (("" (flatten) (("" (case "boundedpts(j)`1 AND boundedpts(j)`2") (("1" (flatten) (("1" (assert) (("1" (case "Avars(j)<=X(j) AND X(j)<=Bvars(j)") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (case "boundedpts(j)`1") (("1" (assert) (("1" (case "Avars(j)<=X(j)") (("1" (assert) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "X(j)<=Bvars(j)") (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((unitbox? const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" util nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (interval_between? const-decl "bool" util 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) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IntervalEndpoints type-eq-decl nil util nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util 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) (real_times_real_is_real application-judgement "real" reals nil) (div_mult_pos_le2 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Vars type-eq-decl nil util nil) (<= const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (boxbetween? const-decl "bool" util nil) (normalize_lambda const-decl "Vars" util nil)) nil) (normalize_lambda_unitbox-1 nil 3509354299 ("" (skeep) (("" (hide -2) (("" (expand "normalize_lambda") (("" (expand "unitbox?") (("" (expand "boxbetween?") (("" (skeep) (("" (inst - "j") (("" (flatten) (("" (case "boundedpts(j)`1 AND boundedpts(j)`2") (("1" (flatten) (("1" (assert) (("1" (case "Avars(j)<=X(j) AND X(j)<=Bvars(j)") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (case "boundedpts(j)`1") (("1" (assert) (("1" (case "Avars(j)<=X(j)") (("1" (assert) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "X(j)<=Bvars(j)") (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (denormalize_listreal_rec_TCC1 0 (denormalize_listreal_rec_TCC1-1 nil 3509627050 ("" (subtype-tcc) nil nil) nil nil)) (denormalize_listreal_rec_TCC2 0 (denormalize_listreal_rec_TCC2-1 nil 3509627050 ("" (subtype-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (denormalize_listreal_rec_TCC3 0 (denormalize_listreal_rec_TCC3-1 nil 3509627050 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (upfrom nonempty-type-eq-decl nil integers nil) (lt_realorder name-judgement "RealOrder" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (length def-decl "nat" list_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (denormalize_listreal_rec_TCC4 0 (denormalize_listreal_rec_TCC4-1 nil 3509627050 ("" (subtype-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (denormalize_listreal_rec_TCC5 0 (denormalize_listreal_rec_TCC5-1 nil 3509627050 ("" (subtype-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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)) nil)) (denormalize_listreal_rec_TCC6 0 (denormalize_listreal_rec_TCC6-1 nil 3509627050 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil) (ge_realorder name-judgement "RealOrder" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (denormalize_listreal_rec_TCC7 0 (denormalize_listreal_rec_TCC7-1 nil 3509627050 ("" (termination-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)) nil)) (denormalize_listreal_rec_TCC8 0 (denormalize_listreal_rec_TCC8-2 nil 3509627195 ("" (skosimp* :preds? t) (("" (name-replace "V47__" "v!1(cdr[real](l!1), nnvars!1, Avars!1, Bvars!1,boundedpts!1)" :hide? t) (("1" (typepred "V47__") (("1" (assert) (("1" (hide (-1 -4)) (("1" (expand "length" 1 1) (("1" (replace -6) (("1" (assert) (("1" (expand "length" 1 2) (("1" (skosimp* :preds? t) (("1" (case-replace "i!1=0") (("1" (expand "nth" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "nth" 2) (("2" (assert) (("2" (expand "length" 2) (("2" (inst -3 "i!1-1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (replaces -6) (("2" (assert) (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide (-1 -3 2)) (("2" (grind) nil nil)) nil)) nil) ("3" (assert) (("3" (hide (-1 -4 2)) (("3" (grind) nil nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" util nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vars type-eq-decl nil util nil) (IntervalEndpoints type-eq-decl nil util nil) (pred type-eq-decl nil defined_types nil) (strict_well_founded? const-decl "bool" orders nil) (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!1 skolem-const-decl "below(length(l!1))" util nil) (l!1 skolem-const-decl "list[real]" util nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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 "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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (upfrom nonempty-type-eq-decl nil integers nil)) nil) (denormalize_listreal_rec_TCC8-1 nil 3509627050 ("" (subtype-tcc) nil nil) nil nil)) (denormalize_listreal_TCC1 0 (denormalize_listreal_TCC1-1 nil 3509627050 ("" (subtype-tcc) nil nil) nil nil)) (translist_polylist_id 0 (translist_polylist_id-1 nil 3509627120 ("" (skosimp* :preds? t) (("" (expand "translist") (("" (expand "polylist") (("" (rewrite "array2list_inv") (("" (rewrite "array2list_inv") (("" (rewrite "array2list_inv") nil nil)) nil)) nil)) nil)) nil)) nil) ((translist const-decl "real" util nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (array2list_inv formula-decl nil array2list "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Polynomial type-eq-decl nil util nil) (Polyproduct type-eq-decl nil util nil) (MultiPolynomial type-eq-decl nil util nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (polylist const-decl "PolyList" util 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (DegreeMono type-eq-decl nil util nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (corner_to_point_TCC1 0 (corner_to_point_TCC1-1 nil 3499445915 ("" (skeep) (("" (expand "unitbox?") (("" (skeep :preds? t) (("" (lemma "array2list_inv[real]") (("" (inst?) (("" (replaces -1) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((unitbox? const-decl "bool" util 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) (array2list_inv formula-decl nil array2list "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" util nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (CoeffMono type-eq-decl nil util nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def 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)) nil))) ¤ Dauer der Verarbeitung: 1.242 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 |
