products/Sources/formale Sprachen/COBOL/Test-Suite/COBOL/SQ/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: abs_rews.prf   Sprache: Unknown

(abs_rews
 (abs_nat_rew 0
  (abs_nat_rew-1 nil 3408099560 ("" (grind) nil nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (abs_0_rew 0
  (abs_0_rew-1 nil 3408099564 ("" (grind) nil nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil))
   shostak))
 (abs_neg_rew 0
  (abs_neg_rew-1 nil 3408099569 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (real nonempty-type-from-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (sgn_nat_rew 0
  (sgn_nat_rew-1 nil 3408099573 ("" (grind) nil nil)
   ((sgn const-decl "int" real_defs nil)) shostak)))

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]