|
(vs_circle
(vs_circle_TCC1 0
(vs_circle_TCC1-2 nil 3451136094
("" (skeep) (("" (expand "vs_only?") (("" (assert) nil nil)) nil))
nil)
((vs_only? const-decl "bool" definitions_3D nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(vect2_eq formula-decl nil vect_3D_2D "vectors/"))
nil)
(vs_circle_TCC1-1 nil 3451065822
("" (skosimp :preds? t)
(("" (assert)
(("" (lemma "horizontal_conflict")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(horizontal_conflict formula-decl nil horizontal nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(horizontal_conflict? const-decl "bool" horizontal nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(Sign type-eq-decl nil sign "reals/"))
nil))
(vs_circle_TCC2 0
(vs_circle_TCC2-2 nil 3451136002
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (lemma "Delta_gt_0_nzv")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(D formal-const-decl "posreal" vs_circle 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)
(Delta_gt_0_nzv formula-decl nil horizontal nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/"))
nil)
(vs_circle_TCC2-1 nil 3451065822
("" (skosimp :preds? t) (("" (assert) nil nil)) nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(horizontal_conflict? const-decl "bool" horizontal nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/")
(Sign type-eq-decl nil sign "reals/"))
nil))
(vs_circle_TCC3 0
(vs_circle_TCC3-2 nil 3466271730
("" (skeep)
(("" (skeep 2)
(("" (expand "vs_only?") (("" (assert) nil nil)) nil)) nil))
nil)
((vect2_eq formula-decl nil vect_3D_2D "vectors/")
(nzv2 application-judgement "Nz_vect2" definitions_3D nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vs_only? const-decl "bool" definitions_3D nil))
nil)
(vs_circle_TCC3-1 nil 3466260271
("" (skeep)
(("" (lemma "Theta_D_exit_gt_0")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil)
((Theta_D_exit_gt_0 formula-decl nil horizontal nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vector type-eq-decl nil vectors_3D "vectors/"))
nil))
(vs_circle_TCC4 0
(vs_circle_TCC4-1 nil 3466260271
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/"))
nil))
(vs_circle_TCC5 0
(vs_circle_TCC5-1 nil 3466260271
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vect2_zero formula-decl nil vect_3D_2D "vectors/"))
nil))
(vs_circle_meets_vertical_criterion 0
(vs_circle_meets_vertical_criterion-1 nil 3471192910
("" (skeep)
(("" (expand "vs_circle?")
(("" (flatten)
(("" (expand "vs_circle")
(("" (lift-if)
(("" (split -)
(("1" (flatten)
(("1" (expand "vertical_criterion?")
(("1" (flatten)
(("1" (hide 3)
(("1" (assert)
(("1" (rewrite "vect2_sub")
(("1" (rewrite "vz_distr_sub")
(("1" (replace -1)
(("1"
(expand "horizontal_conflict?")
(("1"
(skosimp*)
(("1"
(replace -3)
(("1"
(assert)
(("1"
(typepred "sp")
(("1"
(assert)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "vertical_criterion?")
(("2" (flatten)
(("2" (split -1)
(("1" (flatten)
(("1" (split -)
(("1" (flatten)
(("1" (assert)
(("1"
(lemma "Delta_gt_0_nzv")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 1)
(("1"
(hide 2)
(("1"
(flatten)
(("1"
(name-replace
"vso"
"vs_only(sp, vect2(vo - vi), Theta_D(vect2(sp), vect2(vo - vi), 1),
eps)"
:hide?
nil)
(("1"
(label "vsoname" -1)
(("1"
(name
"ddir"
"IF abs(sp`z) >= H THEN eps * sign(sp`z)
ELSE -1
ENDIF")
(("1"
(label "ddirname" -1)
(("1"
(case
"ddir = 1 or ddir = -1")
(("1"
(label
"ddirtp"
-1)
(("1"
(replace
"ddirname")
(("1"
(lift-if)
(("1"
(replaces
-5)
(("1"
(expand
"closed_region_3D")
(("1"
(assert)
(("1"
(rewrite
"vect2_sub")
(("1"
(rewrite
"vect2_sub")
(("1"
(rewrite
"vect2_add")
(("1"
(rewrite
"vect2_scal")
(("1"
(rewrite
"vz_distr_sub")
(("1"
(case
"eps*(eps*H) = H")
(("1"
(assert)
(("1"
(name
"thetad"
"Theta_D(vect2(sp), vect2(vo) - vect2(vi), ddir)")
(("1"
(replace
-1)
(("1"
(label
"thetadname"
-1)
(("1"
(name
"ppoint"
"vect2(sp) + thetad * vect2(vo - vi)")
(("1"
(label
"ppointname"
-1)
(("1"
(replace
-1)
(("1"
(case
"sqv(ppoint) = sq(D)")
(("1"
(assert)
(("1"
(case
"NOT (vect2(vo) - vect2(vi)) * ppoint = 0")
(("1"
(assert)
(("1"
(lemma
"Theta_D_line_intersection")
(("1"
(inst
-
"ddir"
"sp"
"vect2(vo)-vect2(vi)")
(("1"
(assert)
(("1"
(replace
"thetadname")
(("1"
(rewrite
"vect2_sub")
(("1"
(replace
"ppointname")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(lemma
"Theta_D_positive_conflict")
(("1"
(inst
-
"sp"
"vect2(vo)-vect2(vi)")
(("1"
(assert)
(("1"
(label
"td1pos"
-1)
(("1"
(case
"sign((vect2(vo) - vect2(vi)) * ppoint) = ddir")
(("1"
(assert)
(("1"
(expand
"vs_only")
(("1"
(lift-if)
(("1"
(split
"vsoname")
(("1"
(flatten)
(("1"
(replace
-3
:dir
rl)
(("1"
(assert)
(("1"
(hide
-3
-13)
(("1"
(split
"ddirtp")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(split
"ddirname")
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"vs_at_H")
(("1"
(hide-all-but
(-2
-3
-4))
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(split
"ddirname")
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"Theta_D_entry_gt_0")
(("1"
(inst
-
"vect2(vo)-vect2(vi)"
"sp")
(("1"
(assert)
(("1"
(lemma
"vs_at_H")
(("1"
(inst
-
"eps"
"thetad"
"sp`z")
(("1"
(mult-by
-1
"eps")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"Theta_D_entry_gt_0")
(("2"
(inst
-
"vect2(vo)-vect2(vi)"
"sp")
(("2"
(assert)
(("2"
(lemma
"vs_at_H")
(("2"
(inst
-
"eps"
"thetad"
"sp`z")
(("2"
(mult-by
-1
"eps")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split
-1)
(("1"
(flatten)
(("1"
(replace
-2
:dir
rl)
(("1"
(assert)
(("1"
(hide
-2
-12
1)
(("1"
(case-replace
"eps*sp`z = abs(sp`z)")
(("1"
(assert)
(("1"
(case
"ddir = 1")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(lemma
"vs_at_H")
(("1"
(inst?)
(("1"
(mult-by
-1
"eps")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
"ddirtp"
"ddirname"
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(typepred
"eps")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(replace
-1
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"Theta_D_horizontal_dir")
(("2"
(inst
-
"ddir"
"sp"
"vect2(vo)-vect2(vi)")
(("2"
(assert)
(("2"
(replace
"thetadname")
(("2"
(replace
"ppointname")
(("2"
(hide-all-but
(-1
"ddirtp"
1
2))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.78 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.
|
