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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: class_equation_scaf.prf   Sprache: Lisp

Original von: PVS©
(class_equation_scaf
 (card_rest_aux_TCC1 0
  (card_rest_aux_TCC1-1 nil 3526046475
   ("" (skosimp*)
    (("" (typepred "FP!1")
      (("" (expand "finite_partition?")
        (("" (flatten)
          (("" (assert)
            (("" (lemma "Union_finite[T]")
              (("" (inst?) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil class_equation_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Union_finite formula-decl nil finite_sets_of_sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
   nil))
 (card_rest_aux_TCC2 0
  (card_rest_aux_TCC2-1 nil 3526046475
   ("" (skosimp*)
    (("" (typepred "FP!1")
      (("" (expand "finite_partition?")
        (("" (flatten)
          (("" (hide (-1 -2))
            (("" (expand "every") (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil class_equation_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (every const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil))
   nil))
 (card_rest_aux_TCC3 0
  (card_rest_aux_TCC3-1 nil 3526046475
   ("" (skosimp*)
    (("" (typepred "FP!1")
      (("" (expand "finite_partition?")
        (("" (flatten)
          (("" (lemma "Union_finite[T]")
            (("" (inst?)
              (("" (assert)
                (("" (hide (-1 2))
                  (("" (prop)
                    (("1" (rewrite "finite_rest") nil nil)
                     ("2" (expand "every")
                      (("2" (skosimp*)
                        (("2" (inst?)
                          (("2" (typepred "x!1")
                            (("2" (lemma "rest_member[setof[T]]")
                              (("2"
                                (inst -1 "FP!1" "x!1")
                                (("2"
                                  (expand "member")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil class_equation_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (rest const-decl "set" sets nil)
    (every const-decl "bool" sets nil)
    (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf
     nil)
    (x!1 skolem-const-decl "(rest[setof[T]](FP!1))" class_equation_scaf
     nil)
    (rest_member formula-decl nil sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_rest judgement-tcc nil finite_sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Union_finite formula-decl nil finite_sets_of_sets nil))
   nil))
 (card_rest_aux 0
  (card_rest_aux-1 nil 3526047645
   ("" (skosimp*)
    (("" (lemma "card_Union_rest")
      (("" (inst?)
        (("" (assert)
          (("" (replaces -1)
            (("" (rewrite "card_disj_union")
              (("" (hide 2)
                (("" (typepred "FP!1")
                  (("" (expand "finite_partition?")
                    (("" (flatten)
                      (("" (expand "partition?")
                        (("" (expand "disjoint?")
                          (("" (expand "empty?")
                            (("" (skosimp*)
                              ((""
                                (expand "member")
                                ((""
                                  (expand "intersection")
                                  ((""
                                    (expand "member")
                                    ((""
                                      (flatten)
                                      ((""
                                        (expand "Union")
                                        ((""
                                          (skosimp*)
                                          ((""
                                            (inst
                                             -1
                                             "a!1"
                                             "choose(FP!1)")
                                            (("1"
                                              (prop)
                                              (("1"
                                                (typepred "a!1")
                                                (("1"
                                                  (replaces -2)
                                                  (("1"
                                                    (hide
                                                     (-2 -3 -4 -5))
                                                    (("1"
                                                      (lemma
                                                       "choose_not_member[setof[T]]")
                                                      (("1"
                                                        (inst?)
                                                        (("1"
                                                          (expand
                                                           "nonempty?")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst?)
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but 1)
                                              (("2"
                                                (typepred "a!1")
                                                (("2"
                                                  (lemma
                                                   "rest_member[setof[T]]")
                                                  (("2"
                                                    (inst
                                                     -1
                                                     "FP!1"
                                                     "a!1")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil class_equation_scaf nil)
    (card_Union_rest formula-decl nil lagrange_scaf "algebra/")
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (card_disj_union formula-decl nil finite_sets 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)
    (Union const-decl "set" sets nil) (rest const-decl "set" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (disjoint? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (rest_member formula-decl nil sets_lemmas nil)
    (choose_not_member formula-decl nil sets_lemmas nil)
    (a!1 skolem-const-decl "(rest(FP!1))" class_equation_scaf nil)
    (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf
     nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (partition? const-decl "bool" lagrange_scaf "algebra/")
    (finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (card_partition_TCC1 0
  (card_partition_TCC1-1 nil 3526042692
   ("" (skosimp*)
    (("" (typepred "A!1")
      (("" (typepred "FP!1")
        (("" (expand "finite_partition?")
          (("" (flatten)
            (("" (expand "every") (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil class_equation_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (every const-decl "bool" sets nil))
   nil))
 (card_partition_TCC2 0
  (card_partition_TCC2-1 nil 3526042692
   ("" (skosimp*)
    (("" (expand "convergent?")
      (("" (prop)
        (("1" (typepred "FP!1")
          (("1" (expand "finite_partition?")
            (("1" (flatten)
              (("1" (hide -1)
                (("1" (rewrite "finite_countable")
                  (("1" (hide 2)
                    (("1" (expand "is_finite" (-1 1))
                      (("1" (skosimp)
                        (("1" (inst 1 "N!1" "f!1")
                          (("1" (hide (-2 -3))
                            (("1" (expand "injective?")
                              (("1" (grind) nil nil)) nil))
                            nil)
                           ("2" (skosimp*)
                            (("2" (prop)
                              (("1"
                                (expand "every")
                                (("1" (inst?) nil nil))
                                nil)
                               ("2"
                                (expand "nonzero_elts")
                                (("2"
                                  (expand "restrict")
                                  (("2"
                                    (assert)
                                    (("2" (inst?) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (expand "nonzero_elts")
                                (("3"
                                  (expand "restrict")
                                  (("3" (flatten) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "convergent?")
          (("2" (flatten)
            (("2" (hide 2)
              (("2" (typepred "FP!1")
                (("2" (expand "finite_partition?")
                  (("2" (flatten)
                    (("2" (hide -1)
                      (("2" (expand "is_finite" (-1 1))
                        (("2" (skosimp)
                          (("2" (inst 1 "N!1" "f!1")
                            (("1" (hide (-2 -3))
                              (("1"
                                (expand "injective?")
                                (("1" (grind) nil nil))
                                nil))
                              nil)
                             ("2" (skosimp*)
                              (("2"
                                (prop)
                                (("1"
                                  (expand "every")
                                  (("1" (inst?) nil nil))
                                  nil)
                                 ("2"
                                  (expand "nonzero_elts")
                                  (("2"
                                    (expand "restrict")
                                    (("2"
                                      (assert)
                                      (("2" (inst?) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (expand "nonzero_elts")
                                  (("3"
                                    (expand "restrict")
                                    (("3" (flatten) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set "sigma_set/")
    (convergent? const-decl "bool" countable_convergence "sigma_set/")
    (x!1 skolem-const-decl "setof[T]" class_equation_scaf nil)
    (finite_partition type-eq-decl nil lagrange_scaf "algebra/")
    (finite_partition? const-decl "bool" lagrange_scaf "algebra/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil class_equation_scaf nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_countable judgement-tcc nil countable_props "sets_aux/")
    (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)
    (nonzero_elts const-decl "set[T]" convergence_set "sigma_set/")
    (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 "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (restrict const-decl "R" restrict 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (FP!1 skolem-const-decl "finite_partition[T]" class_equation_scaf
     nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (injective? const-decl "bool" functions nil)
    (/= const-decl "boolean" notequal nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "setof[T]" class_equation_scaf nil)
    (every const-decl "bool" sets nil))
   nil))
 (card_partition 0
  (card_partition-1 nil 3526051917
   ("" (measure-induct+ "card(FP)" "FP")
    (("1" (inst -1 "rest(x!1)")
      (("1" (prop)
        (("1" (lemma "choose_rest[setof[T]]")
          (("1" (inst?)
            (("1" (expand "nonempty?")
              (("1" (assert)
                (("1" (rewrite "add_as_union")
                  (("1"
                    (name "ZZ"
                          "restrict[setof[T], finite_set[T], boolean](x!1)")
                    (("1" (replace -1 2)
                      (("1" (lemma "sigma_set.sigma_disjoint_union")
                        (("1"
                          (inst -1 "rest(x!1)" "singleton(choose(x!1))"
                           "card")
                          (("1" (prop)
                            (("1" (replace -4 -1 rl)
                              (("1"
                                (case
                                 "ZZ = union(restrict[setof[T], finite_set[T], boolean](rest(x!1)),
                                                    singleton(choose(x!1)))")
                                (("1"
                                  (replace -1 -2 rl)
                                  (("1"
                                    (replace -2 2)
                                    (("1"
                                      (lemma "card_rest_aux")
                                      (("1"
                                        (inst -1 "x!1")
                                        (("1"
                                          (expand "nonempty?")
                                          (("1"
                                            (replaces -1)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (hide-all-but 2)
                                                (("1"
                                                  (rewrite
                                                   "sigma_countable")
                                                  (("1"
                                                    (lemma
                                                     "sigma_countable.sigma_finite"
                                                     ("F"
                                                      "singleton(choose(x!1))"))
                                                    (("1"
                                                      (inst?)
                                                      (("1"
                                                        (case
                                                         "card(singleton(choose(x!1))) = 1")
                                                        (("1"
                                                          (replaces -1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (hide
                                                                 -1)
                                                                (("1"
                                                                  (expand
                                                                   "sigma")
                                                                  (("1"
                                                                    (expand
                                                                     "o ")
                                                                    (("1"
                                                                      (typepred
                                                                       "finite_enumeration(singleton(choose(x!1)))(0)")
                                                                      (("1"
                                                                        (expand
                                                                         "singleton")
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (replace
                                                                             -2)
                                                                            (("1"
                                                                              (expand
                                                                               "sigma")
                                                                              (("1"
                                                                                (propax)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide (-1 2))
                                                          (("2"
                                                            (rewrite
                                                             "card_def")
                                                            (("2"
                                                              (rewrite
                                                               "Card_bijection")
                                                              (("2"
                                                                (inst
                                                                 1
                                                                 "LAMBDA (y : (singleton(choose(x!1)))) : 0")
                                                                (("2"
                                                                  (grind)
                                                                  (("2"
                                                                    (inst
                                                                     1
                                                                     "choose(x!1)")
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (prop)
                                                        (("1"
                                                          (expand
                                                           "empty?")
                                                          (("1"
                                                            (inst
                                                             -1
                                                             "choose[setof[T]](x!1)")
                                                            (("1"
                                                              (expand
                                                               "member")
                                                              (("1"
                                                                (expand
                                                                 "singleton")
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (typepred
                                                               "x!1")
                                                              (("2"
                                                                (expand
                                                                 "finite_partition?")
                                                                (("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (expand
                                                                     "every")
                                                                    (("2"
                                                                      (inst
                                                                       -3
                                                                       "choose[setof[T]](x!1)")
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (lemma
                                                           "finite_singleton[(x!1)]")
                                                          (("2"
                                                            (inst
                                                             -1
                                                             "choose[setof[T]](x!1)")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (expand
                                                       "convergent?")
                                                      (("2"
                                                        (prop)
                                                        (("2"
                                                          (hide 2)
                                                          (("2"
                                                            (lemma
                                                             "finite_singleton[(x!1)]")
                                                            (("2"
                                                              (inst?)
                                                              (("2"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (hide 2)
                                                    (("3"
                                                      (rewrite
                                                       "finite_countable")
                                                      (("3"
                                                        (hide 2)
                                                        (("3"
                                                          (lemma
                                                           "finite_singleton[(x!1)]")
                                                          (("3"
                                                            (inst?)
                                                            (("3"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide (-1 -4 -5 3))
                                  (("2"
                                    (replace -2 -1 rl)
                                    (("2"
                                      (hide -2)
                                      (("2"
                                        (replace -1 1 rl)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (decompose-equality 1)
                                            (("2"
                                              (iff)
                                              (("2"
                                                (prop)
                                                (("1"
                                                  (expand*
                                                   "restrict"
                                                   "union"
                                                   "member")
                                                  (("1"
                                                    (prop)
                                                    (("1"
                                                      (hide (1 3))
                                                      (("1"
                                                        (grind)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand*
                                                   "restrict"
                                                   "union"
                                                   "member")
                                                  (("2"
                                                    (prop)
                                                    (("2"
                                                      (hide (1 3))
                                                      (("2"
                                                        (grind)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (1 2))
                              (("2"
                                (expand "disjoint?")
                                (("2"
                                  (expand "empty?" 1)
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (expand "intersection")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (expand "member")
                                            (("2"
                                              (expand "restrict")
                                              (("2"
                                                (expand "singleton")
                                                (("2"
                                                  (lemma
                                                   "choose_not_member[setof[T]]")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide-all-but (1 2))
                            (("2" (expand "convergent?")
                              (("2"
                                (prop)
                                (("1"
                                  (rewrite "finite_countable")
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (lemma
                                       "finite_union[finite_set[T]]")
                                      (("1"
                                        (case
                                         "nonzero_elts[finite_set[T]]
               (card[T],
                union[finite_set[T]]
                    (restrict[setof[T], finite_set[T], boolean]
                         (rest[setof[T]](x!1)),
                     singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]]
                    (restrict[setof[T], finite_set[T], boolean]
                         (rest[setof[T]](x!1)),
                     singleton[(x!1)](choose[setof[T]](x!1)))")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (hide 2)
                                                (("1"
                                                  (lemma
                                                   "finite_singleton[(x!1)]")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2)
                                                (("2"
                                                  (lemma
                                                   "finite_rest[setof[T]]")
                                                  (("2"
                                                    (inst?)
                                                    (("1"
                                                      (expand*
                                                       "is_finite"
                                                       "restrict")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (inst
                                                           1
                                                           "N!1"
                                                           "f!1")
                                                          (("1"
                                                            (expand
                                                             "injective?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (prop)
                                                              (("1"
                                                                (typepred
                                                                 "x!1")
                                                                (("1"
                                                                  (expand
                                                                   "finite_partition?")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (hide
                                                                       (-1
                                                                        -2
                                                                        -5
                                                                        2))
                                                                      (("1"
                                                                        (lemma
                                                                         "rest_member[setof[T]]")
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "x!1"
                                                                           "x!2")
                                                                          (("1"
                                                                            (expand
                                                                             "member")
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (expand
                                                                                 "every")
                                                                                (("1"
                                                                                  (inst?)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (expand
                                                                 "restrict")
                                                                (("2"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (expand
                                                                 "restrict")
                                                                (("3"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide (2 3))
                                                      (("2"
                                                        (typepred
                                                         "x!1")
                                                        (("2"
                                                          (expand
                                                           "finite_partition?")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2"
                                            (decompose-equality 1)
                                            (("2"
                                              (iff)
                                              (("2"
                                                (prop)
                                                (("1"
                                                  (expand
                                                   "nonzero_elts")
                                                  (("1"
                                                    (prop)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand
                                                   "nonzero_elts")
                                                  (("2"
                                                    (prop)
                                                    (("2"
                                                      (expand "union")
                                                      (("2"
                                                        (expand
                                                         "member")
                                                        (("2"
                                                          (expand
                                                           "restrict")
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (lemma
                                                               "rest_member[setof[T]]")
                                                              (("1"
                                                                (inst
                                                                 -1
                                                                 "x!1"
                                                                 "x!2")
                                                                (("1"
                                                                  (expand
                                                                   "member")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (reveal
                                                                       -7)
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "singleton")
                                                              (("2"
                                                                (reveal
                                                                 -6)
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "convergent?")
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (hide 2)
                                      (("2"
                                        (case
                                         "nonzero_elts(card[T],
                             union[finite_set[T]]
                                 (restrict[setof[T], finite_set[T], boolean]
                                      (rest[setof[T]](x!1)),
                                  singleton[(x!1)](choose[setof[T]](x!1)))) = union[finite_set[T]]
                                 (restrict[setof[T], finite_set[T], boolean]
                                      (rest[setof[T]](x!1)),
                                  singleton[(x!1)](choose[setof[T]](x!1)))")
                                        (("1"
                                          (replaces -1)
                                          (("1"
                                            (lemma
                                             "finite_union[finite_set[T]]")
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (hide 2)
                                                (("1"
                                                  (lemma
                                                   "finite_singleton[(x!1)]")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2)
                                                (("2"
                                                  (lemma
                                                   "finite_rest[setof[T]]")
                                                  (("2"
                                                    (inst?)
                                                    (("1"
                                                      (expand*
                                                       "is_finite"
                                                       "restrict")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (inst
                                                           1
                                                           "N!1"
                                                           "f!1")
                                                          (("1"
                                                            (expand
                                                             "injective?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (prop)
                                                              (("1"
                                                                (typepred
                                                                 "x!1")
                                                                (("1"
                                                                  (expand
                                                                   "finite_partition?")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (hide
                                                                       (-1
                                                                        -2
                                                                        -5
                                                                        2))
                                                                      (("1"
                                                                        (lemma
                                                                         "rest_member[setof[T]]")
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "x!1"
                                                                           "x!2")
                                                                          (("1"
                                                                            (expand
                                                                             "member")
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (expand
                                                                                 "every")
                                                                                (("1"
                                                                                  (inst?)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (expand
                                                                 "restrict")
                                                                (("2"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (expand
                                                                 "restrict")
                                                                (("3"
                                                                  (propax)
                                                                  nil
--> --------------------

--> maximum size reached

--> --------------------

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


Bot Zugriff