Quelle cd3d_ii.prf
Sprache: Lisp
(cd3d_iinil 3482767958 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3482767958 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3482767958 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3482767958 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3482767958 ("" (subtype-tcc) nil nil )nil nil ))nil 3482767958"" (skeep)"" "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 )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"FlightPlan[N]" cd3d_ii nil )nil flightplan nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3482836778"" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3483457740"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3483200922 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3483206183 ("" (subtype-tcc) nil nil )nil nil ))nil 3483267537 ("" (subtype-tcc) nil nil )nil nil ))nil 3483377850 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"bool" reals nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil ))nil ))nil 3482836778 ("" (subtype-tcc) nil nil )"real" flightplan nil )"real" flightplan nil ))nil ))nil 3483457740 ("" (subtype-tcc) nil nil )"real" flightplan nil )"real" flightplan nil ))nil ))nil 3483437086 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"bool" reals nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )nil cd3d_ii nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"int" integers nil )"[SS: non_empty_finite_set[nat] -> AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" nil )"below[N]" flightplan nil ))nil ))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" "1" "jj+1" )"1" assert )"1" "1" "1" expand "min" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma segment_def[N])"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"below[N]" cd3d_ii nil )"(total_order?[real])" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil flightplan nil )nil flightplan nil )"real" reals nil ))nil ))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" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil flightplan nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil ))nil ))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" "1" assert )"1" "1" "1" "1" "1" assert )"1" "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" "2" "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 )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil flightplan nil )nil flightplan nil )nil flightplan nil )"(total_order?[real])" nil )"bool" reals nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil )"below[N]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))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 )nil flightplan nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil )"real" reals nil ))nil ))"nooooo!" 3483365871"" (skeep)"" (assert )"" (skeep)"" (typepred t1)"" (typepred t2)"" (typepred fp)"" (skeep -8)"" (name jj "segment(fp)(t1)" )"" (replace -1)"" "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" "1" assert )"1" "1" "1" (assert ) nil nil )"2" assert )"2" "2" "2" assert )"2" "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" "1" "j-1" "1" assert )"1" replace "1" assert )"1" case "fp(j)`time < fp(jj+1)`time" )"1" assert )"1" "1" "1" case "j-1 < jj+1" )"1" assert )nil nil )"2" assert )"2" "2" "2" case "jj <= j-2" )"1" assert )"1" "1" "1" replace "1" "1" "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" "2" "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 )nil cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"real" reals nil )nil flightplan nil )"posint" nil )"(total_order?[real])" nil )nil flightplan nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"below[N]" flightplan nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )nil cd3d_si nil )"real" reals nil ))nil 3483278009"" (skeep)"" (assert )"" (skeep)"" (typepred t1)"" (typepred t2)"" (typepred fp)"" (skeep -8)"" (name jj "segment(fp)(t1)" )"" (replace -1)"" "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" "1" assert )"1" "1" "1" (assert ) nil nil )"2" assert )"2" "2" "2" assert )"2" "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" "1" "j-1" "1" assert )"1" replace "1" assert )"1" case "fp(j)`time < fp(jj+1)`time" )"1" assert )"1" "1" "1" case "j-1 < jj+1" )"1" assert )nil nil )"2" assert )"2" "2" "2" case "jj <= j-2" )"1" assert )"1" "1" "1" replace "1" "1" "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" "2" "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 )nil cd3d_si nil )"below[N]" flightplan nil )nil flightplan nil )nil flightplan nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil ))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 )nil cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil flightplan nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"posint" nil ))nil ))nil 3483438693 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"bool" reals nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )nil cd3d_ii nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[SS: non_empty_finite_set[nat] -> AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" nil )"below[N]" flightplan nil )"real" reals nil ))nil ))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" "2" assert )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil flightplan nil )nil flightplan nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"posint" nil )nil cd3d_ii nil )"real" reals nil ))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 )nil cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"above[1]" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil flightplan nil ))nil ))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 )"" "" "" assert )"" case "jj=j" )"1" (assert ) nil nil )"2" "2" "2" assert )"2" "2" "2" assert )"2" "2" "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 )nil cd3d_ii nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil flightplan nil )"(total_order?[real])" nil )nil flightplan nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"posint" nil )"posint" nil )nil cd3d_ii nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"real" flightplan nil )"real" flightplan nil )"bool" reals nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"above[1]" cd3d_ii nil )nil flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))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 )nil flightplan nil )nil flightplan nil )"posint" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"below[N]" cd3d_ii nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil ))nil ))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 )nil flightplan nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" reals nil )"(total_order?[real])" nil )"posint" nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil ))nil ))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)"" "" "" expand "start_time" )"" expand "end_time" )"" "" "" assert )"" "" "j+1" )"1" assert )"1" "1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_ii nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"below[N]" cd3d_ii nil )nil flightplan nil )"(total_order?[real])" nil )nil flightplan nil )NOT const-decl "[bool -> bool]" booleans nil )nil flightplan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil ))nil ))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" "1" "1" assert )"1" replace -1)"1" assert )"1" "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" "1" assert )"1" expand "min" )"1" "1" "1" replace -2 :dir rl)"1" replace -1)"1" replace -2)"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "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" "2" assert )"2" "1" assert )"1" "1" assert )"1" "flight_plan_ascending_time[N]" )"1" "1" "1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "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" "conflict_3D_flightplan_open_interval[D, H, 0, min(fp(1 + j)`time - fp(j)`time, fp(0)`time - fp(j)`time + T), M]" )"1" (assert )"1" (inst?)"1" (replace -1)"1" (hide -1)"1" (skolem - tt)"1" (flatten)"1" "1" "1" "1" assert )"1" expand "start_time" )"1" expand "end_time" )"1" case "jj=j" )"1" "1" "1" replace -10)"1" assert )"1" "1" "1" assert )"1" case "tt < fp(N-1)`time AND fp2(0)`time <= tt" )"1" "1" assert )"1" "1" expand "1" expand "1" assert )"1" "1" "1" "1" assert )"1" case "(fp(j)`position + (tt - jt) * velocity[N](fp)(j))=fp(segment(fp)(tt))`position + ") "1" replace "1" assert )"1" expand "+ ") "1" expand "*" )"1" expand "-" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" assert )"2" "2" assert )"2" "segment(fp)(tt)" )"2" replace "2" case "j=k" )"1" replace "1" replace "1" replace "1" nil nil ))nil ))nil ))nil )"2" "2" "2" "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" "2" expand "start_time" )"2" expand "end_time" )"2" assert )"2" case "tt < fp(j+1)`time" )"1" assert )"1" "1" "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" "2" "2" "2" "2" assert )"2" "2" assert )"2" "2" "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" "2" assert )"2" "2" "2" assert )"2" "2" assert )"2" replace -10)"2" "2" "2" assert )"2" 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" "2" "2" assert )"2" "2" "2" "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" "3" assert )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"below[N]" cd3d_ii nil )nil flightplan nil )"even_int" integersnil )"real" reals nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil cd3d_si nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )nil flightplan nil )nil flightplan nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"int" integers nil )"Vect3" flightplan nil )"below[N]" cd3d_ii nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil flightplan nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" cd3d_si nil )"real" reals nil )nil cd3d_ii nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )"real" flightplan nil )"FlightPlan[N]" cd3d_ii nil )"real" flightplan nil )nil flightplan nil )"below[N]" flightplan nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )"above[1]" cd3d_ii nil )nil cd3d_ii nil )"FlightPlanRelevant2(fp)" cd3d_ii nil )nil cd3d_ii nil )"FlightTimesRelevant2(fp, fp2)" cd3d_ii nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"bool" cd3d_ii nil )"real" reals nil )nil cd3d_si nil )"below[N]" cd3d_ii nil )"FlightTimesLimited2(fp, fp2)" cd3d_ii nil )nil cd3d_si nil )"Vect3" flightplan nil )nil cd3d_ii nil )"FlightTimesRelevant min (fp(1 + j)`time - fp(j)`time, fp(0)`time - fp(j)`time + T), M](jt," nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )nil flightplan nil ))nil 3482767958 ("" (subtype-tcc) nil nil )"real" reals nil ))nil ))nil 3482767958 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"real" reals nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" reals nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"Vect3" flightplan nil )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))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" reals nil )"int" integers nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil ))nil ))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" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_3D_def "vectors/" )nil flightplan nil ))nil ))nil 3483179897"" (skeep)"" (skeep)"" (skeep)"" (skeep)"" (skeep)"" (assert )"" (expand "min" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"real" reals nil ))nil ))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" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"bool" reals nil )"(total_order?[real])" nil )"int" integers nil )nil bounded_nat_inductions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil int_types nil )"above[1]" cd3d_ii nil )"bool" reals nil )"bool" cd3d_ii nil )"[bool, bool -> bool]" booleans nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"above[1]" cd3d_ii nil )nil flightplan nil )"[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )nil nat_types nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil ))nil 3482767958 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))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" "cd3d_si_correct[D, H, 0, min(fp(1)`time - fp(0)`time, T), M]" )"1" "1" (assert ) nil nil ))nil )"2" assert )"2" expand "min" )"2" "2" "2" "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" "cd3d_si_correct[D, H, 0, min (fp(2 + jb)`time - fp(1 + jb)`time,") "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" "4" "j+1" )"4" assert )"4" "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" reals nil )"posint" nil )"real" reals nil )"Vect3" flightplan nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"FlightPlanRelevant2(fp)" cd3d_ii nil )"FlightPlan[N]" cd3d_ii nil )"bool" cd3d_ii nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_3D_def "vectors/" )"above[1]" cd3d_ii nil )nil flightplan nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )nil defined_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )"bool" cd3d_si nil )"bool" booleans nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_nat_inductions nil )"int" integers nil )"(total_order?[real])" nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )nil cd3d_si nil )nil cd3d_si nil )NOT const-decl "[bool -> bool]" booleans nil )"even_int" integersnil ))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" "cd3d_si_complete[D, H, 0, min (fp(1)`time - fp(0)`time,") "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 min (fp(1 + j)`time, fp(0)`time + T) AND 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" "1" "1" "1" expand "cd3d_ii_ind?" )"1" "1" assert )"1" "cd3d_si_complete[D, H, 0, min (fp(1 + j)`time - fp(j)`time, fp(0)`time - fp(j)`time + T), M]") "1" "1" (assert ) nil nil ))nil )"2" expand "min" )"2" "2" assert )"2" "2" "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" "4" assert )"4" "4" "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" reals nil )"posint" nil )"real" reals nil )"above[1]" cd3d_ii nil )"Vect3" flightplan nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"FlightPlan[N]" cd3d_ii nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )"FlightPlanRelevant2(fp)" cd3d_ii nil )nil cd3d_ii nil )nil naturalnumbers nil )nil defined_types nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )"bool" cd3d_si nil )"bool" booleans nil )"bool" cd3d_ii nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil bounded_nat_inductions nil )"int" integers nil )"(total_order?[real])" nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"odd_int" integers nil )"even_int" integersnil )NOT const-decl "[bool -> bool]" booleans nil )nil cd3d_si nil )nil cd3d_si nil ))nil 3483721809"" (skeep)"" (typepred fp2) (("" (assert ) (("" (postpone) nil nil )) nil ))nil ))nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil ))nil ))nil 3483723761"" (subtype-tcc) nil nil )nil cd3d_si nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )nil flightplan nil )"real" flightplan nil )"real" flightplan nil )"bool" reals nil )nil cd3d_ii nil )"posreal" cd3d_ii nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"above[1]" cd3d_ii nil )nil flightplan nil )nil vectors_3D_def "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"Vector" vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"[SS: non_empty_finite_set[nat] -> AND (FORALL (x: nat): SS(x) IMPLIES x <= a)}]" nil )"below[N]" flightplan nil )"Vector" vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"bool" cd3d_si nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3483721810"" (skeep)"" (assert )"" (lemma "cd3d_si_complete[D, H, 0, t1, M]" )"" (inst?) (("" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil vectors_3D_def "vectors/" )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil flightplan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil cd3d_si nil )"above[1]" cd3d_ii nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )nil cd3d_si nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil int_types nil )"above[1]" cd3d_ii nil ))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" "1" case "segment(fp)(jt) = j" )"1" replace -1)"1" (assert ) nil nil ))nil )"2" "2" "2" "2" assert )"2" "2" "2" assert )"2" "2" "j+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "start_time" )"2" expand "end_time" )"2" "2" "2" "2" "N-1" j)"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "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 )nil cd3d_ii nil )"(total_order?[real])" nil )"int" integers nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil cd3d_ii nil )"[T, T -> boolean]" equalities nil )nil flightplan nil )"below[N]" flightplan nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )nil flightplan nil )nil flightplan nil )nil flightplan nil )nil cd3d_ii nil )"FlightPlanRelevant2(fp)" cd3d_ii nil )"real" flightplan nil )"real" cd3d_ii nil )"FlightPlan[N]" cd3d_ii nil )"real" flightplan nil )"bool" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"bool" cd3d_ii nil ))"" 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" "T - (fp(j)`time - fp(0)`time)" )"1" (replace -1)"1" "min(fp(j + 1)`time - fp(j)`time, relT)" )"1" "1" assert )"1" "1" "1" "1" assert )"1" "1" "1" expand "start_time" )"1" expand "end_time" )"1" case "jj=j" )"1" replace -1)"1" assert )"1" "1" expand "conflict_3D?" )"1" assert )"1" "1" "1" replace "1" case "segment(fp)(fp(j)`time)=j" )"1" replace "1" nil nil ))nil )"2" replace "2" "2" "2" assert )"2" "2" assert )"2" "2" "2" assert )"2" "2" "j+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "start_time" )"2" expand "end_time" )"2" "2" "2" assert )"2" "2" "j+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )"2" "2" "jj+1" )"2" assert )"2" replace "2" "2" "fp(jj)`position" "velocity[N](fp)(jj)" "min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, " "1" case "min(fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time, min (fp(1 + jj)`time - fp(jj)`time,") "1" replace "1" assert )"1" "1" "1" expand "cd3d_ii?" )"1" "1" "1" assert )"1" "1" "1" expand "cd3d_ii_ind?" )"1" "1" assert )"1" case "fp2(0)`time < min(fp(1 + jj)`time, fp(0)`time + T)" )"1" assert )"1" expand "min" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "min" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "min" )"2" "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 )nil cd3d_ii nil )"(total_order?[real])" nil )"above[1]" cd3d_ii nil )nil int_types nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil vectors_3D_def "vectors/" )"[bool, bool -> bool]" booleans nil )nil flightplan nil )"above[1]" cd3d_ii nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" cd3d_ii nil )nil cd3d_ii nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"posint" nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" flightplan nil )"real" flightplan nil )nil flightplan nil )nil cd3d_ii nil )"(total_order?[real])" nil )nil cd3d_ii nil )nil cd3d_ii nil )"bool" cd3d_ii nil )"Vect3" flightplan nil )"FlightPlan[N]" cd3d_ii nil )"FlightPlanRelevant2(fp)" cd3d_ii nil )"FlightTimesLimited2(fp, fp2)" cd3d_ii nil )"below[N]" flightplan nil )"posreal" cd3d_ii nil )"posreal" cd3d_ii nil )nil cd3d_si nil )"FlightTimesRelevant min (fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time," cd3d_ii nil) "below[N - 1]" cd3d_ii nil )"real" cd3d_ii nil )nil flightplan nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )nil flightplan nil )"bool" cd3d_si nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )nil cd3d_ii nil )"bool" cd3d_ii nil )"int" integers nil ))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" "T - (fp(j)`time - fp(0)`time)" )"1" (replace -1)"1" "min(fp(j + 1)`time - fp(j)`time, relT)" )"1" "1" assert )"1" "1" "1" "1" assert )"1" "1" "1" expand "start_time" )"1" expand "end_time" )"1" case "jj=j" )"1" replace -1)"1" assert )"1" "1" expand "conflict_3D?" )"1" assert )"1" "1" "1" replace "1" case "segment(fp)(fp(j)`time)=j" )"1" replace "1" nil nil ))nil )"2" replace "2" "2" "2" assert )"2" "2" assert )"2" "2" "2" assert )"2" "2" "j+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "start_time" )"2" expand "end_time" )"2" "2" "2" assert )"2" "2" "j+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "min" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" assert )"2" "2" "2" assert )"2" "2" "jj+1" )"2" assert )"2" replace "2" "2" "2" assert )"2" "cd3d_si_complete[D, H, 0, min (fp(1 + segment(fp)(tt))`time - fp(segment(fp)(tt))`time,") "1" "1" assert )"1" nil nil ))nil ))nil )"2" "2" expand "min" )"2" "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)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.232 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
