|
(path_ops
(walk?_del_vert 0
(walk?_del_vert-1 nil 3363193931
("" (skosimp*)
(("" (expand "walk?")
(("" (flatten)
(("" (prop)
(("1" (hide -2)
(("1" (expand "verts_in?")
(("1" (skosimp*) (("1" (inst?) (("1" (grind) nil)))))))))
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst?)
(("2" (assert)
(("2" (lemma "edges_del_vert")
(("2" (expand "edge?")
(("2" (flatten)
(("2" (inst?)
(("1" (assert) nil)
("2" (inst?)
(("2" (assert)
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 path_ops 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)
(finite_remove application-judgement "finite_set" finite_sets nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(del_vert const-decl "graph[T]" graph_ops 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)
(nil application-judgement "finite_set[T]" path_ops nil)
(edge? const-decl "bool" graphs 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)
(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)
(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)
(edges_del_vert formula-decl nil graph_ops nil))
nil))
(walk?_del_vert_not 0
(walk?_del_vert_not-1 nil 3363193931
("" (skosimp*)
(("" (expand "walk?")
(("" (flatten)
(("" (prop)
(("1" (hide -2)
(("1" (expand "verts_in?")
(("1" (skosimp*)
(("1" (expand "verts_of")
(("1" (inst 2 "i!1")
(("1" (expand "finseq_appl")
(("1" (inst?)
(("1" (expand "del_vert")
(("1" (expand "remove")
(("1" (expand "member")
(("1" (assert) nil)))))))))))))))))))))
("2" (skosimp*)
(("2" (inst?)
(("2" (hide -2)
(("2" (expand "del_vert")
(("2" (expand "edge?")
(("2" (assert)
(("2" (flatten)
(("2" (assert)
(("2" (expand "verts_of")
(("2" (expand "dbl")
(("2"
(hide -3 1)
(("2"
(split)
(("1" (inst?) (("1" (assert) nil)))
("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))
nil)
((walk? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks nil)
(verts_of const-decl "finite_set[T]" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets 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 path_ops 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)
(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)
(dbl const-decl "set[T]" doubletons nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" path_ops nil))
nil))
(path?_del_vert 0
(path?_del_vert-1 nil 3363193931
("" (skosimp*)
(("" (expand "path?")
(("" (flatten)
(("" (lemma "walk?_del_vert")
(("" (inst?) (("" (assert) nil))))))))))
nil)
((path? const-decl "bool" paths nil)
(walk?_del_vert formula-decl nil path_ops 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 path_ops nil))
nil))
(path?_del_verts 0
(path?_del_verts-1 nil 3363193931
("" (skosimp*)
(("" (expand "path?")
(("" (flatten)
(("" (split +)
(("1" (hide -2)
(("1" (expand "walk?")
(("1" (flatten)
(("1" (split +)
(("1" (hide -2)
(("1" (expand "verts_in?")
(("1" (expand "del_verts")
(("1" (expand "difference")
(("1" (expand "member")
(("1" (skosimp*)
(("1"
(inst?)
(("1" (assert) nil)))))))))))))))
("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (inst?)
(("2" (assert)
(("2" (expand "edge?")
(("2" (flatten)
(("2"
(assert)
(("2"
(expand "del_verts")
(("2"
(propax)
nil)))))))))))))))))))))))))
("2" (propax) nil))))))))
nil)
((path? const-decl "bool" paths nil)
(walk? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks nil)
(difference const-decl "set" sets 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 path_ops 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)
(member const-decl "bool" sets nil)
(del_verts const-decl "graph[T]" sep_sets 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" path_ops nil))
nil))
(walk_to_path 0
(walk_to_path-1 nil 3363193931
("" (skolem!)
((""
(case "FORALL (w: prewalk): NOT walk_from?(G!1, w, s!1, t!1)
OR (EXISTS (p: prewalk): path?(G!1, p) AND walk_from?(G!1, p, s!1, t!1))")
(("1" (flatten)
(("1" (skosimp*)
(("1" (inst -1 "w!1") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (hide 2)
(("2" (induct "w" 1 "graph_induction_walk")
(("2" (skosimp*)
(("2"
(case "(EXISTS (i,j: below(length(w!1))): i /= j AND w!1`seq(i) = w!1`seq(j))")
(("1" (skosimp*)
(("1" (case "i!1 < j!1")
(("1"
(inst -3 "w!1^(0,i!1) o w!1^(j!1+1,length(w!1)-1)")
(("1" (split -3)
(("1" (rewrite "walk?_cut") nil nil)
("2" (propax) nil nil)
("3" (hide -2 -3 3)
(("3" (expand "o ")
(("3" (expand* "^" min empty_seq)
(("3" (lift-if) (("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o ")
(("2" (expand* "^" min empty_seq)
(("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(inst -2
"w!1^(0,j!1) o w!1^(i!1+1,length(w!1)-1)")
(("1" (assert)
(("1" (split -2)
(("1" (hide 4)
(("1" (rewrite "walk?_cut") nil nil)) nil)
("2" (propax) nil nil)
("3" (expand "o ")
(("3" (expand* "^" min empty_seq)
(("3"
(lift-if)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o ")
(("2" (expand* "^" min empty_seq)
(("2" (lift-if) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (inst 2 "w!1")
(("2" (assert)
(("2" (expand "path?")
(("2" (expand "walk_from?")
(("2" (expand "finseq_appl")
(("2" (flatten)
(("2" (assert)
(("2"
(skosimp*)
(("2"
(inst?)
(("2" (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)
(walk_from? const-decl "bool" walks nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(prewalk type-eq-decl nil walks 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)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil path_ops nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(graph_induction_walk formula-decl nil walk_inductions 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)
(walk?_cut formula-decl nil walks nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j!1 skolem-const-decl "below(length(w!1))" path_ops nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(i!1 skolem-const-decl "below(length(w!1))" path_ops nil)
(w!1 skolem-const-decl "prewalk[T]" path_ops nil)
(^ const-decl "finseq" finite_sequences nil)
(O const-decl "finseq" finite_sequences nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
nil))
(walk_to_path_less 0
(walk_to_path_less-2 "underconstr" 3363278454
("" (skolem * ("G!1" "s!1" "t!1" "_"))
(("" (induct "w" 1 "graph_induction_walk")
(("" (skosimp*)
((""
(case "(EXISTS (i,j: below(length(w!1))): i /= j AND seq(w!1)(i) = seq(w!1)(j))")
(("1" (skosimp*)
(("1" (case "i!1 < j!1")
(("1" (inst -3 "w!1^(0,i!1) o w!1^(j!1+1,length(w!1)-1)")
(("1" (split -3)
(("1" (skosimp*)
(("1"
(case " length(w!1 ^ (0, i!1) o w!1 ^ (j!1 + 1, length(w!1) - 1)) <= length(w!1)")
(("1" (inst 2 "p!1") (("1" (assert) nil nil))
nil)
("2" (hide -1 -2 -3 3)
(("2" (install-rewrites "walks[T]")
(("2" (assert)
(("2" (hide -3) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (install-rewrites "walks[T]")
(("2" (expand "walk_from?")
(("2" (bddsimp)
(("1" (lemma "walk?_cut")
(("1"
(inst -1 "G!1" "w!1" "s!1" "t!1" "i!1"
"j!1")
(("1"
(prop)
(("1"
(expand "walk_from?")
(("1" (prop) nil nil))
nil)
("2"
(expand "walk_from?")
(("2" (prop) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide -5)
(("2"
(lift-if 1)
(("2"
(bddsimp)
(("1"
(expand* "^" min empty_seq)
(("1"
(lift-if 1)
(("1"
(bddsimp)
(("1"
(lift-if)
(("1"
(prop)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil)
("3"
(lift-if -1)
(("3"
(bddsimp)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand* "^" min empty_seq)
(("2"
(lift-if 2)
(("2"
(lift-if 1)
(("2"
(bddsimp)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (hide -3 3)
(("3" (typepred "j!1") (("3" (grind) nil nil))
nil))
nil))
nil)
("2" (hide -3 3)
(("2" (install-rewrites "walks[T]")
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (inst -2 "w!1^(0,j!1) o w!1^(i!1+1,length(w!1)-1)")
(("1" (assert)
(("1" (split -2)
(("1" (skosimp*)
(("1" (inst 3 "p!1")
(("1" (bddsimp)
(("1" (hide -1 -2 -5)
(("1" (install-rewrites "walks[T]")
(("1"
(assert)
(("1"
(expand* "^" min empty_seq)
(("1"
(lift-if -1)
(("1"
(bddsimp)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 4)
(("2" (lemma "walk?_cut")
(("2"
(inst -1 "G!1" "w!1" "s!1" "t!1" "j!1" "i!1")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (hide -2 4)
(("3" (install-rewrites "walks[T]")
(("3" (assert)
(("3" (expand* "^" min empty_seq)
(("3" (lift-if 1)
(("3"
(bddsimp)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 4)
(("2" (install-rewrites "walks[T]")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (inst 2 "w!1")
(("2" (assert)
(("2" (install-rewrites "paths[T]")
(("2" (expand "path?")
(("2" (expand "walk_from?")
(("2" (bddsimp)
(("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (inst 1 "i!1" "j!1")
(("2" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(prewalk type-eq-decl nil walks nil)
(pred type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" 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)
(graph type-eq-decl nil graphs nil)
(walk_from? const-decl "bool" walks nil)
(path? const-decl "bool" paths nil)
(<= const-decl "bool" reals nil)
(T formal-type-decl nil path_ops nil)
(graph_induction_walk formula-decl nil walk_inductions 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_lt_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)
(empty_seq const-decl "finseq" finite_sequences nil)
(walk? const-decl "bool" walks nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(verts_in? const-decl "bool" walks nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "finite_set[T]" path_ops nil)
(walk?_cut formula-decl nil walks nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(j!1 skolem-const-decl "below(length(w!1))" path_ops nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(i!1 skolem-const-decl "below(length(w!1))" path_ops nil)
(w!1 skolem-const-decl "prewalk[T]" path_ops nil)
(^ const-decl "finseq" finite_sequences nil)
(O const-decl "finseq" finite_sequences nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(odd_plus_even_is_odd application-judgement "odd_int" integers
nil))
shostak)
(walk_to_path_less-1 nil 3363193979
("" (skolem!)
((""
(case "FORALL (w: prewalk): NOT walk_from?(G!1, w, s!1, t!1)
OR (EXISTS (p: prewalk): path?(G!1, p) AND walk_from?(G!1, p, s!1, t!1))")
(("1" (flatten)
(("1" (skosimp*)
(("1" (inst -1 "w!1") (("1" (assert) nil)))))))
("2" (hide 2)
(("2" (induct "w" 1 "graph_induction_walk")
(("2" (skosimp*)
(("2"
(case "(EXISTS (i,j: below(length(w!1))): i /= j AND seq(w!1)(i) = seq(w!1)(j))")
(("1" (skosimp*)
(("1" (case "i!1 < j!1")
(("1"
(inst -3 "w!1^(0,i!1) o w!1^(j!1+1,length(w!1)-1)")
(("1" (split -3)
(("1" (rewrite "walk?_cut") nil)
("2" (propax) nil)
("3" (hide -2 -3 3)
(("3" (expand "o ")
(("3" (expand* "^" min empty_seq)
(("3" (expand "empty_seq")
(("3"
(lift-if)
(("3" (ground) nil)))))))))))))
("2" (expand "o ")
(("2" (expand* "^" min empty_seq)
(("2" (lift-if)
(("2" (expand "empty_seq")
(("2" (propax) nil)))))))))))
("2" (assert)
(("2"
(inst -2
"w!1^(0,j!1) o w!1^(i!1+1,length(w!1)-1)")
(("1" (assert)
(("1" (split -2)
(("1" (hide 4)
(("1" (rewrite "walk?_cut") nil)))
("2" (propax) nil)
("3" (expand "o ")
(("3" (expand* "^" min empty_seq)
(("3"
(lift-if)
(("3"
(expand "empty_seq")
(("3" (propax) nil)))))))))))))
("2" (expand "o ")
(("2" (expand* "^" min empty_seq)
(("2" (expand "empty_seq")
(("2" (lift-if)
(("2" (ground) nil)))))))))))))))))
("2" (hide -1)
(("2" (inst 2 "w!1")
(("2" (assert)
(("2" (expand "path?")
(("2" (expand "walk_from?")
(("2" (flatten)
(("2" (assert)
(("2" (skosimp*)
(("2"
(expand "finseq_appl")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))
nil)
nil nil))
(walk_to_path_from 0
(walk_to_path_from-1 nil 3363193931
("" (skosimp*)
(("" (lemma "walk_to_path")
(("" (inst?)
(("" (inst -1 "s!1" "t!1")
(("" (split -1)
(("1" (skosimp*)
(("1" (inst?)
(("1" (expand "path_from?")
(("1" (assert)
(("1" (expand "walk_from?")
(("1" (flatten)
(("1" (expand "from?")
(("1" (assert) nil)))))))))))))))
("2" (inst?) nil))))))))))
nil)
((walk_to_path formula-decl nil path_ops nil)
(path_from? const-decl "bool" paths nil)
(walk_from? const-decl "bool" walks nil)
(from? const-decl "bool" walks nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(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 path_ops nil))
nil))
(walk_to_path_from_less 0
(walk_to_path_from_less-1 nil 3363292497
("" (skosimp*)
(("" (lemma "walk_to_path_less")
(("" (inst?)
(("" (prop)
(("" (skosimp*)
(("" (inst?)
(("" (expand "path_from?")
(("" (expand "walk_from?")
(("" (prop)
(("" (expand "from?") (("" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((walk_to_path_less formula-decl nil path_ops nil)
(walk_from? const-decl "bool" walks nil)
(from? const-decl "bool" walks nil)
(path_from? const-decl "bool" paths 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 path_ops nil))
nil))
(path_disjoint_TCC1 0
(path_disjoint_TCC1-1 nil 3389448101 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dbl const-decl "set[T]" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(T formal-type-decl nil path_ops nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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]" path_ops nil))
nil))
(path_disjoint_TCC2 0
(path_disjoint_TCC2-1 nil 3389448101 ("" (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)
(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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(T formal-type-decl nil path_ops nil)
(trunc1 const-decl "prewalk" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(verts_of const-decl "finite_set[T]" walks nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(verts_in? const-decl "bool" walks 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)
(O const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil)
(nil application-judgement "finite_set[T]" path_ops nil))
nil))
(path_disjoint 0
(path_disjoint-1 nil 3389448102
("" (skosimp*)
(("" (case "walk_from?(G!1, p!1, u!1, yt!1)")
(("1" (case " walk_from?(G!1, q!1, yt!1, v!1)")
(("1" (lemma "walk_concat")
(("1" (lemma "walk?_rev")
(("1" (inst -1 "G!1" "q!1")
(("1" (expand "walk_from?" (-3 -4))
(("1"
(inst -2 "G!1" "u!1" "v!1" "yt!1" "p!1" "rev(q!1)")
(("1" (lemma "rev_rev")
(("1" (case "length(p!1)>1")
(("1" (prop)
(("1" (inst -4 "q!1")
(("1" (replace -4 -1 lr)
(("1" (expand "path_from?")
(("1"
(prop)
(("1"
(expand "path?")
(("1"
(expand "finseq_appl")
(("1"
(prop)
(("1"
(expand "walk_from?")
(("1"
(prop)
(("1"
(expand "trunc1")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(hide -2 -3 -5 -11 -12)
(("2"
(hide -10)
(("2"
(expand "o ")
(("2"
(lift-if -1)
(("2"
(prop)
(("1"
(lift-if -2)
(("1"
(prop)
(("1"
(hide
-5
-6
-11
-13
-14)
(("1"
(inst
-8
"i!1"
"j!1")
(("1"
(assert)
(("1"
(hide
-5
-9)
(("1"
(expand
"trunc1")
(("1"
(expand
"^")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"trunc1")
(("2"
(expand
"^")
(("2"
(expand
"empty_seq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(expand
"trunc1")
(("3"
(expand
"^")
(("3"
(expand
"empty_seq")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"empty?")
(("2"
(expand
"member")
(("2"
(inst
-13
"seq(trunc1(p!1))(i!1)")
(("2"
(expand
"intersection")
(("2"
(expand
"member")
(("2"
(prop)
(("1"
(expand
"verts_of")
(("1"
(inst
1
"i!1")
(("1"
(expand
"finseq_appl")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(replace
-1
1
lr)
(("2"
(expand
"verts_of")
(("2"
(expand
"finseq_appl")
(("2"
(inst
1
"j!1-length(trunc1(p!1))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lift-if -1)
(("2"
(prop)
(("1"
(hide
-4
-5
-6
-7
-8
-9
-10
-11
-12)
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(inst
-4
"seq(trunc1(p!1))(j!1)")
(("1"
(expand
"intersection")
(("1"
(expand
"member")
(("1"
(prop)
(("1"
(expand
"verts_of")
(("1"
(expand
"finseq_appl")
(("1"
(inst
1
"j!1")
nil
nil))
nil))
nil)
("2"
(replace
-2
1
rl)
(("2"
(expand
"verts_of")
(("2"
(expand
"finseq_appl")
(("2"
(inst
1
"i!1-length(trunc1(p!1))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-10
"i!1-length(trunc1(p!1))"
"j!1-length(trunc1(p!1))")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-2 -4 -7 -10 -11 -13 -15))
(("2"
(install-rewrites "walks[T]")
(("2"
(assert)
(("2"
(expand* "^" min empty_seq)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-10 1))
(("2" (expand "path_from?")
(("2" (install-rewrites "paths[T]")
(("2"
(expand "walk_from?")
(("2"
(prop)
(("1"
(expand "from?")
(("1" (prop) nil nil))
nil)
("2"
(expand "from?")
(("2" (prop) nil nil))
nil)
("3"
(expand "path?")
(("3" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but (-1 -4 -5 -6 1 2))
(("3" (install-rewrites "paths[T]")
(("3" (expand "walk_from?")
(("3"
(prop)
(("1"
(expand "rev")
(("1" (propax) nil nil))
nil)
("2"
(expand "rev")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "length(p!1)=1")
(("1" (replace -1 - lr)
(("1" (assert)
(("1" (prop)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "rev")
(("2" (typepred "q!1") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-3 1))
(("2" (install-rewrites "paths[T]")
(("2" (expand "path_from?")
(("2" (prop)
(("2" (expand "walk_from?")
(("2" (prop)
(("1" (expand "from?") (("1" (prop) nil nil)) nil)
("2" (expand "from?") (("2" (prop) nil nil)) nil)
("3" (expand "path?") (("3" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (expand "path_from?")
(("2" (expand "walk_from?")
(("2" (prop)
(("1" (expand "from?") (("1" (prop) nil nil)) nil)
("2" (expand "from?") (("2" (prop) nil nil)) nil)
("3" (expand "path?") (("3" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((walk_from? const-decl "bool" walks nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.83 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.
|
