|
(cycles
(cycle?_TCC1 0
(cycle?_TCC1-1 nil 3312559967 ("" (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)
(verts_in? const-decl "bool" walks nil)
(Seq type-eq-decl nil walks 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)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(/= const-decl "boolean" notequal nil)
(T formal-type-decl nil cycles nil)
(edge? const-decl "bool" graphs nil)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" walks nil)
(nil application-judgement "finite_set[T]" cycles nil))
nil))
(cycle?_TCC2 0
(cycle?_TCC2-1 nil 3312559967 ("" (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)
(verts_in? const-decl "bool" walks nil)
(Seq 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)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(/= const-decl "boolean" notequal nil)
(T formal-type-decl nil cycles nil)
(edge? const-decl "bool" graphs nil)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" walks nil)
(nil application-judgement "finite_set[T]" cycles nil))
nil))
(cycle_l_gt_3 0
(cycle_l_gt_3-1 nil 3312559967
("" (skosimp*)
(("" (expand "cycle?")
(("" (flatten)
(("" (expand "pre_circuit?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cycle? const-decl "bool" cycles nil)
(pre_circuit? 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))
nil))
(cycle_has_path_TCC1 0
(cycle_has_path_TCC1-1 nil 3312559967
("" (skosimp*)
(("" (expand* "^" min empty_seq)
(("" (typepred "j!1") (("" (assert) nil))))))
nil)
((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(^ const-decl "finseq" finite_sequences 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)
(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)
(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 cycles nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals 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)
(below type-eq-decl nil naturalnumbers nil))
nil))
(cycle_has_path 0
(cycle_has_path-2 "Fewer" 3368782121
("" (skosimp*)
(("" (lemma "cycle_l_gt_3")
(("" (inst?)
(("" (assert)
(("" (case "walk?(G!1, w!1)")
(("1" (inst 1 "length(w!1)-2")
(("1" (expand "path?")
(("1" (expand "finseq_appl")
(("1" (prop)
(("1" (rewrite "walk?_caret") nil nil)
("2" (skosimp*)
(("2" (expand "^")
(("2" (typepred "j!1")
(("2" (typepred "i!1")
(("2" (expand* "^" min empty_seq)
(("2"
(expand "cycle?")
(("2"
(expand "finseq_appl")
(("2"
(flatten)
(("2"
(inst -7 "i!1" "j!1")
(("2"
(bddsimp)
(("2"
(install-rewrites "walks[T]")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "cycle?")
(("2" (expand "finseq_appl")
(("2" (flatten)
(("2" (expand "pre_circuit?")
(("2" (expand "finseq_appl")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cycle_l_gt_3 formula-decl nil cycles nil)
(real_lt_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_minus_int_is_int application-judgement "int" integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(nil application-judgement "finite_set[T]" cycles nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(endpoint? const-decl "bool" paths nil)
(pre_circuit? const-decl "bool" walks nil)
(edge? const-decl "bool" graphs nil)
(cycle? const-decl "bool" cycles nil)
(^ const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(walk?_caret formula-decl nil walks nil)
(path? const-decl "bool" paths nil)
(walk? const-decl "bool" walks nil)
(Seq type-eq-decl nil walks nil)
(verts_in? 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 cycles nil))
shostak)
(cycle_has_path-1 nil 3312559967
("" (skosimp*)
(("" (auto-rewrite "finseq_appl")
(("" (lemma "cycle_l_gt_3")
(("" (inst?)
(("" (assert)
(("" (case "walk?(G!1, w!1)")
(("1" (inst 1 "length(w!1)-2")
(("1" (expand "path?")
(("1" (prop)
(("1" (rewrite "walk?_caret") nil)
("2" (skosimp*)
(("2" (expand* "^" min empty_seq)
(("2" (typepred "j!1")
(("2" (typepred "i!1")
(("2" (expand* "^" min empty_seq)
(("2"
(expand "cycle?")
(("2"
(flatten)
(("2"
(inst -7 "i!1" "j!1")
(("1"
(assert)
(("1"
(expand "finseq_appl")
(("1"
(assert)
(("1"
(flatten)
(("1"
(expand "endpoint?")
(("1"
(assert)
nil)))))))))))
("2" (assert) nil)
("3"
(assert)
nil)))))))))))))))))))))))
("2" (hide 2)
(("2" (expand "cycle?")
(("2" (expand "pre_circuit?")
(("2" (flatten)
(("2" (propax) nil))))))))))))))))))))
nil)
((walk?_caret formula-decl nil walks nil)
(endpoint? const-decl "bool" paths nil)
(pre_circuit? const-decl "bool" walks nil)
(edge? const-decl "bool" graphs nil)
(path? const-decl "bool" paths nil)
(walk? const-decl "bool" walks nil)
(Seq type-eq-decl nil walks nil)
(verts_in? const-decl "bool" walks nil)
(prewalk type-eq-decl nil walks nil)
(graph type-eq-decl nil graphs nil)
(pregraph type-eq-decl nil graphs nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil))
nil))
(cycle_gt3 0
(cycle_gt3-1 nil 3312560646
("" (skosimp*)
(("" (expand "cycle?")
(("" (expand "pre_circuit?")
(("" (flatten)
(("" (inst - "1" "(length(w!1) - 2)")
(("1" (expand "endpoint?") (("1" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((cycle? const-decl "bool" cycles nil)
(endpoint? const-decl "bool" paths nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(below 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)
(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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil cycles nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals 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)
(G!1 skolem-const-decl "graph[T]" cycles nil)
(Seq type-eq-decl nil walks nil)
(w!1 skolem-const-decl "Seq[T](G!1)" cycles nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pre_circuit? const-decl "bool" walks nil))
shostak))
(cycle_def 0
(cycle_def-1 nil 3312561988
("" (skosimp*)
(("" (expand "cycle?")
(("" (expand "endpoint?")
(("" (expand "pre_circuit?")
(("" (ground)
(("" (inst - "1" "(length(w!1) - 2)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cycle? const-decl "bool" cycles nil)
(pre_circuit? const-decl "bool" walks nil)
(real_ge_is_total_order name-judgement "(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 cycles nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals 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)
(below type-eq-decl nil naturalnumbers 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(endpoint? const-decl "bool" paths nil))
nil)))
¤ Dauer der Verarbeitung: 0.29 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.
|
