|
(vertical_cr
(hor_circle_horizontal_only 0
(hor_circle_horizontal_only-1 nil 3471199310
("" (skeep)
(("" (expand "hor_circle?")
(("" (split)
(("1" (expand "gs_vertical?")
(("1" (flatten)
(("1" (typepred "gs_vertical(sp, vo, vi, epsh, epsv)")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "trk_vertical?")
(("2" (flatten)
(("2" (skeep -1)
(("2"
(typepred
"trk_vertical_irt(sp, vo, vi, epsh, epsv, irt)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("3" (expand "opt_vertical?")
(("3" (flatten)
(("3" (typepred "opt_vertical(sp, vo, vi, epsh, epsv)")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((hor_circle? const-decl "bool" vertical_cr nil)
(opt_vertical? const-decl "bool" opt_vertical nil)
(opt_vertical const-decl
"{nvo | vect2(nvo) /= zero => vo`z = nvo`z}" opt_vertical nil)
(trk_vertical? const-decl "bool" trk_circle nil)
(trk_only? const-decl "bool" definitions nil)
(trk_vertical_irt const-decl "{nvo |
vect2(nvo) /= zero =>
trk_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}"
trk_circle nil)
(gs_vertical? const-decl "bool" gs_circle nil)
(Sp_vect3 type-eq-decl nil space_3D nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(gs_vertical const-decl "{nvo |
vect2(nvo) /= zero =>
gs_only?(vect2(vo))(vect2(nvo)) AND vo`z = nvo`z}" gs_circle
nil)
(H formal-const-decl "posreal" vertical_cr nil)
(D formal-const-decl "posreal" vertical_cr 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)
(gs_only? const-decl "bool" definitions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real nonempty-type-from-decl nil reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(vertical_cr_meets_vertical_criterion 0
(vertical_cr_meets_vertical_criterion-1 nil 3471192580
("" (skeep)
(("" (expand "vertical_cr?")
(("" (split -2)
(("1" (lemma "vs_circle_meets_vertical_criterion")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "hor_circle?")
(("2" (split)
(("1" (lemma "gs_vertical_meets_vertical_criterion")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (lemma "trk_vertical_meets_vertical_criterion")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil)
("3" (lemma "opt_vertical_meets_vertical_criterion")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((vertical_cr? const-decl "bool" vertical_cr nil)
(hor_circle? const-decl "bool" vertical_cr nil)
(opt_vertical_meets_vertical_criterion formula-decl nil
opt_vertical nil)
(trk_vertical_meets_vertical_criterion formula-decl nil trk_circle
nil)
(gs_vertical_meets_vertical_criterion formula-decl nil gs_circle
nil)
(H formal-const-decl "posreal" vertical_cr nil)
(D formal-const-decl "posreal" vertical_cr 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)
(vs_circle_meets_vertical_criterion formula-decl nil vs_circle nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp_vect3 type-eq-decl nil space_3D nil)
(sq const-decl "nonneg_real" sq "reals/")
(vect2 const-decl "Vect2" vect_3D_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil))
shostak))
(hor_circle_meets_horizontal_criterion 0
(hor_circle_meets_horizontal_criterion-1 nil 3471200403
("" (skeep)
(("" (expand "hor_circle?")
(("" (split)
(("1" (lemma "gs_vertical_meets_horizontal_criterion")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (lemma "trk_vertical_meets_horizontal_criterion")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil)
("3" (lemma "opt_vertical_meets_horizontal_criterion")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((hor_circle? const-decl "bool" vertical_cr nil)
(opt_vertical_meets_horizontal_criterion formula-decl nil
opt_vertical nil)
(trk_vertical_meets_horizontal_criterion formula-decl nil
trk_circle nil)
(H formal-const-decl "posreal" vertical_cr nil)
(D formal-const-decl "posreal" vertical_cr 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)
(gs_vertical_meets_horizontal_criterion formula-decl nil gs_circle
nil)
(Nzv2_vect3 type-eq-decl nil definitions_3D nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp2_vect3 type-eq-decl nil space_3D nil)
(Sign type-eq-decl nil sign "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(sqv 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/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect3 type-eq-decl nil space_3D nil)
(sp skolem-const-decl "Sp_vect3[D, H]" vertical_cr nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/"))
nil)))
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
