| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 248 kB |
|
Quelle cd3d_ii.prfSprache: Lisp |
|||||||||||||||
|
(cd3d_ii (FlightPlanRelevant2_TCC1 0 (FlightPlanRelevant2_TCC1-1 nil 3482767958 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (FlightPlanRelevant2_TCC2 0 (FlightPlanRelevant2_TCC2-1 nil 3482767958 ("" (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)) (FlightPlanRelevant2_TCC3 0 (FlightPlanRelevant2_TCC3-1 nil 3482767958 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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)) (FlightPlanRelevant2_TCC4 0 (FlightPlanRelevant2_TCC4-1 nil 3482767958 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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)) (FlightPlanRelevant2_TCC5 0 (FlightPlanRelevant2_TCC5-1 nil 3482767958 ("" (subtype-tcc) nil nil) nil nil)) (FlightPlanRelevant2_TCC6 0 (FlightPlanRelevant2_TCC6-1 nil 3482767958 ("" (skeep) (("" (inst + "lambda (j: below[M]): (# time:= IF j < N THEN fp(j)`time ELSE j+fp(N-1)`time ENDIF,position:= (("1" (ground) (("1" (skeep) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (typepred fp) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "flight_plan_ascending_time[N]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (ground) (("1" (lemma "flight_plan_ascending_time[N]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "flight_plan_ascending_time[N]") (("2" (inst - fp "N-1" 0) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) 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_minus_int_is_int application-judgement "int" integers 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) (M formal-const-decl "above[1]" cd3d_ii 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) (N formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Vector type-eq-decl nil vectors_3D "vectors/") (zero const-decl "Vector" vectors_3D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (flight_plan_ascending_time formula-decl nil flightplan 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (FlightTimesRelevant2_TCC1 0 (FlightTimesRelevant2_TCC1-1 nil 3482836778 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (FlightTimesRelevant2_TCC2 0 (FlightTimesRelevant2_TCC2-1 nil 3483457740 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii 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_plus_real_is_real application-judgement "real" reals 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)) (FlightTimesLimited2_TCC1 0 (FlightTimesLimited2_TCC1-1 nil 3483200922 ("" (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)) nil)) (FlightTimesLimited2_TCC2 0 (FlightTimesLimited2_TCC2-1 nil 3483206183 ("" (subtype-tcc) nil nil) nil nil)) (FlightTimesLimited2_TCC3 0 (FlightTimesLimited2_TCC3-1 nil 3483267537 ("" (subtype-tcc) nil nil) nil nil)) (FlightTimesLimited2_TCC4 0 (FlightTimesLimited2_TCC4-1 nil 3483377850 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (<= const-decl "bool" reals nil) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan 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_plus_real_is_real application-judgement "real" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (conflict_3D_ii?_TCC1 0 (conflict_3D_ii?_TCC1-1 nil 3482836778 ("" (subtype-tcc) nil nil) ((start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil)) nil)) (conflict_3D_ii?_TCC2 0 (conflict_3D_ii?_TCC2-1 nil 3483457740 ("" (subtype-tcc) nil nil) ((start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil)) nil)) (seg_allowable_TCC1 0 (seg_allowable_TCC1-1 nil 3483437086 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (<= const-decl "bool" reals nil) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii 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) (real_le_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) (real_minus_real_is_real application-judgement "real" reals nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (segment_max const-decl "[SS: non_empty_finite_set[nat] -> {a: nat | SS(a) AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" flightplan nil) (segment const-decl "below[N]" flightplan nil)) nil)) (seg_allowable 0 (seg_allowable-1 nil 3483437086 ("" (skeep) (("" (typepred t1) (("" (expand "start_time") (("" (expand "end_time") (("" (skolem - jj) (("" (flatten) (("" (lemma segment_index[N]) (("" (inst - fp jj t1) (("" (flatten) (("" (assert) (("" (lemma segment_index[N]) (("" (inst - fp j t1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred fp) (("1" (inst - "jj+1") (("1" (assert) (("1" (hide -5) (("1" (typepred jj) (("1" (expand "min") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst - fp t1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (M formal-const-decl "above[1]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (start_time const-decl "real" 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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) (<= 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) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (j skolem-const-decl "below[N]" cd3d_ii nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (segment_def formula-decl nil flightplan nil) (segment_index formula-decl nil flightplan nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (time_in_range_TCC1 0 (time_in_range_TCC1-1 nil 3483276637 ("" (skeep) (("" (assert) (("" (typepred t1) (("" (expand "start_time") (("" (expand "end_time") (("" (skolem -3 jj) (("" (flatten) (("" (assert) (("" (lemma segment_max[N]) (("" (inst - fp t1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment_max formula-decl nil flightplan nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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]" cd3d_ii 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) (start_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil)) nil)) (time_in_range_TCC2 0 (time_in_range_TCC2-1 nil 3483276637 ("" (skeep) (("" (expand "min") (("" (lift-if) (("" (typepred fp) (("" (inst - "j+1") (("1" (assert) (("1" (typepred t1) (("1" (expand "start_time") (("1" (expand "end_time") (("1" (skolem -3 jj) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma segment_max[N]) (("1" (inst - fp t1) (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp j 0) (("1" (lemma segment_def[N]) (("1" (inst - fp t1) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred t1) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (skolem -3 jj) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (typepred j) (("2" (lemma segment_max[N]) (("2" (inst - fp t1) (("2" (assert) 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) (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]" cd3d_ii 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) (real_plus_real_is_real application-judgement "real" reals 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment_max formula-decl nil flightplan nil) (segment_def formula-decl nil flightplan nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (start_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (j skolem-const-decl "below[N]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" 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)) nil)) (time_in_range_TCC3 0 (time_in_range_TCC3-1 nil 3483276637 ("" (skeep) (("" (skeep) (("" (typepred t1) (("" (expand "start_time") (("" (expand "end_time") (("" (lemma segment_max[N]) (("" (inst - fp t1) (("" (assert) (("" (skolem -4 jj) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((segment_max formula-decl nil flightplan nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= 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) (< 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]" cd3d_ii 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) (start_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (time_in_range 0 (time_in_range-2 "nooooo!" 3483365871 ("" (skeep) (("" (assert) (("" (skeep) (("" (typepred t1) (("" (typepred t2) (("" (typepred fp) (("" (skeep -8) (("" (name jj "segment(fp)(t1)") (("" (replace -1) (("" (name segend "min(fp(1 + jj)`time - fp(jj)`time, fp(0)`time - fp(jj)`time + T)") (("" (replace -1) (("" (case "segend <= fp(1 + jj)`time - fp(jj)`time") (("1" (expand "min") (("1" (lift-if) (("1" (assert) (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (assert) (("1" (inst - fp jj 0) (("1" (split +) (("1" (assert) nil nil) ("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst - fp t1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -6) (("2" (case "jj<j") (("1" (assert) (("1" (case "j=jj+1") (("1" (assert) nil nil) ("2" (assert) (("2" (case "jj < j-1") (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp "j-1" jj) (("1" (assert) (("1" (replace -17) (("1" (assert) (("1" (case "fp(j)`time < fp(jj+1)`time") (("1" (assert) (("1" (typepred j) (("1" (typepred jj) (("1" (case "j-1 < jj+1") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp j jj) (("2" (case "jj <= j-2") (("1" (assert) (("1" (hide -2) (("1" (hide -6 -7) (("1" (replace -19 :dir rl) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp j "jj+1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp jj j) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (M formal-const-decl "above[1]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (start_time const-decl "real" 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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) (<= 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (segment_def formula-decl nil flightplan nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (flight_plan_ascending_time formula-decl nil flightplan 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (segment const-decl "below[N]" flightplan nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (D formal-const-decl "posreal" cd3d_ii nil) (H formal-const-decl "posreal" cd3d_ii nil) (FlightTimesRelevant type-eq-decl nil cd3d_si nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak) (time_in_range-1 nil 3483278009 ("" (skeep) (("" (assert) (("" (skeep) (("" (typepred t1) (("" (typepred t2) (("" (typepred fp) (("" (skeep -8) (("" (name jj "segment(fp)(t1)") (("" (replace -1) (("" (name segend "min(fp(1 + jj)`time - fp(jj)`time, fp(0)`time - fp(jj)`time + T)") (("" (replace -1) (("" (case "segend <= fp(1 + jj)`time - fp(jj)`time") (("1" (expand "min") (("1" (lift-if) (("1" (assert) (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (assert) (("1" (inst - fp jj 0) (("1" (split +) (("1" (assert) nil nil) ("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst - fp t1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -6) (("2" (case "jj<j") (("1" (assert) (("1" (case "j=jj+1") (("1" (assert) nil nil) ("2" (assert) (("2" (case "jj < j-1") (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp "j-1" jj) (("1" (assert) (("1" (replace -17) (("1" (assert) (("1" (case "fp(j)`time < fp(jj+1)`time") (("1" (assert) (("1" (typepred j) (("1" (typepred jj) (("1" (case "j-1 < jj+1") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp j jj) (("2" (case "jj <= j-2") (("1" (assert) (("1" (hide -2) (("1" (hide -6 -7) (("1" (replace -19 :dir rl) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp j "jj+1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp jj j) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesRelevant type-eq-decl nil cd3d_si nil) (segment const-decl "below[N]" flightplan nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (segment_def formula-decl nil flightplan nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil)) shostak)) (limited_bounds_TCC1 0 (limited_bounds_TCC1-1 nil 3483438693 ("" (skeep) (("" (typepred jt) (("" (skolem - jj) (("" (assert) (("" (expand "end_time") (("" (expand "start_time") (("" (assert) (("" (flatten) (("" (assert) (("" (lemma segment_def[N]) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (M formal-const-decl "above[1]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (start_time const-decl "real" 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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) (<= 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) (nnint_plus_posint_is_posint application-judgement "posint" 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) (segment_def formula-decl nil flightplan 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_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (limited_bounds_TCC2 0 (limited_bounds_TCC2-1 nil 3483438693 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (<= const-decl "bool" reals nil) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (segment_max const-decl "[SS: non_empty_finite_set[nat] -> {a: nat | SS(a) AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" flightplan nil) (segment const-decl "below[N]" flightplan nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (limited_bounds 0 (limited_bounds-1 nil 3483438817 ("" (skeep) (("" (typepred jt) (("" (skolem - jj) (("" (flatten) (("" (lemma seg_allowable) (("" (inst - fp fp2 jt j) (("" (assert) (("" (flatten) (("" (expand "min") (("" (lift-if) (("" (case "jj=j") (("1" (replace -1) (("1" (hide -1) (("1" (case "fp(j+1)`time>fp(0)`time+T") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst - fp jt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp jj jt) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (M formal-const-decl "above[1]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (start_time const-decl "real" 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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) (<= 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) (segment_index formula-decl nil flightplan nil) (segment_def formula-decl nil flightplan nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (seg_allowable formula-decl nil cd3d_ii nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (upper_seg_bounds_TCC1 0 (upper_seg_bounds_TCC1-1 nil 3483459080 ("" (skeep) (("" (typepred jt) (("" (skolem - jj) (("" (assert) (("" (flatten) (("" (assert) (("" (expand "start_time") (("" (expand "end_time") (("" (assert) (("" (case "jj=j") (("1" (assert) nil nil) ("2" (lemma segment_def[N]) (("2" (inst?) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (M formal-const-decl "above[1]" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (start_time const-decl "real" 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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) (<= 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) (posint_plus_nnint_is_posint application-judgement "posint" 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) (int_minus_int_is_int application-judgement "int" 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) (segment_def formula-decl nil flightplan nil)) nil)) (upper_seg_bounds 0 (upper_seg_bounds-1 nil 3483459081 ("" (skeep) (("" (lemma seg_allowable) (("" (inst?) (("" (inst - j) (("" (assert) (("" (flatten) (("" (assert) (("" (expand "min") (("" (lift-if) (("" (assert) (("" (typepred jt) (("" (expand "start_time") (("" (expand "end_time") (("" (assert) (("" (skolem - jj) (("" (flatten) (("" (assert) (("" (case "jj=j") (("1" (assert) nil nil) ("2" (lemma segment_def[N]) (("2" (inst?) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp jj jt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "jj+1") (("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) ((seg_allowable formula-decl nil cd3d_ii nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (segment_index formula-decl nil flightplan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment_def formula-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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_le_is_total_order name-judgement "(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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (= const-decl "[T, T -> boolean]" equalities nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (start_time const-decl "real" flightplan nil) (<= const-decl "bool" reals nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (M formal-const-decl "above[1]" cd3d_ii 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" cd3d_ii 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_minus_real_is_real application-judgement "real" reals nil)) shostak)) (cd3d_ii_rew_TCC1 0 (cd3d_ii_rew_TCC1-1 nil 3483179145 ("" (skeep) (("" (skeep) (("" (typepred tt) (("" (lemma segment_index[N]) (("" (inst - fp j tt) (("1" (assert) (("1" (assert) (("1" (skolem -4 jj) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma segment_max[N]) (("2" (inst?) (("2" (assert) (("2" (skolem -4 jj) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((segment_index formula-decl nil flightplan nil) (segment_max formula-decl nil flightplan nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (j skolem-const-decl "below[N]" cd3d_ii nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (<= 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) (< 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]" cd3d_ii 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) (start_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil)) nil)) (cd3d_ii_rew_TCC2 0 (cd3d_ii_rew_TCC2-1 nil 3483179145 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (typepred tt) (("" (lemma segment_max[N]) (("" (inst?) (("" (assert) (("" (skolem -4 jj) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((segment_max formula-decl nil flightplan 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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]" cd3d_ii 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) (start_time const-decl "real" flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil)) nil)) (cd3d_ii_rew_TCC3 0 (cd3d_ii_rew_TCC3-1 nil 3483365688 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (hide -4 -5) (("" (replace -1) (("" (replace -2) (("" (replace -3) (("" (hide -2 -3) (("" (expand "min") (("" (lift-if) (("" (lemma segment_ident[N]) (("" (inst?) (("" (replace -2 :dir rl) (("" (hide -1) (("" (typepred tt) (("" (expand "start_time") (("" (expand "end_time") (("" (skolem - jj) (("" (flatten) (("" (assert) (("" (typepred fp) (("" (inst - "j+1") (("1" (assert) (("1" (lemma segment_def[N]) (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma segment_max[N]) (("2" (inst?) (("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) ((>= 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) (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 "bool" reals nil) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (M formal-const-decl "above[1]" cd3d_ii nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (j skolem-const-decl "below[N]" cd3d_ii nil) (segment_def formula-decl nil flightplan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment_max formula-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (segment_ident formula-decl nil flightplan 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) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" cd3d_ii nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (cd3d_ii_rew 0 (cd3d_ii_rew-1 nil 3483179145 ("" (skeep) (("" (prop) (("1" (expand "conflict_3D_ii?") (("1" (skeep -1) (("1" (inst + "fp(segment(fp)(tt))`time") (("1" (assert) (("1" (expand "conflict_3D?") (("1" (inst + tt) (("1" (name loc1 "location_at[N](fp)(tt)") (("1" (lemma "segment_ident[N]") (("1" (inst?) (("1" (replace -1) (("1" (name j "segment(fp)(tt)") (("1" (replace -1) (("1" (expand location_at -4 1) (("1" (expand location_at -5 1) (("1" (assert) (("1" (lemma segment_max[N]) (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (hide -4) (("1" (expand "*") (("1" (expand "+ ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred tt) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (name j "segment(fp)(tt)") (("2" (replace -1) (("2" (inst - fp j tt) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "min") (("1" (lemma segment_ident[N]) (("1" (inst - fp tt) (("1" (replace -2 :dir rl) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma segment_max[N]) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred tt) (("2" (name j "segment(fp)(tt)") (("2" (replace -1) (("2" (assert) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (hide -7 -8) (("2" (typepred fp2) (("2" (inst - 1) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (assert) (("2" (inst - fp j tt) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "flight_plan_ascending_time[N]") (("1" (inst - fp j 0) (("1" (split +) (("1" (assert) nil nil) ("2" (typepred tt) (("2" (inst + j) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma segment_max[N]) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem -1 jt) (("2" (name j "segment(fp)(jt)") (("2" (replace -1) (("2" (assert) (("2" (expand "conflict_3D_ii?") (("2" (lemma "conflict_3D_flightplan_open_interval[D, H, 0, min(fp(1 + j)`time - fp(j)`time, fp(0)`ti (("1" (assert) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (skolem - tt) (("1" (flatten) (("1" (typepred jt) (("1" (skolem - jj) (("1" (flatten) (("1" (assert) (("1" (expand "start_time") (("1" (expand "end_time") (("1" (case "jj=j") (("1" (lemma time_in_range) (("1" (inst?) (("1" (replace -10) (("1" (assert) (("1" (inst - tt) (("1" (flatten) (("1" (assert) (("1" (case "tt < fp(N-1)`time AND fp2(0)`time <= tt") (("1" (flatten) (("1" (assert) (("1" (inst + tt) (("1" (expand location_at 1 1) (("1" (expand location_at 1 2) (("1" (assert) (("1" (lift-if) (("1" (lemma segment_max[N]) (("1" (inst - fp tt) (("1" (assert) (("1" (case "(fp(j)`position + (tt - jt) * velocity[N](fp)(j))=fp(segment(fp)(tt))`position + (tt - fp(segment(fp)(tt))`time) * velocity(fp)(segment(fp)(tt))") (("1" (replace -1) (("1" (assert) (("1" (expand "+ ") (("1" (expand "*") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -17 -18 3) (("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (name k "segment(fp)(tt)") (("2" (replace -1) (("2" (case "j=k") (("1" (replace -1) (("1" (replace -9) (("1" (replace -12) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma segment_index[N]) (("2" (inst - fp j tt) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "end_time") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred tt) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (assert) (("2" (case "tt < fp(j+1)`time") (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - fp "N-1" "j+1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma segment_def[N]) (("2" (inst?) (("2" (lemma segment_index[N]) (("2" (inst - fp jj jt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (typepred fp) (("2" (inst - "jj+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (typepred jt) (("2" (skolem - jj) (("2" (flatten) (("2" (assert) (("2" (expand "end_time") (("2" (expand "start_time") (("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst - fp jt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -10) (("2" (lemma segment_index[N]) (("2" (inst - fp jj jt) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand "min") (("2" (lift-if) (("2" (typepred jt) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (skolem - jj) (("2" (flatten) (("2" (assert) (("2" (lemma segment_def[N]) (("2" (inst?) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred jt) (("3" (skolem -3 jj) (("3" (flatten) (("3" (assert) (("3" (expand "end_time") (("3" (expand "start_time") (("3" (typepred jj) (("3" (assert) (("3" (lemma segment_max[N]) (("3" (inst - fp jt) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((j skolem-const-decl "below[N]" cd3d_ii nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (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) (FlightTimesRelevant type-eq-decl nil cd3d_si nil) (H formal-const-decl "posreal" cd3d_ii nil) (D formal-const-decl "posreal" cd3d_ii nil) (segment_ident formula-decl nil flightplan nil) (segment_max formula-decl nil flightplan nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (int_minus_int_is_int application-judgement "int" integers nil) (location_at const-decl "Vect3" flightplan nil) (j skolem-const-decl "below[N]" cd3d_ii 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) (segment_index formula-decl nil flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (conflict_3D? const-decl "bool" cd3d_si nil) (real_times_real_is_real application-judgement "real" reals nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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]" cd3d_ii 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) (start_time const-decl "real" flightplan nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (segment const-decl "below[N]" flightplan 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) (T formal-const-decl "posreal" cd3d_ii nil) (M formal-const-decl "above[1]" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (fp2 skolem-const-decl "FlightPlanRelevant2(fp)" cd3d_ii nil) (FlightTimesRelevant2 type-eq-decl nil cd3d_ii nil) (tt skolem-const-decl "FlightTimesRelevant2(fp, fp2)" cd3d_ii nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (conflict_3D_ii? const-decl "bool" cd3d_ii nil) (real_minus_real_is_real application-judgement "real" reals nil) (conflict_3D_flightplan_open_interval formula-decl nil cd3d_si nil) (j skolem-const-decl "below[N]" cd3d_ii nil) (jt skolem-const-decl "FlightTimesLimited2(fp, fp2)" cd3d_ii nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (velocity const-decl "Vect3" flightplan nil) (time_in_range formula-decl nil cd3d_ii nil) (tt skolem-const-decl "FlightTimesRelevant [D, H, 0, min(fp(1 + j)`time - fp(j)`time, fp(0)`time - fp(j)`time + T), M](jt, fp2)" cd3d_ii nil) (Vector type-eq-decl nil vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (segment_def formula-decl nil flightplan nil)) shostak)) (cd3d_ii_ind?_TCC1 0 (cd3d_ii_ind?_TCC1-1 nil 3482767958 ("" (subtype-tcc) nil nil) ((real_minus_real_is_real application-judgement "real" reals nil)) nil)) (cd3d_ii_ind?_TCC2 0 (cd3d_ii_ind?_TCC2-1 nil 3482767958 ("" (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]" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(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) (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) (<= const-decl "bool" reals nil) (- const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (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)) nil)) (cd3d_ii_ind?_TCC3 0 (cd3d_ii_ind?_TCC3-1 nil 3483179897 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (assert) (("" (expand "min") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil)) (cd3d_ii_ind?_TCC4 0 (cd3d_ii_ind?_TCC4-1 nil 3483179897 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (expand "min") (("" (lift-if) (("" (assert) (("" (typepred fp) (("" (inst - "j+1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (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]" cd3d_ii 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)) nil)) (cd3d_ii_ind?_TCC5 0 (cd3d_ii_ind?_TCC5-1 nil 3483179897 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (assert) (("" (expand "min") (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_plus_real_is_real application-judgement "real" reals 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (some_cd3d_ii 0 (some_cd3d_ii-1 nil 3483719267 ("" (induct i) (("1" (assert) (("1" (flatten) (("1" (skeep) (("1" (split) (("1" (prop) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (skeep -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (assert) (("2" (inst?) (("2" (prop) (("1" (skeep -3) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand cd3d_ii_ind? 1) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (inst?) (("3" (assert) nil nil)) nil) ("4" (skeep -1) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep 2) (("3" (split) (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (skeep -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skeep 2) (("4" (prop) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (>= const-decl "bool" 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) (below_induction formula-decl nil bounded_nat_inductions 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" 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) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" cd3d_ii nil) (<= const-decl "bool" reals nil) (cd3d_ii_ind? inductive-decl "bool" cd3d_ii nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (M formal-const-decl "above[1]" cd3d_ii nil) (FlightPlan nonempty-type-eq-decl nil flightplan 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) (pred type-eq-decl nil defined_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (cd3d_ii?_TCC1 0 (cd3d_ii?_TCC1-1 nil 3482767958 ("" (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)) (cd3d_ii_ind_correct 0 (cd3d_ii_ind_correct-1 nil 3482839910 ("" (skeep) (("" (induct i) (("1" (skeep -1) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "cd3d_ii_ind?") (("2" (assert) (("2" (split) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (inst 1 0) (("1" (assert) (("1" (lemma "cd3d_si_correct[D, H, 0, min(fp(1)`time - fp(0)`time, T), M]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "min") (("2" (lift-if) (("2" (typepred fp) (("2" (inst - 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (prop) (("1" (skeep -1) (("1" (inst + j) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand cd3d_ii_ind? -2) (("2" (prop) (("2" (lemma "cd3d_si_correct[D, H, 0, min(fp(2 + jb)`time - fp(1 + jb)`time, fp(0)`time - fp(1 + jb)`time + T), M]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (typepred fp) (("2" (inst - "jb+2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (hide 2) (("4" (replace -2) (("4" (hide -2) (("4" (replace -2) (("4" (hide -2) (("4" (hide -1 -2 -3 -5 -6 -8 -9) (("4" (expand "min") (("4" (typepred fp) (("4" (inst - "j+1") (("4" (assert) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (typepred M) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (typepred M) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (velocity const-decl "Vect3" flightplan nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (fp2 skolem-const-decl "FlightPlanRelevant2(fp)" cd3d_ii nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (cd3d_ii_ind? inductive-decl "bool" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (M formal-const-decl "above[1]" cd3d_ii nil) (FlightPlan nonempty-type-eq-decl nil flightplan 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) (below type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (D formal-const-decl "posreal" cd3d_ii nil) (H formal-const-decl "posreal" cd3d_ii nil) (conflict_3D? const-decl "bool" cd3d_si nil) (FALSE const-decl "bool" booleans nil) (N formal-const-decl "above[1]" cd3d_ii 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) (below_induction formula-decl nil bounded_nat_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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (cd3d_si_correct formula-decl nil cd3d_si nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (NOT const-decl "[bool -> bool]" booleans nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil)) shostak)) (cd3d_ii_ind_complete 0 (cd3d_ii_ind_complete-1 nil 3482852346 ("" (skeep) (("" (induct i) (("1" (skeep -1) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst 1 0) (("1" (flatten) (("1" (assert) (("1" (lemma "cd3d_si_complete[D, H, 0, min(fp(1)`time - fp(0)`time, fp(0)`time - fp(0)`time + T), M]") (("1" (prop) (("1" (inst?) (("1" (ground) (("1" (expand "cd3d_ii_ind?") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "min") (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (typepred fp) (("2" (inst - 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (skeep) (("3" (skeep -2) (("3" (assert) (("3" (lift-if) (("3" (assert) (("3" (case "fp(0)`time - fp(j)`time + T > 0 AND fp2(0)`time < min(fp(1 + j)`time, fp(0)`time + T) AND fp2(M - 1)`time > fp(j)`time AND j <= jb") (("1" (flatten) (("1" (assert) (("1" (inst?) (("1" (prop) (("1" (expand "cd3d_ii_ind?" 1) (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (inst?) (("2" (prop) (("2" (case "j=jb+1") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (typepred j) (("1" (hide -2 -8 1) (("1" (hide -3 -4) (("1" (expand "cd3d_ii_ind?") (("1" (prop) (("1" (assert) (("1" (lemma "cd3d_si_complete[D, H, 0, min(fp(1 + j)`time - fp(j)`time, fp(0)`time - fp(j)`time + T), M]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (skeep) (("4" (replace -1) (("4" (hide -1) (("4" (hide 2) (("4" (assert) (("4" (replace -1) (("4" (hide -1) (("4" (expand "min") (("4" (lift-if) (("4" (assert) (("4" (typepred fp) (("4" (inst - "j+1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skeep) (("5" (hide 2) (("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (skeep) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (skeep) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (M formal-const-decl "above[1]" cd3d_ii nil) (velocity const-decl "Vect3" flightplan nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (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) (= const-decl "[T, T -> boolean]" equalities 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) (fp2 skolem-const-decl "FlightPlanRelevant2(fp)" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (below type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (D formal-const-decl "posreal" cd3d_ii nil) (H formal-const-decl "posreal" cd3d_ii nil) (conflict_3D? const-decl "bool" cd3d_si nil) (FALSE const-decl "bool" booleans nil) (cd3d_ii_ind? inductive-decl "bool" cd3d_ii nil) (N formal-const-decl "above[1]" cd3d_ii 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) (below_induction formula-decl nil bounded_nat_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) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (cd3d_si_complete formula-decl nil cd3d_si nil)) shostak)) (cd3d_si_complete_parameters_TCC1 0 (cd3d_si_complete_parameters_TCC1-1 nil 3483721809 ("" (skeep) (("" (typepred fp2) (("" (assert) (("" (postpone) nil nil)) nil)) nil)) nil) ((FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (N formal-const-decl "above[1]" cd3d_ii nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (M formal-const-decl "above[1]" cd3d_ii 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (cd3d_si_complete_parameters_TCC2 0 (cd3d_si_complete_parameters_TCC2-1 nil 3483723761 ("" (subtype-tcc) nil nil) ((FlightTimesRelevant type-eq-decl nil cd3d_si nil) (H formal-const-decl "posreal" cd3d_ii nil) (D formal-const-decl "posreal" cd3d_ii nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (start_time const-decl "real" flightplan nil) (<= const-decl "bool" reals nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (M formal-const-decl "above[1]" cd3d_ii nil) (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]" cd3d_ii nil) (above nonempty-type-eq-decl nil int_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (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 "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (segment_max const-decl "[SS: non_empty_finite_set[nat] -> {a: nat | SS(a) AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" flightplan nil) (segment const-decl "below[N]" flightplan nil) (- const-decl "Vector" vectors_3D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (conflict_3D? const-decl "bool" cd3d_si nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (cd3d_si_complete_parameters 0 (cd3d_si_complete_parameters-1 nil 3483721810 ("" (skeep) (("" (assert) (("" (lemma "cd3d_si_complete[D, H, 0, t1, M]") (("" (inst?) (("" (flatten) (("" (assert) 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (FlightPlanRelevant nonempty-type-eq-decl nil cd3d_si nil) (N formal-const-decl "above[1]" cd3d_ii nil) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (cd3d_si_complete formula-decl nil cd3d_si 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" cd3d_ii nil) (H formal-const-decl "posreal" cd3d_ii 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) (M formal-const-decl "above[1]" cd3d_ii nil)) shostak)) (cd3d_ii_correct 0 (cd3d_ii_correct-1 nil 3482855369 ("" (skeep) (("" (lemma cd3d_ii_ind_correct) (("" (expand "cd3d_ii?") (("" (inst?) (("1" (assert) (("1" (hide -2) (("1" (skeep -1) (("1" (assert) (("1" (ground) (("1" (lemma cd3d_ii_rew) (("1" (inst - fp fp2) (("1" (replace -1) (("1" (hide -1) (("1" (name jt "fp(j)`time") (("1" (inst 1 jt) (("1" (case "segment(fp)(jt) = j") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma segment_def[N]) (("2" (inst - fp jt) (("2" (flatten) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp j jt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp j 0) (("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - fp "N-1" j) (("2" (assert) (("2" (ground) (("1" (inst + j) (("1" (assert) nil nil)) nil) ("2" (inst + j) (("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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((cd3d_ii_ind_correct formula-decl nil cd3d_ii nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (N formal-const-decl "above[1]" cd3d_ii 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (cd3d_ii_rew formula-decl nil cd3d_ii nil) (= const-decl "[T, T -> boolean]" equalities nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (segment const-decl "below[N]" flightplan nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (segment_index formula-decl nil flightplan nil) (segment_def formula-decl nil flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (fp2 skolem-const-decl "FlightPlanRelevant2(fp)" cd3d_ii nil) (end_time const-decl "real" flightplan nil) (jt skolem-const-decl "real" cd3d_ii nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (start_time const-decl "real" flightplan nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cd3d_ii? const-decl "bool" cd3d_ii nil)) shostak)) (cd3d_ii_complete 0 (cd3d_ii_complete-2 "" 3483718981 ("" (skeep) (("" (lemma cd3d_ii_ind_complete) (("" (copy 1) (("" (hide 1) (("" (expand "cd3d_ii?") (("" (inst?) (("1" (lemma cd3d_ii_rew) (("1" (inst - fp fp2) (("1" (replace -1) (("1" (hide -1) (("1" (skeep -1) (("1" (name relT "T - (fp(j)`time - fp(0)`time)") (("1" (replace -1) (("1" (name t "min(fp(j + 1)`time - fp(j)`time, relT)") (("1" (typepred j) (("1" (assert) (("1" (skolem - tt) (("1" (typepred tt) (("1" (skolem - jj) (("1" (assert) (("1" (flatten) (("1" (hide 2) (("1" (expand "start_time") (("1" (expand "end_time") (("1" (case "jj=j") (("1" (replace -1) (("1" (assert) (("1" (ground) (("1" (expand "conflict_3D?") (("1" (assert) (("1" (skolem - jt) (("1" (inst + jt) (("1" (replace -5) (("1" (case "segment(fp)(fp(j)`time)=j") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (replace -5 :dir rl) (("2" (lemma segment_def[N]) (("2" (inst - fp tt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp j tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred jt) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (lemma segment_index[N]) (("2" (inst - fp j tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (hide -10) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal 2) (("2" (lemma segment_index[N]) (("2" (inst - fp jj tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "jj+1") (("2" (assert) (("2" (replace -2) (("2" (lemma cd3d_si_complete_parameters) (("2" (inst - "fp(jj)`position" "velocity[N](fp)(jj)" tt "min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, fp(0)`time - fp(segment(fp)(tt))`time + T)" fp fp2) (("1" (case "min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, fp(0)`time - fp(segment(fp)(tt))`time + T) = min(fp(1 + jj)`time - fp(jj)`time, fp(0)`time - fp(jj)`time + T)") (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (hide -14 3) (("1" (expand "cd3d_ii?") (("1" (lemma some_cd3d_ii) (("1" (inst - fp fp2 N-2) (("1" (assert) (("1" (inst 1 jj) (("1" (hide 2) (("1" (expand "cd3d_ii_ind?") (("1" (flatten) (("1" (assert) (("1" (case "fp2(0)`time < min(fp(1 + jj)`time, fp(0)`time + T)") (("1" (assert) (("1" (expand "min") (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "min") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (hide -1 -14) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -13 2 3 4) (("2" (expand "min") (("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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cd3d_ii_ind_complete formula-decl nil cd3d_ii nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (N formal-const-decl "above[1]" cd3d_ii 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (M formal-const-decl "above[1]" cd3d_ii 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) (T formal-const-decl "posreal" cd3d_ii nil) (FlightPlanRelevant2 nonempty-type-eq-decl nil cd3d_ii nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (<= const-decl "bool" reals 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) (real_plus_real_is_real application-judgement "real" reals 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) (start_time const-decl "real" flightplan nil) (end_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (FlightTimesLimited2 type-eq-decl nil cd3d_ii nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cd3d_si_complete_parameters formula-decl nil cd3d_ii nil) (some_cd3d_ii formula-decl nil cd3d_ii nil) (cd3d_ii_ind? inductive-decl "bool" cd3d_ii nil) (velocity const-decl "Vect3" flightplan nil) (fp skolem-const-decl "FlightPlan[N]" cd3d_ii nil) (fp2 skolem-const-decl "FlightPlanRelevant2(fp)" cd3d_ii nil) (tt skolem-const-decl "FlightTimesLimited2(fp, fp2)" cd3d_ii nil) (segment const-decl "below[N]" flightplan nil) (D formal-const-decl "posreal" cd3d_ii nil) (H formal-const-decl "posreal" cd3d_ii nil) (FlightTimesRelevant type-eq-decl nil cd3d_si nil) (jt skolem-const-decl "FlightTimesRelevant [D, H, 0, min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, fp(0)`time - fp(segment(fp)(tt))`time + T), M](tt, fp2)" cd3d_ii nil) (j skolem-const-decl "below[N - 1]" cd3d_ii nil) (relT skolem-const-decl "real" cd3d_ii nil) (segment_def formula-decl nil flightplan nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (segment_index formula-decl nil flightplan nil) (conflict_3D? const-decl "bool" cd3d_si nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cd3d_ii_rew formula-decl nil cd3d_ii nil) (cd3d_ii? const-decl "bool" cd3d_ii nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak) (cd3d_ii_complete-1 nil 3483697637 ("" (skeep) (("" (lemma cd3d_ii_ind_complete) (("" (copy 1) (("" (hide 1) (("" (expand "cd3d_ii?") (("" (inst?) (("1" (lemma cd3d_ii_rew) (("1" (inst - fp fp2) (("1" (replace -1) (("1" (hide -1) (("1" (skeep -1) (("1" (name relT "T - (fp(j)`time - fp(0)`time)") (("1" (replace -1) (("1" (name t "min(fp(j + 1)`time - fp(j)`time, relT)") (("1" (typepred j) (("1" (assert) (("1" (skolem - tt) (("1" (typepred tt) (("1" (skolem - jj) (("1" (assert) (("1" (flatten) (("1" (hide 2) (("1" (expand "start_time") (("1" (expand "end_time") (("1" (case "jj=j") (("1" (replace -1) (("1" (assert) (("1" (ground) (("1" (expand "conflict_3D?") (("1" (assert) (("1" (skolem - jt) (("1" (inst + jt) (("1" (replace -5) (("1" (case "segment(fp)(fp(j)`time)=j") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (replace -5 :dir rl) (("2" (lemma segment_def[N]) (("2" (inst - fp tt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp j tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred jt) (("2" (expand "start_time") (("2" (expand "end_time") (("2" (lemma segment_index[N]) (("2" (inst - fp j tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "j+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (hide -10) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma segment_def[N]) (("2" (inst - fp tt) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma segment_index[N]) (("2" (inst - fp jj tt) (("2" (assert) (("2" (typepred fp) (("2" (inst - "jj+1") (("2" (assert) (("2" (replace -2) (("2" (lemma limited_bounds) (("2" (inst - fp fp2 tt jj) (("2" (assert) (("2" (lemma "cd3d_si_complete[D, H, 0, min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, fp(0)`time - fp(segment(fp)(tt))`time + T), M]") (("1" (inst?) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil) ("2" (hide 3) (("2" (expand "min") (("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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)))
¤ Dauer der Verarbeitung: 0.203 Sekunden (vorverarbeitet am 2026-05-05) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26