| products/sources/formale sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: checker.mli Sprache: LispOriginal von: PVS© |
|
||||||
|
(bands_si
(FlightPlanRelevant_nz_TCC1 0 (FlightPlanRelevant_nz_TCC1-1 nil 3482079804 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (FlightPlanRelevant_nz_TCC2 0 (FlightPlanRelevant_nz_TCC2-1 nil 3482079804 ("" (subtype-tcc) nil nil) nil nil)) (FlightPlanRelevant_nz_TCC3 0 (FlightPlanRelevant_nz_TCC3-1 nil 3482079804 ("" (skeep) (("" (inst + "lambda (jj: below[N]): (# time:= B+to+jj,position:= (# x:=jj, y:=jj, z:=jj #) # (("" (assert) (("" (grind) (("" (expand "zero") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (FlightPlanRelevant_nz_TCC4 0 (FlightPlanRelevant_nz_TCC4-1 nil 3483101761 ("" (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) (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) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (FlightPlanRelevant_nz_TCC5 0 (FlightPlanRelevant_nz_TCC5-1 nil 3483101761 ("" (skeep) (("" (inst + "lambda (jj: below[N]): (# time:= B+to+jj,position:= (# x:=jj, y:=jj, z:=jj #) # (("" (assert) (("" (assert) (("" (skeep) (("" (expand "velocity") (("" (expand "vect2") (("" (assert) (("" (expand "zero") (("" (assert) (("" (expand "-") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_types nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" bands_si nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_si nil) (D formal-const-decl "posreal" bands_si nil) (H formal-const-decl "posreal" bands_si nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (velocity const-decl "Vect3" flightplan nil) (zero const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (to skolem-const-decl "real" bands_si nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (scal_1 formula-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/")) nil)) (trk_bands_si_i_TCC1 0 (trk_bands_si_i_TCC1-1 nil 3478881738 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_i_TCC2 0 (trk_bands_si_i_TCC2-1 nil 3478881738 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_i_TCC3 0 (trk_bands_si_i_TCC3-1 nil 3478881738 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (default const-decl "T" fseqs "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/") (trk_fseq? const-decl "bool" fseqs_aux_2D nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (trk_bands_si_i_TCC4 0 (trk_bands_si_i_TCC4-1 nil 3478881738 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (trk_bands_si_i_TCC5 0 (trk_bands_si_i_TCC5-1 nil 3478881738 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nzv2 application-judgement "Nz_vect2" definitions_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (trk_bands_si_i_TCC6 0 (trk_bands_si_i_TCC6-1 nil 3478881738 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep 3) (("" (skeep 3) (("" (skeep 3) (("" (skeep 3) (("" (skeep 3) (("" (skeep 3) (("" (skeep 3) (("" (replace -1) (("" (replace -2) (("" (replace -4) (("" (replace -5) (("" (typepred fp) (("" (inst - "i+1") (("" (assert) (("" (hide -3 -4 -6 -7) (("" (replace -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (replace -3) (("" (hide -3) (("" (expand "min") (("" (expand "max") (("" (lift-if) (("" (ground) (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_minus_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) (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) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (velocity const-decl "Vect3" flightplan nil) (zero const-decl "Vector" vectors_2D "vectors/") (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (expand_trk_bands_si_i_TCC1 0 (expand_trk_bands_si_i_TCC1-1 nil 3482583015 ("" (subtype-tcc) nil nil) nil nil)) (expand_trk_bands_si_i_TCC2 0 (expand_trk_bands_si_i_TCC2-1 nil 3482583015 ("" (subtype-tcc) nil nil) nil nil)) (expand_trk_bands_si_i_TCC3 0 (expand_trk_bands_si_i_TCC3-1 nil 3482583015 ("" (subtype-tcc) nil nil) nil nil)) (expand_trk_bands_si_i_TCC4 0 (expand_trk_bands_si_i_TCC4-1 nil 3482583015 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (int_minus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals 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) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (expand_trk_bands_si_i_TCC5 0 (expand_trk_bands_si_i_TCC5-1 nil 3482583015 ("" (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) (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) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (velocity const-decl "Vect3" flightplan nil) (zero const-decl "Vector" vectors_2D "vectors/") (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (expand_trk_bands_si_i_TCC6 0 (expand_trk_bands_si_i_TCC6-1 nil 3482583015 ("" (skeep) (("" (skeep) (("" (skeep) (("" (replace -3) (("" (replace -4) (("" (expand "max") (("" (expand "min") (("" (lift-if) (("" (assert) (("" (typepred fp) (("" (ground) (("" (inst - "i+1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (zero const-decl "Vector" vectors_2D "vectors/") (velocity const-decl "Vect3" flightplan nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil)) (expand_trk_bands_si_i 0 (expand_trk_bands_si_i-1 nil 3482583017 ("" (skeep) (("" (assert) (("" (expand "trk_bands_si_i") (("" (propax) nil nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers 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_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil)) shostak)) (trk_bands_si_TCC1 0 (trk_bands_si_TCC1-1 nil 3478861570 ("" (typepred "N") (("" (assert) (("" (skeep) (("" (assert) nil nil)) nil)) nil)) nil) ((real_gt_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) (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) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil)) nil)) (trk_bands_si_TCC2 0 (trk_bands_si_TCC2-1 nil 3478861570 ("" (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) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (< 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_types 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) (nzv2 application-judgement "Nz_vect2" definitions_3D nil)) nil)) (trk_bands_si_TCC3 0 (trk_bands_si_TCC3-1 nil 3478861570 ("" (skeep) (("" (assert) nil nil)) 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)) (trk_bands_si_TCC4 0 (trk_bands_si_TCC4-1 nil 3483101761 ("" (skeep) (("" (assert) (("" (typepred " v(so, vo, to, fp)(i - 1)") (("" (typepred "trk_bands_si_i(so, vo, to, fp)(i)") (("" (auto-rewrite "sort_trk_fseq") (("" (auto-rewrite "comp_trk_fseq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (sort_trk_fseq judgement-tcc nil fseqs_aux_2D nil) (comp_trk_fseq judgement-tcc nil fseqs_aux_2D 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (>= 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) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (trk_fseq? const-decl "bool" fseqs_aux_2D nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" bands_si nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/")) nil)) (gs_bands_si_i_TCC1 0 (gs_bands_si_i_TCC1-1 nil 3482673238 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (default const-decl "T" fseqs "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (gs_bands_si_TCC1 0 (gs_bands_si_TCC1-1 nil 3482673238 ("" (skeep) (("" (typepred " v(so, vo, to, fp)(i-1)") (("1" (auto-rewrite "sort_gs_fseq") (("1" (auto-rewrite "comp_gs_fseq") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types nil) (< const-decl "bool" reals 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) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (gsmin formal-const-decl "posreal" bands_si nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (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) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers 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) (sort_gs_fseq judgement-tcc nil fseqs_aux_2D nil) (comp_gs_fseq judgement-tcc nil fseqs_aux_2D nil)) nil)) (vs_bands_si_i_TCC1 0 (vs_bands_si_i_TCC1-1 nil 3482684663 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (velocity const-decl "Vect3" flightplan nil) (default const-decl "T" fseqs "structures/") (empty_seq const-decl "fsq" fseqs "structures/") (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (vs_bands_si_TCC1 0 (vs_bands_si_TCC1-1 nil 3482684663 ("" (skeep) (("" (typepred " v(so, vo, to, fp)(i - 1)") (("1" (assert) (("1" (auto-rewrite sort_vs_fseq) (("1" (auto-rewrite comp_vs_fseq) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((increasing? const-decl "bool" sort_fseq "structures/") (<= const-decl "bool" reals nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals 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) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (zero const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil) (> const-decl "bool" reals nil) (vsmin formal-const-decl "real" bands_si nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (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) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers 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) (comp_vs_fseq judgement-tcc nil fseqs_aux_vertical nil) (sort_vs_fseq judgement-tcc nil fseqs_aux_vertical nil)) nil)) (red_trk_band_fp?_TCC1 0 (red_trk_band_fp?_TCC1-1 nil 3478960506 ("" (subtype-tcc) nil nil) nil nil)) (red_trk_band_fp?_TCC2 0 (red_trk_band_fp?_TCC2-1 nil 3478960506 ("" (subtype-tcc) nil nil) nil nil)) (red_gs_band_fp?_TCC1 0 (red_gs_band_fp?_TCC1-1 nil 3482673238 ("" (subtype-tcc) nil nil) nil nil)) (red_gs_band_fp?_TCC2 0 (red_gs_band_fp?_TCC2-1 nil 3482673238 ("" (subtype-tcc) nil nil) nil nil)) (red_vs_band_fp?_TCC1 0 (red_vs_band_fp?_TCC1-1 nil 3482684663 ("" (subtype-tcc) nil nil) nil nil)) (red_vs_band_fp?_TCC2 0 (red_vs_band_fp?_TCC2-1 nil 3482684663 ("" (subtype-tcc) nil nil) nil nil)) (segdefs_TCC1 0 (segdefs_TCC1-1 nil 3482252086 ("" (subtype-tcc) nil nil) nil nil)) (segdefs_TCC2 0 (segdefs_TCC2-1 nil 3482252086 ("" (subtype-tcc) nil nil) nil nil)) (segdefs_TCC3 0 (segdefs_TCC3-1 nil 3482252086 ("" (subtype-tcc) nil nil) ((N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (T formal-const-decl "{AB: posreal | AB > B}" bands_si nil) (B formal-const-decl "nnreal" bands_si nil) (nnreal type-eq-decl nil real_types nil) (H formal-const-decl "posreal" bands_si nil) (D formal-const-decl "posreal" bands_si nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (seg_lh_bottom const-decl "nnreal" cd3d_si nil)) nil)) (segdefs 0 (segdefs-1 nil 3482252087 ("" (skeep) (("" (expand "seg_lh_bottom") (("" (expand "seg_lh_top") (("" (propax) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (seg_lh_bottom const-decl "nnreal" cd3d_si nil) (seg_lh_top const-decl "real" cd3d_si nil)) shostak)) (trk_bands_si_combines_TCC1 0 (trk_bands_si_combines_TCC1-1 nil 3479234100 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_combines 0 (trk_bands_si_combines-1 nil 3479234134 ("" (skolem 1 (fp so to vo _ x)) (("" (induct i) (("1" (flatten) (("1" (inst 1 0) (("1" (expand "trk_bands_si") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep -1 (0)) (("2" (expand "trk_bands_si") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) (("3" (assert) (("3" (prop) (("1" (assert) (("1" (skosimp*) (("1" (inst 1 "j!1") nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (typepred "j!1") (("2" (typepred "j!2") (("2" (assert) (("2" (expand trk_bands_si 1) (("2" (lemma member_sort) (("2" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k) o trk_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) (("2" (lemma member_composition) (("2" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k)" "trk_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand trk_bands_si -1) (("3" (assert) (("3" (inst 1 "1+k") (("3" (assert) (("3" (lemma member_sort) (("3" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k) o trk_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) (("3" (lemma member_composition) (("3" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k)" "trk_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) (("4" (skosimp*) (("4" (typepred "j!1") (("4" (assert) (("4" (expand "trk_bands_si") (("4" (assert) (("4" (lemma member_sort) (("4" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k) o trk_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (lemma member_composition) (("4" (inst - "trk_bands_si_i(so, vo, to, fp)(1 + k)" "trk_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (case "j!1 = k+1") (("1" (assert) nil nil) ("2" (assert) (("2" (inst 5 "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "trk_bands_si") (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil) ("5" (expand "trk_bands_si") (("5" (assert) nil nil)) nil)) nil)) nil) ((AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (member const-decl "bool" fseqs "structures/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (trk_fseq? const-decl "bool" fseqs_aux_2D nil) (increasing? const-decl "bool" sort_fseq "structures/") (trk_bands_si def-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (N formal-const-decl "above[1]" bands_si nil) (above nonempty-type-eq-decl nil int_types 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-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) (subrange_induction formula-decl nil subrange_inductions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (O const-decl "fseq" fseqs "structures/") (member_composition formula-decl nil fseqs "structures/") (member_sort formula-decl nil sort_fseq "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (empty_no_members_TCC1 0 (empty_no_members_TCC1-1 nil 3481476958 ("" (subtype-tcc) nil 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) (default const-decl "T" fseqs "structures/") (empty_seq const-decl "fsq" fseqs "structures/")) nil)) (empty_no_members 0 (empty_no_members-1 nil 3481476959 ("" (skeep) (("" (expand "member") (("" (skosimp) (("" (typepred "i!1") (("" (assert) (("" (expand "empty_seq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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 "bool" 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) (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)) shostak)) (trk_bands_si_component_TCC1 0 (trk_bands_si_component_TCC1-1 nil 3481474538 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.69 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 |
