products/sources/formale Sprachen/PVS/graphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Tauto.v   Sprache: PVS

Untersuchung PVS©
(min_walk_reduced
 (reduced?_TCC1 0
  (reduced?_TCC1-1 nil 3251113238
   ("" (skosimp*) (("" (assert) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (reduced?_TCC2 0
  (reduced?_TCC2-1 nil 3251113238
   ("" (skosimp*) (("" (assert) nil)) nil)
   ((nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (min_walk_vert 0
  (min_walk_vert-1 nil 3251113238
   ("" (skosimp*)
    (("" (expand "finseq_appl")
      (("" (lemma "min_walk_in")
        (("" (inst?)
          (("" (expand "walk_from?")
            (("" (flatten)
              (("" (expand "walk?")
                (("" (flatten)
                  (("" (hide -4)
                    (("" (expand "verts_in?")
                      (("" (inst -3 "i!1") nil))))))))))))))))))))
    nil)
   ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences 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)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (verts_in? const-decl "bool" walks nil)
    (Seq type-eq-decl nil walks nil)
    (walk_from? const-decl "bool" walks nil)
    (gr_walk type-eq-decl nil min_walks nil)
    (below type-eq-decl nil naturalnumbers nil)
    (min_walk_from const-decl "Walk(Gw)" min_walks nil)
    (Walk type-eq-decl nil walks nil) (< const-decl "bool" reals 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)
    (walk? const-decl "bool" walks nil)
    (min_walk_in formula-decl nil min_walks nil)
    (T formal-type-decl nil min_walk_reduced nil))
   nil))
 (min_walk_is_reduced_TCC1 0
  (min_walk_is_reduced_TCC1-1 nil 3251113238
   ("" (skosimp*)
    (("" (expand "verts_in?")
      (("" (skosimp*)
        (("" (lemma "min_walk_vert")
          (("" (inst?)
            (("" (inst?)
              (("" (assert)
                (("" (expand finseq_appl) (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((verts_in? const-decl "bool" walks nil)
    (min_walk_vert formula-decl nil min_walk_reduced 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) (< const-decl "bool" reals nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (min_walk_from const-decl "Walk(Gw)" min_walks nil)
    (below type-eq-decl nil naturalnumbers nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gr_walk type-eq-decl nil min_walks nil)
    (walk_from? const-decl "bool" walks nil)
    (Seq type-eq-decl nil walks nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals 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)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil min_walk_reduced nil))
   nil))
 (min_walk_is_reduced 0
  (min_walk_is_reduced-3 nil 3251113531
   ("" (skosimp*)
    (("" (expand "reduced?")
      (("" (expand "finseq_appl")
        (("" (skosimp*)
          (("" (name MIN_W "min_walk_from(x!1,y!1,Gw!1)")
            (("" (replace -1)
              (("" (lemma "min_walk_is_min")
                (("" (inst?)
                  (("" (lemma "min_walk_in")
                    (("" (inst?)
                      (("" (replace -3)
                        (("" (expand "walk_from?")
                          (("" (flatten)
                            (("" (case "k!1 = length(MIN_W) - 2")
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (name
                                       RED_W
                                       "MIN_W ^ (0, length(MIN_W) - 3)")
                                      (("1"
                                        (inst -5 "RED_W")
                                        (("1"
                                          (replace -1 * rl)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (expand*
                                               "^"
                                               min
                                               empty_seq)
                                              (("1"
                                                (expand "walk?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (expand
                                                     "verts_in?")
                                                    (("1"
                                                      (split +)
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst?)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "finseq_appl")
                                                          (("2"
                                                            (hide -4)
                                                            (("2"
                                                              (inst
                                                               -4
                                                               "n!1")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (prop)
                                          (("1"
                                            (replace -1 * rl)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (expand*
                                                 "^"
                                                 min
                                                 empty_seq)
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "verts_in?")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (replace -1 * rl)
                                                (("2"
                                                  (typepred "i!1")
                                                  (("2"
                                                    (replace -2 * rl)
                                                    (("2"
                                                      (hide -2)
                                                      (("2"
                                                        (expand*
                                                         "^"
                                                         min
                                                         empty_seq)
                                                        (("2"
                                                          (expand
                                                           "walk?")
                                                          (("2"
                                                            (flatten)
                                                            (("2"
                                                              (hide -5)
                                                              (("2"
                                                                (expand
                                                                 "verts_in?")
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "i!1")
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (inst
                                 -4
                                 "MIN_W ^ (0, k!1 - 1) o MIN_W ^ (2 + k!1, length(MIN_W) - 1)")
                                (("1"
                                  (split -4)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (expand "empty_seq")
                                        (("1"
                                          (lift-if)
                                          (("1"
                                            (lift-if)
                                            (("1" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (expand "o ")
                                    (("2"
                                      (expand* "^" min empty_seq)
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (expand "empty_seq")
                                          (("2"
                                            (lift-if)
                                            (("2" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (expand "o ")
                                    (("3"
                                      (expand* "^" min empty_seq)
                                      (("3"
                                        (expand "empty_seq")
                                        (("3"
                                          (lift-if)
                                          (("3"
                                            (lift-if)
                                            (("3" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("4"
                                    (lemma "walk?_cut")
                                    (("4"
                                      (inst?)
                                      (("1"
                                        (inst -1 "Gw!1" "x!1" "y!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "walk_from?")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil)
                                       ("3" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (split +)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (lift-if)
                                        (("1" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (expand "verts_in?")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (typepred "i!1")
                                        (("2"
                                          (expand "o ")
                                          (("2"
                                            (expand* "^" min empty_seq)
                                            (("2"
                                              (lift-if)
                                              (("2"
                                                (expand "walk?")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (hide -5)
                                                    (("2"
                                                      (expand
                                                       "verts_in?")
                                                      (("2"
                                                        (ground)
                                                        (("1"
                                                          (inst?)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (inst?)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3" (assert) nil nil)
                                 ("4" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((reduced? const-decl "bool" min_walk_reduced nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "finseq" finite_sequences nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (Gw!1 skolem-const-decl "gr_walk[T](x!1, y!1)" min_walk_reduced
     nil)
    (y!1 skolem-const-decl "T" min_walk_reduced nil)
    (x!1 skolem-const-decl "T" min_walk_reduced nil)
    (RED_W skolem-const-decl "finseq[T]" min_walk_reduced nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (even_minus_even_is_even application-judgement "even_int" integers
     nil)
    (walk?_cut formula-decl nil walks nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (O const-decl "finseq" finite_sequences nil)
    (MIN_W skolem-const-decl "Walk[T](Gw!1)" min_walk_reduced nil)
    (k!1 skolem-const-decl "nat" min_walk_reduced nil)
    (min_walk_in formula-decl nil min_walks nil)
    (min_walk_is_min formula-decl nil min_walks nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil min_walk_reduced nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs 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)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (verts_in? const-decl "bool" walks nil)
    (Seq type-eq-decl nil walks nil)
    (walk_from? const-decl "bool" walks nil)
    (gr_walk type-eq-decl nil min_walks nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (min_walk_from const-decl "Walk(Gw)" min_walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil))
   nil)
  (min_walk_is_reduced-2 nil 3251113396
   ("" (skosimp*)
    (("" (expand "reduced?")
      (("" (expand "finseq_appl")
        (("" (skosimp*)
          (("" (name MIN_W "min_walk_from(x!1,y!1,Gw!1)")
            (("" (replace -1)
              (("" (lemma "min_walk_is_min")
                (("" (inst?)
                  (("" (lemma "min_walk_in")
                    (("" (inst?)
                      (("" (replace -3)
                        (("" (expand "walk_from?")
                          (("" (flatten)
                            (("" (case "k!1 = length(MIN_W) - 2")
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (name
                                       red_w
                                       "MIN_W ^ (0, length(MIN_W) - 3)")
                                      (("1"
                                        (inst -5 "RED_W")
                                        (("1"
                                          (replace -1 * rl)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (expand*
                                               "^"
                                               min
                                               empty_seq)
                                              (("1"
                                                (expand "walk?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (expand
                                                     "verts_in?")
                                                    (("1"
                                                      (split +)
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst?)
                                                          nil)))
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "finseq_appl")
                                                          (("2"
                                                            (hide -4)
                                                            (("2"
                                                              (inst
                                                               -4
                                                               "n!1")
                                                              (("2"
                                                                (assert)
                                                                nil)))))))))))))))))))))))
                                         ("2"
                                          (prop)
                                          (("1"
                                            (replace -1 * rl)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (expand*
                                                 "^"
                                                 min
                                                 empty_seq)
                                                (("1"
                                                  (propax)
                                                  nil)))))))
                                           ("2"
                                            (expand "verts_in?")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (replace -1 * rl)
                                                (("2"
                                                  (typepred "i!1")
                                                  (("2"
                                                    (replace -2 * rl)
                                                    (("2"
                                                      (hide -2)
                                                      (("2"
                                                        (expand*
                                                         "^"
                                                         min
                                                         empty_seq)
                                                        (("2"
                                                          (expand
                                                           "walk?")
                                                          (("2"
                                                            (flatten)
                                                            (("2"
                                                              (hide -5)
                                                              (("2"
                                                                (expand
                                                                 "verts_in?")
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "i!1")
                                                                  (("2"
                                                                    (assert)
                                                                    nil)))))))))))))))))))))))))))))))))))))
                               ("2"
                                (inst
                                 -4
                                 "MIN_W ^ (0, k!1 - 1) o MIN_W ^ (2 + k!1, length(MIN_W) - 1)")
                                (("1"
                                  (split -4)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (expand "empty_seq")
                                        (("1"
                                          (lift-if)
                                          (("1"
                                            (lift-if)
                                            (("1"
                                              (ground)
                                              nil)))))))))))
                                   ("2"
                                    (expand "o ")
                                    (("2"
                                      (expand* "^" min empty_seq)
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (expand "empty_seq")
                                          (("2"
                                            (lift-if)
                                            (("2"
                                              (ground)
                                              nil)))))))))))
                                   ("3"
                                    (expand "o ")
                                    (("3"
                                      (expand* "^" min empty_seq)
                                      (("3"
                                        (expand "empty_seq")
                                        (("3"
                                          (lift-if)
                                          (("3"
                                            (lift-if)
                                            (("3"
                                              (ground)
                                              nil)))))))))))
                                   ("4"
                                    (lemma "walk?_cut")
                                    (("4"
                                      (inst?)
                                      (("1"
                                        (inst -1 "Gw!1" "x!1" "y!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "walk_from?")
                                            (("1" (propax) nil)))))))
                                       ("2" (assert) nil)
                                       ("3" (assert) nil)))))))
                                 ("2"
                                  (split +)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (lift-if)
                                        (("1" (ground) nil)))))))
                                   ("2"
                                    (expand "verts_in?")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (typepred "i!1")
                                        (("1"
                                          (expand "o ")
                                          (("1"
                                            (expand* "^" min empty_seq)
                                            (("1"
                                              (lift-if)
                                              (("1"
                                                (expand "walk?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (hide -5)
                                                    (("1"
                                                      (expand
                                                       "verts_in?")
                                                      (("1"
                                                        (ground)
                                                        (("1"
                                                          (inst?)
                                                          nil)
                                                         ("2"
                                                          (inst?)
                                                          nil)))))))))))))))))
                                         ("2"
                                          (skosimp*)
                                          (("2" (assert) nil)))
                                         ("3"
                                          (skosimp*)
                                          (("3" (assert) nil)))))))))))
                                 ("3" (assert) nil)
                                 ("4"
                                  (assert)
                                  nil))))))))))))))))))))))))))))))
    nil)
   nil nil)
  (min_walk_is_reduced-1 nil 3251113238
   ("" (skosimp*)
    (("" (expand "reduced?")
      (("" (expand "finseq_appl")
        (("" (skosimp*)
          (("" (name min_w "min_walk_from(x!1,y!1,Gw!1)")
            (("" (replace -1)
              (("" (lemma "min_walk_is_min")
                (("" (inst?)
                  (("" (lemma "min_walk_in")
                    (("" (inst?)
                      (("" (replace -3)
                        (("" (expand "walk_from?")
                          (("" (flatten)
                            (("" (case "k!1 = length(MIN_W) - 2")
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (name
                                       red_w
                                       "MIN_W ^ (0, length(MIN_W) - 3)")
                                      (("1"
                                        (inst -5 "RED_W")
                                        (("1"
                                          (replace -1 * rl)
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (expand*
                                               "^"
                                               min
                                               empty_seq)
                                              (("1"
                                                (expand "walk?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (expand
                                                     "verts_in?")
                                                    (("1"
                                                      (split +)
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst?)
                                                          nil)))
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "finseq_appl")
                                                          (("2"
                                                            (hide -4)
                                                            (("2"
                                                              (inst
                                                               -4
                                                               "n!1")
                                                              (("2"
                                                                (assert)
                                                                nil)))))))))))))))))))))))
                                         ("2"
                                          (prop)
                                          (("1"
                                            (replace -1 * rl)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (expand*
                                                 "^"
                                                 min
                                                 empty_seq)
                                                (("1"
                                                  (propax)
                                                  nil)))))))
                                           ("2"
                                            (expand "verts_in?")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (replace -1 * rl)
                                                (("2"
                                                  (typepred "i!1")
                                                  (("2"
                                                    (replace -2 * rl)
                                                    (("2"
                                                      (hide -2)
                                                      (("2"
                                                        (expand*
                                                         "^"
                                                         min
                                                         empty_seq)
                                                        (("2"
                                                          (expand
                                                           "walk?")
                                                          (("2"
                                                            (flatten)
                                                            (("2"
                                                              (hide -5)
                                                              (("2"
                                                                (expand
                                                                 "verts_in?")
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "i!1")
                                                                  (("2"
                                                                    (assert)
                                                                    nil)))))))))))))))))))))))))))))))))))))
                               ("2"
                                (inst
                                 -4
                                 "MIN_W ^ (0, k!1 - 1) o MIN_W ^ (2 + k!1, length(MIN_W) - 1)")
                                (("1"
                                  (split -4)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (expand "empty_seq")
                                        (("1"
                                          (lift-if)
                                          (("1"
                                            (lift-if)
                                            (("1"
                                              (ground)
                                              nil)))))))))))
                                   ("2"
                                    (expand "o ")
                                    (("2"
                                      (expand* "^" min empty_seq)
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (expand "empty_seq")
                                          (("2"
                                            (lift-if)
                                            (("2"
                                              (ground)
                                              nil)))))))))))
                                   ("3"
                                    (expand "o ")
                                    (("3"
                                      (expand* "^" min empty_seq)
                                      (("3"
                                        (expand "empty_seq")
                                        (("3"
                                          (lift-if)
                                          (("3"
                                            (lift-if)
                                            (("3"
                                              (ground)
                                              nil)))))))))))
                                   ("4"
                                    (lemma "walk?_cut")
                                    (("4"
                                      (inst?)
                                      (("1"
                                        (inst -1 "Gw!1" "x!1" "y!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "walk_from?")
                                            (("1" (propax) nil)))))))
                                       ("2" (assert) nil)
                                       ("3" (assert) nil)))))))
                                 ("2"
                                  (split +)
                                  (("1"
                                    (expand "o ")
                                    (("1"
                                      (expand* "^" min empty_seq)
                                      (("1"
                                        (lift-if)
                                        (("1" (ground) nil)))))))
                                   ("2"
                                    (expand "verts_in?")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (typepred "i!1")
                                        (("1"
                                          (expand "o ")
                                          (("1"
                                            (expand* "^" min empty_seq)
                                            (("1"
                                              (lift-if)
                                              (("1"
                                                (expand "walk?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (hide -5)
                                                    (("1"
                                                      (expand
                                                       "verts_in?")
                                                      (("1"
                                                        (ground)
                                                        (("1"
                                                          (inst?)
                                                          nil)
                                                         ("2"
                                                          (inst?)
                                                          nil)))))))))))))))))
                                         ("2"
                                          (skosimp*)
                                          (("2" (assert) nil)))
                                         ("3"
                                          (skosimp*)
                                          (("3" (assert) nil)))))))))))
                                 ("3" (assert) nil)
                                 ("4"
                                  (assert)
                                  nil))))))))))))))))))))))))))))))
    nil)
   nil nil)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.99Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff