Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: critical_pairs_aux.prf Sprache: Lisp

Original von: PVS^©

(critical_pairs_aux
(IMP_rewrite_rules_TCC1 0
  (IMP_rewrite_rules_TCC1-1 nil 3463227045
   ("" (lemma "var_countable") (("" (propax) nil nil)) nil)
   ((var_countable formula-decl nil critical_pairs_aux nil)) nil))
(CP_lemma_aux2b_TCC1 0
  (CP_lemma_aux2b_TCC1-1 nil 3420220323
   ("" (skosimp*)
    (("" (typepred "fstp!1")
      (("" (expand "SPP?")
        (("" (flatten)
          (("" (assert)
            (("" (hide -1)
              (("" (expand "SP?")
                (("" (skosimp*)
                  (("" (inst -1 "i!1")
                    (("" (expand "finseq_appl")
                      (("" (rewrite "ext_preserv_pos") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((SPP type-eq-decl nil positions nil)
    (SPP? const-decl "bool" positions nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (position type-eq-decl nil positions nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil nat_types nil)
    (term type-decl nil term_adt nil)
    (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil)
    (variable formal-nonempty-type-decl nil critical_pairs_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (Sub type-eq-decl nil substitution nil)
    (Sub? const-decl "bool" substitution nil)
    (V const-decl "set[term]" variables_term nil)
    (set type-eq-decl nil sets nil)
    (ext_preserv_pos formula-decl nil substitution nil)
    (< const-decl "bool" reals nil)
    (SP? const-decl "bool" positions nil))
   nil))
(CP_lemma_aux2b_TCC2 0
  (CP_lemma_aux2b_TCC2-1 nil 3455274769 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (variable formal-nonempty-type-decl nil critical_pairs_aux nil)
    (symbol formal-nonempty-type-decl nil critical_pairs_aux 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)
    (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil)
    (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
    (V const-decl "set[term]" variables_term nil)
    (Sub? const-decl "bool" substitution nil)
    (Sub type-eq-decl nil substitution nil)
    (below type-eq-decl nil nat_types nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (position type-eq-decl nil positions nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (SPP? const-decl "bool" positions nil)
    (SPP type-eq-decl nil positions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (SP? const-decl "bool" positions nil)
    (< const-decl "bool" reals nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(CP_lemma_aux2b 0
  (CP_lemma_aux2b-1 nil 3420225063
   ("" (measure-induct+ "length(fstp)" ("t" "fstp"))
    (("1" (skosimp*)
      (("1" (expand "finseq_appl")
        (("1" (case-replace "length(x!2) = 0")
          (("1" (hide-all-but (-1 1))
            (("1" (expand "replace_pos")
              (("1" (lift-if)
                (("1" (assert)
                  (("1" (expand "iterate") (("1" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "iterate" 2)
            (("2" (prop)
              (("2" (hide 3)
                (("2" (expand "o")
                  (("2"
                    (inst 2
                     "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2,length(x!2) - 1))")
                    (("1" (prop)
                      (("1"
                        (inst -1 "x!1" "delete(x!2, length(x!2) - 1)")
                        (("1" (inst -1 "R!1" "x!3" "sg1!1" "sg2!1")
                          (("1" (prop)
                            (("1"
                              (case "length(delete(x!2, length(x!2) - 1)) = length(x!2) - 1")
                              (("1" (replaces -1) nil nil)
                               ("2"
                                (hide-all-but (1 3))
                                (("2" (grind) nil nil))
                                nil)
                               ("3"
                                (hide-all-but (1 3))
                                (("3" (grind) nil nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-1 1 3))
                              (("2"
                                (skosimp*)
                                (("2"
                                  (lemma "fspos.delete_pos")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (inst -1 "i!1")
                                        (("1"
                                          (inst -2 "i!1")
                                          (("1"
                                            (expand "finseq_appl")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2"
                                            (typepred "i!1")
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (hide-all-but (1 3))
                              (("3" (rewrite "length_delete") nil nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but (1 3))
                          (("2" (typepred "x!2")
                            (("2" (expand "SPP?")
                              (("2"
                                (flatten)
                                (("2"
                                  (rewrite "delete_of_PP_is_PP")
                                  (("2"
                                    (rewrite "delete_of_SP_is_SP")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (hide-all-but (1 3))
                          (("3" (grind) nil nil)) nil))
                        nil)
                       ("2" (hide -1)
                        (("2" (lemma "preserv_unchanged_subterms")
                          (("2"
                            (inst -1 "ext(sg2!1)(x!3)"
                             "ext(sg1!1)(x!1)"
                             "delete(x!2, length(x!2) - 1)"
                             "last(x!2)")
                            (("1" (prop)
                              (("1"
                                (lemma "replace_subterm_of_term")
                                (("1"
                                  (inst
                                   -1
                                   "last(x!2)"
                                   "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1))")
                                  (("1"
                                    (prop)
                                    (("1"
                                      (replaces -2 -1)
                                      (("1"
                                        (expand "last")
                                        (("1"
                                          (expand "finseq_appl")
                                          (("1"
                                            (inst -2 "x!2`length - 1")
                                            (("1"
                                              (lemma
                                               "subterm_ext_commute")
                                              (("1"
                                                (inst
                                                 -1
                                                 "x!2`seq(x!2`length - 1)"
                                                 "x!1"
                                                 "sg1!1")
                                                (("1"
                                                  (prop)
                                                  (("1"
                                                    (replaces -1 -2)
                                                    (("1"
                                                      (replaces -2 -1)
                                                      (("1"
                                                        (expand*
                                                         "comp_cont?"
                                                         "RSigma")
                                                        (("1"
                                                          (inst
                                                           -3
                                                           "x!3")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (inst
                                                               -2
                                                               "x!2`seq(x!2`length - 1)"
                                                               "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1))")
                                                              (("1"
                                                                (prop)
                                                                (("1"
                                                                  (inst
                                                                   -1
                                                                   "sg1!1(x!3)"
                                                                   "sg2!1(x!3)")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (replace
                                                                       -2
                                                                       1
                                                                       rl)
                                                                      (("1"
                                                                        (hide
                                                                         (-2
                                                                          -3))
                                                                        (("1"
                                                                          (typepred
                                                                           "x!3")
                                                                          (("1"
                                                                            (expand
                                                                             "V")
                                                                            (("1"
                                                                              (expand
                                                                               "ext"
                                                                               1
                                                                               (3
                                                                                5))
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (case-replace
                                                                                   "replace_pos(ext(sg1!1)(x!1), sg2!1(x!3), x!2) = replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1)), sg2!1(x!3), x!2`seq(x!2`length - 1))")
                                                                                  (("1"
                                                                                    (hide-all-but
                                                                                     (1
                                                                                      3))
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "fspos.add_last_delete")
                                                                                      (("1"
                                                                                        (inst?)
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (name-replace
                                                                                             "RTermTemp"
                                                                                             "replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1)), sg2!1(x!3), x!2`seq(x!2`length - 1))")
                                                                                            (("1"
                                                                                              (hide
                                                                                               2)
                                                                                              (("1"
                                                                                                (replaces
                                                                                                 -1)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "RTermTemp")
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "CP_lemma_aux2a")
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       -1
                                                                                                       "sg2!1(x!3)"
                                                                                                       "ext(sg1!1)(x!1)"
                                                                                                       "delete(x!2, length(x!2) - 1)"
                                                                                                       "last(x!2)")
                                                                                                      (("1"
                                                                                                        (prop)
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "ext"
                                                                                                           1
                                                                                                           3)
                                                                                                          (("1"
                                                                                                            (expand*
                                                                                                             "last"
                                                                                                             "finseq_appl")
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (hide
                                                                                                           2)
                                                                                                          (("2"
                                                                                                            (case
                                                                                                             "length(x!2) = 1")
                                                                                                            (("1"
                                                                                                              (grind)
                                                                                                              nil
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (skosimp*)
                                                                                                              (("2"
                                                                                                                (typepred
                                                                                                                 "x!2")
                                                                                                                (("2"
                                                                                                                  (reveal
                                                                                                                   4)
                                                                                                                  (("2"
                                                                                                                    (lemma
                                                                                                                     "fspos.delete_pos")
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "finseq_appl")
                                                                                                                      (("2"
                                                                                                                        (inst?)
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          (("2"
                                                                                                                            (inst
                                                                                                                             -1
                                                                                                                             "i!1")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "SPP?")
                                                                                                                              (("1"
                                                                                                                                (flatten)
                                                                                                                                (("1"
                                                                                                                                  (hide
                                                                                                                                   -3)
                                                                                                                                  (("1"
                                                                                                                                    (expand*
                                                                                                                                     "last"
                                                                                                                                     "finseq_appl")
                                                                                                                                    (("1"
                                                                                                                                      (replace
                                                                                                                                       -1
                                                                                                                                       3
                                                                                                                                       rl)
                                                                                                                                      (("1"
                                                                                                                                        (expand
                                                                                                                                         "PP?")
                                                                                                                                        (("1"
                                                                                                                                          (inst
                                                                                                                                           -2
                                                                                                                                           "i!1"
                                                                                                                                           "x!2`length - 1")
                                                                                                                                          (("1"
                                                                                                                                            (expand
                                                                                                                                             "finseq_appl")
                                                                                                                                            (("1"
                                                                                                                                              (assert)
                                                                                                                                              (("1"
                                                                                                                                                (hide
                                                                                                                                                 (-1
                                                                                                                                                  4))
                                                                                                                                                (("1"
                                                                                                                                                  (typepred
                                                                                                                                                   "i!1")
                                                                                                                                                  (("1"
                                                                                                                                                    (grind)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil)
                                                                                                                             ("2"
                                                                                                                              (hide-all-but
                                                                                                                               1)
                                                                                                                              (("2"
                                                                                                                                (typepred
                                                                                                                                 "i!1")
                                                                                                                                (("2"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (hide
                                                                                                         2)
                                                                                                        (("2"
                                                                                                          (typepred
                                                                                                           "x!2")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "SPP?")
                                                                                                            (("2"
                                                                                                              (flatten)
                                                                                                              (("2"
                                                                                                                (hide
                                                                                                                 -1)
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "SP?")
                                                                                                                  (("2"
                                                                                                                    (expand*
                                                                                                                     "last"
                                                                                                                     "finseq_appl")
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -1
                                                                                                                       "x!2`length - 1")
                                                                                                                      (("2"
                                                                                                                        (rewrite
                                                                                                                         "ext_preserv_pos")
                                                                                                                        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"
                                                                  (hide-all-but
                                                                   (1
                                                                    3))
                                                                  (("2"
                                                                    (lemma
                                                                     "preserv_all_parallel_positions")
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "ext(sg2!1)(x!3)"
                                                                       "ext(sg1!1)(x!1)"
                                                                       "delete(x!2, length(x!2) - 1)"
                                                                       "x!2`seq(x!2`length - 1)")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (case
                                                                           "length(delete(x!2, length(x!2) - 1)) = 0")
                                                                          (("1"
                                                                            (hide
                                                                             2)
                                                                            (("1"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide
                                                                             3)
                                                                            (("2"
                                                                              (skosimp*)
                                                                              (("2"
                                                                                (typepred
                                                                                 "x!2")
                                                                                (("2"
                                                                                  (expand
                                                                                   "SPP?")
                                                                                  (("2"
                                                                                    (flatten)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "PP?")
                                                                                      (("2"
                                                                                        (prop)
                                                                                        (("1"
                                                                                          (hide
                                                                                           2)
                                                                                          (("1"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (lemma
                                                                                           "fspos.delete_pos")
                                                                                          (("2"
                                                                                            (inst?)
                                                                                            (("2"
                                                                                              (assert)
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -1
                                                                                                 "i!1")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "finseq_appl")
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -2
                                                                                                     "i!1"
                                                                                                     "x!2`length - 1")
                                                                                                    (("1"
                                                                                                      (prop)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (hide-all-but
                                                                                                         (-1
                                                                                                          4))
                                                                                                        (("2"
                                                                                                          (typepred
                                                                                                           "i!1")
                                                                                                          (("2"
                                                                                                            (grind)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (hide-all-but
                                                                                                   1)
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "i!1")
                                                                                                    (("2"
                                                                                                      (grind)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         2)
                                                                        (("2"
                                                                          (typepred
                                                                           "x!2")
                                                                          (("2"
                                                                            (expand
                                                                             "SPP?")
                                                                            (("2"
                                                                              (flatten)
                                                                              (("2"
                                                                                (hide
                                                                                 -1)
                                                                                (("2"
                                                                                  (expand
                                                                                   "SP?")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -1
                                                                                     "x!2`length - 1")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "finseq_appl")
                                                                                      (("2"
                                                                                        (rewrite
                                                                                         "ext_preserv_pos")
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (typepred "x!2")
                                                      (("2"
                                                        (expand "SPP?")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (hide -1)
                                                            (("2"
                                                              (expand
                                                               "SP?")
                                                              (("2"
                                                                (inst
                                                                 -1
                                                                 "x!2`length - 1")
                                                                (("1"
                                                                  (expand
                                                                   "finseq_appl")
                                                                  (("1"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   2)
                                                                  (("2"
                                                                    (reveal
                                                                     4)
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide-all-but (1 3))
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but (1 3))
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but (1 3))
                                      (("2"
                                        (expand* "last" "finseq_appl")
                                        (("2"
                                          (lemma
                                           "preserv_all_parallel_positions")
                                          (("2"
                                            (inst
                                             -1
                                             "ext(sg2!1)(x!3)"
                                             "ext(sg1!1)(x!1)"
                                             "delete(x!2, length(x!2) - 1)"
                                             "x!2`seq(x!2`length - 1)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (case
                                                 "length(delete(x!2, length(x!2) - 1)) = 0")
                                                (("1"
                                                  (hide 2)
                                                  (("1"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 3)
                                                  (("2"
                                                    (skosimp*)
                                                    (("2"
                                                      (typepred "x!2")
                                                      (("2"
                                                        (expand "SPP?")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (expand
                                                             "PP?")
                                                            (("2"
                                                              (prop)
                                                              (("1"
                                                                (hide
                                                                 2)
                                                                (("1"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (lemma
                                                                 "fspos.delete_pos")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "i!1")
                                                                      (("1"
                                                                        (inst
                                                                         -2
                                                                         "i!1"
                                                                         "x!2`length - 1")
                                                                        (("1"
                                                                          (prop)
                                                                          (("1"
                                                                            (expand
                                                                             "finseq_appl")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
--> --------------------

--> maximum size reached

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

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