Quelle min_walks.prf
Sprache: Lisp
(min_walksnil 3507100597"" (skosimp*) (("" (typepred "Gw!1" ) (("" (propax) nil )))) nil )nil min_walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil min_walks nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3507100597"" (skosimp*)"" (typepred "Gw!1" )"" (hide -1 -2 -3 -4)"" "min_in[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): length(w)), LAMBDA (w: Seq(Gw!1)): walk_from?(Gw!1, w, x!1, y!1))]") "1" (beta)"1" (expand "walk_from?" )"1" (flatten) (("1" (propax) nil )))))))"2" (hide 2)"2" (typepred "Gw!1" ) (("2" (propax) nil ))))))))))))nil )nil min_walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil min_walks nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil abstract_min nil ))nil ))nil 3507100597 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )nil walks nil )nil min_walks nil )"Walk(Gw)" min_walks nil )nil min_walks nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )nil application-judgement "finite_set[T]" min_walks nil ))nil ))nil 3507100597"" (skosimp*)"" (typepred "min_walk_from(x!1, y!1,Gw!1)" )"" (prop)"1" "min_in[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): length(w)), LAMBDA (w: Seq(Gw!1)):") "1" (hide -2 -3 -4)"1" (beta)"1" (expand "min_walk_from" ) (("1" (propax) nil )))))))"2" (hide -1 -2 -3 2)"2" (typepred "Gw!1" ) (("2" (propax) nil )))))))"2" "min_is_min[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): length(w)), LAMBDA (w: Seq(Gw!1)):") "1" (hide -3 -4)"1" (expand "is_min" )"1" (assert )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "min_walk_from" )"1" (propax) nil )))))))))))))))"2" (hide -1 -2 -3 2)"2" (typepred "Gw!1" ) (("2" (propax) nil ))))))))))))nil )"Walk(Gw)" min_walks nil )nil walks nil )"bool" walks nil )nil min_walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil min_walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil abstract_min nil )"bool" min_walks nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil abstract_min nil ))nil ))nil 3507100597"" (skosimp*)"" (lemma "min_walk_def" )"" (inst?) (("" (flatten) (("" (propax) nil ))))))))nil )nil min_walks nil )nil min_walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil min_walks nil ))nil ))nil 3507100597"" (skosimp*)"" (lemma "min_walk_def" )"" (inst?)"" (flatten)"" (hide -1)"" (expand "is_min" )"" (flatten)"" (inst?) (("" (assert ) nil ))))))))))))))))nil )nil min_walks nil )"bool" min_walks nil )"(total_order?[real])" nil )nil min_walks nil )"bool" walks nil )nil walks nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil min_walks nil ))nil )))quality 99%
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
