(losr_iterativenil 3535802573"" (skeep)"" (expand "trk_only?" )"" (lemma "norms_eq_sqv" )"" (inst?)"" (assert )"" (hide 2)"" (rewrite "sqv_add" )"" (case-replace "nvo*perpR(nvo) = 0" )"1" (assert )"1" (rewrite "sqv_scal" )"1" (rewrite "sqv_scal" )"1" (rewrite "sqv_perpR" )"1" (lemma "sin2_cos2" )"1" (inst - "dir*step" )"1" "sqv(nvo)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" definitions nil )"nzreal" nil )nil reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_2D "vectors/" )"real" trig_basic "trig/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil vectors_2D_def "vectors/" )"real" trig_basic "trig/" )"Vect2" perpendicular_2D "vectors/" )"real" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" nil )nil perpendicular_2D "vectors/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil extra_real_props nil )nil trig_basic "trig/" )"real" reals nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" reals nil )"nnreal" nil )"real" reals nil )nil vectors_2D "vectors/" )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )nil vectors_2D "vectors/" ))nil ))nil 3535288278"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"int" integers nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(total_order?[real])" nil )"posint" nil )"nat" floor_ceil nil ))nil ))nil 3535288278"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" nil )"(total_order?[real])" nil ))nil ))nil 3535288278"" (skosimp*)"" (typepred "nvo!1" )"" (split +)"1" (hide-all-but (-1 -6 1))"1" (typepred "incr_trk_vect(nvo!1, step!1, dir!1)" )"1" (replaces -3 :dir rl)"1" (expand "trk_only?" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "repulsive_criteria_transitive" )"2" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"bool" definitions nil )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil repulsive nil )"posreal" nil )"(total_order?[real])" nil )"posreal" vectors_2D"vectors/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{nvo2: Vect2 | trk_only?(nvo)(nvo2)}" nil ))nil ))nil 3535884573"" (skosimp*)"" (typepred "nvo!1" )"" (hide 1)"" (split +)"1" (hide-all-but (-1 -4 1))"1" (typepred "incr_trk_vect(nvo!1, step!1, dir!1)" )"1" (replaces -3 :dir rl)"1" (expand "trk_only?" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "repulsive_criteria_transitive" )"2" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )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 )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"bool" definitions nil )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{nvo2: Vect2 | trk_only?(nvo)(nvo2)}" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"posreal" vectors_2D"vectors/" )"(total_order?[real])" nil )"posreal" nil )nil repulsive nil ))nil )nil 3535288278"" (skosimp*)"" (hide -)"" (assert )"" (case "floor(maxtrk!1 / step!1) - i!1 + 1 > 0" )"1" (grind) nil nil )"2" (hide 3)"2" (typepred "floor(maxtrk!1 / step!1)" )"2" (name-replace "FF" "floor(maxtrk!1 / step!1)" )"2" (case "i!1 < maxtrk!1/step!1" )"1" (assert ) nil nil )"2" (hide-all-but (1 3))"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3535884446"" (skosimp*)"" (hide -)"" (hide 1)"" (assert )"" (case "floor(maxtrk!1 / step!1) - i!1 >= 0" )"1" (grind) nil nil )"2" (hide 3)"2" (typepred "floor(maxtrk!1 / step!1)" )"2" (name-replace "FF" "floor(maxtrk!1 / step!1)" )"2" (case "i!1 < maxtrk!1/step!1" )"1" (assert ) nil nil )"2" (hide-all-but (1 3))"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"int" integers nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )nil real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integers nil )nil integers nil )nil integers nil )"posint" nil )"nat" floor_ceil nil ))nil )nil 3535884239 ("" (termination-tcc) nil nil )nil nil ))nil 3535288278 ("" (skosimp*) nil nil ) nil nil ))nil 3535288278"" (skosimp* :preds? t) (("" (assert ) nil nil )) nil )"Sign" sign "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sign3 "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" ))nil ))nil 3535288278"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"Sign" sign "reals/" ))nil ))nil 3535473716"" (skosimp*)"" "losr_trk_iter_i(s!1, vo!1, vi!1, minrelgs!1, maxtrk!1, ") "" "vv" "losr_trk_iter_i(s!1, vo!1, vi!1, minrelgs!1, maxtrk!1, step!1, 1, ") "" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sign3 "reals/" )"{nvo2 | AND " nil )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )"bool" definitions nil )AND const-decl "[bool, bool -> bool]" booleans 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 integers nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "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 )"Sign" sign "reals/" ))nil ))nil 3535802573 ("" (skosimp*) nil nil ) nil nil ))nil 3560175723"" (skeep)"" (lemma "gs_only_normalize" )"" (inst?) (("" (assert ) (("" (inst? 1) nil nil )) nil )) nil ))nil ))nil )nil definitions nil )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"Normalized" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities 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 )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil reals nil )"real" reals nil ))nil ))nil 3560262748"" (skosimp*) (("" (rewrite "max_ge" ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil )"real" reals nil )"real" reals nil )"int" integers nil )nil real_defs nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil integers nil )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil integers nil )nil integers nil )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil ))nil ))nil 3560262748"" (skosimp*)"" (assert )"" (typepred "nvo!1" )"" (lemma "gs_only_normalize" )"" (inst? -) (("" (assert ) (("" (inst? 1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil definitions nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil integers nil )"bool" reals nil )nil integers nil )nil real_types nil )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Normalized" vectors_2D "vectors/" )"bool" repulsive nil )"Vector" vectors_2D "vectors/" )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil ))nil ))nil 3560263323"" (skosimp*)"" (lemma "repulsive_criteria_transitive" )"" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"" (assert )"" (typepred "incr_gs_vect(nvo!1, step!1, dir!1)" )"" (assert )"" (replaces -3 :dir rl)"" (typepred "nvo!1" )"" (lemma "gs_only_normalize" )"" (inst -1 "vo!1" "nvo!1" )"" (flatten)"" (hide -1)"" (split -)"1" (lemma "gs_only_trans" )"1" "vo!1" "nvo!1" "nvop!1" )"1" (assert ) nil nil ))nil ))nil )"2" (inst? 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil repulsive nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil definitions nil )nil definitions nil )"{nvo: Vect2 | norm(vo) + dir * step > 0 IMPLIES gs_only?(vo)(nvo)}" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" definitions nil )"[bool, bool -> bool]" booleans nil )"bool" repulsive nil )"Normalized" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )nil real_types nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )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 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 )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil ))nil )nil 3560262748 ("" (subtype-tcc) nil nil ) nil nil ))nil 3560267127"" (skosimp*)"" (typepred "nvo!1" )"" (hide 1)"" (lemma "repulsive_criteria_transitive" )"" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"" (assert )"" (hide (-1 -4 -6))"" (expand "incr_gs_vect" )"" case "norm(nvo!1) = norm((norm(vo!1) + dir!1 * i!1 * step!1) * ^(vo!1))" )"1" (rewrite "norm_scal" )"1" (replaces -1)"1" (replaces -1)"1" (rewrite "normalize_scal" )"1" (rewrite "normalize_normalize" )"1" rewrite "scal_assoc" )"1" rewrite "sign_times_abs" )"1" expand "sign" )"1" assert )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )"Normalized" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil real_types nil )nil real_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil sign "reals/" )"[numfield -> numfield]" 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 )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil repulsive nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"{nvo: Vect2 | norm(vo) + dir * step > 0 IMPLIES gs_only?(vo)(nvo)}" nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil )"nnreal" nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )"real" reals nil )"Sign" sign "reals/" )nil vectors_2D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Sign" sign "reals/" )"Nz_vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil reals nil )"[bool, bool -> bool]" booleans nil )"bool" definitions nil )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil ))nil )nil 3560264980"" (skosimp*)"" (typepred "nvo!1" )"" (hide 1)"" (split +)"1" (typepred "incr_gs_vect(nvo!1, step!1, dir!1)" )"1" (assert )"1" (replaces -4 :dir rl)"1" (hide-all-but (-1 -2 1))"1" (expand "gs_only?" -)"1" (skosimp*)"1" (replaces -)"1" (lemma "gs_only_scal" )"1" (inst -1 "vo!1" "l!1*l!2" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "repulsive_criteria_transitive" )"2" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" repulsive nil )nil sign "reals/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" definitions nil )nil vectors_2D_def "vectors/" )nil definitions nil )nil vectors_2D "vectors/" )"Nz_vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil repulsive nil ))nil )nil 3560262748 ("" (subtype-tcc) nil nil ) nil nil ))nil 3560267142"" (skosimp*)"" (hide -1 -2 1)"" (typepred "nvo!1" )"" (hide -3)"" case "norm(nvo!1) = norm((norm(vo!1) + dir!1 * i!1 * step!1) * ^(vo!1))" )"1" (hide -2)"1" (rewrite "norm_scal" )"1" (expand "abs" )"1" (replaces -1)"1" (assert )"1" (typepred "dir!1" )"1" (hide -1)"1" (split -)"1" (replaces -1)"1" assert )"1" case "floor((maxgs!1 - norm(vo!1)) / step!1) - i!1 >= 0" )"1" (grind) nil nil )"2" "2" "floor((maxgs!1 - norm(vo!1)) / step!1)" )"2" "FF" "floor((maxgs!1 - norm(vo!1)) / step!1)" )"2" case "i!1 < (maxgs!1-norm(vo!1))/step!1" )"1" (assert ) nil nil )"2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replaces -1)"2" assert )"2" case "floor((norm(vo!1) - mings!1) / step!1) - i!1 >= 0" )"1" (grind) nil nil )"2" "2" "floor((norm(vo!1)-mings!1) / step!1)" )"2" case "i!1 < (norm(vo!1)-mings!1)/step!1" )"1" (assert ) nil nil )"2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posint" nil )"int" integers nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"posreal" sqrt "reals/" )"posreal" vectors_2D "vectors/" )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )nil real_props nil )"odd_int" integers nil )"posreal" nil )"posreal" nil )"posint" nil )"real" reals nil )nil vectors_2D "vectors/" )"nnreal" nil )"(total_order?[real])" nil )"real" reals nil )nil vectors_2D "vectors/" )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil integers nil )"bool" reals nil )nil integers nil )nil real_types nil )nil real_types nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Normalized" vectors_2D "vectors/" )"bool" repulsive nil )"Vector" vectors_2D "vectors/" )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil ))nil )nil 3560266338"" (skosimp*)"" (typepred "nvo!1" )"" (hide 1)"" (split +)"1" (typepred "incr_gs_vect(nvo!1, step!1, dir!1)" )"1" (assert )"1" (replaces -4 :dir rl)"1" (hide-all-but (-1 -2 1))"1" (expand "gs_only?" -)"1" (skosimp*)"1" (replaces -)"1" (lemma "gs_only_scal" )"1" (inst -1 "vo!1" "l!1*l!2" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "repulsive_criteria_transitive" )"2" "eps!1" "nvo!1-vi!1" "nvop!1-vi!1" "s!1" "vo!1-vi!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil repulsive nil )"nnreal" vectors_2D "vectors/" )"Nz_vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil definitions nil )nil vectors_2D_def "vectors/" )"bool" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )"bool" repulsive nil ))nil )nil 3560265196"" (skosimp*)"" (hide -)"" (hide 1)"" (case "floor((maxgs!1-mings!1) / step!1) - i!1 + 1 > 0" )"1" (grind) nil nil )"2" (hide 4)"2" (typepred "floor((maxgs!1 - mings!1) / step!1)" )"2" "FF" "floor((maxgs!1 - mings!1) / step!1)" )"2" (case "i!1 < (maxgs!1 - mings!1) / step!1" )"1" (assert ) nil nil )"2" (typepred "maxgs!1" )"2" (typepred "mings!1" )"2" (grind-reals)"2" (case "maxgs!1 > mings!1" )"1" (grind-reals)"1" (postpone) nil nil )) nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3560262748 ("" (termination-tcc) nil nil )nil nil ))nil 3560267166"" (skosimp* :preds? t)"" (case "gs_only?(vo!1)(nvo!1)" )"1" (replaces -10)"1" (rewrite "gs_only_zero_right" ) nil nil )) nil )"2" (lemma "gs_only_normalize" )"2" (inst?) (("2" (assert ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" definitions nil )nil definitions nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil definitions nil )"nzreal" nil )"posreal" vectors_2D"vectors/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Normalized" vectors_2D "vectors/" )"bool" repulsive nil )"Vector" vectors_2D "vectors/" ))nil )nil 3560266318"" (skosimp*)"" (hide -)"" (hide 1)"" (case "floor((maxgs!1-mings!1) / step!1) - i!1 + 1 > 0" )"1" (grind) nil )"2" (hide 4)"2" (typepred "floor((maxgs!1 - mings!1) / step!1)" )"2" "FF" "floor((maxgs!1 - mings!1) / step!1)" )"2" (case "i!1 < (maxgs!1 - mings!1) / step!1" )"1" (assert ) nil )"2" (typepred "maxgs!1" )"2" (typepred "mings!1" )"2" (grind-reals)"2" (case "maxgs!1 > mings!1" )"1" (grind-reals) (("1" (postpone) nil )))"2" (postpone) nil ))))))))))))))))))))))))nil )nil nil )nil 3560262748"" (skosimp* :preds? t)"" (replaces -5) (("" (rewrite "gs_only_zero_right" ) nil nil ))nil ))nil )nil definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )nil vectors_2D_def "vectors/" )"bool" definitions nil )"bool" repulsive nil ))nil ))nil 3560452362 ("" (skosimp*) nil nil ) nil nil ))nil 3560452362"" (skosimp* :preds? t) (("" (assert ) nil nil )) nil )"Sign" sign "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sign3 "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" ))nil ))nil 3560452362"" (skosimp*)"" (assert )"" (expand "incr_gs_vect" )"" (assert )"" (expand "losr_gs_iter_dir" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )"(total_order?[real])" nil )"Sign" sign "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posreal" nil )"Sign3" losr_iterative nil )"odd_int" integers nil )"posreal" nil )"{nvo: Vect2 | norm(vo) + dir * step > 0 IMPLIES gs_only?(vo)(nvo)}" nil )"real" reals nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3560452362"" (skosimp*)"" "losr_gs_iter_i(s!1, vo!1, vi!1, minrelgs!1, mings!1, ") "" "LGS" "losr_gs_iter_i(s!1, ") "" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sign3 "reals/" )"{nvo2 | AND " nil )"bool" definitions nil )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )"Normalized" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans 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 integers nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "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 )"nzreal" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"(total_order?[real])" nil )"Sign" sign "reals/" )"real" reals nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3560452362 ("" (skosimp*) nil nil )"posreal" vectors_2D"vectors/" )"real" reals nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.36 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
