| products/sources/formale sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: gs_line.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(gs_line
(gs_line_eps_TCC1 0 (gs_line_eps_TCC1-1 nil 3429885199 ("" (skeep) (("" (typepred "gs_only_line(tangent_line(sp, eps),vo, vi)") (("" (assert) nil nil)) nil)) nil) ((tangent_line const-decl "Nz_vect2" tangent_line nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (Sp_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only nil) (D formal-const-decl "posreal" gs_line 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) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (gs_only? const-decl "bool" definitions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (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) (Vect2 type-eq-decl nil vectors_2D_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (gs_line_eps_TCC2 0 (gs_line_eps_TCC2-1 nil 3429885199 ("" (skosimp*) nil nil) nil nil)) (gs_line_eps_tangent_line 0 (gs_line_eps_tangent_line-1 nil 3433243037 ("" (skeep) (("" (expand "gs_line_eps?") (("" (flatten) (("" (expand "gs_line_eps" :assert? none) (("" (skoletin -1 :postfix "a") (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (typepred "gs_only_line(tangent_line(sp, eps),vo, vi)") (("1" (replaces (-4 -5) :dir rl) (("1" (assert) (("1" (flatten) (("1" (expand "tangent_line?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_line_eps? const-decl "bool" gs_line nil) (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_line nil) (tangent_line? const-decl "bool" tangent_line nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (tangent_line const-decl "Nz_vect2" tangent_line nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (Sp_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only nil) (D formal-const-decl "posreal" gs_line 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) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (gs_only? const-decl "bool" definitions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil)) nil)) (gs_line_is_line_solution 0 (gs_line_is_line_solution-1 nil 3471194277 ("" (skeep) (("" (lemma "gs_line_eps_tangent_line") (("" (inst?) (("" (assert) (("" (lemma "tangent_line_solution") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gs_line_eps_tangent_line formula-decl nil gs_line nil) (- const-decl "Vector" vectors_2D "vectors/") (tangent_line_solution formula-decl nil tangent_line nil) (Sp_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" gs_line nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_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) (bool nonempty-type-eq-decl nil 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) (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)) nil)) (gs_line_complete 0 (gs_line_complete-1 nil 3443974345 ("" (skeep) (("" (skeep -2) (("" (rewrite "tangent_line_solution" :dir rl) (("" (expand "tangent_line?") (("" (skeep -2) (("" (lemma "gs_only_line_complete") (("" (inst -1 "nnk" "nvo" "tangent_line(sp,eps)" "vi" "vo") (("" (assert) (("" (expand "gs_only_line?") (("" (split -1) (("1" (flatten) (("1" (expand "gs_line?") (("1" (assert) (("1" (inst 3 "eps") (("1" (expand "gs_line_eps") (("1" (decompose-equality -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "two_parallel?") (("2" (assert) (("2" (inst 1 "eps") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tangent_line? const-decl "bool" tangent_line nil) (gs_only_line_complete formula-decl nil gs_only nil) (gs_line? const-decl "bool" gs_line nil) (gs_only_line const-decl "{k: real, nvo: Vect2 | nvo /= zero => gs_only?(vo)(nvo) AND k * v = nvo - vi}" gs_only nil) (* const-decl "Vector" vectors_2D "vectors/") (gs_only? const-decl "bool" definitions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (gs_line_eps const-decl "{nvo | nvo /= zero => gs_only?(vo)(nvo)}" gs_line nil) (two_parallel? const-decl "bool" gs_line nil) (gs_only_line? const-decl "bool" gs_only nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (tangent_line const-decl "Nz_vect2" tangent_line nil) (D formal-const-decl "posreal" gs_line 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) (- const-decl "Vector" vectors_2D "vectors/") (Sp_vect2 type-eq-decl nil horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_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) (tangent_line_solution formula-decl nil tangent_line nil)) nil))) ¤ Dauer der Verarbeitung: 0.2 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.Bot Zugriff |
