Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: reduce_choice.prf Sprache: Lisp

Original von: PVS^©

(reduce_choice
(in_rcvd 0
  (in_rcvd-1 nil 3403623763
   ("" (skosimp*)
    (("" (expand "reduce_choice")
      (("" (expand "reduce_choice")
        (("" (assert)
          ((""
            (typepred
             "icf!1(reduce(tau!1)(rcvd!1(d!1), enabled(rcvd!1, check!1)(d!1)))")
            (("" (expand "in?")
              (("" (skosimp* t)
                (("" (replace -2 :hide? T)
                  (("" (use "reduce_overlap")
                    (("" (rewrite "reduce_length[S,T,<=]")
                      (("" (assert)
                        (("" (skosimp*)
                          (("" (inst + "n!1")
                            (("" (assert)
                              ((""
                                (typepred "<=")
                                ((""
                                  (expand "total_order?")
                                  ((""
                                    (expand "partial_order?")
                                    ((""
                                      (expand "antisymmetric?")
                                      ((""
                                        (flatten)
                                        ((""
                                          (inst?)
                                          (("" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((reduce_choice const-decl "T" reduce_choice nil)
    (reduce_length formula-decl nil reduce_properties nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (reduce_overlap formula-decl nil reduce_properties nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (in? const-decl "bool" seqs "structures/")
    (ne_seqs type-eq-decl nil seqs "structures/")
    (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)
    (in_consensus_function type-eq-decl nil finite_seqs nil)
    (posnat nonempty-type-eq-decl nil integers 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) (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (tau_type type-eq-decl nil tau_declaration nil)
    (S formal-const-decl "posnat" reduce_choice nil)
    (below type-eq-decl nil naturalnumbers nil)
    (vec type-eq-decl nil node nil) (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" reduce_choice nil)
    (reduce const-decl "ne_seqs" reduce_properties nil)
    (D formal-const-decl "posnat" reduce_choice nil)
    (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil)
    (check_stage type-eq-decl nil node_functions_stage nil)
    (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage
     nil)
    (reduce_choice const-decl "T" reduce_properties nil))
   shostak))
(min_reduce_choice 0
  (min_reduce_choice-1 nil 3403606705
   ("" (skosimp*)
    (("" (expand "reduce_choice")
      (("" (expand "reduce_choice")
        (("" (lift-if)
          (("" (ground) (("" (use "reflexive") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((reduce_choice const-decl "T" reduce_choice nil)
    (default formal-const-decl "T" reduce_choice nil)
    (<= formal-const-decl "(total_order?[T])" reduce_choice nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (reflexive formula-decl nil relations_extra nil)
    (min_in_consensus name-judgement "in_consensus_function"
     reduce_choice nil)
    (reduce_choice const-decl "T" reduce_properties nil))
   shostak))
(max_reduce_choice 0
  (max_reduce_choice-1 nil 3403606806
   ("" (skosimp*)
    (("" (expand "reduce_choice")
      (("" (expand "reduce_choice")
        (("" (lift-if)
          (("" (ground) (("" (use "reflexive") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((reduce_choice const-decl "T" reduce_choice nil)
    (default formal-const-decl "T" reduce_choice nil)
    (<= formal-const-decl "(total_order?[T])" reduce_choice nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (reflexive formula-decl nil relations_extra nil)
    (max_in_consensus name-judgement "in_consensus_function"
     reduce_choice nil)
    (reduce_choice const-decl "T" reduce_properties nil))
   nil))
(reduce_overlap?_TCC1 0
  (reduce_overlap?_TCC1-1 nil 3403688060 ("" (subtype-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (injective? const-decl "bool" functions nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (D formal-const-decl "posnat" reduce_choice nil)
    (S formal-const-decl "posnat" reduce_choice nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage
     nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   nil))
(reduce_overlap?_TCC2 0
  (reduce_overlap?_TCC2-1 nil 3403688060 ("" (subtype-tcc) nil nil)
   ((finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (min_in_consensus name-judgement "in_consensus_function"
     reduce_choice nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (injective? const-decl "bool" functions nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (D formal-const-decl "posnat" reduce_choice nil)
    (S formal-const-decl "posnat" reduce_choice nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage
     nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (vec2seq const-decl "finite_sequence[T]" node nil)
    (<= formal-const-decl "(total_order?[T])" reduce_choice nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (reduce const-decl "ne_seqs" reduce_properties nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(max_length_TCC1 0
  (max_length_TCC1-1 nil 3403688060
   ("" (skosimp*)
    (("" (use "finite_image[below(D), nat]")
      (("1" (assert)
        (("1" (expand "empty?")
          (("1" (expand "member")
            (("1" (inst - "M(rcvd!1, check!1, tau!1)(0)")
              (("1" (assert)
                (("1" (expand "image")
                  (("1" (inst?)
                    (("1" (expand "fullset") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) (("2" (rewrite "finite_below[D]") nil nil)) nil))
      nil))
    nil)
   ((finite_image judgement-tcc nil function_image_aux nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (D formal-const-decl "posnat" reduce_choice nil)
    (below type-eq-decl nil naturalnumbers nil)
    (M const-decl "nat" reduce_choice nil)
    (tau_type type-eq-decl nil tau_declaration nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (check_stage type-eq-decl nil node_functions_stage nil)
    (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (S formal-const-decl "posnat" reduce_choice nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (fullset const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (image const-decl "set[R]" function_image nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/"))
   nil))
(max_length_bound 0
  (max_length_bound-1 nil 3403688061
   ("" (skosimp*)
    (("" (expand "max_length")
      ((""
        (typepred
         "max(image(M(rcvd!1, check!1, tau!1), fullset[below(D)]))")
        (("" (inst?)
          (("" (assert)
            (("" (expand "image")
              (("" (inst?)
                (("" (expand "fullset") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max_length const-decl "nat" reduce_choice nil)
    (d!1 skolem-const-decl "below(D)" reduce_choice nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     restrict_order_props nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_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)
    (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)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (D formal-const-decl "posnat" reduce_choice nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (S formal-const-decl "posnat" reduce_choice nil)
    (T formal-nonempty-type-decl nil reduce_choice nil)
    (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil)
    (check_stage type-eq-decl nil node_functions_stage nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (tau_type type-eq-decl nil tau_declaration nil)
    (M const-decl "nat" reduce_choice nil)
    (fullset const-decl "set" sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (max const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
         finite_sets_minmax "finite_sets/"))
   shostak)))

¤ Dauer der Verarbeitung: 0.11 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.