(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) (("" (assert) nil 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) (("" (assert) nil 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 "^") (("" (assert) nil 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 "^") (("" (assert) nil 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) (("" (assert) nil 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") (("" (assert) 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_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) (("" (assert) 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)
(= 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)
(("" (assert) nil 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") (("" (assert) nil 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))")
(("" (assert) nil 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") (("" (assert) nil 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") (("" (assert) nil 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)
¤
|
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.
|