Quelle bands_3D.prf
Sprache: Lisp
(bands_3Dnil 3477656172 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"(strict_total_order?[real])" real_props nil )"Nz_vect2" definitions_3D nil ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )"real" reals nil )"boolean" notequal nil ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"{x: posreal | x > B}" bands_3D nil )"bool" reals nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )"nnreal" bands_3D nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"real" vertical nil )"boolean" notequal nil )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"{x: posreal | x > B}" bands_3D nil )"bool" reals nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )"nnreal" bands_3D nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"real" vertical nil )"boolean" notequal nil )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3477656172 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"{x: posreal | x > B}" bands_3D nil )"bool" reals nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )"nnreal" bands_3D nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"real" vertical nil )"boolean" notequal nil )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"real" vertical nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"fsq" fseqs "structures/" )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3477736096"" (skeep)"" (skosimp*)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 4)"1" (expand "trk_fseq?" )"1" (skosimp*)"1" (lift-if)"1" (split +)"1" (flatten)"1" (assert ) (("1" (assert ) nil nil )) nil ))nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (case "i!1 = 0 AND j!1 = 1" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (typepred "i!1" )"2" (typepred "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"bool" fseqs_aux_2D nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"int" integers nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities 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" sort_fseq "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" ))nil ))nil 3477736096 ("" (subtype-tcc) nil nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"fsq" fseqs "structures/" ))nil ))"" 3504804745"" (skeep)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 2)"1" (expand "trk_fseq?" )"1" (skosimp*)"1" (lift-if)"1" (ground)"1" (lift-if) (("1" (ground) nil nil )) nil )"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (case "i!1 = 0 AND j!1 = 1" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (typepred "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"bool" sort_fseq "structures/" )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 )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" fseqs_aux_2D nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"fseq" fseqs_ops "structures/" ))nil 3477736096"" (skeep)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 2)"1" (expand "trk_fseq?" )"1" (skosimp*)"1" (lift-if) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (case "i!1 = 0 AND j!1 = 1" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (typepred "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs_aux_2D nil )"fseq" fseqs_ops "structures/" ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"{x: posreal | x > B}" bands_3D nil )"int" integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )"nnreal" bands_3D nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"boolean" notequal nil )"real" vertical nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" )"fseq" fseqs_ops "structures/" )"bool" fseqs_aux_2D nil )"bool" reals nil )nil booleans nil )"bool" sort_fseq "structures/" )"real" reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3477736096 ("" (subtype-tcc) nil nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"Nz_vect2" definitions_3D nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" )"fseq" fseqs_ops "structures/" )"bool" fseqs_aux_2D nil )"bool" reals nil )nil booleans nil )"bool" sort_fseq "structures/" ))nil ))nil 3477656172 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"Nz_vect2" definitions_3D nil )"Vector" vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )"real" reals nil ))nil ))nil 3477656172"" (skeep)"" (assert )"" (lemma "Delta_gt_0_nzv" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_3D_def "vectors/" )nil vectors_2D_def "vectors/" )nil horizontal 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" bands_3D nil ))nil ))nil 3477656172"" (skeep)"" (skosimp*)"" (replace -2)"" (hide-all-but 2) (("" (grind :exclude "Theta_D" ) nil nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"(total_order?[real])" nil )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_3D "vectors/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil ))nil ))nil 3477656172"" (skeep)"" (hide-all-but (-2 2))"" (grind :exclude "Theta_D" ) nil nil )) nil ))nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"Vector" vectors_3D "vectors/" )"Vect2" vect_3D_2D "vectors/" )"bool" reals nil )"{x: posreal | x > B}" bands_3D nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" bands_3D nil )nil real_types nil )nil definitions_3D nil )nil vectors_3D "vectors/" )nil vectors_3D_def "vectors/" )"real" horizontal nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" horizontal nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )AND const-decl "[bool, bool -> bool]" booleans 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 ))nil 3477656172"" (skeep) (("" (skosimp*) (("" (assert ) nil nil )) nil )) nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3477656172"" (skeep)"" (skosimp*)"" (typepred "i!1" )"" (expand "empty_seq" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"fsq" fseqs "structures/" )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 )nil naturalnumbers nil ))nil ))"" 3504804951"" (skeep)"" (skosimp*)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 3)"1" (expand "vs_fseq?" )"1" (skosimp*)"1" (lift-if)"1" (ground)"1" (lift-if) (("1" (ground) nil nil )) nil )"2" (lift-if) (("2" (ground) nil nil )) nil )"3" (lift-if) (("3" (ground) nil nil )) nil )"4" (lift-if) (("4" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (typepred "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"bool" fseqs_aux_vertical nil )"int" integers nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" sort_fseq "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" ))nil 3477744697"" (skeep)"" (skosimp*)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 3)"1" (expand "vs_fseq?" )"1" (skosimp*)"1" (lift-if) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (expand "increasing?" )"2" (skosimp*)"2" (typepred "i!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"bool" fseqs_aux_vertical nil )"bool" sort_fseq "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" ))nil ))nil 3477744697"" (skeep)"" (skosimp*)"" (expand "empty_seq" ) (("" (propax) nil nil )) nil )) nil ))nil )"fsq" fseqs "structures/" )) nil ))"" 3504805194"" (skeep)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 3)"1" (expand "vs_fseq?" )"1" (skosimp*)"1" (lift-if)"1" (ground)"1" (lift-if) (("1" (ground) nil nil )) nil )"2" (lift-if) (("2" (ground) nil nil )) nil )"3" (lift-if) (("3" (ground) nil nil )) nil )"4" (lift-if) (("4" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "increasing?" )"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"bool" sort_fseq "structures/" )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs_aux_vertical nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"fseq" fseqs_ops "structures/" ))nil 3477744697"" (skeep)"" (expand "add" )"" (expand "insert" )"" (expand "empty_seq" )"" (split 3)"1" (expand "vs_fseq?" )"1" (skosimp*)"1" (lift-if) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (expand "increasing?" )"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs_aux_vertical nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"fseq" fseqs_ops "structures/" ))nil ))nil 3481653292"" (skeep)"" (expand "trk_bands_3D" )"" (lift-if)"" (ground)"1" (lemma "trk_bands_not_empty[D,B,T,gsmin,gsmax]" )"1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"2" "trk_bands_not_empty[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"3" (expand "max" )"3" (expand "min" )"3" (expand "add" )"3" (expand "insert" )"3" (expand "empty_seq" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "trk_bands_not_empty max (Theta_H(s`z, vo`z - vi`z, -1), B),min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"5" (expand "add" )"5" (expand "insert" )"5" (expand "empty_seq" ) (("5" (assert ) nil nil )) nil ))nil ))nil )"6" (expand "add" )"6" (expand "empty_seq" )"6" (expand "insert" ) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil definitions_3D nil )"bool" reals nil )nil bands_2D 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" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )"posreal" bands_3D nil )"{x: posreal | x > gsmin}" bands_3D nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"posreal" bands_3D nil )"real" vertical nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" ))nil 3482239733"" (skeep)"" (lemma "trk_bands_3D_not_empty" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil bands_3D nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil ))nil ))"" 3504805750"" (skeep)"" (name "trkbb" "trk_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(2*pi,trkbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "trkbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "trkbb`length-1" )"1" (assert )"1" (expand "trk_fseq?" )"1" (inst - "trkbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "trkbb" )"2" (expand "trk_bands_3D" )"2" (lift-if)"2" (ground)"1" "trk_bands_critical[D,B,T,gsmin,gsmax]" )"1" (inst?)"1" (assert )"1" "1" "1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" assert )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"5" (expand "member" )"5" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"posreal" nil )"int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"posint" nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" vertical nil )"posreal" bands_3D nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil bands_2D nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )"nat" floor_ceil nil )"nnreal" nil )"nnreal_lt_2pi" to2pi "trig_fnd/" )"posreal" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"Nz_vect2" definitions_3D nil )"odd_int" integers nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" atan "trig_fnd/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" fseqs "structures/" ))nil 3482239733"" (skeep)"" (name "trkbb" "trk_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(2*pi,trkbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "trkbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "trkbb`length-1" )"1" (assert )"1" (expand "trk_fseq?" )"1" (inst - "trkbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "trkbb" )"2" (expand "trk_bands_3D" )"2" (lift-if)"2" (ground)"1" "trk_bands_critical[D,B,T,gsmin,gsmax]" )"1" (inst?)"1" (assert )"1" "1" "1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"5" (expand "member" )"5" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )"bool" fseqs_aux_2D nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil fseqs "structures/" )nil fseqs "structures/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"fseq" fseqs_ops "structures/" )"fseq" fseqs_ops "structures/" )nil fsq "structures/" )"fsq" fseqs "structures/" )"real" vertical nil )nil sign "reals/" )nil bands_2D nil )"nnreal_lt_2pi" to2pi "trig_fnd/" )nil vectors_2D "vectors/" )"Nz_vect2" definitions_3D nil )"posreal" atan "trig_fnd/" )"bool" fseqs "structures/" ))nil 3482241439"" (skeep)"" (name "trkbb" "trk_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(0,trkbb)" )"1" (typepred "trkbb" )"1" (expand "increasing?" )"1" (expand "member" )"1" (skosimp*)"1" (inst - "0" "i!1" )"1" (assert )"1" (expand "trk_fseq?" )"1" (inst - "0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "trkbb" )"2" (expand "trk_bands_3D" )"2" (lift-if)"2" (ground)"1" "trk_bands_critical[D, B, T, gsmin, gsmax]" )"1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"3" (expand "member" )"3" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "trk_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert )"1" "1" expand "to2pi" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"5" (expand "member" )"5" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vertical nil )"posreal" bands_3D nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil bands_2D nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )"nat" floor_ceil nil )"nnreal_lt_2pi" to2pi "trig_fnd/" )"real" reals nil )"nnreal" nil )"nnreal" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"posreal" atan "trig_fnd/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Nz_vect2" definitions_3D nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs "structures/" ))nil 3481653604"" (skeep)"" (expand "gs_bands_3D" )"" (lift-if)"" (ground)"1" (lemma "gs_bands_not_empty[D, B, T, gsmin, gsmax]" )"1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"2" "gs_bands_not_empty max (Theta_H(s`z, vo`z - vi`z, -1), B),min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"3" (expand "add" )"3" (expand "insert" )"3" (expand "empty_seq" ) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" "gs_bands_not_empty max (Theta_H(s`z, vo`z - vi`z, -1), B),min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"5" (expand "empty_seq" )"5" (expand "add" )"5" (expand "insert" ) (("5" (assert ) nil nil )) nil ))nil ))nil )"6" (expand "empty_seq" )"6" (expand "add" )"6" (expand "insert" ) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"odd_int" integers nil )"Nz_vect2" definitions_3D nil )nil vectors_2D_def "vectors/" )nil vectors_3D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil definitions_3D nil )"bool" reals nil )nil bands_2D 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" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )"posreal" bands_3D nil )"{x: posreal | x > gsmin}" bands_3D nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"posreal" bands_3D nil )"real" vertical nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" ))nil 3482240281"" (skeep)"" (lemma "gs_bands_3D_not_empty" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil bands_3D nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil ))nil ))"" 3504805883"" (skeep)"" (name "gsbb" "gs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(gsmax,gsbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "gsbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "gsbb`length-1" )"1" (assert )"1" (expand "gs_fseq?" )"1" (inst - "gsbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "gsbb" )"2" (expand "gs_bands_3D" )"2" (lift-if)"2" (ground)"1" "gs_bands_critical[D,B,T,gsmin,gsmax]" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "4" (inst?) (("4" (assert ) nil nil )) nil ))nil )"5" (expand "member" )"5" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"int" integers nil )"{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" vertical nil )"posreal" bands_3D nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil bands_2D nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"Nz_vect2" definitions_3D nil )"odd_int" integers nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs "structures/" ))nil 3482240330"" (skeep)"" (name "gsbb" "gs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(gsmax,gsbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "gsbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "gsbb`length-1" )"1" (assert )"1" (expand "gs_fseq?" )"1" (inst - "gsbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "gsbb" )"2" (expand "gs_bands_3D" )"2" (lift-if)"2" (ground)"1" "gs_bands_critical[D,B,T,gsmin,gsmax]" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "4" (inst?) (("4" (assert ) nil nil )) nil ))nil )"5" (expand "member" )"5" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sort_fseq "structures/" )"bool" fseqs_aux_2D nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil fseqs "structures/" )nil fseqs "structures/" )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )"real" vertical nil )nil sign "reals/" )nil bands_2D nil )nil vectors_2D "vectors/" )"Nz_vect2" definitions_3D nil )"bool" fseqs "structures/" ))nil ))nil 3482241931"" (skeep)"" (name "gsbb" "gs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(gsmin,gsbb)" )"1" (typepred "gsbb" )"1" (expand "increasing?" )"1" (expand "member" )"1" (skosimp*)"1" (inst - "0" "i!1" )"1" (assert )"1" (expand "gs_fseq?" )"1" (inst - "0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "gsbb" )"2" (expand "gs_bands_3D" )"2" (lift-if)"2" (ground)"1" "gs_bands_critical[D, B, T, gsmin, gsmax]" )"1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"3" (expand "member" )"3" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "gs_bands_critical[D, max(Theta_H(s`z, vo`z - vi`z, -1), B), min (Theta_H(s`z, vo`z - vi`z, 1), T), gsmin, gsmax]") "1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"5" (expand "member" )"5" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "member" )"6" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"{fs: (gs_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vertical nil )"posreal" bands_3D nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil bands_2D nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"Nz_vect2" definitions_3D nil )"odd_int" integers nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs "structures/" ))nil ))nil 3481653846"" (skeep)"" (expand "vs_bands_3D" )"" (lift-if)"" (ground)"1" (lemma "vs_bands_not_empty[H, B, T, vsmin, vsmax]" )"1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"2" "vs_bands_not_empty max (Theta_D(vect2(s), vect2(vo - vi), -1), B),min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin, vsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"3" (expand "empty_seq" )"3" (expand "add" )"3" (expand "insert" ) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (expand "empty_seq" )"4" (expand "add" )"4" (expand "insert" ) (("4" (assert ) nil nil )) nil ))nil ))nil )"5" "vs_bands_not_empty max (Theta_D(vect2(s), vect2(vo - vi), -1), B),min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin, vsmax]") "1" (inst?) nil nil ) ("2" (assert ) nil nil )) nil )"6" (expand "empty_seq" )"6" (expand "add" )"6" (expand "insert" ) (("6" (assert ) nil nil )) nil ))nil ))nil )"7" (expand "empty_seq" )"7" (expand "add" )"7" (expand "insert" ) (("7" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"odd_int" integers nil )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"bool" reals nil )nil bands_1D 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" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )"real" bands_3D nil )"{x: real | x > vsmin}" bands_3D nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil vectors_2D "vectors/" )"posreal" bands_3D nil )"real" horizontal nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"real" horizontal nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"fseq" fseqs_ops "structures/" )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" ))nil 3482240478"" (skeep)"" (lemma "vs_bands_3D_not_empty" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil bands_3D nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil ))nil ))"" 3504805998"" (skeep)"" (name "vsbb" "vs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(vsmax,vsbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "vsbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "vsbb`length-1" )"1" (assert )"1" (expand "vs_fseq?" )"1" (inst - "vsbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "vsbb" )"2" (expand "vs_bands_3D" )"2" (lift-if)"2" (ground)"1" "vs_bands_critical[H,B,T,vsmin,vsmax]" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "member" )"4" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"5" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "5" (inst?) (("5" (assert ) nil nil )) nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "member" )"7" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_vertical nil )"{x: real | x > vsmin}" bands_3D nil )"bool" reals nil )"real" bands_3D nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"int" integers nil )"{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" horizontal nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"real" horizontal nil )"posreal" bands_3D nil )nil vectors_2D "vectors/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil bands_1D nil )nil real_types nil )nil real_types nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs "structures/" ))nil 3482240492"" (skeep)"" (name "vsbb" "vs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(vsmax,vsbb)" )"1" (expand "member" )"1" (skosimp*)"1" (typepred "vsbb" )"1" (expand "increasing?" )"1" (inst - "i!1" "vsbb`length-1" )"1" (assert )"1" (expand "vs_fseq?" )"1" (inst - "vsbb`length-1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "vsbb" )"2" (expand "vs_bands_3D" )"2" (lift-if)"2" (ground)"1" "vs_bands_critical[H,B,T,vsmin,vsmax]" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (expand "member" )"3" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "member" )"4" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"5" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "5" (inst?) (("5" (assert ) nil nil )) nil ))nil )"6" (expand "member" )"6" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "member" )"7" (inst + "1" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" fseqs "structures/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )nil bands_1D nil )nil vectors_2D "vectors/" )"real" horizontal nil )nil sign "reals/" )"real" horizontal nil )nil vectors_3D "vectors/" )"fseq" fseqs_ops "structures/" )nil fsq "structures/" )"fsq" fseqs "structures/" )"fseq" fseqs_ops "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )nil vectors_3D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"Vect2" vect_3D_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil definitions_3D nil )"bool" fseqs_aux_vertical nil )"bool" sort_fseq "structures/" ))nil ))nil 3482242090"" (skeep)"" (name "vsbb" "vs_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (case "member(vsmin,vsbb)" )"1" (typepred "vsbb" )"1" (expand "increasing?" )"1" (expand "member" )"1" (skosimp*)"1" (inst - "0" "i!1" )"1" (assert )"1" (expand "vs_fseq?" )"1" (inst - "0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (expand "vsbb" )"2" (expand "vs_bands_3D" )"2" (lift-if)"2" (ground)"1" "vs_bands_critical[H, B, T, vsmin, vsmax]" )"1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"3" (expand "member" )"3" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "member" )"4" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"5" "vs_bands_critical[H, max(Theta_D(vect2(s), vect2(vo - vi), -1), B), min (Theta_D(vect2(s), vect2(vo - vi), 1), T), vsmin,") "1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"6" (expand "member" )"6" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "member" )"7" (inst + "0" )"1" (expand "add" )"1" expand "insert" )"1" expand "empty_seq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_vertical nil )"{x: real | x > vsmin}" bands_3D nil )"bool" reals nil )"real" bands_3D nil )nil booleans nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil fseqs "structures/" )nil fseqs "structures/" )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 )"{fs: (vs_fseq?[vsmin, vsmax]) | increasing?(fs)}" bands_3D nil )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Vector" vectors_3D "vectors/" )nil vectors_3D "vectors/" )"real" horizontal nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"real" horizontal nil )"posreal" bands_3D nil )nil vectors_2D "vectors/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )nil bands_1D nil )nil real_types nil )nil real_types nil )"posreal" bands_3D nil )nil real_types nil )"nnreal" bands_3D nil )"{x: posreal | x > B}" bands_3D nil )AND const-decl "[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" fseqs "structures/" ))nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil nil ))nil 3477656172 ("" (subtype-tcc) nil nil )nil nil ))nil 3477656172 ("" (subtype-tcc) nil nil ) nil nil ))nil 3477656172 ("" (subtype-tcc) nil nil ) nil nil ))nil 3477656172 ("" (subtype-tcc) nil nil ) nil nil ))nil 3477656172 ("" (subtype-tcc) nil nil ) nil nil ))"" 3504809305"" (skeep)"" (case "vo`z = vi`z and abs(s`z)<H" )"1" (flatten)"1" case "trk_bands_3D(s,vo,vi) = trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, B, T, gsmin, gsmax] ") "1" (case "mp >= 0" )"1" (expand "red_trk_band_3D?" )"1" (replace -2)"1" (rewrite "cd3d_rewrite" )"1" (expand "Vtrk_3D" 1 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 1 1)"1" "trk_red_bands[D,B,T,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace -3)"1" expand "Vtrk" -1 1)"1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" replace -1)"1" "1" "1" "1" "1" case "x!1 >=0 AND x!1 < 2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" "cd3d_rewrite" )"1" "s" "Vtrk_3D(vo,vi)(x!1)" )"1" replace "1" "1" expand "Vtrk_3D" "1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" rewrite "cd2d" "1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" expand "conflict_3D?" )"1" "1" expand "conflict_2D?" )"1" "t!1" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "Vtrk" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"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 )"2" (hide 2)"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" "i!1+1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" (expand "trk_fseq?" )"2" (expand "trk_bands_3D" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (case "vo`z /= vi`z" )"1" (flatten)"1" (expand "trk_bands_3D" :assert ? none)"1" (name "BB" "max(Theta_H(s`z,vo`z-vi`z,Entry),B)" )"1" (name "TT" "min(Theta_H(s`z,vo`z-vi`z,Exit),T)" )"1" (replace -1)"1" (replace -2)"1" (assert )"1" (case "BB<TT" )"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, BB, TT, gsmin, gsmax] ") "1" case "mp >= 0" )"1" expand "red_trk_band_3D?" )"1" replace -2)"1" rewrite "cd3d_rewrite" )"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" assert )"1" "trk_red_bands[D,BB,TT,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace "1" expand "Vtrk" "1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" "1" expand "trk2v2" "1" expand "cd2d?" )"1" replace "1" "1" "1" "1" "1" "1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd2d" )"1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" )"1" assert )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" replace "1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "x!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "omega_vv" )"2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" assert )nil nil )"2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil )"3" "3" "3" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!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 )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" (hide 3)"2" "1" "1" "1" expand "red_trk_band_3D?" )"1" "mp" "(structures@add(gsmin, structures@add(gsmax, empty_seq))`seq(1 + i!1) + ") "1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" rewrite "cd3d_rewrite" )"1" (assert ) nil nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "red_trk_band_3D?" )"2" "mp" "(structures@add(0, structures@add(2 * pi, empty_seq))`seq(1 + i!1) + ") "2" replace -1)"2" "mp" )"1" rewrite "cd3d" )nil nil )"2" expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" case "i!1 = 0" )"1" assert )"1" "gsmax" )"1" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )"2" expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"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 )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (skosimp*)"2" (split)"1" (flatten)"1" (hide 1)"1" (expand "red_trk_band_3D?" )"1" (rewrite "cd3d" :dir rl)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (expand "Vtrk_3D" -1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "trk_bands_3D(s, vo, vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" (inst - "i!1+1" )"2" (flatten)"2" (expand "red_trk_band_3D?" )"2" "mp" "(trk_bands_3D(s, vo, vi)`seq(1 + i!1) + ") "2" replace -1)"2" "mp" )"1" (rewrite "cd3d" ) nil nil )"2" "trk_bands_3D(s, vo, vi)" )"2" expand "increasing?" )"2" "i!1" "i!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{fs: (trk_fseq?) | increasing?(fs)}" nil )"{x: posreal | x > B}" bands_3D nil )"nnreal" bands_3D nil )nil real_types nil )"posreal" bands_3D nil )nil vectors_2D "vectors/" )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"Nz_vect2" definitions_3D nil )"(strict_total_order?[real])" real_props nil )nil bands_util nil )"continuous_rv_fun" nil )"Nz_vect2" bands_util nil )nil Lookahead nil )"bool" cd2d nil )"bool" cd3d nil )"real" reals nil )"continuous_rv_fun" nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" atan "trig_fnd/" )nil cd2d nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil cd3d nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil vect_3D_2D "vectors/" )"Vect2" bands_util nil )"bool" bands_2D nil )nil bands_2D nil )"real" reals nil )"Nzv2_vect3" bands_util nil )nil vectors_3D "vectors/" )"bool" definitions nil )"(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)" nil )nil cd3d nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" nil )"bool" bands_3D nil )"real" reals nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )"real" reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )"{i: subrange(0, trk_bands_3D(s, vo, vi)`length - 2) | NOT trk_bands_3D(s, vo, vi)`seq(i) =" bands_3D nil) "real" bands_3D nil )"real" vertical nil )nil sign "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integers nil )"{i: IF BB < TTNOT IF BB < TTIF BB < TT" bands_3D nil) "real" bands_3D nil )"fseq" fseqs_ops "structures/" )"posreal" nil )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"(strict_total_order?[real])" real_props nil )"Vect3" bands_3D nil )"Nzv2_vect3" bands_3D nil )"Nzv2_vect3" bands_3D nil )"{p: real | p >= Theta_H(s`z, vo`z - vi`z, -1) AND p >= B}" nil )"{p: real | p <= Theta_H(s`z, vo`z - vi`z, 1) AND p <= T}" nil )"{i: IF BB < TTNOT IF BB < TTIF BB < TT" bands_3D nil) "{x | IF BB < TTAND IF BB < TT" bands_3D nil) "posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" cd2d nil )"real" reals nil )"nnreal" nil )"real" cd2d nil )"nnreal" nil )"posreal" vectors_2D"vectors/" )"bool" cd2d nil )"(trk_only?(vo2))" bands_util nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil ))nil 3477656709"" (skeep)"" (case "vo`z = vi`z and abs(s`z)<H" )"1" (flatten)"1" case "trk_bands_3D(s,vo,vi) = trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, B, T, gsmin, gsmax] ") "1" (case "mp >= 0" )"1" (expand "red_trk_band_3D?" )"1" (replace -2)"1" (rewrite "cd3d_rewrite" )"1" (expand "Vtrk_3D" 1 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 1 1)"1" "trk_red_bands[D,B,T,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace -3)"1" expand "Vtrk" -1 1)"1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" replace -1)"1" "1" "1" "1" "1" case "x!1 >=0 AND x!1 < 2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" "cd3d_rewrite" )"1" "s" "Vtrk_3D(vo,vi)(x!1)" )"1" replace "1" "1" expand "Vtrk_3D" "1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" rewrite "cd2d" "1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" expand "conflict_3D?" )"1" "1" expand "conflict_2D?" )"1" "t!1" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "Vtrk" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"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 )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" (inst - "i!1+1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "trk_bands_3D" ) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ))nil ))nil )"2" (case "vo`z /= vi`z" )"1" (flatten)"1" (expand "trk_bands_3D" :assert ? none)"1" (name "BB" "max(Theta_H(s`z,vo`z-vi`z,Entry),B)" )"1" (name "TT" "min(Theta_H(s`z,vo`z-vi`z,Exit),T)" )"1" (replace -1)"1" (replace -2)"1" (assert )"1" (case "BB<TT" )"1" (lift-if)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, BB, TT, gsmin, gsmax] ") "1" case "mp >= 0" )"1" expand "red_trk_band_3D?" )"1" replace -2)"1" rewrite "cd3d_rewrite" )"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" assert )"1" "trk_red_bands[D,BB,TT,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace "1" expand "Vtrk" "1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" "1" expand "trk2v2" "1" expand "cd2d?" )"1" replace "1" "1" "1" "1" "1" "1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd2d" )"1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" )"1" assert )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" replace "1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "x!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "omega_vv" )"2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" assert )nil nil )"2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil )"3" "3" "3" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (lift-if)"2" (assert )"2" (skosimp*)"2" "2" "1" "1" "1" expand "red_trk_band_3D?" )"1" "mp" "(add(gsmin, add(gsmax, empty_seq))`seq(1 + i!1) + ") "1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" rewrite "cd3d_rewrite" )"1" (assert ) nil nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "red_trk_band_3D?" )"2" "mp" "(add(0, add(2 * pi, empty_seq))`seq(1 + i!1) + ") "2" replace -1)"2" "mp" )"1" rewrite "cd3d" )nil nil )"2" expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"2" case "i!1 = 0" )"1" assert )"1" "gsmax" )"1" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )"2" expand "add" )"2" expand "insert" )"2" expand "empty_seq" )"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 )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (skosimp*)"2" (split)"1" (flatten)"1" (hide 1)"1" (expand "red_trk_band_3D?" )"1" (rewrite "cd3d" :dir rl)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (expand "Vtrk_3D" -1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "trk_bands_3D(s, vo, vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" (inst - "i!1+1" )"2" (flatten)"2" (expand "red_trk_band_3D?" )"2" "mp" "(trk_bands_3D(s, vo, vi)`seq(1 + i!1) + ") "2" replace -1)"2" "mp" )"1" (rewrite "cd3d" ) nil nil )"2" "trk_bands_3D(s, vo, vi)" )"2" expand "increasing?" )"2" "i!1" "i!1+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 definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"{fs: (trk_fseq?) | increasing?(fs)}" nil )nil vectors_2D "vectors/" )"bool" sort_fseq "structures/" )"bool" fseqs_aux_2D nil )nil fseqs "structures/" )nil fseqs "structures/" )"Nz_vect2" definitions_3D nil )nil bands_util nil )"continuous_rv_fun" nil )"Nz_vect2" bands_util nil )nil Lookahead nil )"bool" cd2d nil )"bool" cd3d nil )"continuous_rv_fun" nil )"posreal" atan "trig_fnd/" )nil cd2d nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil cd3d nil )nil vect_3D_2D "vectors/" )"Vect2" bands_util nil )"bool" bands_2D nil )nil bands_2D nil )"Nzv2_vect3" bands_util nil )nil vectors_3D "vectors/" )"bool" definitions nil )"(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)" nil )nil cd3d nil )nil vectors_3D "vectors/" )"(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" nil )"real" vertical nil )nil sign "reals/" )"fseq" fseqs_ops "structures/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" cd2d nil )"real" cd2d nil )"posreal" vectors_2D"vectors/" )"bool" cd2d nil )"(trk_only?(vo2))" bands_util nil ))"" 3504810627"" (skeep)"" (case "vo`z = vi`z and abs(s`z)<H" )"1" (flatten)"1" case "trk_bands_3D(s,vo,vi) = trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, B, T, gsmin, gsmax] ") "1" (case "mp >= 0" )"1" (expand "red_trk_band_3D?" )"1" (replace -2)"1" (rewrite "cd3d_rewrite" )"1" (expand "Vtrk_3D" 1 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 1 1)"1" "trk_green_bands[D,B,T,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace -3)"1" expand "Vtrk" -1 1)"1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" replace -1)"1" "1" "1" "1" "1" "x!1" )"1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" expand "conflict_3D?" )"1" "1" expand "conflict_2D?" )"1" "t!1" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "Vtrk" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" "cd3d_rewrite" )"1" "s" "Vtrk_3D(vo,vi)(x!1)" )"1" replace "1" "1" expand "Vtrk_3D" "1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" rewrite "cd2d" "1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"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 )"2" (hide 2)"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" "i!1+1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "trk_bands_3D" ) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ))nil ))nil )"2" (case "vo`z /= vi`z" )"1" (flatten)"1" (expand "trk_bands_3D" :assert ? none)"1" (name "BB" "max(Theta_H(s`z,vo`z-vi`z,Entry),B)" )"1" (name "TT" "min(Theta_H(s`z,vo`z-vi`z,Exit),T)" )"1" (replace -1)"1" (replace -2)"1" (assert )"1" (case "BB<TT" )"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, BB, TT, gsmin, gsmax] ") "1" case "mp >= 0" )"1" expand "red_trk_band_3D?" )"1" replace -2)"1" rewrite "cd3d_rewrite" )"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" assert )"1" "trk_green_bands[D,BB,TT,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace "1" expand "Vtrk" "1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" "1" expand "trk2v2" "1" expand "cd2d?" )"1" replace "1" "1" "1" "1" "1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil )"3" expand "omega_vv" "3" expand "tau_vv" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "1" "1" "1" assert )nil nil ))nil )"2" "2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!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 )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )"1" expand "Vtrk_3D" )"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "2" assert )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "1" "i!1+1" )"1" "1" (assert ) nil nil ))nil )"2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 3)"2" (split)"1" "1" "1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" (assert ) nil nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "red_trk_band_3D?" )"2" assert )"2" "mp" "(structures@add(0, structures@add(2 * pi, empty_seq))`seq(1 + i!1) + ") "2" replace -1)"2" rewrite "cd3d_rewrite" )"2" case "Vtrk_3D(vo, vi)(mp)`z = vo`z-vi`z" )"1" (assert ) nil nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" 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 )"2" (assert )"2" (skosimp*)"2" (split)"1" (flatten)"1" (skosimp*)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (expand "Vtrk_3D" )"1" (rewrite "vz_distr_sub" )"1" (expand "trk2v3" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "red_trk_band_3D?" )"2" (hide -1)"2" (rewrite "cd3d" :dir rl)"2" (expand "conflict_3D?" )"2" (skosimp*)"2" (expand "Vtrk_3D" )"2" (rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" bands_3D nil )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{fs: (trk_fseq?) | increasing?(fs)}" nil )"{x: posreal | x > B}" bands_3D nil )"nnreal" bands_3D nil )nil real_types nil )"posreal" bands_3D nil )nil vectors_2D "vectors/" )"{fs: (trk_fseq?[gsmin, gsmax]) | increasing?(fs)}" bands_3D nil )"bool" sort_fseq "structures/" )"bool" reals nil )"bool" fseqs_aux_2D nil )"{x: posreal | x > gsmin}" bands_3D nil )"posreal" bands_3D nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )"Nz_vect2" definitions_3D nil )"(strict_total_order?[real])" real_props nil )nil bands_util nil )"continuous_rv_fun" nil )"Nz_vect2" bands_util nil )nil cd2d nil ) (cd3d formula-decl nil cd3d nil )nil naturalnumbers nil )"(total_order?[real])" nil )"continuous_rv_fun" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil Lookahead nil )"bool" cd2d nil )"bool" cd3d nil )"real" reals nil )"posreal" atan "trig_fnd/" )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )nil vect_3D_2D "vectors/" )"Vect2" bands_util nil )"bool" bands_2D nil )nil bands_2D nil )"real" reals nil )"Nzv2_vect3" bands_util nil )nil vectors_3D "vectors/" )"bool" definitions nil )"(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)" nil )nil cd3d nil )nil vectors_3D "vectors/" )"Vector" vectors_3D "vectors/" )"(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" nil )"bool" bands_3D nil )"real" reals nil )"(total_order?[real])" nil )"int" integers nil )"int" integers nil )"real" reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )"real" vertical nil )nil sign "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integers nil )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"(strict_total_order?[real])" real_props nil )"Vect3" bands_3D nil )"Nzv2_vect3" bands_3D nil )"Nzv2_vect3" bands_3D nil )"{p: real | p >= Theta_H(s`z, vo`z - vi`z, -1) AND p >= B}" nil )"{p: real | p <= Theta_H(s`z, vo`z - vi`z, 1) AND p <= T}" nil )"{i: IF BB < TTNOT IF BB < TTIF BB < TT" bands_3D nil) "{x | IF BB < TTAND IF BB < TT" bands_3D nil) "posreal" sq "reals/" )"posreal" vectors_2D"vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" cd2d nil )"nnreal" nil )"real" reals nil )"real" cd2d nil )"nnreal" nil )"bool" cd2d nil )"(trk_only?(vo2))" bands_util nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil ))nil 3477738484"" (skeep)"" (case "vo`z = vi`z and abs(s`z)<H" )"1" (flatten)"1" case "trk_bands_3D(s,vo,vi) = trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"1" (replace -1)"1" (hide -1)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, B, T, gsmin, gsmax] ") "1" (case "mp >= 0" )"1" (expand "red_trk_band_3D?" )"1" (replace -2)"1" (rewrite "cd3d_rewrite" )"1" (expand "Vtrk_3D" 1 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 1 1)"1" "trk_green_bands[D,B,T,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace -3)"1" expand "Vtrk" -1 1)"1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" replace -1)"1" "1" "1" "1" "1" "x!1" )"1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" expand "conflict_3D?" )"1" "1" expand "conflict_2D?" )"1" "t!1" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "Vtrk" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" "cd3d_rewrite" )"1" "s" "Vtrk_3D(vo,vi)(x!1)" )"1" replace "1" "1" expand "Vtrk_3D" "1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" rewrite "cd2d" "1" expand "Vtrk" )"1" expand "Vtrk_3D" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"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 )"2" "trk_bands[D,B,T,gsmin,gsmax](s,vo,vi)" )"2" (expand "trk_fseq?" )"2" (inst-cp - "i!1" )"2" (inst - "i!1+1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "trk_bands_3D" ) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ))nil ))nil )"2" (case "vo`z /= vi`z" )"1" (flatten)"1" (expand "trk_bands_3D" :assert ? none)"1" (name "BB" "max(Theta_H(s`z,vo`z-vi`z,Entry),B)" )"1" (name "TT" "min(Theta_H(s`z,vo`z-vi`z,Exit),T)" )"1" (replace -1)"1" (replace -2)"1" (assert )"1" (case "BB<TT" )"1" (lift-if)"1" (assert )"1" (skosimp*)"1" "mp" "(trk_bands[D, BB, TT, gsmin, gsmax] ") "1" case "mp >= 0" )"1" expand "red_trk_band_3D?" )"1" replace -2)"1" rewrite "cd3d_rewrite" )"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" 2 1)"1" expand "Vtrk_3D" 2 1)"1" rewrite "vz_distr_sub" )"1" expand "trk2v3" "1" case "Vtrk_3D(vo,vi)(mp)`z = vo`z-vi`z" )"1" assert )"1" "trk_green_bands[D,BB,TT,gsmin,gsmax]" )"1" "s" "vi" "vo" )"1" assert )"1" "i!1" )"1" expand "red_trk_band?" )"1" replace "1" expand "Vtrk" "1" expand "Vtrk_3D" "1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v2" "1" expand "trk2v2" "1" expand "cd2d?" )"1" replace "1" "1" "1" "1" "1" case "x!1 >= 0 AND x!1 <2*pi" )"1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil )"3" expand "omega_vv" "3" expand "tau_vv" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "1" "1" "1" assert )nil nil ))nil )"2" "2" expand "omega_vv" "2" expand "tau_vv" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x!1 >= 0 AND x!1 <2*pi" )"1" "1" "x!1" )"1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" rewrite "cd2d" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" expand "cd2d?" )"1" expand "Vtrk_3D" )"1" expand "Vtrk" )"1" rewrite "vz_distr_sub" )"1" rewrite "vect2_sub" )"1" rewrite "vect2_trk2v3" )"1" expand "trk2v3" )"1" expand "trk2v2" )"1" "1" assert )"1" expand "omega_vv" )"1" expand "tau_vv" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "i!1+1" )"1" "1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"2" "i!1+1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk_bands[D,BB,TT,gsmin,gsmax](s,vo,vi)" )"2" expand "trk_fseq?" )"2" "i!1" )"1" "1" "i!1+1" )"1" "1" (assert ) nil nil ))nil )"2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 3)"2" (split)"1" "1" "1" rewrite "cd3d" )"1" rewrite "cd3d_rewrite" )"1" case "Vtrk_3D(vo, vi)(x!1)`z = vo`z-vi`z" )"1" (assert ) nil nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "red_trk_band_3D?" )"2" assert )"2" "mp" "(add(0, add(2 * pi, empty_seq))`seq(1 + i!1) + ") "2" replace -1)"2" rewrite "cd3d_rewrite" )"2" case "Vtrk_3D(vo, vi)(mp)`z = vo`z-vi`z" )"1" (assert ) nil nil )"2" expand "Vtrk_3D" )"2" rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" 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 )"2" (assert )"2" (skosimp*)"2" (split)"1" (flatten)"1" (skosimp*)"1" (expand "conflict_3D?" )"1" (skosimp*)"1" (expand "Vtrk_3D" )"1" (rewrite "vz_distr_sub" )"1" (expand "trk2v3" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "red_trk_band_3D?" )"2" (hide -1)"2" (rewrite "cd3d" :dir rl)"2" (expand "conflict_3D?" )"2" (skosimp*)"2" (expand "Vtrk_3D" )"2" (rewrite "vz_distr_sub" )"2" expand "trk2v3" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil definitions_3D nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_3D_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil vectors_3D_def "vectors/" )"{fs: (trk_fseq?) | increasing?(fs)}" nil )nil vectors_2D "vectors/" )"bool" sort_fseq "structures/" )"bool" fseqs_aux_2D nil )nil fseqs "structures/" )nil fseqs "structures/" )"Nz_vect2" definitions_3D nil )nil bands_util nil )"continuous_rv_fun" nil )"Nz_vect2" bands_util nil )nil cd2d nil ) (cd3d formula-decl nil cd3d nil )"continuous_rv_fun" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil Lookahead nil )"bool" cd2d nil )"bool" cd3d nil )"posreal" atan "trig_fnd/" )nil vect_3D_2D "vectors/" )"Vect2" bands_util nil )"bool" bands_2D nil )nil bands_2D nil )"Nzv2_vect3" bands_util nil )nil vectors_3D "vectors/" )"bool" definitions nil )"(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)" nil )nil cd3d nil )nil vectors_3D "vectors/" )"(LAMBDA (vo2): (vo3 - vi3)`z = vo2`z)" nil )"real" vertical nil )nil sign "reals/" )"fsq" fseqs "structures/" )nil fsq "structures/" )"fseq" fseqs_ops "structures/" )"posreal" sq "reals/" )"posreal" vectors_2D"vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" cd2d nil )"real" cd2d nil )"bool" cd2d nil )"(trk_only?(vo2))" bands_util nil ))nil ))nil 3482238747"" (subtype-tcc) nil nil )"real" integral_def "analysis/" )"real" atan "trig_fnd/" )"posreal" atan "trig_fnd/" ))nil ))nil 3482238747"" (skeep)"" (name "trkbb" "trk_bands_3D(s, vo, vi)" )"" (replace -1)"" (assert )"" (skeep)"" "mmax" "finite_sets@finite_sets_minmax[naturalnumbers.nat,restrict[[real, real], [nat, nat], boolean].restrict(reals.<=)].max" )"" "ii" "mmax({ij: nat | ij<=trkbb`length-1 AND trkbb`seq(ij) < x})" )"1" (case "ii <= trkbb`length-2" )"1" case "trkbb`seq(ii) < x AND y < trkbb`seq(ii+1)" )"1" (flatten)"1" case "(conflict_3D?(s, Vtrk_3D(vo, vi)(x)) OR ") "1" case "red_trk_band_3D?(s,vo,vi,trkbb)(ii)" )"1" (lemma "trk_red_bands_3D" )"1" (inst - "s" "vi" "vo" )"1" replace -9)"1" assert )"1" "ii" )"1" assert )"1" "1" assert )"1" (inst - "y" ) nil nil ))nil )"2" assert )"2" (inst - "x" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "trk_green_bands_3D" )
Messung V0.5 C=100 H=100 G=100
¤ Dauer der Verarbeitung: 1.159 Sekunden
¤ *© Formatika GbR, Deutschland
2026-04-08
