products/Sources/formale Sprachen/PVS/graphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: newman_yokouchi.pvs   Sprache: PVS

Original von: PVS©
(reduce_walks
 (reduce_TCC1 0
  (reduce_TCC1-1 nil 3254571090 ("" (subtype-tcc) nil nil) nil nil))
 (reduce_TCC2 0
  (reduce_TCC2-1 nil 3254571090 ("" (subtype-tcc) nil nil) nil nil))
 (reduce_TCC3 0
  (reduce_TCC3-1 nil 3254571090 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
 (reduce_TCC4 0
  (reduce_TCC4-1 nil 3254571090 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
 (reduce_TCC5 0
  (reduce_TCC5-1 nil 3254571090 ("" (grind) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
 (reduce_TCC6 0
  (reduce_TCC6-1 nil 3254571372
   ("" (skosimp*)
    (("" (expand "finseq_appl")
      (("" (typepred "w!1")
        (("" (expand "walk?")
          (("" (expand "finseq_appl")
            (("" (flatten)
              (("" (split +)
                (("1" (hide -3)
                  (("1" (expand "verts_in?")
                    (("1" (skosimp*)
                      (("1" (ground)
                        (("1" (inst?) nil nil) ("2" (inst?) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (lift-if)
                    (("2" (typepred "k!1")
                      (("2" (lift-if)
                        (("2" (ground)
                          (("1" (inst?) (("1" (assert) nil nil)) nil)
                           ("2" (case-replace "k!1=n!1+1")
                            (("1" (assert)
                              (("1"
                                (replace -10)
                                (("1"
                                  (hide -10)
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil)
                           ("3" (inst?) (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (verts_in? const-decl "bool" walks 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)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil reduce_walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (Long_walk type-eq-decl nil reduce_walks nil))
   shostak))
 (reduce_lem_TCC1 0
  (reduce_lem_TCC1-1 nil 3254571090 ("" (subtype-tcc) nil nil) nil
   nil))
 (reduce_lem_TCC2 0
  (reduce_lem_TCC2-1 nil 3254571090 ("" (subtype-tcc) nil nil) nil
   nil))
 (reduce_lem_TCC3 0
  (reduce_lem_TCC3-1 nil 3254571090 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
 (reduce_lem_TCC4 0
  (reduce_lem_TCC4-1 nil 3559559064 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
 (reduce_lem 0
  (reduce_lem-1 nil 3254571090
   ("" (skosimp*)
    (("" (expand "o ")
      (("" (expand* "^" min empty_seq)
        (("" (auto-rewrite "finseq_appl")
          (("" (typepred "k!1")
            (("" (apply-extensionality 1 :hide? t)
              (("1" (expand "reduce")
                (("1" (lift-if)
                  (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
                nil)
               ("2" (apply-extensionality 1 :hide? t)
                (("1" (typepred "x!1")
                  (("1" (lift-if) (("1" (grind) nil nil)) nil)) nil)
                 ("2" (skosimp*)
                  (("2" (expand* "^" min empty_seq)
                    (("2" (expand "reduce")
                      (("2" (lift-if)
                        (("2" (assert) (("2" (ground) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (skosimp*)
                  (("3" (typepred "n!1")
                    (("3" (expand* "^" min empty_seq)
                      (("3" (lift-if) (("3" (ground) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("4" (skosimp*)
                  (("4" (assert)
                    (("4" (typepred "n!1")
                      (("4" (expand* "^" min empty_seq)
                        (("4" (lift-if) (("4" (ground) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("5" (skosimp*)
                  (("5" (typepred "n!1")
                    (("5" (expand* "^" min empty_seq)
                      (("5" (lift-if) (("5" (ground) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (skosimp*)
                (("3" (expand* "^" min empty_seq) nil nil)) nil)
               ("4" (skosimp*)
                (("4" (typepred "n!1")
                  (("4" (expand* "^" min empty_seq)
                    (("4" (lift-if) (("4" (ground) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("5" (skosimp*)
                (("5" (typepred "n!1")
                  (("5" (expand* "^" min empty_seq)
                    (("5" (lift-if) (("5" (ground) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("6" (skosimp*)
                (("6" (typepred "n!1")
                  (("6" (expand* "^" min empty_seq)
                    (("6" (lift-if) (("6" (ground) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("7" (lift-if) (("7" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "finseq" finite_sequences nil)
    (Long_walk type-eq-decl nil reduce_walks nil)
    (reduce const-decl "Walk(G)" reduce_walks nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon const-decl "T" epsilons nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (k!1 skolem-const-decl "{n: nat | n > 0 AND n < length(w!1) - 1}"
     reduce_walks nil)
    (w!1 skolem-const-decl "Walk[T](G!1)" reduce_walks nil)
    (G!1 skolem-const-decl "graph[T]" reduce_walks nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (> const-decl "bool" 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil reduce_walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (^ const-decl "finseq" finite_sequences nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil)))


¤ Dauer der Verarbeitung: 0.34 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




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.


Bot Zugriff