products/sources/formale sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: xop725s.cob   Sprache: Lisp

(permutations_fseq
 (perm_length 0
  (perm_length-1 nil 3506271679
   ("" (skosimp*)
    (("" (expand "permutation?")
      (("" (skosimp*)
        (("" (expand "bijective?")
          (("" (flatten)
            ((""
              (lemma
               "injection_and_cardinal[below(length(A!1)),below(length(B!1))]")
              ((""
                (inst -1 "fullset[below(length(A!1))]"
                 "fullset[below(length(B!1))]")
                (("1" (split -1)
                  (("1"
                    (lemma
                     "surjection_and_cardinal[below(length(A!1)),below(length(B!1))]")
                    (("1"
                      (inst -1 "fullset[below(length(A!1))]"
                       "fullset[below(length(B!1))]")
                      (("1" (split -1)
                        (("1" (rewrite "card_below_fullset")
                          (("1" (rewrite "card_below_fullset")
                            (("1" (assert) nil)))))
                         ("2" (inst + "f!1")
                          (("1" (hide -1 -2 -4 2)
                            (("1" (expand "surjective?")
                              (("1"
                                (skosimp*)
                                (("1"
                                  (inst -1 "y!1")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (inst + "x!1")
                                      (("1"
                                        (expand "restrict")
                                        (("1" (propax) nil)))
                                       ("2"
                                        (expand "fullset")
                                        (("2"
                                          (propax)
                                          nil)))))))))))))))
                           ("2" (skosimp*)
                            (("2" (hide -1 -2 -3 2)
                              (("2"
                                (ground)
                                (("2" (grind) nil)))))))))))
                       ("2" (rewrite "finite_below") nil)
                       ("3" (rewrite "finite_below") nil)))))
                   ("2" (inst + "f!1")
                    (("1" (hide -2 -3 2)
                      (("1" (expand "injective?")
                        (("1" (skosimp*)
                          (("1" (expand "restrict")
                            (("1" (inst - "x1!1" "x2!1")
                              (("1" (assert) nil)))))))))))
                     ("2" (skosimp*)
                      (("2" (hide -1 -2 -3 2)
                        (("2" (grind) nil)))))))))
                 ("2" (rewrite "finite_below") nil)
                 ("3" (rewrite "finite_below") nil))))))))))))))
    nil)
   ((permutation? const-decl "bool" permutations_fseq nil)
    (bijective? const-decl "bool" functions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (fsq type-eq-decl nil fsq nil)
    (T formal-nonempty-type-decl nil permutations_fseq nil)
    (< const-decl "bool" reals 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)
    (injection_and_cardinal formula-decl nil finite_sets_card_eq
     "finite_sets/")
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (f!1 skolem-const-decl "[below(length(A!1)) -> below(length(B!1))]"
     permutations_fseq nil)
    (restrict const-decl "R" restrict nil)
    (surjective? const-decl "bool" functions nil)
    (x!1 skolem-const-decl "below(length(A!1))" permutations_fseq nil)
    (card_below_fullset formula-decl nil finite_sets_below
     "finite_sets/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (surjection_and_cardinal formula-decl nil finite_sets_card_eq
     "finite_sets/")
    (injective? const-decl "bool" functions nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (B!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
    (A!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (fullset const-decl "set" sets nil))
   nil))
 (perm_reflexive 0
  (perm_reflexive-1 nil 3506271679
   ("" (skosimp*)
    (("" (expand "permutation?")
      (("" (inst 1 "(LAMBDA (ii: below(length(A!1))): ii)")
        (("" (prop)
          (("1" (expand "bijective?") (("1" (grind) nil)))
           ("2" (skosimp*) (("2" (assert) nil))))))))))
    nil)
   ((permutation? const-decl "bool" permutations_fseq nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (fsq type-eq-decl nil fsq nil)
    (T formal-nonempty-type-decl nil permutations_fseq nil)
    (< const-decl "bool" reals 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))
 (perm_symmetric 0
  (perm_symmetric-1 nil 3506271679
   ("" (skosimp*)
    (("" (lemma "perm_length")
      (("" (inst?)
        (("" (assert)
          (("" (hide -1)
            (("" (expand "permutation?")
              (("" (skosimp*)
                (("" (case "length(A!1) = 0")
                  (("1" (inst 1 "(LAMBDA (ii: below(0)): 0)")
                    (("1" (grind) nil)
                     ("2" (skosimp*) (("2" (assert) nil)))
                     ("3" (skosimp*) nil) ("4" (skosimp*) nil)))
                   ("2" (inst + "inverse(f!1)")
                    (("1" (rewrite "bij_inv_is_bij")
                      (("1" (assert)
                        (("1" (skosimp*)
                          (("1" (inst -2 "inverse(f!1)(ii!1)")
                            (("1"
                              (case-replace
                               "f!1(inverse(f!1)(ii!1)) = ii!1")
                              (("1" (assert) nil)
                               ("2"
                                (hide -2 3)
                                (("2"
                                  (expand "bijective?")
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (lemma
                                       "surjective_inverse[below(length(A!1)),below(length(B!1))]")
                                      (("1"
                                        (inst
                                         -1
                                         "inverse(f!1)(ii!1)"
                                         "ii!1"
                                         "f!1")
                                        (("1" (assert) nil)
                                         ("2"
                                          (hide 2)
                                          (("2" (inst 1 "0") nil)))))
                                       ("2"
                                        (assert)
                                        (("2"
                                          (inst 1 "0")
                                          nil)))))))))))
                               ("3" (inst 1 "0") nil)))
                             ("2" (inst 1 "0") nil)))))))
                       ("2" (inst 1 "0") nil)))
                     ("2" (inst 1 "0")
                      (("2" (assert) nil))))))))))))))))))))
    nil)
   ((perm_length formula-decl nil permutations_fseq nil)
    (permutation? const-decl "bool" permutations_fseq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (B!1 skolem-const-decl "fsq[T]" permutations_fseq 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)
    (FALSE const-decl "bool" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (A!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
    (bij_inv_is_bij formula-decl nil function_inverse nil)
    (surjective_inverse formula-decl nil function_inverse nil)
    (f!1 skolem-const-decl "[below(length(A!1)) -> below(length(B!1))]"
     permutations_fseq nil)
    (inverse const-decl "D" function_inverse nil)
    (TRUE const-decl "bool" booleans nil)
    (fsq type-eq-decl nil fsq nil)
    (T formal-nonempty-type-decl nil permutations_fseq nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (perm_tran 0
  (perm_tran-1 nil 3506271679
   ("" (skosimp*)
    (("" (expand "permutation?")
      (("" (skosimp*)
        ((""
          (inst 1 "(LAMBDA (ii: below(length(A1!1))): f!2(f!1(ii)))")
          (("" (prop)
            (("1" (expand "bijective?")
              (("1" (prop)
                (("1" (expand "injective?")
                  (("1" (skosimp*)
                    (("1" (inst -5 "f!1(x1!1)" "f!1(x2!1)")
                      (("1" (inst -2 "x1!1" "x2!1")
                        (("1" (assert) nil)))))))))
                 ("2" (expand "surjective?")
                  (("2" (skosimp*)
                    (("2" (inst -5 "y!1")
                      (("2" (skosimp*)
                        (("2" (replace -5 * rl)
                          (("2" (inst -2 "x!1")
                            (("2" (skosimp*)
                              (("2"
                                (inst 1 "x!2")
                                (("2" (assert) nil)))))))))))))))))))))
             ("2" (skosimp*)
              (("2" (inst?)
                (("2" (inst?) (("2" (assert) nil))))))))))))))))
    nil)
   ((permutation? const-decl "bool" permutations_fseq 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)
    (T formal-nonempty-type-decl nil permutations_fseq nil)
    (fsq type-eq-decl nil fsq nil)
    (below type-eq-decl nil naturalnumbers nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil))
   nil))
 (perm_in? 0
  (perm_in?-1 nil 3506271679
   ("" (skosimp*)
    (("" (iff 1)
      (("" (prop)
        (("1" (expand "in?")
          (("1" (skosimp*)
            (("1" (expand "permutation?")
              (("1" (skosimp*)
                (("1" (inst -3 "ii!1")
                  (("1" (inst 1 "f!1(ii!1)")
                    (("1" (assert) nil)))))))))))))
         ("2" (expand "in?")
          (("2" (skosimp*)
            (("2" (lemma "perm_symmetric")
              (("2" (inst -1 "A1!1" "A2!1")
                (("2" (assert)
                  (("2" (hide -3)
                    (("2" (expand "permutation?")
                      (("2" (skosimp*)
                        (("2" (inst -2 "ii!1")
                          (("2" (inst 1 "f!1(ii!1)")
                            (("2" (assert)
                              nil))))))))))))))))))))))))))
    nil)
   ((perm_symmetric formula-decl nil permutations_fseq nil)
    (in? const-decl "bool" fsq nil)
    (permutation? const-decl "bool" permutations_fseq 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)
    (T formal-nonempty-type-decl nil permutations_fseq nil)
    (fsq type-eq-decl nil fsq nil)
    (below type-eq-decl nil naturalnumbers nil))
   nil)))

[ Verzeichnis aufwärts0.34unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]