SSL circles_and_lines.prf   Sprache: Lisp

(circles_and_lines
 (t1_lt_t2_lt_D 0
  (t1_lt_t2_lt_D-1 nil 3402827007
   ("" (skeep)
    (("" (lemma "quad_min_eq_intv")
      ((""
        (inst - "sq(vx) + sq(vy)" "2*sx*vx + 2*sy*vy"
         "D+ sq(sx) + sq(sy)" "t" "t1" "t2")
        (("1" (split -1)
          (("1" (expand "quadratic")
            (("1" (expand "sq") (("1" (assert) nil nil)) nil)) nil)
           ("2" (hide 3)
            (("2" (hide -)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("3" (hide 3)
            (("3" (replace -2 -3 rl)
              (("3" (hide -2)
                (("3" (expand "quadratic")
                  (("3" (expand "sq") (("3" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (propax) nil nil) ("5" (propax) nil nil))
          nil)
         ("2" (expand "sq" 1) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((quad_min_eq_intv formula-decl nil quad_minmax nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (quadratic const-decl "real" quadratic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" 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)
    (sq const-decl "nonneg_real" sq nil)
    (vx skolem-const-decl "real" circles_and_lines nil)
    (vy skolem-const-decl "real" circles_and_lines nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (lt_D_t1_lt_t2 0
  (lt_D_t1_lt_t2-1 nil 3402827094
   ("" (skeep)
    (("" (lemma "quad_min_eq_is_in")
      ((""
        (inst - "sq(vx) + sq(vy)" "2*sx*vx + 2*sy*vy"
         "D+ sq(sx) + sq(sy)" "t" "t1" "t2")
        (("1" (split -1)
          (("1" (propax) nil nil)
           ("2" (hide -)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)
           ("3" (expand "quadratic")
            (("3" (expand "sq") (("3" (assert) nil nil)) nil)) nil)
           ("4" (expand "quadratic")
            (("4" (expand "sq") (("4" (assert) nil nil)) nil)) nil)
           ("5" (propax) nil nil))
          nil)
         ("2" (expand "sq" 1) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((quad_min_eq_is_in formula-decl nil quad_minmax 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (quadratic const-decl "real" quadratic nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" 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)
    (sq const-decl "nonneg_real" sq nil)
    (vx skolem-const-decl "real" circles_and_lines nil)
    (vy skolem-const-decl "real" circles_and_lines nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (discr_le_0 0
  (discr_le_0-1 nil 3402827119
   ("" (skeep)
    (("" (name-replace "aa" "vx*vx + vy*vy")
      (("" (name-replace "bb" "2*(sx*vx + sy*vy)")
        (("" (name-replace "cc" "sx*sx+sy*sy-D")
          (("" (case "4*discrm=discr(aa,bb,cc)")
            (("1" (lemma "a_gt_0_discr_gt_0")
              (("1" (inst?)
                (("1" (inst -1 "t")
                  (("1" (assert)
                    (("1" (split)
                      (("1" (hide-all-but (1 2))
                        (("1" (expand "aa")
                          (("1" (grind-reals) nil nil)) nil))
                        nil)
                       ("2" (hide-all-but (1 3))
                        (("2" (expand* "aa" "bb" "cc")
                          (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but (-1 1))
              (("2" (expand* "aa" "bb" "cc") (("2" (grind) nil nil))
                nil))
              nil)
             ("3" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (a_gt_0_discr_gt_0 formula-decl nil quadratic nil)
    (aa skolem-const-decl "real" circles_and_lines nil)
    (bb skolem-const-decl "real" circles_and_lines nil)
    (cc skolem-const-decl "real" circles_and_lines nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (discr const-decl "real" quadratic nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil))
   nil)))