Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/C/Lyx/lib/tex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

sichere Verbindung greek.kmap   Sprache: Unknown

(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)))

[ Verzeichnis aufwärts0.74unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]

                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik