Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: compatibility.prf Sprache: Lisp

Original von: PVS^©

(compatibility
(close_op?_TCC1 0
  (close_op?_TCC1-1 nil 3391347121 ("" (subtype-tcc) nil nil) nil nil))
(close_op?_TCC2 0
  (close_op?_TCC2-1 nil 3391347121 ("" (subtype-tcc) nil nil) nil nil))
(close_op?_TCC3 0
  (close_op?_TCC3-1 nil 3391347121 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
(close_op?_TCC4 0
  (close_op?_TCC4-1 nil 3391347121
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil))
(comp_op?_TCC1 0
  (comp_op?_TCC1-1 nil 3393127360 ("" (subtype-tcc) nil nil) nil nil))
(comp_op?_TCC2 0
  (comp_op?_TCC2-1 nil 3393127360 ("" (subtype-tcc) nil nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" compatibility 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)
    (symbol formal-nonempty-type-decl nil compatibility nil)
    (variable formal-nonempty-type-decl nil compatibility nil)
    (replace const-decl "finseq" seq_extras "structures/"))
   nil))
(comp_op?_TCC3 0
  (comp_op?_TCC3-1 nil 3393127360 ("" (subtype-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (arity_eq type-eq-decl nil compatibility nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (fs_len type-eq-decl nil seq_extras "structures/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" compatibility 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)
    (symbol formal-nonempty-type-decl nil compatibility nil)
    (variable formal-nonempty-type-decl nil compatibility nil)
    (replace const-decl "finseq" seq_extras "structures/"))
   nil))
(comp_op_iff_comp_cont 0
  (comp_op_iff_comp_cont-1 nil 3433010598
   ("" (skeep)
    (("" (expand* "comp_cont?" "comp_op?")
      (("" (split)
        (("1" (flatten)
          (("1" (measure-induct+ "length(p)" "p")
            (("1" (skeep)
              (("1" (skeep)
                (("1" (expand "replaceTerm" 1)
                  (("1" (lift-if)
                    (("1" (prop)
                      (("1" (inst -1 "rest(x!1)")
                        (("1" (inst -1 "args(s)(first(x!1) - 1)")
                          (("1" (lemma "fsepn.length_rest")
                            (("1" (inst?)
                              (("1"
                                (lemma "rest_of_positions")
                                (("1"
                                  (inst -1 "x!1" "s")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (inst -3 "r" "t")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (hide (-1 -2))
                                          (("1"
                                            (inst
                                             -4
                                             "arity(f(s))"
                                             "first(x!1) - 1"
                                             "f(s)"
                                             "replace(replaceTerm(args(s)(first(x!1) - 1), r, rest(x!1)), args(s), first(x!1) - 1)"
                                             "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))")
                                            (("1"
                                              (prop)
                                              (("1"
                                                (lemma
                                                 "fset.replace_n2")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "args(s)"
                                                   "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))"
                                                   "replaceTerm(args(s)(first(x!1) - 1), r, rest(x!1))")
                                                  (("1"
                                                    (prop)
                                                    (("1"
                                                      (inst
                                                       -1
                                                       "first(x!1) - 1")
                                                      (("1"
                                                        (replaces -1)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but
                                                       (-1 -4 1))
                                                      (("2"
                                                        (expand
                                                         "positionsOF")
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (expand
                                                               "only_empty_seq")
                                                              (("1"
                                                                (rewrite
                                                                 "empty_0")
                                                                nil
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "only_empty_seq")
                                                              (("2"
                                                                (rewrite
                                                                 "empty_0")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (lemma "fset.nth_x")
                                                (("2"
                                                  (inst
                                                   -1
                                                   "args(s)"
                                                   "replaceTerm(args(s)(first(x!1) - 1), r, rest(x!1))"
                                                   "first(x!1) - 1")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but (-2 1 2))
                                              (("2"
                                                (expand "positionsOF")
                                                (("2"
                                                  (lift-if)
                                                  (("2"
                                                    (prop)
                                                    (("1"
                                                      (expand
                                                       "only_empty_seq")
                                                      (("1"
                                                        (rewrite
                                                         "empty_0")
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand
                                                       "only_empty_seq")
                                                      (("2"
                                                        (rewrite
                                                         "empty_0")
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (expand*
                                                       "union"
                                                       "member"
                                                       "only_empty_seq")
                                                      (("3"
                                                        (prop)
                                                        (("1"
                                                          (rewrite
                                                           "empty_0")
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (expand
                                                           "IUnion")
                                                          (("2"
                                                            (skolem
                                                             *
                                                             "i1")
                                                            (("2"
                                                              (expand
                                                               "catenate")
                                                              (("2"
                                                                (skolem
                                                                 *
                                                                 "y")
                                                                (("2"
                                                                  (expand
                                                                   "member")
                                                                  (("2"
                                                                    (flatten)
                                                                    (("2"
                                                                      (hide
                                                                       -1)
                                                                      (("2"
                                                                        (lemma
                                                                         "fsepn.seq_first_rest")
                                                                        (("2"
                                                                          (inst?)
                                                                          (("2"
                                                                            (prop)
                                                                            (("2"
                                                                              (replaces
                                                                               -1
                                                                               -2)
                                                                              (("2"
                                                                                (lemma
                                                                                 "fsepn.first_equal")
                                                                                (("2"
                                                                                  (inst?)
                                                                                  (("2"
                                                                                    (assert)
                                                                                    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))
                              nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (skosimp*)
            (("2"
              (inst -1 "add_first(i!1 + 1, empty_seq)"
               "app(f!1, st1!1)")
              (("2" (prop)
                (("1" (inst -1 "st1!1(i!1)" "t!1")
                  (("1" (assert)
                    (("1" (expand "replaceTerm")
                      (("1" (lift-if)
                        (("1" (prop)
                          (("1" (assert)
                            (("1" (expand "add_first")
                              (("1"
                                (expand "insert?")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "fsepn.rest_add_first")
                            (("2" (inst -1 "empty_seq" "1 + i!1")
                              (("2"
                                (lemma "fsepn.first_add")
                                (("2"
                                  (inst -1 "empty_seq" "1 + i!1")
                                  (("2"
                                    (replaces -1)
                                    (("2"
                                      (replaces -1)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "replaceTerm")
                                          (("2"
                                            (lift-if)
                                            (("2"
                                              (prop)
                                              (("1"
                                                (lemma
                                                 "fset.replace_nth")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "st1!1"
                                                   "i!1")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide -1)
                                                (("2"
                                                  (rewrite "empty_0")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide (-1 2))
                  (("2" (expand "positionsOF")
                    (("2" (expand* "union" "member" "only_empty_seq")
                      (("2" (prop)
                        (("2" (hide 1)
                          (("2" (expand "IUnion")
                            (("2" (inst 1 "1 + i!1")
                              (("2"
                                (expand "catenate")
                                (("2"
                                  (inst 1 "empty_seq")
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (expand "positionsOF")
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (prop)
                                          (("1"
                                            (expand "only_empty_seq")
                                            (("1" (propax) nil nil))
                                            nil)
                                           ("2"
                                            (expand "only_empty_seq")
                                            (("2" (propax) nil nil))
                                            nil)
                                           ("3"
                                            (expand* "union" "member")
                                            (("3"
                                              (prop)
                                              (("3"
                                                (expand
                                                 "only_empty_seq")
                                                (("3"
                                                  (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)
   ((comp_op? const-decl "bool" compatibility nil)
    (comp_cont? const-decl "bool" compatibility nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (add_first const-decl "finseq" seq_extras "structures/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (app adt-constructor-decl
     "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
   (app?)]" term_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (insert? const-decl "finseq" seq_extras "structures/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (replace_nth formula-decl nil seq_extras "structures/")
    (first_add formula-decl nil seq_extras "structures/")
    (rest_add_first formula-decl nil seq_extras "structures/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (not_empty_seq type-eq-decl nil seq_extras "structures/")
    (first const-decl "T" seq_extras "structures/")
    (x!1 skolem-const-decl "position[variable, symbol, arity]"
     compatibility nil)
    (args adt-accessor-decl
          "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]"
          term_adt nil)
    (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (catenate const-decl "positions" positions nil)
    (upto? nonempty-type-eq-decl nil IUnion_extra nil)
    (<= const-decl "bool" reals nil)
    (first_equal formula-decl nil seq_extras "structures/")
    (seq_first_rest formula-decl nil seq_extras "structures/")
    (only_empty_seq const-decl "positions" positions nil)
    (empty_0 formula-decl nil seq_extras "structures/")
    (replace_n2 formula-decl nil seq_extras "structures/")
    (nth_x formula-decl nil seq_extras "structures/")
    (arity_eq type-eq-decl nil compatibility nil)
    (fs_len type-eq-decl nil seq_extras "structures/")
    (replace const-decl "finseq" seq_extras "structures/")
    (s skolem-const-decl "term[variable, symbol, arity]" compatibility
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rest_of_positions formula-decl nil positions nil)
    (length_rest formula-decl nil seq_extras "structures/")
    (finseq type-eq-decl nil finite_sequences nil)
    (rest const-decl "finseq" seq_extras "structures/")
    (replaceTerm def-decl "term" replacement nil)
    (positions? type-eq-decl nil positions nil)
    (positionsOF def-decl "positions" positions nil)
    (positions type-eq-decl nil positions nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (term type-decl nil term_adt nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (position type-eq-decl nil positions nil)
    (arity formal-const-decl "[symbol -> nat]" compatibility nil)
    (symbol formal-nonempty-type-decl nil compatibility nil)
    (variable formal-nonempty-type-decl nil compatibility nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (measure_induction formula-decl nil measure_induction nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
(closure_comp_op 0
  (closure_comp_op-1 nil 3433010729
   ("" (skeep)
    (("" (expand "comp_op?")
      (("" (split)
        (("1" (skosimp*)
          (("1" (expand "TC")
            (("1" (expand "IUnion")
              (("1" (skolem * "j")
                (("1" (generalize "st1!1" "st" :fnums (-1 1))
                  (("1" (generalize "t!1" "t" :fnums 1)
                    (("1" (generalize "f!1" "f" :fnums 1)
                      (("1" (generalize "j" "n" :fnums 1)
                        (("1" (induct "n")
                          (("1" (assert) nil nil)
                           ("2" (assert) nil nil)
                           ("3" (skosimp*)
                            (("3" (prop)
                              (("1"
                                (expand "iterate" -3)
                                (("1"
                                  (expand "o")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (inst -1 "f!2" "y!1" "st!1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst
                                             -5
                                             "arity(f!2)"
                                             "i!1"
                                             "f!2"
                                             "replace(y!1, st!1, i!1)"
                                             "t!2")
                                            (("1"
                                              (lemma "fset.nth_x")
                                              (("1"
                                                (prop)
                                                (("1"
                                                  (lemma
                                                   "fset.replace_n2")
                                                  (("1"
                                                    (inst
                                                     -1
                                                     "st1!1"
                                                     "t!2"
                                                     "y!1")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (inst -1 "i!1")
                                                        (("1"
                                                          (inst
                                                           1
                                                           "i!2 + 1")
                                                          (("1"
                                                            (expand
                                                             "iterate"
                                                             1)
                                                            (("1"
                                                              (expand
                                                               "o")
                                                              (("1"
                                                                (inst
                                                                 1
                                                                 "app(f!2, replace(y!1, st!1, i!1))")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (hide
                                                                     (-3
                                                                      -4
                                                                      -6))
                                                                    (("1"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (inst?)
                                                  (("2"
                                                    (hide-all-but
                                                     (-1 -5 1))
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (typepred "j!1")
                                (("2"
                                  (case "j!1 = 0")
                                  (("1"
                                    (replaces -1 -4)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (inst 2 "1")
                                        (("1"
                                          (inst
                                           -4
                                           "n!1"
                                           "i!1"
                                           "f!2"
                                           "st!1"
                                           "t!2")
                                          (("1"
                                            (rewrite "iterate_1")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("4" (grind) nil nil))
                          nil)
                         ("2" (grind) nil nil))
                        nil)
                       ("2" (grind) nil nil))
                      nil)
                     ("2" (grind) nil nil))
                    nil)
                   ("2" (grind) nil nil) ("3" (grind) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (expand "RTC")
            (("2" (expand "IUnion")
              (("2" (skolem * "j")
                (("2" (generalize "st1!1" "st" :fnums (-1 1))
                  (("1" (generalize "t!1" "t" :fnums 1)
                    (("1" (generalize "f!1" "f" :fnums 1)
                      (("1" (generalize "j" "n" :fnums 1)
                        (("1" (induct "n")
                          (("1" (skosimp*)
                            (("1" (expand "iterate" -1)
                              (("1"
                                (replace -1 1 rl)
                                (("1"
                                  (inst 1 "0")
                                  (("1"
                                    (lemma "fset.replace_nth")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (expand "iterate")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2" (expand "iterate" -2)
                              (("2"
                                (expand "o")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (inst -1 "f!2" "y!1" "st!1")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (inst
                                           -4
                                           "arity(f!2)"
                                           "i!1"
                                           "f!2"
                                           "replace(y!1, st!1, i!1)"
                                           "t!2")
                                          (("2"
                                            (lemma "fset.nth_x")
                                            (("2"
                                              (prop)
                                              (("1"
                                                (lemma
                                                 "fset.replace_n2")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "st1!1"
                                                   "t!2"
                                                   "y!1")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (inst -1 "i!1")
                                                      (("1"
                                                        (inst
                                                         1
                                                         "i!2 + 1")
                                                        (("1"
                                                          (expand
                                                           "iterate"
                                                           1)
                                                          (("1"
                                                            (expand
                                                             "o")
                                                            (("1"
                                                              (inst
                                                               1
                                                               "app(f!2, replace(y!1, st!1, i!1))")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-1
                                                                    -2
                                                                    1))
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst?)
                                                (("2"
                                                  (hide-all-but
                                                   (-1 -4 1))
                                                  (("2"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (grind) nil nil))
                          nil)
                         ("2" (grind) nil nil))
                        nil)
                       ("2" (grind) nil nil))
                      nil)
                     ("2" (grind) nil nil))
                    nil)
                   ("2" (grind) nil nil) ("3" (grind) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (skosimp*)
          (("3" (expand "EC")
            (("3" (expand "RTC")
              (("3" (expand "IUnion")
                (("3" (skolem * "j")
                  (("3" (generalize "st1!1" "st" :fnums (-1 1))
                    (("1" (generalize "t!1" "t" :fnums 1)
                      (("1" (generalize "f!1" "f" :fnums 1)
                        (("1" (generalize "j" "n" :fnums 1)
                          (("1" (induct "n")
                            (("1" (skosimp*)
                              (("1"
                                (inst 1 "0")
                                (("1"
                                  (hide -2)
                                  (("1"
                                    (expand "iterate")
                                    (("1"
                                      (replace -1 1 rl)
                                      (("1"
                                        (lemma "fset.replace_nth")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (inst?)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (skosimp*)
                              (("2"
                                (expand "iterate" -2)
                                (("2"
                                  (expand "o")
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (inst -1 "f!2" "y!1" "st!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (expand "SC" -3)
                                            (("2"
                                              (expand*
                                               "union"
                                               "member")
                                              (("2"
                                                (lemma "R_subset_SC")
                                                (("2"
                                                  (lemma "fset.nth_x")
                                                  (("2"
                                                    (lemma
                                                     "fset.replace_n2")
                                                    (("2"
                                                      (prop)
                                                      (("1"
                                                        (inst -4 "R")
                                                        (("1"
                                                          (expand*
                                                           "subset?"
                                                           "member")
                                                          (("1"
                                                            (inst
                                                             -7
                                                             "arity(f!2)"
                                                             "i!1"
                                                             "f!2"
                                                             "replace(y!1, st!1, i!1)"
                                                             "t!2")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (inst
                                                                 -2
                                                                 "st1!1"
                                                                 "t!2"
                                                                 "y!1")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (inst
                                                                     -2
                                                                     "i!1")
                                                                    (("1"
                                                                      (inst
                                                                       -4
                                                                       "(app(f!2, replace(y!1, st!1, i!1)), app(f!2, replace(t!2, replace(y!1, st!1, i!1), i!1)))")
                                                                      (("1"
                                                                        (inst
                                                                         1
                                                                         "i!2 + 1")
                                                                        (("1"
                                                                          (expand
                                                                           "iterate"
                                                                           1)
                                                                          (("1"
                                                                            (expand
                                                                             "o")
                                                                            (("1"
                                                                              (inst
                                                                               1
                                                                               "app(f!2, replace(y!1, st!1, i!1))")
                                                                              (("1"
                                                                                (grind)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (grind)
                                                                        nil
                                                                        nil)
                                                                       ("3"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (expand
                                                         "converse")
                                                        (("2"
                                                          (inst
                                                           -7
                                                           "arity(f!2)"
                                                           "i!1"
                                                           "f!2"
                                                           "replace(t!2, st!1, i!1)"
                                                           "y!1")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (inst
                                                               -2
                                                               "st1!1"
                                                               "y!1"
                                                               "t!2")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (inst
                                                                   -2
                                                                   "i!1")
                                                                  (("1"
                                                                    (inst
                                                                     1
                                                                     "i!2 + 1")
                                                                    (("1"
                                                                      (expand
                                                                       "iterate"
                                                                       1)
                                                                      (("1"
                                                                        (expand
                                                                         "o")
                                                                        (("1"
                                                                          (inst
                                                                           1
                                                                           "app(f!2, replace(y!1, st!1, i!1))")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (expand
                                                                               "SC"
                                                                               1)
                                                                              (("1"
                                                                                (expand*
                                                                                 "union"
                                                                                 "member")
                                                                                (("1"
                                                                                  (expand
                                                                                   "converse")
                                                                                  (("1"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (grind) nil nil))
                            nil)
                           ("2" (grind) nil nil))
                          nil)
                         ("2" (grind) nil nil))
                        nil)
                       ("2" (grind) nil nil))
                      nil)
                     ("2" (grind) nil nil) ("3" (grind) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((comp_op? const-decl "bool" compatibility nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (subset? const-decl "bool" sets nil)
    (y!1 skolem-const-decl "term[variable, symbol, arity]"
     compatibility nil)
    (st!1 skolem-const-decl
     "fs_len[term[variable, symbol, arity]](n!1)" compatibility nil)
    (t!2 skolem-const-decl "term[variable, symbol, arity]"
     compatibility nil)
    (f!2 skolem-const-decl "arity_eq(n!1)" compatibility nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (R_subset_SC formula-decl nil relations_closure nil)
    (i!1 skolem-const-decl "below[n!1]" compatibility nil)
    (n!1 skolem-const-decl "nat" compatibility nil)
    (PRED type-eq-decl nil defined_types nil)
    (symmetric? const-decl "bool" relations nil)
    (symmetric type-eq-decl nil relations_closure nil)
    (SC const-decl "symmetric" relations_closure nil)
    (EC const-decl "equivalence" relations_closure nil)
    (n!1 skolem-const-decl "nat" compatibility nil)
    (i!1 skolem-const-decl "below[n!1]" compatibility nil)
    (replace_nth formula-decl nil seq_extras "structures/")
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (replace const-decl "finseq" seq_extras "structures/")
    (arity_eq type-eq-decl nil compatibility nil)
    (app adt-constructor-decl
     "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] ->
   (app?)]" term_adt nil)
    (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (fs_len type-eq-decl nil seq_extras "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (< const-decl "bool" reals nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
    (pred type-eq-decl nil defined_types nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" compatibility nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (symbol formal-nonempty-type-decl nil compatibility nil)
    (variable formal-nonempty-type-decl nil compatibility nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (n!1 skolem-const-decl "nat" compatibility nil)
    (R skolem-const-decl "pred[[term, term]]" compatibility nil)
    (i!1 skolem-const-decl "below[n!1]" compatibility nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "bool" relation_props nil)
    (nth_x formula-decl nil seq_extras "structures/")
    (replace_n2 formula-decl nil seq_extras "structures/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (iterate_1 formula-decl nil relation_iterate "orders/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (TC const-decl "transitive" relations_closure nil))
   shostak))
(closure_comp_cont 0
  (closure_comp_cont-1 nil 3433011384
   ("" (skeep)
    (("" (lemma "comp_op_iff_comp_cont")
      (("" (lemma "closure_comp_op")
        (("" (copy -2)
          (("" (inst -1 "R")
            (("" (inst -2 "R")
              (("" (assert)
                (("" (copy -3)
                  (("" (copy -1)
                    (("" (flatten)
                      (("" (inst -7 "EC(R)")
                        (("" (inst -1 "TC(R)")
                          (("" (inst -2 "RTC(R)")
                            (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((comp_op_iff_comp_cont formula-decl nil compatibility nil)
    (TC const-decl "transitive" relations_closure nil)
    (transitive type-eq-decl nil relations_closure nil)
    (transitive? const-decl "bool" relations nil)
    (reflexive_transitive? const-decl "bool" relations_closure nil)
    (reflexive_transitive type-eq-decl nil relations_closure nil)
    (RTC const-decl "reflexive_transitive" relations_closure nil)
    (EC const-decl "equivalence" relations_closure nil)
    (equivalence type-eq-decl nil relations_closure nil)
    (equivalence? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (term type-decl nil term_adt nil)
--> --------------------

--> maximum size reached

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

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