|
(walks
(walk?_TCC1 0
(walk?_TCC1-1 nil 3253634007 ("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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 3253634007 ("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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))
(from?_TCC1 0
(from?_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(from?_TCC2 0
(from?_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(verts_of_TCC1 0
(verts_of_TCC1-1 nil 3253634007
("" (skosimp*)
(("" (lemma "is_finite_surj[T]")
((""
(inst -
"{t: T | EXISTS (i: below(length(ww!1))): finseq_appl[T](ww!1)(i) = t}")
(("" (assert)
(("" (hide 2)
((""
(inst 1 "length(ww!1)"
"(LAMBDA (i: below(length(ww!1))): seq(ww!1)(i))")
(("1" (expand "surjective?")
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (expand "finseq_appl")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst?)
(("2" (expand "finseq_appl") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil walks nil)
(is_finite_surj formula-decl nil finite_sets nil)
(ww!1 skolem-const-decl "prewalk" walks nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(surjective? const-decl "bool" functions nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(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)
(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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(edges_of_TCC1 0
(edges_of_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(edges_of_TCC2 0
(edges_of_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(edges_of_TCC3 0
(edges_of_TCC3-1 nil 3253634007
("" (skosimp*)
(("" (lemma "is_finite_surj[edgetype[T]]")
(("" (inst?)
(("" (assert)
(("" (hide 2)
((""
(inst + "length(ww!1)-1"
"(LAMBDA (i: below[length(ww!1)-1]): (ww!1(i),ww!1(i+1)))")
(("1" (expand "finseq_appl")
(("1" (expand "surjective?")
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1" (skosimp*)
(("1" (inst + "i!1")
(("1" (expand "finseq_appl")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((edgetype type-eq-decl nil digraphs nil)
(T formal-type-decl nil walks nil)
(is_finite_surj formula-decl nil finite_sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(ww!1 skolem-const-decl "prewalk" walks nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(below type-eq-decl nil nat_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals 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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(walk_from_l 0
(walk_from_l-2 nil 3560851290
("" (skosimp*)
(("" (expand* "walk_from?" "from?")
(("" (flatten)
(("" (expand "walk?")
(("" (flatten)
(("" (inst - "0") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((from? const-decl "bool" walks nil)
(walk_from? const-decl "bool" walks 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)
(walk_from_l-1 nil 3253634007
("" (skosimp*)
(("" (expand "walk_from?")
(("" (flatten)
(("" (expand "walk?")
(("" (flatten)
(("" (inst - "0") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
nil nil))
(verts_in?_concat_TCC1 0
(verts_in?_concat_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil)
((O const-decl "finseq" finite_sequences nil)) nil))
(verts_in?_concat 0
(verts_in?_concat-1 nil 3253634007
("" (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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs 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 3253634007
("" (skosimp*)
(("" (expand "verts_in?")
(("" (expand "^")
(("" (expand min)
(("" (expand "empty_seq")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((verts_in? const-decl "bool" walks nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
(empty_seq const-decl "finseq" finite_sequences 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))
nil))
(verts_in?_caret 0
(verts_in?_caret-1 nil 3253634007
("" (skosimp*)
(("" (expand "verts_in?")
(("" (skosimp*)
(("" (inst?)
(("1" (typepred "i!2")
(("1" (expand "^")
(("1" (expand "empty_seq")
(("1" (lift-if)
(("1" (ground)
(("1" (typepred "i!2")
(("1" (expand "^")
(("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 "^")
(("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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_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)
(empty_seq const-decl "finseq" finite_sequences nil)
(^ const-decl "finseq" finite_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(vert_seq_lem 0
(vert_seq_lem-1 nil 3253634007
("" (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)
(edgetype type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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 3253634007
("" (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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs 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 3253634007
("" (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" digraphs 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[edgetype[T]]" walks nil))
nil))
(walk_verts_in 0
(walk_verts_in-1 nil 3253634007
("" (skosimp*) (("" (expand "walk?") (("" (flatten) nil nil)) nil))
nil)
((walk? const-decl "bool" walks nil)) nil))
(walk_from_vert 0
(walk_from_vert-2 nil 3560851336
("" (skosimp*)
(("" (expand* "walk_from?" "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)
((from? const-decl "bool" walks 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_from_vert-1 nil 3253634007
("" (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)
nil nil))
(walk_edge_in 0
(walk_edge_in-1 nil 3253634007
("" (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" (inst?)
(("2" (expand "edges_of")
(("2" (assert)
(("2" (inst + "n!1") 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)
(edgetype type-eq-decl nil digraphs nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(edges_of const-decl "finite_set[edgetype[T]]" walks nil)
(edge? const-decl "bool" digraphs nil))
nil))
(prewalk_across_TCC1 0
(prewalk_across_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil
nil))
(prewalk_across_TCC2 0
(prewalk_across_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil
nil))
(prewalk_across_TCC3 0
(prewalk_across_TCC3-1 nil 3253634007 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
nil))
(prewalk_across_TCC4 0
(prewalk_across_TCC4-1 nil 3253634007 ("" (subtype-tcc) nil nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
nil))
(prewalk_across 0
(prewalk_across-1 nil 3253634007
("" (skosimp*)
((""
(case "(FORALL (i: below(length(ww!1))): seq(ww!1)(i) = seq(ww!1)(0))")
(("1" (inst -1 "length(ww!1)-1")
(("1" (assert)
(("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 3)
(("2" (induct "i")
(("2" (skosimp*)
(("2" (reveal 1)
(("2" (inst + "jb!1")
(("2" (expand "finseq_appl") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities 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_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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" 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)
(pred type-eq-decl nil defined_types nil)
(below_induction formula-decl nil bounded_nat_inductions nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(jb!1 skolem-const-decl "below(length(ww!1))" walks nil)
(ww!1 skolem-const-decl "prewalk" walks nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(gen_seq1_TCC1 0
(gen_seq1_TCC1-1 nil 3253634007
("" (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 3253634007
("" (skosimp*)
(("" (expand "verts_in?") (("" (propax) nil nil)) nil)) nil)
((verts_in? const-decl "bool" walks nil)) nil))
(trunc1_TCC1 0
(trunc1_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(trunc1_TCC2 0
(trunc1_TCC2-1 nil 3253634007 ("" (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 3253634007 ("" (subtype-tcc) nil nil) nil nil))
(gen_seq1_is_walk 0
(gen_seq1_is_walk-1 nil 3253634007
("" (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 3253634007 ("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs nil)
(/= const-decl "boolean" notequal nil))
nil))
(edge_to_walk_TCC2 0
(edge_to_walk_TCC2-1 nil 3253634007
("" (skosimp*)
(("" (typepred "G!1") (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil)
((digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(edgetype type-eq-decl nil digraphs 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))
nil))
(edge_to_walk 0
(edge_to_walk-1 nil 3253634007
("" (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" (propax) 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)
(edge? const-decl "bool" digraphs 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?_caret_TCC1 0
(walk?_caret_TCC1-1 nil 3253634007 ("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(T formal-type-decl nil walks nil)
(edge? const-decl "bool" digraphs nil)
(walk? const-decl "bool" walks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(walk?_caret 0
(walk?_caret-1 nil 3253634007
("" (skosimp*)
(("" (expand "walk?")
(("" (flatten)
(("" (split +)
(("1" (rewrite "verts_in?_caret") nil nil)
("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (expand "edge?")
(("2" (expand "^")
(("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)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs 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)
(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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs 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" digraphs nil))
nil))
(l_trunc1_TCC1 0
(l_trunc1_TCC1-1 nil 3253634007 ("" (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 3253634007
("" (skosimp*)
(("" (expand "trunc1")
(("" (expand "^") (("" (expand min) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((trunc1 const-decl "prewalk" walks nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs 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 "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(walk?_add1 0
(walk?_add1-1 nil 3253634007
("" (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 3253634007 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil walks nil)
(edge? const-decl "bool" digraphs nil)
(from? const-decl "bool" walks 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))
(walk_concat_edge 0
(walk_concat_edge-2 nil 3560851383
("" (skosimp*)
(("" (expand* "walk_from?" "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)
((from? const-decl "bool" walks 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_edge-1 nil 3253634007
("" (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)
nil nil))
(walk_concat_TCC1 0
(walk_concat_TCC1-1 nil 3253634007 ("" (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)
(edgetype type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(from? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(T formal-type-decl nil walks nil)
(edge? const-decl "bool" digraphs nil)
(walk? const-decl "bool" walks nil)
(walk_from? const-decl "bool" walks nil))
nil))
(walk_concat_TCC2 0
(walk_concat_TCC2-1 nil 3253634007
("" (skosimp*)
(("" (expand "o ")
(("" (expand "^")
(("" (expand min) (("" (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)
(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)
(^ const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(walk_concat 0
(walk_concat-2 nil 3560851417
("" (skosimp*)
(("" (expand* "walk_from?" "from?")
(("" (flatten)
(("" (assert)
(("" (expand "o ")
(("" (expand "^")
(("" (expand min)
(("" (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?) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "edge?")
(("2" (case "n!1 < length(w1!1) - 1")
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
(("1"
(case "n!1 = length(w1!1) - 1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(lift-if)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide -6)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((from? const-decl "bool" walks nil)
(walk_from? const-decl "bool" 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(walk? const-decl "bool" walks nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(edge? const-decl "bool" digraphs nil)
(verts_in? const-decl "bool" walks nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(O const-decl "finseq" finite_sequences nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
nil)
(walk_concat-1 nil 3253634007
("" (skosimp*)
(("" (expand "walk_from?")
(("" (flatten)
(("" (assert)
(("" (expand "o ")
(("" (expand "^")
(("" (expand min)
(("" (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?) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "edge?")
(("2" (case "n!1 < length(w1!1) - 1")
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
(("1"
(case "n!1 = length(w1!1) - 1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(lift-if)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide -6)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.44 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.
|
