Quelle  test_vec.prf   Sprache: Lisp

(test_vec
 (t1 0
  (asd "wer" 3256992451
   ("" (skosimp*) (("" (vect-distr-on) (("" (assert) nil nil)) nil))
    nil)
   ((add_zero_left formula-decl nil vectors_3D nil)
    (sub_eq_args formula-decl nil vectors_3D nil))
   shostak)
  (t1-1 nil 3254655353 ("" (skosimp*) (("" (assert) nil nil)) nil) nil
   shostak))
 (t1b 0
  (t1b-1 nil 3255264672
   ("" (skosimp*) (("" (assert) (("" (postpone) nil nil)) nil)) nil)
   ((add_cancel2 formula-decl nil vectors_3D nil)) shostak))
 (t1c 0
  (t1c-1 nil 3255264717 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
 (t2 0
  (t2-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (sub_zero_left formula-decl nil vectors_3D nil))
   shostak))
 (t3 0
  (t3-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((add_cancel formula-decl nil vectors_3D nil)) shostak))
 (t4 0
  (t4-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((add_cancel formula-decl nil vectors_3D nil)) shostak))
 (t5 0
  (t5-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_cancel formula-decl nil vectors_3D nil)) shostak))
 (t6 0
  (t6-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (dot_zero_right formula-decl nil vectors_3D nil))
   shostak))
 (t7 0
  (t7-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (dot_zero_left formula-decl nil vectors_3D nil))
   shostak))
 (t8 0
  (t8-2 nil 3254655652 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (dot_zero_right formula-decl nil vectors_3D nil)
    (add_zero_right formula-decl nil vectors_3D nil))
   nil)
  (t8-1 nil 3254655387
   ("" (skosimp*)
    (("" (assert)
      (("" (lemma "dot_add_right") (("" (inst?) nil nil)) nil)) nil))
    nil)
   nil shostak))
 (t9 0
  (t9-1 nil 3254655387 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (add_zero_left formula-decl nil vectors_3D nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (scal_zero formula-decl nil vectors_3D nil)
    (sub_eq_args formula-decl nil vectors_3D nil))
   shostak))
 (t10 0
  (t10-1 nil 3254655387 ("" (then (skosimp*) (assert)))
   ((sub_eq_args formula-decl nil vectors_3D nil)
    (scal_zero formula-decl nil vectors_3D nil)
    (sub_zero_left formula-decl nil vectors_3D nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (neg_add_left formula-decl nil vectors_3D nil)
    (norm_zero formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (t11 0
  (t11-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((add_cancel_neg formula-decl nil vectors_3D nil)) shostak))
 (t12 0
  (t12-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((sub_cancel_neg formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil))
   shostak))
 (t13 0
  (t13-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((neg_add_left formula-decl nil vectors_3D nil)) shostak))
 (t14 0
  (t14-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((neg_neg formula-decl nil vectors_3D nil)) shostak))
 (t15 0
  (t15-1 nil 3254655388 ("" (then (skosimp*) (assert)))
   ((scal_assoc formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (t16 0
  (t16-1 nil 3254654555 ("" (assert) nil nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil))
   shostak))
 (t17 0
  (t17-1 nil 3254654654 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil))
   shostak))
 (t18 0
  (t18-1 nil 3254654659 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil))
   shostak))
 (t19 0
  (t19-1 nil 3254654664
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_right formula-decl nil vectors_3D nil))
   shostak))
 (t20 0
  (t20-1 nil 3254655388 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil))
   shostak))
 (t21 0
  (t21-1 nil 3254655388
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv_scal formula-decl nil vectors_3D nil))
   shostak))
 (t22 0
  (t22-1 nil 3254655389
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (norm_scal formula-decl nil vectors_3D nil))
   shostak))
 (t23 0
  (t23-1 nil 3254655752
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (dot_add_right formula-decl nil vectors_3D nil))
   shostak))
 (t24 0
  (t24-1 nil 3254656810
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr)
        (("" (vect-distr-off)
          (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
 (t25 0
  (t25-1 nil 3254655832
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
 (t26 0
  (t26-1 nil 3254655838
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
 (t27 0
  (t27-1 nil 3254656905
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (t28 0
  (t28-1 nil 3254657039
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_right formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_sub_right formula-decl nil vectors_3D nil))
   shostak))
 (t29 0
  (t29-1 nil 3254657104
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (scal_assoc formula-decl nil vectors_3D nil)
    (sqv_neg formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (dot_add_right formula-decl nil vectors_3D nil))
   shostak))
 (t30 0
  (t30-1 nil 3254657196
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((sqv_scal formula-decl nil vectors_3D nil)
    (norm_neg formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (dot_add_left formula-decl nil vectors_3D nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (t31 0
  (t31-1 nil 3255264574
   ("" (skosimp*) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
 (t32 0
  (t32-1 nil 3255264605 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((add_cancel_neg2 formula-decl nil vectors_3D nil)) shostak))
 (t33 0
  (t33-1 nil 3255284497 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((sqrt_pos application-judgement "posreal" sqrt "reals/")
    (scal_1 formula-decl nil vectors_3D nil)
    (sqrt_1 formula-decl nil sqrt "reals/"))
   shostak))
 (t34 0
  (t34-1 nil 3256993386
   ("" (skosimp*)
    (("" (replace -1) (("" (hide -1) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (sqrt_4 formula-decl nil sqrt_rew "reals/"))
   shostak))
 (t35 0
  (t35-1 nil 3256993522
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr) (("" (assert) (("" (postpone) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vx_distr_add formula-decl nil vectors_3D nil)
    (vx_scal formula-decl nil vectors_3D nil))
   shostak))
 (t37 0
  (t37-1 nil 3256995164
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_add_right formula-decl nil vectors_3D nil)
    (scal_add_left formula-decl nil vectors_3D nil)
    (vy_distr_add formula-decl nil vectors_3D nil))
   shostak))
 (t38 0
  (t38-1 nil 3256995250
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (dot_sub_right formula-decl nil vectors_3D nil)
    (dot_add_left formula-decl nil vectors_3D nil))
   shostak))
 (t39 0
  (t39-1 nil 3256995382
   ("" (skosimp*)
    (("" (assert) (("" (vect-distr) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dot_scal_right formula-decl nil vectors_3D nil)
    (vx_distr_add formula-decl nil vectors_3D nil))
   shostak))
 (t96 0
  (t96-1 nil 3256995031
   ("" (skosimp*)
    (("" (assert)
      (("" (vect-distr)
        (("" (rewrite "comp_distr_add")
          (("" (rewrite "comp_distr_scal") (("" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (comp_distr_add formula-decl nil vectors 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (* const-decl "Vector" vectors nil)
    (comp_distr_scal formula-decl nil vectors nil))
   nil)))