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