| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: flightplan.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(flightplan
(j_TCC1 0 (j_TCC1-1 nil 3482759352 ("" (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)) (FlightPlan_TCC1 0 (FlightPlan_TCC1-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (FlightPlan_TCC2 0 (FlightPlan_TCC2-2 nil 3482759784 ("" (inst + "lambda (jj: below[N]): (# time:= jj,position:= zero #)") nil nil) ((zero const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan 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)) nil) (FlightPlan_TCC2-1 nil 3482759352 ("" (existence-tcc) nil nil) nil nil)) (start_time_TCC1 0 (start_time_TCC1-1 nil 3482759352 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (end_time_TCC1 0 (end_time_TCC1-1 nil 3482759352 ("" (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)) (flight_plan_ascending_time 0 (flight_plan_ascending_time-1 nil 3482759592 ("" (skeep) (("" (case "FORALL (jj: nat): (k + jj+1) < N IMPLIES (flp(k)`time < flp(k+jj+1)`time)") (("1" (inst - "(i-k)-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "jj") (("1" (assert) (("1" (typepred "flp") (("1" (inst - "1+k") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "flp") (("2" (inst - "2+j!1+k") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan nil) (above nonempty-type-eq-decl nil int_types nil) (> const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i skolem-const-decl "below[N]" flightplan nil) (k skolem-const-decl "below[N]" flightplan nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (flight_plan_unique_times 0 (flight_plan_unique_times-1 nil 3483287614 ("" (skeep) (("" (assert) (("" (prop) (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - flp i k) (("1" (assert) (("1" (lemma flight_plan_ascending_time[N]) (("1" (inst - flp k i) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" flightplan 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (flight_plan_ascending_time formula-decl nil flightplan nil)) shostak)) (FlightTimes_TCC1 0 (FlightTimes_TCC1-2 nil 3482759820 ("" (skeep) (("" (inst + "(start_time(flp) + end_time(flp))/2") (("" (expand "start_time") (("" (expand "end_time") (("" (lemma "flight_plan_ascending_time") (("" (inst - "flp" "N-1" "0") (("1" (ground) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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_div_nzreal_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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]" flightplan 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) (end_time const-decl "real" flightplan nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (flp skolem-const-decl "FlightPlan" flightplan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (flight_plan_ascending_time formula-decl nil flightplan nil)) nil) (FlightTimes_TCC1-1 nil 3482759352 ("" (existence-tcc) nil nil) nil nil)) (velocity_TCC1 0 (velocity_TCC1-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (velocity_TCC2 0 (velocity_TCC2-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (velocity_TCC3 0 (velocity_TCC3-1 nil 3482759352 ("" (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]" flightplan 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (velocity_def 0 (velocity_def-1 nil 3482759633 ("" (skeep) (("" (expand "velocity") (("" (assert) (("" (expand "+ ") (("" (assert) (("" (expand "-") (("" (assert) (("" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((velocity const-decl "Vect3" flightplan nil) (+ const-decl "Vector" vectors_3D "vectors/") (- const-decl "Vector" vectors_3D "vectors/") (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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" flightplan 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (scal_assoc formula-decl nil vectors_3D "vectors/") (scal_1 formula-decl nil vectors_3D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (FlightPlan_nz_TCC1 0 (FlightPlan_nz_TCC1-1 nil 3483101697 ("" (inst + "lambda (jj: below[N]): (# time:= jj,position:= (# x:=jj, y:=jj, z:=jj #) #)") (("" (skeep) (("" (expand "velocity") (("" (expand "vect2") (("" (expand "zero") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "Vector" vectors_3D "vectors/") (scal_1 formula-decl nil vectors_3D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (velocity const-decl "Vect3" flightplan nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan 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)) nil)) (segment_max_TCC1 0 (segment_max_TCC1-1 nil 3482759352 ("" (skolem 1 x) (("" (assert) (("" (skolem 1 y) (("" (typepred "finite_sets@finite_sets_minmax [naturalnumbers.nat, restrict[[real, real], [nat, nat], boolean].restrict (reals.<=)].max (x)") (("" (inst - y) (("" (flatten) (("" (assert) (("" (expand "restrict") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (segment_TCC1 0 (segment_TCC1-2 nil 3482759932 ("" (skosimp*) (("" (split) (("1" (expand "is_finite") (("1" (inst + "N" "(lambda (ii: ({j: below[N] | tt!1 >= flp!1(j)`time})): ii)") (("1" (expand "injective?") (("1" (skosimp*) nil nil)) nil) ("2" (skosimp*) (("2" (expand "extend") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (expand "extend") (("2" (ground) (("2" (typepred "tt!1") (("2" (expand "start_time") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (tt!1 skolem-const-decl "FlightTimes(flp!1)" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan nil) (flp!1 skolem-const-decl "FlightPlan" flightplan 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) (<= const-decl "bool" reals nil) (N formal-const-decl "above[1]" flightplan nil) (above nonempty-type-eq-decl nil int_types nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans 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) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil) (segment_TCC1-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (segment_TCC2 0 (segment_TCC2-2 nil 3482759961 ("" (skeep) (("" (name "iii" "max[nat, restrict[[real, real], [nat, nat], boolean](<=)] (extend[nat, below[N], bool, FALSE] ({j: below[N] | tt >= flp(j)`time}))") (("" (typepred "iii") (("" (expand "extend") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan nil) (above nonempty-type-eq-decl nil int_types nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (segment_TCC2-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (segment_def_TCC1 0 (segment_def_TCC1-1 nil 3482759352 ("" (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]" flightplan 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) (<= 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) (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) (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 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)) (segment_def 0 (segment_def-1 nil 3482759657 ("" (skeep) (("" (split) (("1" (expand "segment") (("1" (typepred "segment_max(extend[nat, below[N], bool, FALSE] ({j: below[N] | tt >= flp(j)`time}))") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "segment") (("2" (typepred "segment_max(extend[nat, below[N], bool, FALSE] ({j: below[N] | tt >= flp(j)`time}))") (("2" (inst - "1+segment_max(extend[nat, below[N], bool, FALSE] ({j: below[N] | tt >= flp(j)`time}))") (("2" (assert) (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (empty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (end_time const-decl "real" flightplan 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/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment const-decl "below[N]" flightplan nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (segment_index 0 (segment_index-1 nil 3482759686 ("" (skeep) (("" (name seg "segment(flp)(tt)") (("" (replace -1) (("" (lemma segment_def) (("" (inst - flp tt) (("" (assert) (("" (flatten) (("" (replace -3) (("" (case "seg=N-1") (("1" (assert) (("1" (hide -3) (("1" (flatten) (("1" (typepred j) (("1" (lemma flight_plan_ascending_time) (("1" (inst - flp seg "j+1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (prop) (("1" (assert) (("1" (case "seg < j") (("1" (lemma flight_plan_ascending_time) (("1" (inst - flp j "seg+1") (("1" (assert) nil nil)) nil)) nil) ("2" (case "seg > j") (("1" (lemma flight_plan_ascending_time) (("1" (inst - flp seg "j+1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((segment const-decl "below[N]" flightplan 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (segment_def 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) (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) (flight_plan_ascending_time formula-decl nil flightplan nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (segment_max 0 (segment_max-1 nil 3483095937 ("" (skeep) (("" (typepred tt) (("" (expand "start_time") (("" (expand "end_time") (("" (lemma segment_def) (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma segment_index) (("" (inst?) (("1" (flatten) (("1" (assert) (("1" (ground) (("1" (typepred flp) (("1" (inst - "N-1") (("1" (assert) (("1" (case "segment(flp)(tt) < N-1") (("1" (assert) (("1" (name seg "segment(flp)(tt)") (("1" (replace -1) (("1" (case "seg = N-2") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "flight_plan_ascending_time[N]") (("2" (inst - flp "N-1" "seg+1") (("2" (assert) 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)) nil)) nil)) nil)) nil)) nil)) 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]" flightplan 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (segment const-decl "below[N]" flightplan nil) (flp skolem-const-decl "FlightPlan" flightplan nil) (tt skolem-const-decl "FlightTimes(flp)" flightplan nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (segment_index formula-decl nil flightplan nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (segment_def formula-decl nil flightplan nil)) shostak)) (segment_ident_TCC1 0 (segment_ident_TCC1-1 nil 3483197485 ("" (skeep) (("" (expand "start_time") (("" (expand "end_time") (("" (typepred tt) (("" (expand "end_time") (("" (expand "start_time") (("" (lemma segment_def) (("" (inst?) (("" (assert) (("" (flatten) (("" (assert) (("" (lemma segment_max) (("" (inst?) (("" (assert) (("" (case "segment(flp)(tt) = 0") (("1" (assert) nil nil) ("2" (lemma flight_plan_ascending_time[N]) (("2" (inst - flp "segment(flp)(tt)" 0) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((start_time const-decl "real" flightplan nil) (FlightTimes nonempty-type-eq-decl nil flightplan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (FlightPlan nonempty-type-eq-decl nil flightplan nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (below type-eq-decl nil nat_types nil) (N formal-const-decl "above[1]" flightplan 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_max formula-decl nil flightplan nil) (flight_plan_ascending_time formula-decl nil flightplan nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (segment const-decl "below[N]" flightplan nil) (= const-decl "[T, T -> boolean]" equalities 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) (segment_def formula-decl nil flightplan nil) (end_time const-decl "real" flightplan nil)) nil)) (segment_ident 0 (segment_ident-1 nil 3483197486 ("" (skeep) (("" (lemma segment_index) (("" (inst?) (("1" (assert) (("1" (typepred flp) (("1" (inst - "1 + segment(flp)(tt)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma segment_max) (("2" (inst?) (("2" (assert) 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_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) (NOT const-decl "[bool -> bool]" booleans 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) (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) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" flightplan 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) (segment const-decl "below[N]" flightplan nil) (flp skolem-const-decl "FlightPlan" flightplan nil) (tt skolem-const-decl "FlightTimes(flp)" flightplan 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)) shostak)) (location_at_TCC1 0 (location_at_TCC1-1 nil 3482759352 ("" (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]" flightplan 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) (<= 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) (real_le_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) (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)) (location_at_check_TCC1 0 (location_at_check_TCC1-2 nil 3482759998 ("" (skeep) (("" (lemma "flight_plan_ascending_time") (("" (inst-cp - "flp" "k" "0") (("" (inst - "flp" "N-1" "k") (("" (expand "start_time") (("" (expand "end_time") (("" (typepred "k") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((flight_plan_ascending_time formula-decl nil flightplan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (end_time const-decl "real" flightplan nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[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]" flightplan 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (location_at_check_TCC1-1 nil 3482759352 ("" (subtype-tcc) nil nil) nil nil)) (location_at_check 0 (location_at_check-1 nil 3482759710 ("" (skeep) (("" (expand "location_at") (("" (lift-if) (("" (ground) (("1" (case "k = N-1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (name "segg" "segment(flp)(flp(k)`time)") (("2" (replace -1) (("2" (copy -1) (("2" (expand "segment" -2) (("2" (typepred "segment_max(extend[nat, below[N], bool, FALSE] ({j: below[N] | flp(k)`time >= flp(j)`time}))") (("2" (expand "segment") (("2" (replace -4) (("2" (expand "extend") (("2" (assert) (("2" (lemma "flight_plan_ascending_time") (("2" (inst - "flp" "N-1" "k") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "segg" "segment(flp)(flp(k)`time)") (("2" (replace -1) (("2" (copy -1) (("2" (expand "segment" -2) (("2" (typepred "segment_max(extend[nat, below[N], bool, FALSE] ({j: below[N] | flp(k)`time >= flp(j)`time}))") (("2" (expand "segment") (("2" (replace -4) (("2" (expand "extend") (("2" (assert) (("2" (case "segg = k") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (inst - "k") (("2" (assert) (("2" (lemma "flight_plan_ascending_time") (("2" (inst - "flp" "segg" "k") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((location_at const-decl "Vect3" flightplan nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (flight_plan_ascending_time formula-decl nil flightplan 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) (NOT const-decl "[bool -> bool]" booleans nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (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) (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) (segment const-decl "below[N]" flightplan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil int_types nil) (N formal-const-decl "above[1]" flightplan nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (scal_0 formula-decl nil vectors_3D "vectors/") (add_zero_right formula-decl nil vectors_3D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil))) ¤ Dauer der Verarbeitung: 0.69 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
