Quelle csequence_length_comp.prf Sprache: Lisp

(csequence_length_comp
(length_lt_le 0
  (length_lt_le-1 nil 3513689376
   ("" (expand* "length_lt" "length_le")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_lt const-decl "bool" csequence_length_comp nil)
    (length_le const-decl "bool" csequence_length_comp nil))
   shostak))
(length_gt_ge 0
  (length_gt_ge-1 nil 3513689391
   ("" (expand* "length_gt" "length_ge")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_gt const-decl "bool" csequence_length_comp nil)
    (length_ge const-decl "bool" csequence_length_comp nil))
   shostak))
(length_eq_le 0
  (length_eq_le-1 nil 3513689401
   ("" (expand* "length_eq" "length_le")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_eq const-decl "bool" csequence_length_comp nil)
    (length_le const-decl "bool" csequence_length_comp nil))
   shostak))
(length_eq_ge 0
  (length_eq_ge-1 nil 3513689413
   ("" (expand* "length_eq" "length_ge")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_eq const-decl "bool" csequence_length_comp nil)
    (length_ge const-decl "bool" csequence_length_comp nil))
   shostak))
(length_lt_neq 0
  (length_lt_neq-1 nil 3513689424
   ("" (expand* "length_lt" "length_eq")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_lt const-decl "bool" csequence_length_comp nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak))
(length_gt_neq 0
  (length_gt_neq-1 nil 3513689440
   ("" (expand* "length_gt" "length_eq")
    (("" (skosimp) (("" (ground) nil nil)) nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_gt const-decl "bool" csequence_length_comp nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak))
(length_eq_empty 0
  (length_eq_empty-1 nil 3513689453
   ("" (skosimp)
    (("" (expand "length_eq")
      (("" (use "length_empty?_rew[T2]")
        (("" (use "length_empty?_rew[T1]") (("" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((length_eq const-decl "bool" csequence_length_comp nil)
    (T1 formal-type-decl nil csequence_length_comp nil)
    (csequence type-decl nil csequence_codt nil)
    (T2 formal-type-decl nil csequence_length_comp nil)
    (length_empty?_rew formula-decl nil csequence_length nil))
   shostak))
(length_eq_rest 0
  (length_eq_rest-1 nil 3513689486
   ("" (expand "length_eq")
    (("" (expand "is_finite" 1 1)
      (("" (expand "is_finite" 1 2)
        (("" (expand "is_finite" 1 3)
          (("" (expand "is_finite" 1 4)
            (("" (expand "length" 1 1)
              (("" (expand "length" 1 2) (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite inductive-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (length_eq const-decl "bool" csequence_length_comp nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.