products/sources/formale Sprachen/PVS/digraphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: monoid_def.pvs   Sprache: Lisp

Original von: PVS©
(ind_paths
 (independent?_TCC1 0
  (independent?_TCC1-1 nil 3507100931 ("" (subtype-tcc) 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)
    (> 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 ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (independent?_TCC2 0
  (independent?_TCC2-1 nil 3507100931 ("" (subtype-tcc) 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)
    (> 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 ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (independent?_comm 0
  (independent?_comm-1 nil 3507100931
   ("" (skosimp*)
    (("" (expand "independent?")
      (("" (skosimp*)
        (("" (inst -1 "j!1" "i!1") (("" (assert) nil))))))))
    nil)
   ((independent? const-decl "bool" ind_paths 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (independent_ne 0
  (independent_ne-1 nil 3507100931
   ("" (skosimp*)
    (("" (expand "independent?")
      (("" (replace -3)
        (("" (hide -3)
          (("" (inst - "1" "1") (("" (assert) nil))))))))))
    nil)
   ((independent? const-decl "bool" ind_paths nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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))
   nil))
 (ind_path_set_2 0
  (ind_path_set_2-1 nil 3507100931
   ("" (skosimp*)
    (("" (lemma "card_2_has_2[Path_from(G!1,s!1,t!1)]")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (inst 2 "x!1" "y!1")
              (("" (expand "ind_path_set?")
                (("" (inst?)
                  (("" (assert)
                    (("" (expand "path_from?")
                      (("" (propax) nil))))))))))))))))))))
    nil)
   ((Path_from type-eq-decl nil paths nil)
    (path_from? const-decl "bool" paths nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-type-decl nil ind_paths nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (card_2_has_2 formula-decl nil finite_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ind_path_set? const-decl "bool" ind_paths nil)
    (set_of_paths type-eq-decl nil ind_paths nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil))
   nil))
 (internal_verts_TCC1 0
  (internal_verts_TCC1-1 nil 3507100931 ("" (subtype-tcc) 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)
    (> 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 ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (internal_verts_TCC2 0
  (internal_verts_TCC2-1 nil 3507100931
   ("" (skosimp*)
    (("" (lemma "finite_subset[T]")
      (("" (inst?)
        (("1" (assert)
          (("1" (inst - "verts_of(w!1)")
            (("1" (assert) (("1" (hide 2) (("1" (grind) nil)))))))))
         ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil))))))))))
    nil)
   ((T formal-type-decl nil ind_paths nil)
    (finite_subset formula-decl nil finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (below type-eq-decl nil naturalnumbers nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (verts_of const-decl "finite_set[T]" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (finseq type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (w!1 skolem-const-decl "prewalk[T]" ind_paths nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (indep?_lem 0
  (indep?_lem-1 nil 3507100931
   ("" (skosimp*)
    (("" (expand "indep?")
      (("" (expand "independent?")
        (("" (prop)
          (("1" (skosimp*)
            (("1" (expand "empty?")
              (("1" (expand "member")
                (("1" (expand "intersection")
                  (("1" (expand "internal_verts")
                    (("1" (expand "member")
                      (("1" (expand "finseq_appl")
                        (("1" (inst - "seq(w1!1)(i!1)")
                          (("1" (prop)
                            (("1" (inst?) (("1" (assert) nil)))
                             ("2" (inst + "j!1")
                              (("2" (assert) nil)))))
                           ("2" (assert) nil)))))))))))))))))
           ("2" (expand "empty?")
            (("2" (expand "intersection")
              (("2" (expand "internal_verts")
                (("2" (expand "member")
                  (("2" (expand "finseq_appl")
                    (("2" (skosimp*)
                      (("2" (inst - "i!1" "i!2")
                        (("2" (assert) nil))))))))))))))))))))))
    nil)
   ((finite_intersection1 application-judgement "finite_set[T]"
     ind_paths nil)
    (indep? const-decl "bool" ind_paths nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (T formal-type-decl nil ind_paths nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (internal_verts const-decl "finite_set[T]" ind_paths nil)
    (member const-decl "bool" sets nil)
    (independent? const-decl "bool" ind_paths nil))
   nil)))


¤ Dauer der Verarbeitung: 0.23 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff