(gs_linenil 3429885199"" (skeep)"" (typepred "gs_only_line(tangent_line(sp, eps),vo, vi)" )"" (assert ) nil nil )) nil ))nil )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"{k: real, nvo: Vect2 | AND k * v = nvo - vi}" nil )"posreal" gs_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )"bool" definitions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil reals nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil ))nil ))nil 3429885199 ("" (skosimp*) nil nil ) nil nil ))nil 3433243037"" (skeep)"" (expand "gs_line_eps?" )"" (flatten)"" (expand "gs_line_eps" :assert ? none)"" (skoletin -1 :postfix "a" )"" (lift-if)"" (split -)"1" (flatten)"1" "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 )"bool" gs_line nil )"{nvo | nvo /= zero => gs_only?(vo)(nvo)}" nil )"bool" tangent_line nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Nz_vect2" tangent_line nil )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"{k: real, nvo: Vect2 | AND k * v = nvo - vi}" nil )"posreal" gs_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" definitions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"[bool, bool -> bool]" booleans nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil vectors_2D_def "vectors/" )nil reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"[bool, bool -> bool]" booleans nil ))nil ))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 )nil gs_line nil )"Vector" vectors_2D "vectors/" )nil tangent_line nil )nil horizontal nil )"posreal" gs_line nil )nil real_types nil )"bool" reals nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"bool" reals nil )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3443974345"" (skeep)"" (skeep -2)"" (rewrite "tangent_line_solution" :dir rl)"" (expand "tangent_line?" )"" (skeep -2)"" (lemma "gs_only_line_complete" )"" "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" "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 )"bool" tangent_line nil )nil gs_only nil )"bool" gs_line nil )"{k: real, nvo: Vect2 | AND k * v = nvo - vi}" nil )"Vector" vectors_2D "vectors/" )"bool" definitions nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{nvo | nvo /= zero => gs_only?(vo)(nvo)}" nil )"bool" gs_line nil )"bool" gs_only nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Nz_vect2" tangent_line nil )"posreal" gs_line nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil tangent_line nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
