| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: paths.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(paths
(path?_verts 0 (path?_verts-2 nil 3495281875 ("" (skosimp*) (("" (expand "path?") (("" (expand "walk?") (("" (flatten) (("" (propax) nil)))))))) nil) ((path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil)) nil) (path?_verts-1 nil 3495200565 ("" (skosimp*) (("" (expand "path?") (("" (expand "walk?") (("" (flatten) (("" (propax) nil)))))))) nil) ((walk? const-decl "bool" walks nil)) nil)) (path_from_l 0 (path_from_l-2 nil 3495281875 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "path?") (("" (flatten) (("" (expand "from?") (("" (flatten) (("" (expand "finseq_appl") (("" (inst -2 "0" "(length(ps!1)-1)") (("" (split -2) (("1" (assert) nil) ("2" (assert) nil)))))))))))))))))))) nil) ((path_from? const-decl "bool" paths nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil paths nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (path_from_l-1 nil 3495200565 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "path?") (("" (flatten) (("" (expand "from?") (("" (flatten) (("" (expand "finseq_appl") (("" (inst -2 "0" "(length(ps!1)-1)") (("" (split -2) (("1" (assert) nil) ("2" (assert) nil)))))))))))))))))))) nil) ((from? const-decl "bool" walks nil) (prewalk type-eq-decl nil walks nil)) nil)) (path_from_in 0 (path_from_in-2 nil 3495281875 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "path?") (("" (flatten) (("" (hide -2) (("" (expand "walk?") (("" (flatten) (("" (hide -2) (("" (expand "from?") (("" (expand "verts_in?") (("" (flatten) (("" (inst-cp -1 "0") (("" (inst -1 "length(ps!1) - 1") (("" (assert) nil)))))))))))))))))))))))))))) nil) ((path_from? const-decl "bool" paths nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil paths nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil)) nil) (path_from_in-1 nil 3495200565 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "path?") (("" (flatten) (("" (hide -2) (("" (expand "walk?") (("" (flatten) (("" (hide -2) (("" (expand "from?") (("" (expand "verts_in?") (("" (flatten) (("" (inst-cp -1 "0") (("" (inst -1 "length(ps!1) - 1") (("" (assert) nil)))))))))))))))))))))))))))) nil) ((from? const-decl "bool" walks nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil)) nil)) (path?_caret_TCC1 0 (path?_caret_TCC1-2 nil 3495281875 ("" (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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil) (path?_caret_TCC1-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_caret 0 (path?_caret-2 nil 3495281875 ("" (skosimp*) (("" (expand "path?") (("" (expand "finseq_appl") (("" (flatten) (("" (split 1) (("1" (expand "walk?") (("1" (split 1) (("1" (flatten) (("1" (hide -4 -5) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!2") (("1" (expand* "^" min empty_seq) (("1" (lift-if) (("1" (assert) (("1" (inst?) nil))))))) ("2" (skosimp*) nil))))))))))) ("2" (skosimp*) (("2" (hide -6) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (inst - "n!1+i!1") (("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))))))))))))) ("2" (skosimp*) (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (inst - "i!1+i!2" "i!1+j!2") (("1" (assert) nil) ("2" (typepred "i!2") (("2" (typepred "j!2") (("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))) ("3" (typepred "i!2") (("3" (typepred "i!1") (("3" (expand* "^" min empty_seq) (("3" (assert) nil)))))))))))))))))))))))) nil) ((path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" paths nil) (verts_in? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (^ const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil paths nil) (below type-eq-decl nil nat_types 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) (< 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil) (path?_caret-1 nil 3495200565 ("" (skosimp*) (("" (expand "path?") (("" (expand "finseq_appl") (("" (flatten) (("" (split 1) (("1" (expand "walk?") (("1" (split 1) (("1" (flatten) (("1" (hide -4 -5) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!2") (("1" (expand* "^" min empty_seq) (("1" (lift-if) (("1" (assert) (("1" (inst?) nil))))))) ("2" (skosimp*) nil))))))))))) ("2" (skosimp*) (("2" (hide -6) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (inst - "n!1+i!1") (("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))))))))))))) ("2" (skosimp*) (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (inst - "i!1+i!2" "i!1+j!2") (("1" (assert) nil) ("2" (typepred "i!2") (("2" (typepred "j!2") (("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))) ("3" (typepred "i!2") (("3" (typepred "i!1") (("3" (expand* "^" min empty_seq) (("3" (assert) nil)))))))))))))))))))))))) nil) ((prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path_from?_caret_TCC1 0 (path_from?_caret_TCC1-2 nil 3495281875 ("" (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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil) (path_from?_caret_TCC1-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (from? const-decl "bool" walks nil)) nil)) (path_from?_caret_TCC2 0 (path_from?_caret_TCC2-2 nil 3495281875 ("" (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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path_from?_caret_TCC2-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (from? const-decl "bool" walks nil)) nil)) (path_from?_caret 0 (path_from?_caret-2 nil 3495281875 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (rewrite "path?_caret") (("" (expand "from?") (("" (expand* "^" min empty_seq) (("" (assert) nil)))))))))))) nil) ((path_from? const-decl "bool" paths nil) (path?_caret formula-decl nil paths nil) (T formal-type-decl nil paths 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) (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) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (from? const-decl "bool" walks nil)) nil) (path_from?_caret-1 nil 3495200565 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (rewrite "path?_caret") (("" (expand "from?") (("" (expand* "^" min empty_seq) (("" (assert) nil)))))))))))) nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (from? const-decl "bool" walks nil)) nil)) (path?_rev_TCC1 0 (path?_rev_TCC1-2 nil 3495281875 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (rev const-decl "finseq[T]" doubletons nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path?_rev_TCC1-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_rev 0 (path?_rev-2 nil 3495281875 ("" (skosimp*) (("" (expand "path?") (("" (flatten) (("" (rewrite "walk?_rev") (("" (assert) (("" (skosimp*) (("" (expand "finseq_appl") (("" (typepred "i!1") (("" (typepred "j!1") (("" (expand "rev") (("" (inst?) (("1" (inst - "length(ps!1) - 1 - j!1") (("1" (assert) nil) ("2" (assert) nil))) ("2" (assert) nil)))))))))))))))))))))) nil) ((path? const-decl "bool" paths nil) (walk?_rev formula-decl nil walks 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) (T formal-type-decl nil paths nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" 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) (rev const-decl "finseq[T]" doubletons nil) (below type-eq-decl nil naturalnumbers nil) (j!1 skolem-const-decl "below(length(rev(ps!1)))" paths nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!1 skolem-const-decl "below(length(rev(ps!1)))" paths nil) (ps!1 skolem-const-decl "prewalk[T]" paths nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil) (path?_rev-1 nil 3495200565 ("" (skosimp*) (("" (expand "path?") (("" (flatten) (("" (rewrite "walk?_rev") (("" (assert) (("" (skosimp*) (("" (expand "finseq_appl") (("" (typepred "i!1") (("" (typepred "j!1") (("" (expand "rev") (("" (inst?) (("1" (inst - "length(ps!1) - 1 - j!1") (("1" (assert) nil) ("2" (assert) nil))) ("2" (assert) nil)))))))))))))))))))))) nil) ((walk?_rev formula-decl nil walks nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil)) nil)) (path?_gen_seq2 0 (path?_gen_seq2-2 nil 3495281875 ("" (skosimp*) (("" (expand "gen_seq2") (("" (expand "path?") (("" (expand "finseq_appl") (("" (split +) (("1" (expand "walk?") (("1" (split +) (("1" (expand "verts_in?") (("1" (propax) nil))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lift-if) (("2" (ground) nil))))))))))) ("2" (skosimp*) (("2" (expand "edge?") (("2" (flatten) (("2" (lift-if) (("2" (ground) nil)))))))))))))))))) nil) ((gen_seq2 const-decl "Seq(G)" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" paths nil) (walk? const-decl "bool" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (path? const-decl "bool" paths nil)) nil) (path?_gen_seq2-1 nil 3495200565 ("" (skosimp*) (("" (expand "gen_seq2") (("" (expand "path?") (("" (expand "finseq_appl") (("" (split +) (("1" (expand "walk?") (("1" (split +) (("1" (expand "verts_in?") (("1" (propax) nil))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lift-if) (("2" (ground) nil))))))))))) ("2" (skosimp*) (("2" (expand "edge?") (("2" (flatten) (("2" (lift-if) (("2" (ground) nil)))))))))))))))))) nil) ((gen_seq2 const-decl "Seq(G)" walks nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil)) nil)) (path?_add1_TCC1 0 (path?_add1_TCC1-2 nil 3495281875 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path?_add1_TCC1-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_add1 0 (path?_add1-2 nil 3495281875 ("" (skosimp*) (("" (expand "path?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (rewrite "walk?_add1") nil nil) ("2" (skosimp*) (("2" (expand "add1") (("2" (lift-if) (("2" (lift-if) (("2" (expand "verts_of") (("2" (typepred "i!1") (("2" (typepred "j!1") (("2" (expand "add1") (("2" (expand "finseq_appl") (("2" (ground) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil) ("2" (inst + "i!1") nil nil) ("3" (inst + "j!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path? const-decl "bool" paths nil) (verts_of const-decl "finite_set[T]" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" 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) (below type-eq-decl nil naturalnumbers nil) (add1 const-decl "prewalk" walks nil) (walk?_add1 formula-decl nil walks 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) (T formal-type-decl nil paths nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil) (path?_add1-1 nil 3495200565 ("" (skosimp*) (("" (expand "path?") (("" (flatten) (("" (split +) (("1" (rewrite "walk?_add1") nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "add1") (("2" (lift-if) (("2" (lift-if) (("2" (expand "verts_of") (("2" (typepred "i!1") (("2" (typepred "j!1") (("2" (expand "add1") (("2" (ground) (("1" (inst - "i!1" "j!1") (("1" (assert) nil))) ("2" (expand "finseq_appl") (("2" (inst + "j!1") (("2" (assert) nil))))) ("3" (inst + "i!1") (("3" (expand "finseq_appl") (("3" (propax) nil)))))))))))))))))))))))))))))))) nil) nil nil)) (path?_trunc1_TCC1 0 (path?_trunc1_TCC1-2 nil 3495281875 ("" (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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path?_trunc1_TCC1-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_trunc1_TCC2 0 (path?_trunc1_TCC2-2 nil 3495281875 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path?_trunc1_TCC2-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_trunc1_TCC3 0 (path?_trunc1_TCC3-2 nil 3495281875 ("" (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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil paths nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" paths nil)) nil) (path?_trunc1_TCC3-1 nil 3495200565 ("" (subtype-tcc) nil nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)) nil)) (path?_trunc1 0 (path?_trunc1-2 nil 3495281875 ("" (skosimp*) (("" (expand "path_from?") (("" (split 1) (("1" (expand "trunc1") (("1" (lemma "path?_caret") (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))) ("2" (expand "from?") (("2" (expand "trunc1") (("2" (expand* "^" min empty_seq) (("2" (assert) nil)))))))))))) nil) ((path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (trunc1 const-decl "prewalk" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (p!1 skolem-const-decl "prewalk[T]" paths nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil paths nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (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) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (path?_caret formula-decl nil paths nil)) nil) (path?_trunc1-1 nil 3495200565 ("" (skosimp*) (("" (expand "path_from?") (("" (split 1) (("1" (expand "trunc1") (("1" (lemma "path?_caret") (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))) ("2" (expand "from?") (("2" (expand "trunc1") (("2" (expand* "^" min empty_seq) (("2" (assert) nil)))))))))))) nil) ((from? const-decl "bool" walks nil) (trunc1 const-decl "prewalk" walks nil) (prewalk type-eq-decl nil walks nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil)) nil))) ¤ Dauer der Verarbeitung: 0.41 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
