products/sources/formale Sprachen/PVS/ACCoRD image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bands_util.prf   Sprache: Lisp

Original von: PVS©

(bands_util
 (trk2v2_TCC1 0
  (trk2v2_TCC1-1 nil 3482508871
   ("" (skeep)
    (("" (expand "trk_only?")
      (("" (expand "trkgs2vect")
        (("" (expand "norm")
          (("" (expand "sqv")
            (("" (expand "*")
              (("" (lemma cos_minus)
                (("" (inst?)
                  (("" (assert)
                    (("" (lemma cos_0)
                      (("" (replace -2) (("" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trk_only? const-decl "bool" definitions nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (cos_0 formula-decl nil trig_basic "trig_fnd/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (cos_minus formula-decl nil trig_basic "trig_fnd/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (trkgs2vect const-decl "Nz_vect2" track nil))
   nil))
 (trk2v2_Nzv 0
  (trk2v2_Nzv-1 nil 3482508871
   ("" (skeep)
    (("" (typepred "trk2v2(vo2)(trk)")
      (("" (expand "trk_only?")
        (("" (typepred vo2)
          (("" (flatten)
            (("" (replaces -2) (("" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (trk_only? const-decl "bool" definitions nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/"))
   nil))
 (gs2v2_gs_only 0
  (gs2v2_gs_only-1 nil 3482667397
   ("" (skeep)
    (("" (expand "gs_only?")
      (("" (inst 1 "gsp/norm(vo2)")
        (("" (assert)
          (("" (expand "gs2v2")
            (("" (expand "^") (("" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((gs_only? const-decl "bool" definitions nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (scal_assoc formula-decl nil vectors_2D "vectors/")
    (gs2v2 const-decl "Vect2" bands_util nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (gs2v2_id 0
  (gs2v2_id-1 nil 3482667524
   ("" (skeep)
    (("" (expand "gs_only?")
      (("" (skosimp*)
        (("" (replace -1)
          (("" (expand "gs")
            (("" (rewrite "norm_scal")
              (("" (expand "abs")
                (("" (expand "gs2v2")
                  (("" (expand "^") (("" (assertnil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gs_only? const-decl "bool" definitions nil)
    (norm_scal formula-decl nil vectors_2D "vectors/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (gs2v2 const-decl "Vect2" bands_util nil)
    (scal_assoc formula-decl nil vectors_2D "vectors/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (gs const-decl "nnreal" definitions nil))
   shostak))
 (trk2v3_TCC1 0
  (trk2v3_TCC1-1 nil 3482508871
   ("" (skeep)
    (("" (expand "trkgs2vect")
      (("" (expand "trk_only?")
        (("" (expand "vect2")
          (("" (expand "norm")
            (("" (expand "sqv")
              (("" (expand "*")
                (("" (lemma cos_minus)
                  (("" (inst?)
                    (("" (assert)
                      (("" (lemma cos_0) (("" (assertnil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trkgs2vect const-decl "Nz_vect2" track nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (cos_minus formula-decl nil trig_basic "trig_fnd/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_0 formula-decl nil trig_basic "trig_fnd/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (* const-decl "real" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (trk_only? const-decl "bool" definitions nil))
   nil))
 (vect2_trk2v3 0
  (vect2_trk2v3-1 nil 3482509069
   ("" (skeep)
    (("" (expand "trk2v3")
      (("" (expand "trk2v2") (("" (assertnil nil)) nil)) nil))
    nil)
   ((trk2v3 const-decl
     "(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)"
     bands_util nil)
    (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (trk2v2 const-decl "(trk_only?(vo2))" bands_util nil))
   shostak))
 (trk2v3_Nzv 0
  (trk2v3_Nzv-1 nil 3482508871
   ("" (skeep)
    (("" (typepred "trk2v3(vo3)(trk)")
      (("" (expand "trk_only?")
        (("" (replace -3) (("" (assertnil nil)) nil)) nil))
      nil))
    nil)
   ((trk2v3 const-decl
     "(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)"
     bands_util nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (trk_only? const-decl "bool" definitions nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (norm_zero formula-decl nil vectors_2D "vectors/"))
   nil))
 (Vtrk_3D_TCC1 0
  (Vtrk_3D_TCC1-1 nil 3482508871 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vector" vectors_3D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan "trig_fnd/")
    (pi const-decl "posreal" atan "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (trkgs2vect const-decl "Nz_vect2" track nil)
    (trk2v3 const-decl
     "(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)"
     bands_util nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (trk2v3_trk2v3 0
  (trk2v3_trk2v3-1 nil 3482509245
   ("" (skeep)
    (("" (expand "trk2v3")
      (("" (expand "trkgs2vect")
        (("" (expand "vect2")
          (("" (expand "norm")
            (("" (expand "sqv")
              (("" (expand "*")
                (("" (lemma sq_sqrt)
                  (("" (inst - "vo3`x*vo3`x+vo3`y*vo3`y")
                    (("" (expand "sq")
                      (("" (assert)
                        ((""
                          (name z
                                "sqrt(vo3`x * vo3`x + vo3`y * vo3`y)")
                          (("" (replace -1)
                            (("" (lemma cos_minus)
                              ((""
                                (inst - trk trk)
                                ((""
                                  (assert)
                                  ((""
                                    (lemma cos_0)
                                    ((""
                                      (replace -1)
                                      (("" (assertnil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trk2v3 const-decl
     "(LAMBDA (vo2): trk_only?(vect2(vo3))(vect2(vo2)) AND vo3`z = vo2`z)"
     bands_util nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_minus formula-decl nil trig_basic "trig_fnd/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_0 formula-decl nil trig_basic "trig_fnd/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (trkgs2vect const-decl "Nz_vect2" track nil))
   shostak))
 (trk2v3_0 0
  (trk2v3_0-1 nil 3482509446
   ("" (skeep)
    (("" (lemma vect2_trk2v3)
      (("" (inst?)
        (("" (replace -1)
          (("" (hide -1)
            (("" (expand "trk2v2") (("" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((vect2_trk2v3 formula-decl nil bands_util nil)
    (trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (gs2v3_gs_only 0
  (gs2v3_gs_only-1 nil 3482667397
   ("" (skeep)
    (("" (expand "gs2v3")
      (("" (expand "gs2v2")
        (("" (expand "^")
          (("" (expand "gs_only?")
            (("" (inst + "gsp/norm(vect2(vo3))")
              (("" (assertnil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gs2v3 const-decl "Vect3" bands_util nil)
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nzv2_vect3 type-eq-decl nil definitions_3D nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/")
    (scal_assoc formula-decl nil vectors_2D "vectors/")
    (gs_only? const-decl "bool" definitions nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (gs2v2 const-decl "Vect2" bands_util nil))
   nil))
 (vect2_gs2v3 0
  (vect2_gs2v3-1 nil 3482667789
   ("" (skeep) (("" (expand "gs2v3") (("" (assertnil nil)) nil)) nil)
   ((gs2v3 const-decl "Vect3" bands_util nil)
    (gs2v2_gs_only application-judgement "(gs_only?(vo2))" bands_util
     nil)
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (vect2_eq_ext formula-decl nil vect_3D_2D "vectors/"))
   shostak))
 (Vgs_3D_TCC1 0
  (Vgs_3D_TCC1-1 nil 3482667397 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vector" vectors_3D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (gs2v2 const-decl "Vect2" bands_util nil)
    (gs2v3 const-decl "Vect3" bands_util nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (vs2v3_TCC1 0
  (vs2v3_TCC1-1 nil 3482678849 ("" (subtype-tcc) nil nil)
   ((vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (vs_only? const-decl "bool" definitions_3D nil))
   nil))
 (vect2_vs2v3 0
  (vect2_vs2v3-1 nil 3482678896
   ("" (skeep) (("" (expand "vs2v3") (("" (assertnil nil)) nil)) nil)
   ((vs2v3 const-decl "(vs_only?(vo3))" bands_util nil)
    (nzv2 application-judgement "Nz_vect2" definitions_3D nil)
    (vect2_eq formula-decl nil vect_3D_2D "vectors/"))
   shostak))
 (Vs_TCC1 0
  (Vs_TCC1-1 nil 3482678849 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vector" vectors_3D "vectors/")
    (vs2v3 const-decl "(vs_only?(vo3))" bands_util nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (vs_only? const-decl "bool" definitions_3D nil))
   nil)))


¤ Dauer der Verarbeitung: 0.25 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff