| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 381 kB |
|
Impressum bands_si.prfSprache: Lisp |
|||||||||||||||
|
(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 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_component_TCC2 0 (trk_bands_si_component_TCC2-1 nil 3481474538 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_component_TCC3 0 (trk_bands_si_component_TCC3-1 nil 3481474538 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_component_TCC4 0 (trk_bands_si_component_TCC4-1 nil 3481536201 ("" (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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_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) (int_minus_int_is_int application-judgement "int" integers 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)) (trk_bands_si_component_TCC5 0 (trk_bands_si_component_TCC5-1 nil 3481557068 ("" (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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil 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) (real_le_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) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (trk_bands_si_component_TCC6 0 (trk_bands_si_component_TCC6-1 nil 3481565581 ("" (skeep) (("" (skeep) (("" (replace -1) (("" (hide -1) (("" (replace -3) (("" (hide -3) (("" (expand "max") (("" (expand "min") (("" (lift-if) (("" (assert) (("" (lift-if) (("" (assert) (("" (ground) (("" (typepred fp) (("" (inst - "j+1") (("" (assert) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (trk_bands_si_component 0 (trk_bands_si_component-1 nil 3481474538 ("" (lemma trk_bands_si_combines) (("" (skeep) (("" (inst?) (("" (assert) (("" (expand "trk_bands_si_i") (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst 1 j) (("1" (lift-if) (("1" (ground) (("1" (expand "member") (("1" (skolem -2 ii) (("1" (typepred ii) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand member) (("2" (skolem -2 ii) (("2" (typepred ii) (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand member) (("3" (skolem -2 ii) (("3" (typepred ii) (("3" (expand "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand member) (("4" (skolem -2 ii) (("4" (typepred ii) (("4" (expand "empty_seq") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (expand member) (("5" (skolem -2 ii) (("5" (typepred ii) (("5" (expand "empty_seq") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("6" (expand member) (("6" (skolem -2 ii) (("6" (typepred ii) (("6" (expand "empty_seq") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst 1 j) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (int_plus_int_is_int application-judgement "int" integers 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_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) (int_minus_int_is_int application-judgement "int" integers nil) (below type-eq-decl nil naturalnumbers nil) (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (- 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (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) (trk_bands_si_combines formula-decl nil bands_si nil)) shostak)) (trk_bands_si_length 0 (trk_bands_si_length-1 nil 3482578246 ("" (skolem 1 (fp so to vo _ _)) (("" (induct i) (("1" (skeep) (("1" (case "not j=0") (("1" (assert) nil nil) ("2" (replace -1) (("2" (expand "trk_bands_si") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (induct j) (("1" (inst -2 0) (("1" (expand trk_bands_si 1) (("1" (assert) (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 m) (("2" (flatten) (("2" (expand trk_bands_si 1) (("2" (assert) (("2" (expand "o") (("2" (case "m <k") (("1" (assert) (("1" (inst -5 "m+1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand trk_bands_si 2) (("3" (assert) nil nil)) nil) ("4" (typepred "j!1") (("4" (assert) nil nil)) nil) ("5" (assert) nil nil) ("6" (assert) nil nil)) nil)) nil) ("3" (typepred N) (("3" (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) (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) (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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (k skolem-const-decl "subrange(0, N - 2)" bands_si nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j!1 skolem-const-decl "subrange(0, 1 + k)" bands_si nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (j!1 skolem-const-decl "subrange(0, 1 + k)" bands_si nil) (O const-decl "fseq" fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sort_length formula-decl nil sort_fseq "structures/") (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)) shostak)) (trk_bands_si_i_relevant_TCC1 0 (trk_bands_si_i_relevant_TCC1-1 nil 3481980322 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_i_relevant 0 (trk_bands_si_i_relevant-1 nil 3481980322 ("" (skeep) (("" (prop) (("1" (expand "trk_bands_si_i") (("1" (assert) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "trk_bands_si_i") (("2" (assert) (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "trk_bands_si_i") (("3" (assert) (("3" (lemma "trk_bands_3D_not_empty[D, H, max(fp(i)`time, B + to) - to, min(fp(1 + i)`time, T + to) - to, gsmin, gsmax, vsmin, vsmax]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fp) (("2" (inst - "i+1") (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_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) (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) (empty_seq const-decl "fsq" fseqs "structures/") (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (Nzv2_vect3 type-eq-decl nil definitions_3D nil) (* const-decl "Vector" vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (trk_bands_3D_not_empty formula-decl nil bands_3D 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) (D formal-const-decl "posreal" bands_si nil) (H formal-const-decl "posreal" bands_si nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (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) (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) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" bands_si nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_si nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil)) shostak)) (trk_bands_si_i_relevant_has_2 0 (trk_bands_si_i_relevant_has_2-1 nil 3482068244 ("" (skeep) (("" (prop) (("1" (assert) (("1" (expand "trk_bands_si_i") (("1" (lift-if) (("1" (lemma trk_bands_si_i_relevant) (("1" (inst - fp so to vo i) (("1" (ground) (("1" (lemma "trk_bands_3D_not_empty[D, H, max(fp(i)`time, B + to) - to, min(fp(1 + i)`time, T + to) - to, gsmin, gsmax, vsmin, vsmax]") (("1" (inst?) nil nil) ("2" (assert) (("2" (expand "max") (("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (typepred fp) (("2" (inst - "i+1") (("2" (assert) (("2" (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) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (trk_bands_si_i_relevant formula-decl nil bands_si 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_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_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) (NOT const-decl "[bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (trk_bands_3D_not_empty formula-decl nil bands_3D nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" bands_si nil) (H formal-const-decl "posreal" bands_si nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (B formal-const-decl "nnreal" bands_si nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (T formal-const-decl "{AB: posreal | AB > B}" bands_si nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (- 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (trk_bands_si_relevant_TCC1 0 (trk_bands_si_relevant_TCC1-1 nil 3481649095 ("" (subtype-tcc) nil nil) nil nil)) (trk_bands_si_relevant 0 (trk_bands_si_relevant-1 nil 3481649096 ("" (skolem 1 (fp so to vo _)) (("" (induct i) (("1" (flatten) (("1" (expand "trk_bands_si") (("1" (expand "trk_bands_si_i") (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (assert) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "N=2") (("1" (assert) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (lemma "flight_plan_ascending_time") (("2" (inst - fp "N-1" 1) (("2" (assert) (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "trk_bands_si") (("2" (lemma trk_bands_si_i_relevant) (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skeep) (("3" (assert) (("3" (typepred fp) (("3" (inst - "k+2") (("3" (assert) (("3" (typepred fp) (("3" (inst - "k+1") (("3" (assert) (("3" (assert) (("3" (ground) (("1" (expand trk_bands_si 1) (("1" (assert) (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand trk_bands_si -1) (("2" (assert) (("2" (expand "o") (("2" (lemma trk_bands_si_i_relevant) (("2" (inst - fp so to vo "1+k") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma flight_plan_ascending_time) (("2" (inst - fp "1+k" 0) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand trk_bands_si -1) (("3" (assert) (("3" (lemma trk_bands_si_i_relevant) (("3" (inst - fp so to vo "1+k") (("3" (assert) (("3" (expand "o") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma trk_bands_si_i_relevant) (("4" (inst - fp so to vo "1+k") (("4" (assert) (("4" (expand trk_bands_si -2) (("4" (assert) (("4" (expand "o") (("4" (assert) (("4" (lemma flight_plan_ascending_time) (("4" (inst - fp "1+k" 0) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand trk_bands_si -1) (("5" (assert) (("5" (lemma trk_bands_si_i_relevant) (("5" (inst - fp so to vo "k+1") (("5" (assert) (("5" (expand "o") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand trk_bands_si 1) (("6" (assert) (("6" (lemma trk_bands_si_i_relevant) (("6" (inst - fp so to vo "k+1") (("6" (assert) (("6" (expand "o") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil) ("5" (expand "trk_bands_si") (("5" (assert) nil nil)) nil) ("6" (expand "trk_bands_si") (("6" (assert) nil nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals 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) (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) (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) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_seq const-decl "fsq" fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (trk_bands_si_i_relevant formula-decl nil bands_si nil) (NOT const-decl "[bool -> bool]" booleans nil) (O const-decl "fseq" fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sort_length formula-decl nil sort_fseq "structures/")) shostak)) (trk_bands_si_relevant_has_2 0 (trk_bands_si_relevant_has_2-1 nil 3482068881 ("" (skolem 1 (fp so to vo _)) (("" (lemma trk_bands_si_relevant) (("" (inst -1 fp so to vo _) (("" (induct i) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (inst -2 0) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "trk_bands_si") (("1" (assert) (("1" (lemma trk_bands_si_i_relevant_has_2) (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil) ("3" (skeep) (("3" (inst - k) (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (split 1) (("1" (flatten) (("1" (assert) (("1" (lemma trk_bands_si_relevant) (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma trk_bands_si_i_relevant_has_2) (("1" (inst - fp so to vo "k+1") (("1" (assert) (("1" (assert) (("1" (expand trk_bands_si 1) (("1" (assert) (("1" (lemma trk_bands_si_i_relevant) (("1" (inst?) (("1" (assert) (("1" (case "fp(1 + k)`time < T + to") (("1" (assert) (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -1) (("2" (expand "trk_bands_si_i") (("2" (assert) (("2" (lemma concat_left_emptyseq) (("2" (inst?) (("2" (replace -1) (("2" (propax) 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) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) nil nil) ("5" (assert) nil nil) ("6" (assert) nil nil)) nil)) nil)) nil)) nil) ((trk_bands_si_relevant formula-decl nil bands_si 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (int_minus_int_is_int application-judgement "int" integers nil) (subrange_induction formula-decl nil subrange_inductions 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) (trk_bands_si_i_relevant_has_2 formula-decl nil bands_si 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (trk_bands_si_i_relevant formula-decl nil bands_si nil) (trk_bands_si_i const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (concat_left_emptyseq formula-decl nil fseqs "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (O const-decl "fseq" fseqs "structures/") (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) (sort_length formula-decl nil sort_fseq "structures/") (int_plus_int_is_int application-judgement "int" integers nil) (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (- 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (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)) shostak)) (trk_bands_si_equivalence_TCC1 0 (trk_bands_si_equivalence_TCC1-1 nil 3482248332 ("" (subtype-tcc) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (trk_bands_si_equivalence_TCC2 0 (trk_bands_si_equivalence_TCC2-1 nil 3482674590 ("" (subtype-tcc) nil nil) ((Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan "trig_fnd/") (pi const-decl "posreal" atan "trig_fnd/")) nil)) (trk_bands_si_equivalence 0 (trk_bands_si_equivalence-1 nil 3482248332 ("" (skeep) (("" (assert) (("" (skeep) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst + j) (("1" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "trk_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vtrk_3D") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma trk_bands_si_component) (("2" (inst?) (("2" (name fred "trk_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst + j) (("2" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "trk_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vtrk_3D") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma trk_bands_si_component) (("2" (inst?) (("2" (name fred "trk_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) 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) ((int_minus_int_is_int application-judgement "int" integers nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (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) (conflict_3D_rew_absolute_time formula-decl nil cd3d_si nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (trk_bands_equivalence formula-decl nil bands_3D nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si 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) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (trk_bands_si def-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (trk_bands_3D const-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil) (increasing? const-decl "bool" sort_fseq "structures/") (trk_fseq? const-decl "bool" fseqs_aux_2D nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (trk_bands_si_component formula-decl nil bands_si nil) (Vtrk_3D const-decl "(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" bands_util nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (j skolem-const-decl "below[N - 1]" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trk2v3_Nzv application-judgement "Nzv2_vect3" bands_util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (seg_lh_top const-decl "real" cd3d_si nil) (seg_lh_bottom const-decl "nnreal" cd3d_si nil) (real_minus_real_is_real application-judgement "real" reals nil) (j skolem-const-decl "below[N - 1]" bands_si nil) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (trk2v3 const-decl "(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)" bands_util nil) (= const-decl "[T, T -> boolean]" equalities nil) (trk_only? const-decl "bool" definitions nil) (AND const-decl "[bool, bool -> bool]" booleans 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/")) shostak)) (trk_red_bands_si 0 (trk_red_bands_si-1 nil 3481472460 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_trk_band_fp?") (("" (name mid "(trk_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i) + trk_bands_si(so, vo, to, fpr)(N - 2)`seq(i)) / 2") (("" (replace -1) (("" (lemma trk_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 1 xxx) (("1" (case "xxx<=mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred xxx) (("1" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "trk_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "trk_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (assert) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "trk_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "trk_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - mid) (("2" (assert) (("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (trk2v3_Nzv application-judgement "Nzv2_vect3" bands_util nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_trk_band_fp? const-decl "bool" bands_si nil) (real_le_is_total_order name-judgement "(total_order?[real])" 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) (below type-eq-decl nil naturalnumbers nil) (so skolem-const-decl "Vect3" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (to skolem-const-decl "real" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (i skolem-const-decl "{i: subrange(0, trk_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT trk_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = trk_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (mid skolem-const-decl "real" bands_si nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (trk_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (trk_bands_si def-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (trk_green_bands_si 0 (trk_green_bands_si-1 nil 3482603069 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_trk_band_fp?") (("" (name mid "(trk_bands_si(so, vo, to, fpr)(N - 2)`seq (1 + i) + trk_bands_si(so, vo, to, fpr)(N - 2)`seq (i)) / 2") (("" (replace -1) (("" (lemma trk_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 2 xxx) (("1" (assert) (("1" (case "xxx <= mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "trk_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "trk_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred xxx) (("1" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "trk_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "trk_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid) (("2" (typepred "trk_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (trk2v3_Nzv application-judgement "Nzv2_vect3" bands_util nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_trk_band_fp? const-decl "bool" bands_si nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers 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) (mid skolem-const-decl "real" bands_si nil) (i skolem-const-decl "{i: subrange(0, trk_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT trk_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = trk_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (so skolem-const-decl "Vect3" bands_si nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (trk_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (trk_bands_si def-decl "{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (gs_bands_si_combines 0 (gs_bands_si_combines-3 nil 3482685050 ("" (skolem 1 (fp so to vo _ x)) (("" (induct i) (("1" (flatten) (("1" (inst 1 0) (("1" (expand "gs_bands_si") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep -1 (0)) (("2" (expand "gs_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 gs_bands_si 1) (("2" (lemma member_sort) (("2" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) (("2" (lemma member_composition) (("2" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 gs_bands_si -1) (("3" (assert) (("3" (inst 1 "1+k") (("3" (assert) (("3" (lemma member_sort) (("3" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) (("3" (lemma member_composition) (("3" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 "gs_bands_si") (("4" (assert) (("4" (lemma member_sort) (("4" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (lemma member_composition) (("4" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 "gs_bands_si") (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil) ("5" (expand "gs_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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (increasing? const-decl "bool" sort_fseq "structures/") (gs_bands_si def-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (gs_bands_si_i const-decl "{fs: (gs_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)) nil) (gs_bands_si_combines-2 nil 3482684953 (";;; Proof gs_bands_si_combines-1 for formula fp_bands.gs_bands_si_combines" (skolem 1 (fp so to vo _ x)) ((";;; Proof gs_bands_si_combines-1 for formula fp_bands.gs_bands_si_combines" (induct i) (("1" (flatten) (("1" (inst 1 0) (("1" (expand "vs_bands_si") (("1" (propax) nil))))))) ("2" (flatten) (("2" (assert) (("2" (skeep -1 (0)) (("2" (expand "vs_bands_si") (("2" (assert) nil))))))))) ("3" (skeep) (("3" (assert) (("3" (assert) (("3" (prop) (("1" (assert) (("1" (skosimp*) (("1" (inst 1 "j!1") nil))))) ("2" (assert) (("2" (skosimp*) (("2" (typepred "j!1") (("2" (typepred "j!2") (("2" (assert) (("2" (expand vs_bands_si 1) (("2" (lemma member_sort) (("2" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) (("2" (lemma member_composition) (("2" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) nil))))))))))))))))))))))) ("3" (assert) (("3" (expand vs_bands_si -1) (("3" (assert) (("3" (inst 1 "1+k") (("3" (assert) (("3" (lemma member_sort) (("3" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) (("3" (lemma member_composition) (("3" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) nil))))))))))))))))))))) ("4" (assert) (("4" (skosimp*) (("4" (typepred "j!1") (("4" (assert) (("4" (expand "vs_bands_si") (("4" (assert) (("4" (lemma member_sort) (("4" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (lemma member_composition) (("4" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (case "j!1 = k+1") (("1" (assert) nil) ("2" (assert) (("2" (inst 5 "j!1") nil))))))))))))))))))))))))))))))))))))) ("4" (expand "vs_bands_si") (("4" (lift-if) (("4" (assert) nil))))) ("5" (expand "vs_bands_si") (("5" (assert) nil)))))) ";;; developed with shostak decision procedures") nil nil) (gs_bands_si_combines-1 nil 3482674675 ("" (skolem 1 (fp so to vo _ x)) (("" (induct i) (("1" (flatten) (("1" (inst 1 0) (("1" (expand "gs_bands_si") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep -1 (0)) (("2" (expand "gs_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 gs_bands_si 1) (("2" (lemma member_sort) (("2" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) (("2" (lemma member_composition) (("2" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 gs_bands_si -1) (("3" (assert) (("3" (inst 1 "1+k") (("3" (assert) (("3" (lemma member_sort) (("3" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) (("3" (lemma member_composition) (("3" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 "gs_bands_si") (("4" (assert) (("4" (lemma member_sort) (("4" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k) o gs_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (lemma member_composition) (("4" (inst - "gs_bands_si_i(so, vo, to, fp)(1 + k)" "gs_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 "gs_bands_si") (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil) ("5" (expand "gs_bands_si") (("5" (assert) nil nil)) nil)) nil)) 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/") (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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (increasing? const-decl "bool" sort_fseq "structures/") (O const-decl "fseq" fseqs "structures/") (member_composition formula-decl nil fseqs "structures/") (member_sort formula-decl nil sort_fseq "structures/")) nil)) (gs_bands_si_component 0 (gs_bands_si_component-2 nil 3482674836 ("" (lemma gs_bands_si_combines) (("" (skeep) (("" (inst?) (("" (assert) (("" (expand "gs_bands_si_i") (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst 1 j) (("1" (lift-if) (("1" (ground) (("1" (expand "member") (("1" (skolem -2 ii) (("1" (typepred ii) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand member) (("2" (skolem -2 ii) (("2" (typepred ii) (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand member) (("3" (skolem -2 ii) (("3" (typepred ii) (("3" (expand "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand member) (("4" (skolem -2 ii) (("4" (typepred ii) (("4" (expand "empty_seq") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (expand member) (("5" (skolem -2 ii) (("5" (typepred ii) (("5" (expand "empty_seq") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("6" (expand member) (("6" (skolem -2 ii) (("6" (typepred ii) (("6" (expand "empty_seq") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst 1 j) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (int_plus_int_is_int application-judgement "int" integers 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_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) (int_minus_int_is_int application-judgement "int" integers nil) (below type-eq-decl nil naturalnumbers nil) (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (gs_bands_si_i const-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (- 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (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) (gs_bands_si_combines formula-decl nil bands_si nil)) nil) (gs_bands_si_component-1 nil 3482674590 (";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (lemma trk_bands_si_combines) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (skeep) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (inst?) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (assert) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (expand "trk_bands_si_i") ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (replace -1) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (hide -1) ((";;; Proof trk_bands_si_component-1 for formula fp_bands.trk_bands_si_component" (prop) (("1" (skeep -1) (("1" (inst 1 j) (("1" (lift-if) (("1" (ground) (("1" (expand "member") (("1" (skolem -2 ii) (("1" (typepred ii) (("1" (expand "empty_seq") (("1" (assert) nil))))))))) ("2" (expand member) (("2" (skolem -2 ii) (("2" (typepred ii) (("2" (expand "empty_seq") (("2" (assert) nil))))))))) ("3" (expand member) (("3" (skolem -2 ii) (("3" (typepred ii) (("3" (expand "empty_seq") (("3" (assert) nil))))))))) ("4" (expand member) (("4" (skolem -2 ii) (("4" (typepred ii) (("4" (expand "empty_seq") (("4" (assert) nil))))))))) ("5" (expand member) (("5" (skolem -2 ii) (("5" (typepred ii) (("5" (expand "empty_seq") (("5" (assert) nil))))))))) ("6" (expand member) (("6" (skolem -2 ii) (("6" (typepred ii) (("6" (expand "empty_seq") (("6" (assert) nil))))))))))))))))) ("2" (skeep -1) (("2" (inst 1 j) (("2" (lift-if) (("2" (assert) nil)))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (gs_bands_si_equivalence_TCC1 0 (gs_bands_si_equivalence_TCC1-1 nil 3482673238 ("" (subtype-tcc) nil nil) nil nil)) (gs_bands_si_equivalence 0 (gs_bands_si_equivalence-1 nil 3482674962 ("" (skeep) (("" (assert) (("" (skeep) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst + j) (("1" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "gs_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vgs_3D") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma gs_bands_si_component) (("2" (inst?) (("2" (name fred "gs_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst + j) (("2" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "gs_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vgs_3D") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma gs_bands_si_component) (("2" (inst?) (("2" (name fred "gs_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) 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) ((int_minus_int_is_int application-judgement "int" integers 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) (conflict_3D_rew_absolute_time formula-decl nil cd3d_si nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (gs_bands_equivalence formula-decl nil bands_3D nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si 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) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (gs_bands_si def-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (gs_bands_3D const-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil) (increasing? const-decl "bool" sort_fseq "structures/") (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (gs_bands_si_component formula-decl nil bands_si nil) (Vgs_3D const-decl "(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" bands_util nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (j skolem-const-decl "below[N - 1]" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si 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) (seg_lh_top const-decl "real" cd3d_si nil) (seg_lh_bottom const-decl "nnreal" cd3d_si nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (j skolem-const-decl "below[N - 1]" bands_si nil) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (gs2v3 const-decl "Vect3" bands_util 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/")) nil)) (gs_red_bands_si 0 (gs_red_bands_si-1 nil 3482675784 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_gs_band_fp?") (("" (name mid "(gs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i) + gs_bands_si(so, vo, to, fpr)(N - 2)`seq(i)) / 2") (("" (replace -1) (("" (lemma gs_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 1 xxx) (("1" (case "xxx<=mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred xxx) (("1" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "gs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "gs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (assert) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "gs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "gs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - mid) (("2" (assert) (("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_gs_band_fp? const-decl "bool" bands_si nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (so skolem-const-decl "Vect3" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (to skolem-const-decl "real" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (i skolem-const-decl "{i: subrange(0, gs_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT gs_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = gs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (mid skolem-const-decl "real" bands_si nil) (gs_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (gs_bands_si def-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (gs_green_bands_si 0 (gs_green_bands_si-1 nil 3482675829 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_gs_band_fp?") (("" (name mid "(gs_bands_si(so, vo, to, fpr)(N - 2)`seq (1 + i) + gs_bands_si(so, vo, to, fpr)(N - 2)`seq (i)) / 2") (("" (replace -1) (("" (lemma gs_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 2 xxx) (("1" (assert) (("1" (case "xxx <= mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "gs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "gs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred xxx) (("1" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "gs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "gs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid) (("2" (typepred "gs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_gs_band_fp? const-decl "bool" bands_si nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mid skolem-const-decl "real" bands_si nil) (i skolem-const-decl "{i: subrange(0, gs_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT gs_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = gs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (so skolem-const-decl "Vect3" bands_si nil) (gs_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (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) (gs_fseq? const-decl "bool" fseqs_aux_2D nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (gs_bands_si def-decl "{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (vs_bands_si_combines 0 (vs_bands_si_combines-1 nil 3482684998 ("" (skolem 1 (fp so to vo _ x)) (("" (induct i) (("1" (flatten) (("1" (inst 1 0) (("1" (expand "vs_bands_si") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep -1 (0)) (("2" (expand "vs_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 vs_bands_si 1) (("2" (lemma member_sort) (("2" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("2" (assert) (("2" (lemma member_composition) (("2" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_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 vs_bands_si -1) (("3" (assert) (("3" (inst 1 "1+k") (("3" (assert) (("3" (lemma member_sort) (("3" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("3" (assert) (("3" (lemma member_composition) (("3" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_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 "vs_bands_si") (("4" (assert) (("4" (lemma member_sort) (("4" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k) o vs_bands_si(so, vo, to, fp)(k)" x) (("4" (assert) (("4" (lemma member_composition) (("4" (inst - "vs_bands_si_i(so, vo, to, fp)(1 + k)" "vs_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 "vs_bands_si") (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil) ("5" (expand "vs_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) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil) (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (increasing? const-decl "bool" sort_fseq "structures/") (vs_bands_si def-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_si nil) (vs_bands_si_i const-decl "{fs: (vs_fseq?[vsmin, vsmax]) | 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)) nil)) (vs_bands_si_component 0 (vs_bands_si_component-1 nil 3482685112 ("" (lemma vs_bands_si_combines) (("" (skeep) (("" (inst?) (("" (assert) (("" (expand "vs_bands_si_i") (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst 1 j) (("1" (lift-if) (("1" (ground) (("1" (expand "member") (("1" (skolem -2 ii) (("1" (typepred ii) (("1" (expand "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand member) (("2" (skolem -2 ii) (("2" (typepred ii) (("2" (expand "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand member) (("3" (skolem -2 ii) (("3" (typepred ii) (("3" (expand "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand member) (("4" (skolem -2 ii) (("4" (typepred ii) (("4" (expand "empty_seq") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (expand member) (("5" (skolem -2 ii) (("5" (typepred ii) (("5" (expand "empty_seq") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("6" (expand member) (("6" (skolem -2 ii) (("6" (typepred ii) (("6" (expand "empty_seq") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst 1 j) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (int_plus_int_is_int application-judgement "int" integers 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_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) (int_minus_int_is_int application-judgement "int" integers nil) (below type-eq-decl nil naturalnumbers nil) (empty_seq const-decl "fsq" fseqs "structures/") (fsq type-eq-decl nil fsq "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" fseqs "structures/") (vs_bands_si_i const-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_si nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Nzv2_vect3 type-eq-decl nil definitions_3D 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) (- 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (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) (vs_bands_si_combines formula-decl nil bands_si nil)) nil)) (vs_bands_si_equivalence_TCC1 0 (vs_bands_si_equivalence_TCC1-1 nil 3482684663 ("" (subtype-tcc) nil nil) nil nil)) (vs_bands_si_equivalence 0 (vs_bands_si_equivalence-1 nil 3482685206 ("" (skeep) (("" (assert) (("" (skeep) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (lemma conflict_3D_rew_absolute_time) (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (skeep -1) (("1" (inst + j) (("1" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("1" (replace -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "vs_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vs") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma vs_bands_si_component) (("2" (inst?) (("2" (name fred "vs_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst + j) (("2" (name LB "seg_lh_bottom(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (name UB "seg_lh_top(fpr, to)(j) + fpr(j)`time - to") (("2" (replace -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vs_bands_equivalence[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax]") (("1" (inst - "so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j))" " velocity(fpr)(j)" vo) (("1" (assert) (("1" (inst - x y) (("1" (assert) (("1" (split -) (("1" (expand "Vs") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (hide -4) (("2" (skeep) (("2" (lemma vs_bands_si_component) (("2" (inst?) (("2" (name fred "vs_bands_3D[D,H,LB,UB,gsmin,gsmax,vsmin,vsmax](so - (fpr(j)`position - (fpr(j)`time - to) * velocity(fpr)(j)), vo, velocity(fpr)(j))`seq (i)") (("1" (inst - fred) (("1" (flatten) (("1" (hide -2) (("1" (split -2) (("1" (expand "member") (("1" (skolem -1 sheep) (("1" (inst - sheep) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (inst + j) (("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (expand "member") (("2" (inst + i) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "seg_lh_bottom") (("2" (expand "min") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (hide -5) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("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) ("2" (typepred fpr) (("2" (inst -4 j) nil nil)) nil)) nil) ("2" (expand "seg_lh_top") (("2" (expand "min") (("2" (expand "seg_lh_bottom") (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (typepred fpr) (("2" (inst - "j+1") (("2" (assert) (("2" (split -6) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "seg_lh_bottom") (("3" (expand "seg_lh_top") (("3" (expand "min") (("3" (expand "max") (("3" (lift-if) (("3" (typepred fpr) (("3" (inst - "j+1") (("3" (ground) 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) ((int_minus_int_is_int application-judgement "int" integers 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) (conflict_3D_rew_absolute_time formula-decl nil cd3d_si nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (vs_bands_equivalence formula-decl nil bands_3D nil) (gsmin formal-const-decl "posreal" bands_si nil) (gsmax formal-const-decl "{x: posreal | x > gsmin}" bands_si nil) (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si 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) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (FlightPlan_nz nonempty-type-eq-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" fseqs "structures/") (below type-eq-decl nil naturalnumbers nil) (vs_bands_si def-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_si nil) (vs_bands_3D const-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil) (increasing? const-decl "bool" sort_fseq "structures/") (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (vs_bands_si_component formula-decl nil bands_si nil) (Vs const-decl "(vs_only?(vo3 - vi3))" bands_util nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (j skolem-const-decl "below[N - 1]" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si 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) (seg_lh_top const-decl "real" cd3d_si nil) (seg_lh_bottom const-decl "nnreal" cd3d_si nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (j skolem-const-decl "below[N - 1]" bands_si nil) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (velocity const-decl "Vect3" flightplan nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (vs2v3 const-decl "(vs_only?(vo3))" bands_util nil) (vs_only? const-decl "bool" definitions_3D 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/")) nil)) (vs_red_bands_si 0 (vs_red_bands_si-1 nil 3482685657 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_vs_band_fp?") (("" (name mid "(vs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i) + vs_bands_si(so, vo, to, fpr)(N - 2)`seq(i)) / 2") (("" (replace -1) (("" (lemma vs_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 1 xxx) (("1" (case "xxx<=mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred xxx) (("1" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "vs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "vs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (assert) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "vs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "vs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - mid) (("2" (assert) (("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_vs_band_fp? const-decl "bool" bands_si nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (so skolem-const-decl "Vect3" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (to skolem-const-decl "real" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (i skolem-const-decl "{i: subrange(0, vs_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT vs_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = vs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (mid skolem-const-decl "real" bands_si nil) (vs_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil) (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (vs_bands_si def-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (vs_green_bands_si 0 (vs_green_bands_si-1 nil 3482685719 ("" (skeep) (("" (assert) (("" (skeep) (("" (expand "red_vs_band_fp?") (("" (name mid "(vs_bands_si(so, vo, to, fpr)(N - 2)`seq (1 + i) + vs_bands_si(so, vo, to, fpr)(N - 2)`seq (i)) / 2") (("" (replace -1) (("" (lemma vs_bands_si_equivalence) (("" (inst?) (("" (assert) (("" (prop) (("1" (skolem 2 xxx) (("1" (assert) (("1" (case "xxx <= mid") (("1" (inst - xxx mid) (("1" (ground) (("1" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "vs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "vs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid xxx) (("2" (ground) (("1" (typepred xxx) (("1" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("1" (expand "vs_fseq?") (("1" (inst - i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "vs_fseq?") (("2" (inst - "i+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skolem 1 ii) (("3" (flatten) (("3" (typepred xxx) (("3" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("3" (expand "increasing?") (("3" (inst-cp - ii i) (("3" (inst-cp - "i+1" ii) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - mid) (("2" (typepred "vs_bands_si(so, vo, to, fpr)(N - 2)") (("2" (expand "increasing?") (("2" (inst - i "i+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (red_vs_band_fp? const-decl "bool" bands_si nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mid skolem-const-decl "real" bands_si nil) (i skolem-const-decl "{i: subrange(0, vs_bands_si(so, vo, to, fpr)(N - 2)`length - 2) | NOT vs_bands_si(so, vo, to, fpr)(N - 2)`seq(i) = vs_bands_si(so, vo, to, fpr)(N - 2)`seq(1 + i)}" bands_si nil) (fpr skolem-const-decl "FlightPlanRelevant_nz(to)" bands_si nil) (to skolem-const-decl "real" bands_si nil) (vo skolem-const-decl "Nzv2_vect3" bands_si nil) (so skolem-const-decl "Vect3" bands_si nil) (vs_bands_si_equivalence formula-decl nil bands_si nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil 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 -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (real_pred const-decl "[number_field -> boolean]" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (vsmin formal-const-decl "real" bands_si nil) (vsmax formal-const-decl "{x: real | x > vsmin}" bands_si nil) (vs_fseq? const-decl "bool" fseqs_aux_vertical nil) (<= const-decl "bool" reals nil) (increasing? const-decl "bool" sort_fseq "structures/") (vs_bands_si def-decl "{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_si nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (FlightPlanRelevant_nz nonempty-type-eq-decl nil bands_si nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)))
¤ 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.0.490Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26