Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sqrt_rew.prf Sprache: Lisp

Original von: PVS^©

(sqrt_rew
(sqrt_4 0
  (sqrt_4-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_4 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(sqrt_9 0
  (sqrt_9-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_9 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(sqrt_16 0
  (sqrt_16-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_16 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(sqrt_25 0
  (sqrt_25-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
   ((sqrt_25 formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(sqrt_36 0
  (sqrt_36-1 nil 3254823310
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil nil)) nil)
     ("2" (rewrite "sq_eq") nil nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil))
(sqrt_49 0
  (sqrt_49-2 nil 3563712260
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_49-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
(sqrt_64 0
  (sqrt_64-2 nil 3563712264
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_64-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
(sqrt_81 0
  (sqrt_81-2 nil 3563712269
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_81-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
(sqrt_100 0
  (sqrt_100-2 nil 3563712274
   ("" (both-sides-f 1 "sq")
    (("1" (assert) (("1" (grind) nil nil)) nil)
     ("2" (rewrite "sq_eq") nil nil))
    nil)
   ((sq_eq formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_sqrt formula-decl nil sqrt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_100-1 nil 3254823310
   ("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
   ((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq const-decl "nonneg_real" sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
   nil))
(sqrt_factor_left 0
  (sqrt_factor_left-1 nil 3254823327
   ("" (skosimp*)
    (("" (case-replace "nna!1 * nnx!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
      (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    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)
    (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)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
(sqrt_factor_middle 0
  (sqrt_factor_middle-1 nil 3254823495
   ("" (skosimp*)
    (("" (case-replace "nnx!1 * nna!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
      (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    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)
    (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)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
(sqrt_factor_right 0
  (sqrt_factor_right-1 nil 3254823514
   ("" (skosimp*)
    (("" (case-replace "nnx!1 * nnx!1 * nna!1 = nnx!1 * nnx!1*nna!1")
      (("" (rewrite "sqrt_times") (("" (assert) nil nil)) nil)) nil))
    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)
    (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)
    (sqrt_square formula-decl nil sqrt nil)
    (sqrt_times formula-decl nil sqrt nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil)))

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.