| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Set.thy Sprache: LispOriginal von: PVS© |
|
||||||
|
(walks
(walk?_TCC1 0 (walk?_TCC1-1 nil 3263033538 ("" (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) (T formal-type-decl nil walks 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) (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) (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) (>= 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) (verts_in? const-decl "bool" walks nil)) nil)) (walk?_TCC2 0 (walk?_TCC2-1 nil 3263033538 ("" (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) (T formal-type-decl nil walks 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) (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) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (verts_in? const-decl "bool" walks nil)) nil)) (list2prewalk_TCC1 0 (list2prewalk_TCC1-1 nil 3507100592 ("" (subtype-tcc) nil nil) nil nil)) (from?_TCC1 0 (from?_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (from?_TCC2 0 (from?_TCC2-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (verts_of_TCC1 0 (verts_of_TCC1-1 nil 3263033538 ("" (skosimp*) (("" (lemma "surjection_from_finite_set[below(length(ww!1)),T]") (("" (inst?) (("" (inst -1 "fullset[below(length(ww!1))]") (("1" (assert) (("1" (hide 2) (("1" (inst 1 "(LAMBDA (i: below(length(ww!1))): ww!1`seq(i))") (("1" (expand "restrict") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst?) (("3" (expand "finseq_appl") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "is_finite") (("2" (inst 1 "length(ww!1)" "(LAMBDA (ii: below(length(ww!1))): ii)") (("2" (expand "injective?") (("2" (expand "restrict") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 walks 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) (surjection_from_finite_set formula-decl nil finite_sets_eq "finite_sets/") (fullset const-decl "set" sets nil) (is_finite const-decl "bool" finite_sets nil) (ww!1 skolem-const-decl "prewalk" walks nil) (finite_set type-eq-decl nil finite_sets nil) (i!1 skolem-const-decl "below(length(ww!1))" walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (restrict const-decl "R" restrict nil) (injective? const-decl "bool" functions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil)) nil)) (edges_of_TCC1 0 (edges_of_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (edges_of_TCC2 0 (edges_of_TCC2-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (edges_of_TCC3 0 (edges_of_TCC3-1 nil 3263033538 ("" (skosimp*) (("" (expand "is_finite") (("" (inst 1 "length(ww!1) - 1" "(LAMBDA (e: {e: doubleton[T] | EXISTS (i: below(length(ww!1) - 1)): e = dbl[T](finseq_appl[T](ww!1)(i), finseq_appl[T](ww!1)(i + 1))}): choose({i: below(length(ww!1) - 1) | e = dbl[T](finseq_appl[T](ww!1)(i), finseq_appl[T](ww!1)(i + 1))}))") (("1" (expand "injective?") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "finseq_appl") (("2" (typepred "ww!1") (("2" (typepred "e!1") (("2" (skosimp*) (("2" (inst -4 "i!1") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_finite const-decl "bool" finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (choose const-decl "(p)" sets nil) (T formal-type-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) (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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (ww!1 skolem-const-decl "prewalk" walks nil) (below type-eq-decl nil naturalnumbers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonempty? const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" walks nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (pre_circuit?_TCC1 0 (pre_circuit?_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (pre_circuit?_TCC2 0 (pre_circuit?_TCC2-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (verts_in?_concat_TCC1 0 (verts_in?_concat_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((O const-decl "finseq" finite_sequences nil)) nil)) (verts_in?_concat 0 (verts_in?_concat-1 nil 3263033538 ("" (skosimp*) (("" (expand "verts_in?") (("" (skosimp*) (("" (typepred "i!1") (("" (expand "o ") (("" (ground) (("1" (typepred "s1!1") (("1" (expand "verts_in?") (("1" (inst?) nil nil)) nil)) nil) ("2" (typepred "s2!1") (("2" (expand "verts_in?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (Seq type-eq-decl nil walks 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) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks 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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) nil)) (verts_in?_caret_TCC1 0 (verts_in?_caret_TCC1-1 nil 3263033538 ("" (skosimp*) (("" (expand "verts_in?") (("" (expand* "^" min empty_seq) (("" (expand "empty_seq") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences 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)) nil)) (verts_in?_caret 0 (verts_in?_caret-1 nil 3263033538 ("" (skosimp*) (("" (expand "verts_in?") (("" (skosimp*) (("" (inst?) (("1" (typepred "i!2") (("1" (expand* "^" min empty_seq) (("1" (expand "empty_seq") (("1" (lift-if) (("1" (ground) (("1" (typepred "i!2") (("1" (expand* "^" min empty_seq) (("1" (typepred "j!1") (("1" (reveal -1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (typepred "i!2") (("2" (expand* "^" min empty_seq) (("2" (lift-if) (("2" (expand "empty_seq") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ps!1 skolem-const-decl "prewalk" walks 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 walks nil) (below type-eq-decl nil nat_types nil) (i!1 skolem-const-decl "nat" walks 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) (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) (below type-eq-decl nil naturalnumbers 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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "finseq" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (vert_seq_lem 0 (vert_seq_lem-1 nil 3263033538 ("" (skosimp*) (("" (expand "finseq_appl") (("" (typepred "w!1") (("" (expand "verts_in?") (("" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (below type-eq-decl nil naturalnumbers 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans 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) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil)) nil)) (verts_of_subset 0 (verts_of_subset-1 nil 3263033538 ("" (skosimp*) (("" (typepred "w!1") (("" (expand "subset?") (("" (skosimp*) (("" (expand "verts_in?") (("" (expand "member") (("" (expand "verts_of") (("" (skosimp*) (("" (expand "finseq_appl") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks 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) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (member const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_of const-decl "finite_set[T]" walks nil) (subset? const-decl "bool" sets nil)) nil)) (edges_of_subset 0 (edges_of_subset-1 nil 3263033538 ("" (skosimp*) (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (expand "edges_of") (("" (expand "finseq_appl") (("" (skosimp*) (("" (replace -2) (("" (hide -2) (("" (expand "walk?") (("" (flatten) (("" (inst - "i!1") (("" (assert) (("" (expand "edge?") (("" (expand "finseq_appl") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (walk? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" walks 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) (int_minus_int_is_int application-judgement "int" integers nil) (edges_of const-decl "finite_set[doubleton[T]]" walks nil)) nil)) (walk_verts_in 0 (walk_verts_in-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) nil nil)) nil)) nil) ((walk? const-decl "bool" walks nil)) nil)) (walk_from_vert 0 (walk_from_vert-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "walk?") (("" (flatten) (("" (expand "verts_in?") (("" (inst-cp -3 "0") (("" (inst -3 "length(w!1)-1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (verts_in? 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 walks 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)) nil)) (walk_edge_in 0 (walk_edge_in-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split 1) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (expand "verts_of") (("1" (hide -2) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst?) (("1" (split -2) (("1" (propax) nil nil) ("2" (inst?) (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -5) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst?) (("2" (assert) (("2" (expand "edge?") (("2" (flatten) (("2" (inst?) (("1" (expand "edges_of") (("1" (split -4) (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (subset? const-decl "bool" sets nil) (verts_of const-decl "finite_set[T]" walks nil) (posint_plus_nnint_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) (edges_of const-decl "finite_set[doubleton[T]]" walks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (gen_seq1_TCC1 0 (gen_seq1_TCC1-1 nil 3263033538 ("" (skosimp*) (("" (expand "verts_in?") (("" (propax) nil nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil)) nil)) (gen_seq2_TCC1 0 (gen_seq2_TCC1-1 nil 3263033538 ("" (skosimp*) (("" (expand "verts_in?") (("" (propax) nil nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil)) nil)) (trunc1_TCC1 0 (trunc1_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (trunc1_TCC2 0 (trunc1_TCC2-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (add1_TCC1 0 (add1_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) nil nil)) (gen_seq1_is_walk 0 (gen_seq1_is_walk-1 nil 3263033538 ("" (skosimp*) (("" (expand "gen_seq1") (("" (expand "walk?") (("" (expand "verts_in?") (("" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ((gen_seq1 const-decl "Seq(G)" walks nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil)) nil)) (edge_to_walk_TCC1 0 (edge_to_walk_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (edge_to_walk_TCC2 0 (edge_to_walk_TCC2-1 nil 3263033538 ("" (skosimp*) (("" (expand "edg") (("" (typepred "G!1") (("" (inst?) (("1" (assert) (("1" (inst?) (("1" (hide -2) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((edg const-decl "doubleton[T]" graphs nil) (nil application-judgement "finite_set[T]" walks nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil walks 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) (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)) nil)) (edge_to_walk_TCC3 0 (edge_to_walk_TCC3-1 nil 3263033538 ("" (skosimp*) (("" (typepred "G!1") (("" (inst?) (("1" (assert) (("1" (inst -1 "v!1") (("1" (expand "edg") (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (T formal-type-decl nil walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (edg const-decl "doubleton[T]" graphs nil)) nil)) (edge_to_walk 0 (edge_to_walk-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (expand "gen_seq2") (("" (split 2) (("1" (expand "verts_in?") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (assert) (("2" (expand "edge?") (("2" (expand "edg") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nil application-judgement "finite_set[T]" walks nil) (edge? const-decl "bool" graphs nil) (edg const-decl "doubleton[T]" graphs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gen_seq2 const-decl "Seq(G)" walks nil)) nil)) (walk?_rev_TCC1 0 (walk?_rev_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (rev const-decl "finseq[T]" doubletons nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (walk?_rev 0 (walk?_rev-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split +) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "rev") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (hide -2) (("2" (expand "rev") (("2" (inst - "length(ps!1) - 2 - n!1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "dbl_comm") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks 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) (rev const-decl "finseq[T]" doubletons nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks 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) (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) (ps!1 skolem-const-decl "prewalk" walks nil) (i!1 skolem-const-decl "below(length(rev(ps!1)))" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (n!1 skolem-const-decl "nat" walks nil) (dbl_comm formula-decl nil doubletons nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (walk?_reverse 0 (walk?_reverse-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (inst 1 "(# length := length(w1!1), seq := (LAMBDA (i: below(length(w1!1))): w1!1`seq(length(w1!1)-1-i)) #)") (("1" (assert) nil nil) ("2" (expand "walk?") (("2" (split) (("1" (assert) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "w1!1") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lemma "edge?_comm") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (typepred "w1!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (typepred "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk_from? const-decl "bool" walks nil) (real_gt_is_strict_total_order name-judgement "(strict_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) (< 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) (w1!1 skolem-const-decl "prewalk" walks nil) (G!1 skolem-const-decl "graph[T]" walks nil) (walk? const-decl "bool" 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 walks nil) (Walk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (NOT const-decl "[bool -> bool]" booleans 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) (n!1 skolem-const-decl "nat" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (edge?_comm formula-decl nil graphs nil)) nil)) (walk?_caret_TCC1 0 (walk?_caret_TCC1-1 nil 3263033538 ("" (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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" walks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk?_caret 0 (walk?_caret-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split +) (("1" (rewrite "verts_in?_caret") nil nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals 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) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (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 walks nil) (verts_in?_caret formula-decl nil walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (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_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) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (l_trunc1_TCC1 0 (l_trunc1_TCC1-1 nil 3263033538 ("" (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) (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) (T formal-type-decl nil walks 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)) nil)) (l_trunc1 0 (l_trunc1-1 nil 3263033538 ("" (skosimp*) (("" (expand "trunc1") (("" (expand* "^" min empty_seq) (("" (assert) nil nil)) nil)) nil)) nil) ((trunc1 const-decl "prewalk" walks 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) (^ const-decl "finseq" finite_sequences 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)) nil)) (walk?_add1 0 (walk?_add1-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split 1) (("1" (expand "verts_in?") (("1" (expand "add1") (("1" (skosimp*) (("1" (hide -2) (("1" (inst?) (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "add1") (("2" (lift-if) (("2" (split 1) (("1" (flatten) (("1" (inst?) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (add1 const-decl "prewalk" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (ww!1 skolem-const-decl "prewalk" walks nil) (x!1 skolem-const-decl "T" walks nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(add1(ww!1, x!1)))" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk_concat_edge_TCC1 0 (walk_concat_edge_TCC1-1 nil 3263033538 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (O const-decl "finseq" finite_sequences nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (walk_concat_edge 0 (walk_concat_edge-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "o ") (("" (assert) (("" (auto-rewrite "finseq_appl") (("" (expand "walk?") (("" (assert) (("" (flatten) (("" (assert) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (hide -4) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -3) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "n!1 < length(w1!1)") (("1" (assert) (("1" (lift-if) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -5) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk_from? const-decl "bool" walks nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (O const-decl "finseq" finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (verts_in? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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 walks 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (walk? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (walk_concat_TCC1 0 (walk_concat_TCC1-1 nil 3263033538 ("" (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) (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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" walks nil)) nil)) (walk_concat_TCC2 0 (walk_concat_TCC2-1 nil 3263033538 ("" (skosimp*) (("" (expand "o ") (("" (expand "rev") (("" (expand* "^" min empty_seq) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((O const-decl "finseq" finite_sequences 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) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rev const-decl "finseq[T]" doubletons nil)) nil)) (walk_concat 0 (walk_concat-1 nil 3263033538 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (assert) (("" (expand "o ") (("" (expand "rev") (("" (expand* "^" min empty_seq) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -2 -3 -4 -5 -6 -7 -9) (("2" (inst - "length(w1!1) + length(w2!1) - 2 - i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (case "n!1 < length(w1!1) - 1") (("1" (assert) (("1" (inst?) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.78 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 |
