Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: compute_sturm_tarski.pvs Sprache: Lisp

Original von: PVS^©

(prime_factorization
(prime_factorization 0
  (prime_factorization-7 nil 3411837217
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1" (inst 1 "fseq1(j!1)")
          (("1" (rewrite "product_fseq1")
            (("1" (skosimp*)
              (("1" (typepred "i!1")
                (("1" (expand "fseq1") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (inst -2 "x!1")
                        (("1" (split -2)
                          (("1" (split -3)
                            (("1" (skosimp*)
                              (("1"
                                (replace -5)
                                (("1"
                                  (hide -5)
                                  (("1"
                                    (inst 3 "fs!1 o fs!2")
                                    (("1"
                                      (rewrite "product_fseq_concat")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (hide -1 -3 -5)
                                            (("1"
                                              (expand "o")
                                              (("1"
                                                (ground)
                                                (("1" (inst?) nil nil)
                                                 ("2"
                                                  (hide -1)
                                                  (("2"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (typepred "i!1")
                                                  (("3"
                                                    (expand "o ")
                                                    (("3"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (hide -1 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (case "x!1 > 1")
                                    (("1"
                                      (lemma
                                       "both_sides_times_pos_lt1")
                                      (("1"
                                        (inst -1 "j!2" "1" "x!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma "pos_times_lt")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "j!1")
                            (("2" (typepred "j!2")
                              (("2"
                                (hide -4 4)
                                (("2"
                                  (lemma "pos_times_lt")
                                  (("2"
                                    (inst?)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide -2 4)
                            (("3" (replace -1)
                              (("3"
                                (hide -1)
                                (("3"
                                  (typepred "j!2")
                                  (("3"
                                    (lemma "pos_times_lt")
                                    (("3"
                                      (inst -1 "x!1" "j!2")
                                      (("3"
                                        (assert)
                                        (("3"
                                          (hide -2 4)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (typepred "j!2")
                                              (("3"
                                                (lemma
                                                 "both_sides_times_pos_lt1")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "x!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -2 4)
                            (("2" (replace -1)
                              (("2"
                                (hide -1)
                                (("2"
                                  (typepred "j!2")
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divides const-decl "bool" divides nil)
    (pos_times_lt formula-decl nil real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (product_fseq_concat formula-decl nil product_fseq_posnat "reals/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (O const-decl "fseq" fseqs "structures/")
    (x!1 skolem-const-decl "int" prime_factorization nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (fsq type-eq-decl nil fsq "structures/")
    (empty_seq const-decl "fsq" fseqs "structures/")
    (empty_seq_fseq name-judgement "fseq[posnat]" product_fseq_posnat
     "reals/")
    (j!1 skolem-const-decl "nat" prime_factorization nil)
    (fseq1 const-decl "fseq" fseqs "structures/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (product_fseq1 formula-decl nil product_fseq_posnat "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (prime? const-decl "bool" primes "ints/")
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (product const-decl "posnat" product_fseq_posnat "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (fseq type-eq-decl nil fseqs "structures/")
    (barray type-eq-decl nil fseqs "structures/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types 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)
  (prime_factorization-6 nil 3410695352
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1" (inst 1 "fseq1(j!1)")
          (("1" (rewrite "product_fseq1")
            (("1" (skosimp*)
              (("1" (typepred "i!1")
                (("1" (expand "fseq1") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (inst -2 "x!1")
                        (("1" (split -2)
                          (("1" (split -3)
                            (("1" (skosimp*)
                              (("1"
                                (replace -5)
                                (("1"
                                  (hide -5)
                                  (("1"
                                    (inst 3 "fs!1 o fs!2")
                                    (("1"
                                      (rewrite "product_fseq_mult")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (hide -1 -3 -5)
                                            (("1"
                                              (expand "o")
                                              (("1"
                                                (ground)
                                                (("1" (inst?) nil nil)
                                                 ("2"
                                                  (hide -1)
                                                  (("2"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (typepred "i!1")
                                                  (("3"
                                                    (expand "o ")
                                                    (("3"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (hide -1 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (case "x!1 > 1")
                                    (("1"
                                      (lemma
                                       "both_sides_times_pos_lt1")
                                      (("1"
                                        (inst -1 "j!2" "1" "x!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma "pos_times_lt")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "j!1")
                            (("2" (typepred "j!2")
                              (("2"
                                (hide -4 4)
                                (("2"
                                  (lemma "pos_times_lt")
                                  (("2"
                                    (inst?)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide -2 4)
                            (("3" (replace -1)
                              (("3"
                                (hide -1)
                                (("3"
                                  (typepred "j!2")
                                  (("3"
                                    (lemma "pos_times_lt")
                                    (("3"
                                      (inst -1 "x!1" "j!2")
                                      (("3"
                                        (assert)
                                        (("3"
                                          (hide -2 4)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (typepred "j!2")
                                              (("3"
                                                (lemma
                                                 "both_sides_times_pos_lt1")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "x!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -2 4)
                            (("2" (replace -1)
                              (("2"
                                (hide -1)
                                (("2"
                                  (typepred "j!2")
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((default const-decl "T" fseqs "structures/")
    (fseq type-eq-decl nil fseqs "structures/")
    (prime? const-decl "bool" primes "ints/")
    (fseq1 const-decl "fseq" fseqs "structures/")
    (empty_seq const-decl "fsq" fseqs "structures/")
    (O const-decl "fseq" fseqs "structures/"))
   nil)
  (prime_factorization-5 nil 3410609469
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1" (inst 1 "gen1(j!1)")
          (("1" (rewrite "product_gen1")
            (("1" (skosimp*)
              (("1" (typepred "i!1")
                (("1" (expand "gen1") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (inst -2 "x!1")
                        (("1" (split -2)
                          (("1" (split -3)
                            (("1" (skosimp*)
                              (("1"
                                (replace -5)
                                (("1"
                                  (hide -5)
                                  (("1"
                                    (inst 3 "fs!1 o fs!2")
                                    (("1"
                                      (rewrite "product_fseq_mult")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (hide -1 -3 -5)
                                            (("1"
                                              (expand "o")
                                              (("1"
                                                (ground)
                                                (("1" (inst?) nil nil)
                                                 ("2"
                                                  (hide -1)
                                                  (("2"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (typepred "i!1")
                                                  (("3"
                                                    (expand "o ")
                                                    (("3"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (hide -1 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (case "x!1 > 1")
                                    (("1"
                                      (lemma
                                       "both_sides_times_pos_lt1")
                                      (("1"
                                        (inst -1 "j!2" "1" "x!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma "pos_times_lt")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "j!1")
                            (("2" (typepred "j!2")
                              (("2"
                                (hide -4 4)
                                (("2"
                                  (lemma "pos_times_lt")
                                  (("2"
                                    (inst?)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide -2 4)
                            (("3" (replace -1)
                              (("3"
                                (hide -1)
                                (("3"
                                  (typepred "j!2")
                                  (("3"
                                    (lemma "pos_times_lt")
                                    (("3"
                                      (inst -1 "x!1" "j!2")
                                      (("3"
                                        (assert)
                                        (("3"
                                          (hide -2 4)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (typepred "j!2")
                                              (("3"
                                                (lemma
                                                 "both_sides_times_pos_lt1")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "x!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -2 4)
                            (("2" (replace -1)
                              (("2"
                                (hide -1)
                                (("2"
                                  (typepred "j!2")
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "fseq" fseqs "structures/")
    (empty_seq const-decl "fsq" fseqs "structures/")
    (prime? const-decl "bool" primes "ints/")
    (fseq type-eq-decl nil fseqs "structures/")
    (default const-decl "T" fseqs "structures/"))
   nil)
  (prime_factorization-4 nil 3410543419
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1"
          (inst 1 "(# length := 1, seq := (LAMBDA (i: nat): j!1) #)")
          (("1" (assert)
            (("1" (expand "product") (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (inst -2 "x!1")
                        (("1" (split -2)
                          (("1" (split -3)
                            (("1" (skosimp*)
                              (("1"
                                (replace -5)
                                (("1"
                                  (hide -5)
                                  (("1"
                                    (inst 3 "fs!1 ++ fs!2")
                                    (("1"
                                      (rewrite "product_mult")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (hide -1 -3 -5)
                                            (("1"
                                              (expand "++")
                                              (("1"
                                                (ground)
                                                (("1" (inst?) nil nil)
                                                 ("2"
                                                  (hide -1)
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (typepred "i!1")
                                                      (("2"
                                                        (expand "++ ")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (hide -1 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (case "x!1 > 1")
                                    (("1"
                                      (lemma
                                       "both_sides_times_pos_lt1")
                                      (("1"
                                        (inst -1 "j!2" "1" "x!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma "pos_times_lt")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "j!1")
                            (("2" (typepred "j!2")
                              (("2"
                                (hide -4 4)
                                (("2"
                                  (lemma "pos_times_lt")
                                  (("2"
                                    (inst?)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide -2 4)
                            (("3" (replace -1)
                              (("3"
                                (hide -1)
                                (("3"
                                  (typepred "j!2")
                                  (("3"
                                    (lemma "pos_times_lt")
                                    (("3"
                                      (inst -1 "x!1" "j!2")
                                      (("3"
                                        (assert)
                                        (("3"
                                          (hide -2 4)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (typepred "j!2")
                                              (("3"
                                                (lemma
                                                 "both_sides_times_pos_lt1")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "x!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -2 4)
                            (("2" (replace -1)
                              (("2"
                                (hide -1)
                                (("2"
                                  (typepred "j!2")
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((prime? const-decl "bool" primes "ints/")
    (product_eq_arg formula-decl nil product "reals/")
    (prod_nat application-judgement "nat" product_nat "reals/"))
   nil)
  (prime_factorization-3 nil 3407856976
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1"
          (inst 1 "(# length := 1, seq := (LAMBDA (i: nat): j!1) #)")
          (("1" (assert)
            (("1" (expand "product")
              (("1" (assert) (("1" (rewrite "product_eq_arg") nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (inst -2 "x!1")
                        (("1" (split -2)
                          (("1" (split -3)
                            (("1" (skosimp*)
                              (("1"
                                (replace -5)
                                (("1"
                                  (hide -5)
                                  (("1"
                                    (inst 3 "fs!1 o fs!2")
                                    (("1"
                                      (rewrite "product_mult")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (hide -1 -3 -5)
                                            (("1"
                                              (expand "o ")
                                              (("1"
                                                (ground)
                                                (("1" (inst?) nil nil)
                                                 ("2"
                                                  (hide -1)
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (typepred "i!1")
                                                      (("2"
                                                        (expand "o ")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (hide -1 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (case "x!1 > 1")
                                    (("1"
                                      (lemma
                                       "both_sides_times_pos_lt1")
                                      (("1"
                                        (inst -1 "j!2" "1" "x!1")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (lemma "pos_times_lt")
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (typepred "j!1")
                            (("2" (typepred "j!2")
                              (("2"
                                (hide -4 4)
                                (("2"
                                  (lemma "pos_times_lt")
                                  (("2"
                                    (inst?)
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide -2 4)
                            (("3" (replace -1)
                              (("3"
                                (hide -1)
                                (("3"
                                  (typepred "j!2")
                                  (("3"
                                    (lemma "pos_times_lt")
                                    (("3"
                                      (inst -1 "x!1" "j!2")
                                      (("3"
                                        (assert)
                                        (("3"
                                          (hide -2 4)
                                          (("3"
                                            (hide -1)
                                            (("3"
                                              (typepred "j!2")
                                              (("3"
                                                (lemma
                                                 "both_sides_times_pos_lt1")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "x!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (hide -2 4)
                            (("2" (replace -1)
                              (("2"
                                (hide -1)
                                (("2"
                                  (typepred "j!2")
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "fseq" fseqs "structures/")
    (empty_seq const-decl "fsq" fseqs "structures/")
    (product_eq_arg formula-decl nil product "reals/")
    (prod_nat application-judgement "nat" product_nat "reals/")
    (prime? const-decl "bool" primes "ints/")
    (fseq type-eq-decl nil fseqs "structures/"))
   nil)
  (prime_factorization-2 nil 3407849196
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1"
          (inst 1
           "(# length := 1, seq := (LAMBDA (i: below(1)): j!1) #)")
          (("1" (assert)
            (("1" (expand "product")
              (("1" (expand "product_rec") (("1" (propax) nil nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*) nil nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides?")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (assert)
                        (("1" (inst -2 "k!1")
                          (("1" (split -2)
                            (("1" (split -3)
                              (("1"
                                (skosimp*)
                                (("1"
                                  (replace -5)
                                  (("1"
                                    (hide -5)
                                    (("1"
                                      (inst 3 "fs!1 o fs!2")
                                      (("1"
                                        (rewrite "product_mult")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (hide -1 -3 -5)
                                              (("1"
                                                (expand "o ")
                                                (("1"
                                                  (ground)
                                                  (("1"
                                                    (inst?)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (hide -1)
                                                    (("2"
                                                      (inst
                                                       -1
                                                       "i!1 - length(fs!1)")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (hide -1 4)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (hide -1)
                                      (("2"
                                        (case "k!1 > 1")
                                        (("1"
                                          (lemma
                                           "both_sides_times_pos_lt1")
                                          (("1"
                                            (inst -1 "j!2" "1" "k!1")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (lemma "pos_times_lt")
                                            (("2"
                                              (inst?)
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (typepred "j!1")
                              (("2"
                                (typepred "j!2")
                                (("2"
                                  (hide -4 4)
                                  (("2"
                                    (lemma "pos_times_lt")
                                    (("2"
                                      (inst?)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (hide -2 4)
                              (("3"
                                (replace -1)
                                (("3"
                                  (hide -1)
                                  (("3"
                                    (typepred "j!2")
                                    (("3"
                                      (lemma "pos_times_lt")
                                      (("3"
                                        (inst -1 "k!1" "j!2")
                                        (("3"
                                          (assert)
                                          (("3"
                                            (hide -2 4)
                                            (("3"
                                              (hide -1)
                                              (("3"
                                                (typepred "j!2")
                                                (("3"
                                                  (lemma
                                                   "both_sides_times_pos_lt1")
                                                  (("3"
                                                    (inst
                                                     -1
                                                     "k!1"
                                                     "1"
                                                     "j!2")
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (hide -2 4)
                              (("2"
                                (replace -1)
                                (("2"
                                  (hide -1)
                                  (("2"
                                    (typepred "j!2")
                                    (("2"
                                      (lemma "pos_times_lt")
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (hide -1)
                  (("2" (inst + "empty_seq[posnat]")
                    (("2" (expand "empty_seq")
                      (("2" (expand "product")
                        (("2" (skosimp*)
                          (("2" (typepred "i!1")
                            (("2" (expand "empty_seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((prime? const-decl "bool" primes "ints/")) nil)
  (prime_factorization-1 nil 3282645260
   ("" (induct "m" 1 "NAT_induction")
    (("1" (assert) nil nil)
     ("2" (skosimp*)
      (("2" (case "prime?(j!1)")
        (("1"
          (inst 1
           "(# length := 1, seq := (LAMBDA (i: below(1)): j!1) #)")
          (("1" (assert)
            (("1" (expand "product")
              (("1" (expand "product_rec") (("1" (propax) nil nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*) nil nil))
          nil)
         ("2" (assert)
          (("2" (expand "prime?" 1)
            (("2" (split +)
              (("1" (skosimp*)
                (("1" (expand "divides")
                  (("1" (skosimp*)
                    (("1" (inst-cp -2 "j!2")
                      (("1" (assert)
                        (("1" (inst -2 "k!1")
                          (("1" (split -2)
                            (("1" (split -3)
                              (("1"
                                (skosimp*)
                                (("1"
                                  (replace -5)
                                  (("1"
                                    (hide -5)
                                    (("1"
                                      (inst 3 "fs!1 o fs!2")
                                      (("1"
                                        (rewrite "product_mult")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (hide -1 -3 -5)
                                              (("1"
                                                (expand "o ")
                                                (("1"
                                                  (ground)
                                                  (("1"
                                                    (inst?)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (hide -1)
                                                    (("2"
                                                      (inst
                                                       -1
                                                       "i!1 - length(fs!1)")
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (typepred
                                                           "i!1")
                                                          (("2"
                                                            (expand
                                                             "o ")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (hide -1 4)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (hide -1)
                                      (("2"
                                        (case "k!1 > 1")
                                        (("1"
                                          (lemma
                                           "both_sides_times_pos_lt1")
                                          (("1"
                                            (inst -1 "j!2" "1" "k!1")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
--> --------------------

--> maximum size reached

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

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