Quelle  opt_trk_gs.prf

(opt_trk_gs
 (k_opt_tangent 0
  (k_opt_tangent-2 nil 3434118271
   ("" (skeep)
    (("" (assert)
      (("" (rewrite "dot_sub_right")
        (("" (expand "k_opt")
          (("" (rewrite "sqv" :dir rl) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (dot_scal_right formula-decl nil vectors_2D "vectors/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (k_opt const-decl "real" opt_trk_gs nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (* 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)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (dot_sub_right formula-decl nil vectors_2D "vectors/"))
   nil)
  (k_opt_tangent-1 nil 3434118248 ("" (postpone) nil nil) nil shostak))
 (opt_trk_gs_line_TCC1 0
  (opt_trk_gs_line_TCC1-2 nil 3445701811
   ("" (skeep)
    (("" (expand "optimal?")
      (("" (skeep)
        (("" (lemma "le_rel")
          (("" (inst? -1)
            (("" (inst -1 "vi")
              (("" (assert)
                (("" (hide 2)
                  (("" (expand "le?")
                    (("" (both-sides-f 1 "sq")
                      (("1" (rewrite "sq_norm")
                        (("1" (rewrite "sq_norm")
                          (("1"
                            (case "sqv(vo2 - vi - (vo - vi)) = sqv(k * nzv - (vo - vi)) + sqv(vo2-vi-k*nzv)")
                            (("1" (assert) nil nil)
                             ("2" (hide 2)
                              (("2"
                                (name-replace
                                 "a"
                                 "k * nzv - (vo - vi)"
                                 :hide?
                                 nil)
                                (("2"
                                  (name-replace
                                   "b"
                                   "vo2 - vi - k * nzv"
                                   :hide?
                                   nil)
                                  (("2"
                                    (case-replace
                                     "vo2 - vi - (vo - vi) = a+b")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (rewrite "sqv_add")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (cancel-by 1 "2")
                                            (("1"
                                              (hide 1)
                                              (("1"
                                                (expand "parallel?")
                                                (("1"
                                                  (skeep -4)
                                                  (("1"
                                                    (lemma
                                                     "k_opt_tangent")
                                                    (("1"
                                                      (inst?)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replaces
                                                           -4
                                                           :dir
                                                           rl)
                                                          (("1"
                                                            (replace
                                                             -3)
                                                            (("1"
                                                              (case-replace
                                                               " vo2 - vi - k * nzv = vo2 - (k * nzv + vi)")
                                                              (("1"
                                                                (hide
                                                                 -1)
                                                                (("1"
                                                                  (replaces
                                                                   -2)
                                                                  (("1"
                                                                    (replaces
                                                                     -3)
                                                                    (("1"
                                                                      (rewrite
                                                                       "dot_scal_right")
                                                                      (("1"
                                                                        (lemma
                                                                         "dot_comm")
                                                                        (("1"
                                                                          (inst?)
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            (("1"
                                                                              (replace
                                                                               -1)
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replaces (-1 -2) :dir rl)
                                      (("2"
                                        (hide-all-but 1)
                                        (("2" (grind) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (rewrite "sq_le") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((optimal? const-decl "bool" definitions nil)
    (le_rel formula-decl nil definitions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (dot_scal_right formula-decl nil vectors_2D "vectors/")
    (dot_comm formula-decl nil vectors_2D "vectors/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (k_opt_tangent formula-decl nil opt_trk_gs nil)
    (parallel? const-decl "bool" vectors_2D "vectors/")
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D "vectors/")
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (dot_scal_left formula-decl nil vectors_2D "vectors/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sqv_add formula-decl nil vectors_2D "vectors/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_norm formula-decl nil vectors_2D "vectors/")
    (sq_le formula-decl nil sq "reals/")
    (le? const-decl "bool" definitions nil)
    (add_cancel_neg2 formula-decl nil vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (* 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil))
   nil)
  (opt_trk_gs_line_TCC1-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil
   nil))
 (opt_trk_gs_line_TCC2 0
  (opt_trk_gs_line_TCC2-2 nil 3445701838
   ("" (skeep) (("" (hide -1) (("" (grind) nil nil)) nil)) nil)
   ((* const-decl "Vector" vectors_2D "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil)
  (opt_trk_gs_line_TCC2-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil
   nil))
 (opt_trk_gs_dot_TCC1 0
  (opt_trk_gs_dot_TCC1-2 nil 3445702005
   ("" (skeep)
    ((""
      (name-replace "opto"
       "opt_trk_gs_line(Vdir(u, vo - vi), vo, vi + W0(u, j))")
      (("" (typepred "opto")
        (("" (case "W0(u,j) + opto`1 * Vdir(u, vo - vi) = opto`2 - vi")
          (("1" (replaces -1 :dir rl) (("1" (rewrite "W_dot") nil nil))
            nil)
           ("2" (replaces -1)
            (("2" (hide-all-but 1)
              (("2" (grind :exclude "W0") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (optimal? const-decl "bool" definitions nil)
    (Vdir const-decl "Nz_vect2" definitions nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (opt_trk_gs_line const-decl
     "{k: real, nvo: (optimal?(vo, nzv)) | k * nzv = nvo - vi}"
     opt_trk_gs nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (W0 const-decl "Vect2" definitions nil)
    (W_dot formula-decl nil definitions nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil)
  (opt_trk_gs_dot_TCC1-1 nil 3445701764 ("" (subtype-tcc) nil nil) nil
   nil))
 (opt_trk_gs_vertical_TCC1 0
  (opt_trk_gs_vertical_TCC1-1 nil 3471177879
   ("" (skeep)
    (("" (assert)
      (("" (lemma "Delta_gt_0_nzv")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Delta_gt_0_nzv formula-decl nil horizontal nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" opt_trk_gs nil))
   nil))
 (opt_trk_gs_vertical_TCC2 0
  (opt_trk_gs_vertical_TCC2-2 nil 3471178012
   ("" (skeep)
    (("" (skeep)
      (("" (lemma "scal_eq_zero")
        (("" (inst?)
          (("" (assert)
            (("" (rewrite "sqv_eq_0" :dir rl)
              (("" (replaces -5)
                (("" (lemma "Theta_D_on_D")
                  (("" (inst?)
                    (("" (assert) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (Theta_D_on_D formula-decl nil horizontal nil)
    (D formal-const-decl "posreal" opt_trk_gs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" 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)
    (= 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (scal_eq_zero formula-decl nil vectors_2D "vectors/"))
   nil)
  (opt_trk_gs_vertical_TCC2-1 nil 3471177879 ("" (subtype-tcc) nil nil)
   nil nil))
 (opt_trk_gs_vertical_on_D 0
  (opt_trk_gs_vertical_on_D-1 nil 3471178124
   ("" (skeep)
    (("" (beta)
      (("" (flatten)
        (("" (expand "opt_trk_gs_vertical?")
          (("" (flatten)
            (("" (expand "opt_trk_gs_vertical")
              (("" (lift-if)
                (("" (split -1)
                  (("1" (flatten)
                    (("1" (assert)
                      (("1"
                        (typepred
                         "opt_trk_gs_dot(t * (s + Theta_D(s, vo - vi, dir) * (vo - vi)), vo, vi,
                           sq(D) - s * (s + Theta_D(s, vo - vi, dir) * (vo - vi)))")
                        (("1" (replaces -5 :dir rl)
                          (("1" (hide-all-but (-2 2))
                            (("1" (grind :exclude "Theta_D") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((opt_trk_gs_vertical? const-decl "bool" opt_trk_gs nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (opt_trk_gs_vertical const-decl "Vect2" opt_trk_gs nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (optimal? const-decl "bool" definitions nil)
    (Vdir const-decl "Nz_vect2" definitions nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (D formal-const-decl "posreal" opt_trk_gs nil)
    (Delta const-decl "real" horizontal nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (Theta_D const-decl "real" horizontal nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (opt_trk_gs_dot const-decl
     "{nvo: (optimal?(vo, Vdir(u, vo - vi))) | u * (nvo - vi) = j}"
     opt_trk_gs nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/"))
   nil)))