Quelle csequence_strict_prefix.prf Sprache: Lisp

(csequence_strict_prefix
(strict_prefix?_TCC1 0
  (strict_prefix?_TCC1-1 nil 3513690303 ("" (subtype-tcc) nil nil) nil
   nil))
(strict_prefix?_prefix? 0
  (strict_prefix?_prefix?-1 nil 3513690320
   ("" (skolem!)
    (("" (prop)
      (("1" (lemma "strict_prefix?_induction")
        (("1" (inst - "LAMBDA cseq1, cseq2: prefix?(cseq1, cseq2)")
          (("1" (split)
            (("1" (inst - "cseq1!1" "cseq2!1") (("1" (assert) nil nil))
              nil)
             ("2" (delete -1 2)
              (("2" (skosimp)
                (("2" (ground)
                  (("1" (expand "prefix?") (("1" (propax) nil nil))
                    nil)
                   ("2" (expand "prefix?" +) (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "strict_prefix?_induction")
        (("2" (inst - "LAMBDA cseq1, cseq2: cseq1 /= cseq2")
          (("2" (split)
            (("1" (inst - "cseq1!1" "cseq2!1") (("1" (assert) nil nil))
              nil)
             ("2" (delete -1 -2)
              (("2" (skosimp)
                (("2" (ground) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (use "prefix?_infinite")
        (("1" (assert) nil nil)
         ("2" (lemma "is_finite_induction")
          (("2"
            (inst -
             "LAMBDA cseq1: FORALL cseq2: prefix?(cseq1, cseq2) IMPLIES cseq1 = cseq2 OR strict_prefix?(cseq1, cseq2)")
            (("2" (split)
              (("1" (inst - "cseq1!1")
                (("1" (assert)
                  (("1" (inst - "cseq2!1") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (delete -1 -2 2 3)
                (("2" (skosimp*)
                  (("2" (expand "prefix?" -2)
                    (("2" (expand "strict_prefix?" +)
                      (("2" (ground)
                        (("2" (inst - "rest(cseq2!2)")
                          (("2" (assert)
                            (("2"
                              (forward-chain
                               "csequence_add_extensionality")
                              nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (prefix? coinductive-decl "bool" csequence_prefix nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (strict_prefix?_induction formula-decl nil csequence_strict_prefix
     nil)
    (/= const-decl "boolean" notequal nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (strict_prefix? inductive-decl "bool" csequence_strict_prefix nil)
    (cseq1!1 skolem-const-decl "csequence[T]" csequence_strict_prefix
     nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (prefix?_infinite formula-decl nil csequence_prefix nil))
   shostak))
(strict_prefix?_finite 0
  (strict_prefix?_finite-1 nil 3513690587
   ("" (skosimp)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (flatten) (("" (rewrite "prefix?_infinite") nil nil)) nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (prefix?_infinite formula-decl nil csequence_prefix nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil))
   shostak))
(strict_prefix?_first_TCC1 0
  (strict_prefix?_first_TCC1-1 nil 3513690303
   ("" (expand "strict_prefix?") (("" (skosimp) nil nil)) nil)
   ((strict_prefix? inductive-decl "bool" csequence_strict_prefix nil))
   nil))
(strict_prefix?_first 0
  (strict_prefix?_first-1 nil 3513690647
   ("" (expand "strict_prefix?") (("" (skosimp) nil nil)) nil)
   ((strict_prefix? inductive-decl "bool" csequence_strict_prefix nil))
   shostak))
(strict_prefix?_rest 0
  (strict_prefix?_rest-1 nil 3513690661
   ("" (expand "strict_prefix?" 1 1) (("" (skosimp) nil nil)) nil)
   ((strict_prefix? inductive-decl "bool" csequence_strict_prefix nil))
   shostak))
(strict_prefix?_length_TCC1 0
  (strict_prefix?_length_TCC1-1 nil 3513690303
   ("" (skosimp) (("" (forward-chain "strict_prefix?_finite") nil nil))
    nil)
   ((strict_prefix?_finite formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil))
   nil))
(strict_prefix?_length 0
  (strict_prefix?_length-1 nil 3513690705
   ("" (skosimp)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (flatten)
        (("" (forward-chain "prefix?_length")
          (("" (use "prefix?_length_eq") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (prefix?_length formula-decl nil csequence_prefix nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (prefix?_length_eq formula-decl nil csequence_prefix nil))
   shostak))
(strict_prefix?_index 0
  (strict_prefix?_index-1 nil 3513690739
   ("" (skosimp)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (flatten) (("" (forward-chain "prefix?_index") nil nil))
        nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (prefix?_index formula-decl nil csequence_prefix nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
(strict_prefix?_nth_TCC1 0
  (strict_prefix?_nth_TCC1-1 nil 3513690303
   ("" (skosimp :preds? t)
    (("" (forward-chain "strict_prefix?_index") nil nil)) nil)
   ((strict_prefix?_index formula-decl nil csequence_strict_prefix nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil))
   nil))
(strict_prefix?_nth 0
  (strict_prefix?_nth-1 nil 3513690796
   ("" (skosimp)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (flatten)
        (("" (use "prefix?_nth") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (prefix?_nth formula-decl nil csequence_prefix nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth 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))
   shostak))
(strict_prefix?_concatenate 0
  (strict_prefix?_concatenate-1 nil 3513690818
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "strict_prefix?" +)
        (("3" (ground)
          (("1" (rewrite "o_first") nil nil)
           ("2" (inst - "nseq!1") (("2" (rewrite "o_rest") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((o_nonempty_right application-judgement "nonempty_csequence[T]"
     csequence_strict_prefix nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (strict_prefix? inductive-decl "bool" csequence_strict_prefix nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(strict_prefix?_def 0
  (strict_prefix?_def-1 nil 3513690864
   ("" (skolem!)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (use "prefix?_def")
        (("" (smash)
          (("1" (skosimp)
            (("1" (inst + "cseq!1")
              (("1" (rewrite "o_empty_right") nil nil)) nil))
            nil)
           ("2" (skosimp) (("2" (rewrite "o_infinite") nil nil)) nil)
           ("3" (skosimp*)
            (("3" (lemma "o_finiteness")
              (("3" (inst - "cseq1!1" "nseq!1")
                (("3" (assert)
                  (("3" (lemma "o_length")
                    (("3" (inst - "cseq1!1" "nseq!1")
                      (("3" (use "length_empty?_rew")
                        (("3" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (skolem!) (("4" (inst + "nseq!1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_strict_prefix
     nil)
    (o_empty_right formula-decl nil csequence_concatenate nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (o_infinite formula-decl nil csequence_concatenate nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (o_finiteness formula-decl nil csequence_concatenate nil)
    (o_nonempty_right application-judgement "nonempty_csequence[T]"
     csequence_strict_prefix nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (o_length formula-decl nil csequence_concatenate nil)
    (prefix?_def formula-decl nil csequence_prefix nil))
   shostak))
(strict_prefix?_is_strict_order 0
  (strict_prefix?_is_strict_order-1 nil 3513690303
   ("" (expand* "strict_order?" "irreflexive?" "transitive?")
    (("" (split)
      (("1" (skolem!)
        (("1" (forward-chain "strict_prefix?_finite")
          (("1" (forward-chain "strict_prefix?_length")
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (skosimp)
        (("2" (lemma "strict_prefix?_finite")
          (("2" (inst-cp - "y!1" "z!1")
            (("2" (inst - "x!1" "y!1")
              (("2" (assert)
                (("2" (rewrite "strict_prefix?_prefix?")
                  (("2" (rewrite "strict_prefix?_prefix?")
                    (("2" (rewrite "strict_prefix?_prefix?")
                      (("2" (prop)
                        (("1" (use "prefix?_is_partial_order")
                          (("1"
                            (expand* "partial_order?" "preorder?"
                             "transitive?")
                            (("1" (flatten)
                              (("1"
                                (inst - "x!1" "y!1" "z!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2" (lemma "prefix?_length")
                            (("2" (inst-cp - "y!1" "z!1")
                              (("2"
                                (inst - "x!1" "y!1")
                                (("2"
                                  (assert)
                                  (("2"
                                    (lemma "prefix?_length_eq")
                                    (("2"
                                      (inst - "x!1" "y!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_prefix?_finite formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (strict_prefix?_length formula-decl nil csequence_strict_prefix
     nil)
    (strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (prefix?_length_eq formula-decl nil csequence_prefix nil)
    (prefix?_length formula-decl nil csequence_prefix nil)
    (prefix?_is_partial_order judgement-tcc nil csequence_prefix nil)
    (partial_order? const-decl "bool" orders nil)
    (preorder? const-decl "bool" orders nil)
    (strict_order? const-decl "bool" orders nil)
    (transitive? const-decl "bool" relations nil)
    (irreflexive? const-decl "bool" relations nil))
   nil))
(strict_prefix?_well_ordered 0
  (strict_prefix?_well_ordered-1 nil 3513691147
   ("" (skolem!)
    ((""
      (expand* "well_ordered?" "strict_total_order?" "restrict"
       "trichotomous?" "well_founded?")
      (("" (split)
        (("1" (skosimp* t)
          (("1" (rewrite "strict_prefix?_prefix?")
            (("1" (rewrite "strict_prefix?_prefix?")
              (("1" (rewrite "strict_prefix?_prefix?")
                (("1" (rewrite "strict_prefix?_prefix?")
                  (("1" (ground)
                    (("1" (lemma "prefix?_total_order")
                      (("1" (inst - "cseq!1")
                        (("1"
                          (expand* "restrict" "total_order?"
                           "dichotomous?")
                          (("1" (flatten)
                            (("1" (inst - "x!1" "y!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp* t)
          (("2" (forward-chain "strict_prefix?_finite")
            (("2"
              (name "min_length"
                    "min({n | EXISTS (seq: (p!1)): is_finite(seq) AND length(seq) = n})")
              (("1" (rewrite "min_def")
                (("1" (expand "minimum?")
                  (("1" (skosimp* t)
                    (("1" (inst + "seq!1")
                      (("1" (skolem-typepred)
                        (("1" (inst - "length(x!1)")
                          (("1" (split)
                            (("1" (lemma "strict_prefix?_length")
                              (("1"
                                (inst - "x!1" "seq!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (inst + "x!1")
                              (("2"
                                (forward-chain "strict_prefix?_finite")
                                nil
                                nil))
                              nil))
                            nil)
                           ("2" (forward-chain "strict_prefix?_finite")
                            nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand* "nonempty?" "empty?" "member")
                (("2" (inst - "length(y!1)")
                  (("2" (inst + "y!1") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_total_order? const-decl "bool" orders nil)
    (trichotomous? const-decl "bool" orders nil)
    (well_founded? const-decl "bool" orders nil)
    (restrict const-decl "R" restrict nil)
    (strict_order_restrict application-judgement "(strict_order?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (irreflexive_restrict application-judgement "(irreflexive?[S])"
     restrict_order_props nil)
    (well_ordered? const-decl "bool" orders nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (pred type-eq-decl nil defined_types nil)
    (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
         min_nat nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (minimum? const-decl "bool" min_nat nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_strict_prefix
     nil)
    (p!1 skolem-const-decl
     "pred[(LAMBDA (cseq1): strict_prefix?(cseq1, cseq!1))]"
     csequence_strict_prefix nil)
    (x!1 skolem-const-decl "(p!1)" csequence_strict_prefix nil)
    (strict_prefix?_length formula-decl nil csequence_strict_prefix
     nil)
    (strict_prefix?_is_strict_order name-judgement
     "(strict_order?[csequence])" csequence_strict_prefix nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (min_def formula-decl nil min_nat nil)
    (y!1 skolem-const-decl
     "(LAMBDA (cseq1): strict_prefix?(cseq1, cseq!1))"
     csequence_strict_prefix nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (strict_prefix?_finite formula-decl nil csequence_strict_prefix
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (strict_prefix? inductive-decl "bool" csequence_strict_prefix nil)
    (prefix?_total_order formula-decl nil csequence_prefix nil)
    (total_order? const-decl "bool" orders nil)
    (dichotomous? const-decl "bool" orders nil)
    (prefix? coinductive-decl "bool" csequence_prefix nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil))
   shostak))
(strict_prefix?_prefix 0
  (strict_prefix?_prefix-1 nil 3513691384
   ("" (skolem!)
    (("" (rewrite "strict_prefix?_prefix?")
      (("" (use "prefix?_prefix")
        (("" (ground)
          (("1" (skosimp)
            (("1" (assert)
              (("1" (use "prefix_length") (("1" (assert) nil nil))
                nil))
              nil))
            nil)
           ("2" (skolem!)
            (("2" (inst + "n!1")
              (("2" (ground)
                (("2" (use "prefix_full")
                  (("2" (rewrite "index?_finite")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (skosimp*)
            (("3" (assert)
              (("3" (use "prefix_length") (("3" (assert) nil nil))
                nil))
              nil))
            nil)
           ("4" (skosimp) (("4" (inst + "n!1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_prefix?_prefix? formula-decl nil csequence_strict_prefix
     nil)
    (T formal-type-decl nil csequence_strict_prefix nil)
    (csequence type-decl nil csequence_codt nil)
    (prefix?_is_partial_order name-judgement
     "(partial_order?[csequence])" csequence_strict_prefix nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (prefix_length formula-decl nil csequence_prefix nil)
    (prefix_full formula-decl nil csequence_prefix nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (prefix?_prefix formula-decl nil csequence_prefix nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.