| products/sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: vs_only.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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:=zero #)") (("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 (("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 (("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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.80 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 |
