|
(cycles
(cycle?_TCC1 0
(cycle?_TCC1-1 nil 3559643154 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil cycles 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)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(/= const-decl "boolean" notequal nil))
nil))
(cycle?_TCC2 0
(cycle?_TCC2-1 nil 3559643154 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil cycles 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)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(/= const-decl "boolean" notequal nil))
nil))
(cycle_is_circuit 0
(cycle_is_circuit-1 nil 3559643176
("" (skeep)
(("" (expand "cycle?")
(("" (expand "circuit?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cycle? const-decl "bool" cycles nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(circuit? const-decl "bool" circuits nil))
shostak))
(circuit_subwalk_cycle_TCC1 0
(circuit_subwalk_cycle_TCC1-1 nil 3564335113
("" (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)
(T formal-type-decl nil cycles 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)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil))
nil))
(circuit_subwalk_cycle 0
(circuit_subwalk_cycle-1 nil 3564335167
("" (measure-induct+ "length(w)" "w")
(("1" (skeep)
(("1" (case "cycle?(G, x!1)")
(("1" (hide -2)
(("1" (inst 1 "x!1")
(("1" (split)
(("1" (expand "sub_walk?")
(("1" (inst 1 "0" "length(x!1) - 1")
(("1" (decompose-equality)
(("1" (expand* "^" "min") nil nil)
("2" (decompose-equality)
(("2" (expand* "^" "min") nil nil)) nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "cycle?" 1)
(("2" (prop)
(("2" (skeep)
(("2" (expand "finseq_appl")
(("2" (case "i < j")
(("1" (inst -3 "x!1^(i, j)")
(("1" (inst -3 "G")
(("1" (expand "^" -3 1)
(("1" (expand* "empty_seq" "min")
(("1" (assert)
(("1" (split -3)
(("1"
(skeep -1)
(("1"
(inst 2 "w1")
(("1"
(assert)
(("1"
(expand "sub_walk?")
(("1"
(skosimp)
(("1"
(typepred
"i"
"j"
"i!1"
"j!1")
(("1"
(inst
2
"i + i!1"
"i + j!1")
(("1"
(replace -5 2 rl)
(("1"
(hide -5)
(("1"
(decompose-equality
2)
(("1"
(expand*
"^"
"min"
"empty_seq")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(decompose-equality)
(("2"
(expand "^" 1 3)
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand*
"^"
"min")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand*
"^"
"min")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -4 1))
(("2"
(expand "^")
(("2"
(expand "min")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide-all-but (-1 -3 1))
(("3"
(expand* "^" "min")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(expand*
"circuit?"
"pre_circuit?"
"finseq_appl")
(("2"
(rewrite "walk?_caret")
(("2"
(expand* "^" "min" "empty_seq")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 -3 3)
(("2" (expand* "^" "min" "empty_seq")
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (inst -2 "x!1^(j, i)")
(("1" (inst -2 "G")
(("1" (expand "^" -2 1)
(("1" (expand* "min" "empty_seq")
(("1" (assert)
(("1" (split -2)
(("1"
(skeep -1)
(("1"
(inst 3 "w1")
(("1"
(assert)
(("1"
(hide -2)
(("1"
(expand "sub_walk?")
(("1"
(skosimp)
(("1"
(typepred
"i"
"j"
"i!1"
"j!1")
(("1"
(inst
3
"j + i!1"
"j + j!1")
(("1"
(replace -5 3 rl)
(("1"
(hide -5)
(("1"
(decompose-equality
3)
(("1"
(expand*
"^"
"min"
"empty_seq")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(decompose-equality
1)
(("2"
(expand
"^"
1
3)
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand*
"^"
"min")
(("1"
(assert)
nil
nil))
nil)
("2"
(expand*
"^"
"min")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-2 -4 +))
(("2"
(expand* "^" "min")
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(hide-all-but
(-2 -3 +))
(("3"
(expand* "^" "min")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 4)
(("2"
(expand*
"circuit?"
"pre_circuit?"
"finseq_appl")
(("2"
(rewrite "walk?_caret")
(("2" (expand* "^" "min") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "^" "min") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (skeep)
(("2" (expand* "circuit?" "pre_circuit?" "finseq_appl")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (hide-all-but (-1 1))
(("3" (skeep)
(("3" (expand* "circuit?" "pre_circuit?" "finseq_appl")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil)
((empty_seq const-decl "finseq" finite_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(j!1 skolem-const-decl "below(length(x!1 ^ (i, j)))" cycles nil)
(i!1 skolem-const-decl "below(length(x!1 ^ (i, j)))" cycles nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(pre_circuit? const-decl "bool" circuits nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(walk?_caret formula-decl nil walks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(j skolem-const-decl "below(length(x!1) - 1)" cycles nil)
(i skolem-const-decl "below(length(x!1) - 1)" cycles nil)
(x!1 skolem-const-decl "prewalk[T]" cycles nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(i!1 skolem-const-decl "below(length(x!1 ^ (j, i)))" cycles nil)
(j!1 skolem-const-decl "below(length(x!1 ^ (j, i)))" cycles nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(cycle? const-decl "bool" cycles nil)
(sub_walk? const-decl "bool" walks nil)
(Walk 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)
(circuit? const-decl "bool" circuits nil)
(walk? const-decl "bool" walks nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber 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)
(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 cycles nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(cycle_prefix_TCC1 0
(cycle_prefix_TCC1-1 nil 3579270878 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil cycles 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)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(/= const-decl "boolean" notequal nil)
(cycle? const-decl "bool" cycles nil)
(O const-decl "finseq" finite_sequences nil))
nil))
(cycle_prefix 0
(cycle_prefix-1 nil 3582385881
("" (auto-rewrite "finseq_appl")
(("" (skeep)
(("" (lemma "circuit_subwalk_cycle")
(("" (inst -1 "G" "w")
(("" (assert)
(("" (skeep -1)
(("" (expand "sub_walk?")
(("" (skeep -1)
(("" (typepred "i" "j")
(("" (case "i = 0 AND j = length(w) - 1")
(("1" (flatten)
(("1" (replaces -1)
(("1" (replaces -1)
(("1" (hide-all-but (-3 -4 1))
(("1"
(case-replace "w1 = w")
(("1"
(hide -2 2)
(("1"
(replace -1 1 rl)
(("1"
(hide -1)
(("1"
(decompose-equality)
(("1"
(expand* "^" "min")
nil
nil)
("2"
(decompose-equality)
(("2"
(typepred "x!1")
(("2"
(expand* "^" "min")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "i > j")
(("1" (expand "^" -4)
(("1" (assert)
(("1" (hide-all-but (-4 -5))
(("1"
(expand* "cycle?" "circuit?")
(("1"
(flatten)
(("1"
(hide -2 -4)
(("1"
(expand "empty_seq")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "j = length(w) - 1")
(("1" (inst 4 "w1" "w^(1, i)")
(("1" (assert)
(("1"
(replace -4 4 rl)
(("1"
(rewrite "commuted_circuit_is_eq")
nil
nil))
nil))
nil)
("2" (hide-all-but (1 3))
(("2"
(expand* "^" "min")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2" (case-replace "i = 0")
(("1" (hide -1 -2 3 4)
(("1"
(inst
3
"w1"
"w^(j + 1, length(w) - 1)")
(("1"
(assert)
(("1"
(case-replace
"w1 o w ^ (1 + j, length(w) - 1) = w")
(("1"
(hide-all-but (-5 3))
(("1"
(rewrite
"eq_circuit_reflexive")
nil
nil))
nil)
("2"
(replace -2 1 rl)
(("2"
(hide -2 -3 -4 3 4)
(("2"
(decompose-equality)
(("1"
(expand*
"o"
"^"
"min"
"empty_seq")
nil
nil)
("2"
(decompose-equality)
(("2"
(typepred "x!1")
(("2"
(expand*
"o"
"^"
"min"
"empty_seq")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide - 3)
(("2"
(expand* "^" "min")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -5 4 5)
(("2"
(inst
4
"w1"
"w^(j+1, length(w)-1) o w^(1, i)")
(("1"
(assert)
(("1"
(rewrite "o_assoc")
(("1"
(replace -2 4 rl)
(("1"
(hide -2 -3)
(("1"
(case-replace
"w^(i, j) o w^(1 + j, length(w) - 1) = w^(i, length(w) - 1)")
(("1"
(hide -1)
(("1"
(rewrite
"commuted_circuit_is_eq")
nil
nil))
nil)
("2"
(hide 5)
(("2"
(decompose-equality)
(("1"
(expand*
"o"
"^"
"min"
"empty_seq")
nil
nil)
("2"
(decompose-equality)
(("2"
(typepred "x!1")
(("2"
(expand*
"o"
"^"
"min"
"empty_seq")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2 -3)
(("2"
(expand* "o" "^" "min" "empty_seq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil cycles nil)
(edgetype type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(commuted_circuit_is_eq formula-decl nil circuits nil)
(i skolem-const-decl "below(length(w))" cycles nil)
(w skolem-const-decl "prewalk[T]" cycles 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)
(o_assoc formula-decl nil finite_sequences nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(eq_circuit_reflexive formula-decl nil circuits nil)
(O const-decl "finseq" finite_sequences nil)
(j skolem-const-decl "below(length(w))" cycles nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(cycle? const-decl "bool" cycles nil)
(circuit? const-decl "bool" circuits 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)
(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)
(sub_walk? const-decl "bool" walks nil)
(circuit_subwalk_cycle formula-decl nil cycles nil))
shostak))
(cycle_o_circuit_TCC1 0
(cycle_o_circuit_TCC1-1 nil 3579270878 ("" (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_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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil cycles 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)
(walk? const-decl "bool" walks nil)
(pre_circuit? const-decl "bool" circuits nil)
(circuit? const-decl "bool" circuits nil)
(/= const-decl "boolean" notequal nil)
(cycle? const-decl "bool" cycles nil)
(rest const-decl "finseq" seq_extras "structures/")
(O const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(cycle_o_circuit 0
(cycle_o_circuit-1 nil 3582583306
("" (auto-rewrite "finseq_appl")
(("" (skeep)
(("" (lemma "cycle_prefix")
(("" (inst -1 "G" "w")
(("" (assert)
(("" (skeep)
(("" (inst 2 "w1" "add_first(last(w1), w2)")
(("1" (rewrite "rest_add_first")
(("1" (assert)
(("1" (expand "eq_circuit?")
(("1" (flatten)
(("1" (hide -2 -4 1)
(("1" (expand* "circuit?" "pre_circuit?")
(("1" (assert)
(("1"
(flatten)
(("1"
(split)
(("1"
(case
"add_first(last(w1), w2) = (w1 o w2) ^ (length(w1) - 1, length(w1 o w2) -1)")
(("1"
(replaces -1)
(("1"
(rewrite "walk?_caret")
(("1"
(expand "o" 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but (-3 1))
(("2"
(decompose-equality)
(("1"
(expand*
"add_first"
"insert?"
"o"
"^"
"min")
nil
nil)
("2"
(decompose-equality)
(("2"
(typepred "x!1")
(("2"
(expand*
"add_first"
"insert?"
"o"
"^"
"min")
(("2"
(assert)
(("2"
(expand "last")
(("2"
(assert)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil)
("2"
(expand* "add_first" "insert?")
(("2"
(expand "last")
(("2"
(assert)
(("2"
(expand "o" -2)
(("2"
(hide -1 -3)
(("2"
(expand*
"cycle?"
"circuit?"
"pre_circuit?")
(("2"
(flatten)
(("2"
(hide -2 -4 -5)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3"
(expand* "add_first" "insert?")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand* "add_first" "insert?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil cycles nil)
(edgetype type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs 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)
(rest_add_first formula-decl nil seq_extras "structures/")
(eq_circuit? const-decl "bool" circuits nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(< const-decl "bool" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(insert? const-decl "finseq" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(walk?_caret formula-decl nil walks 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)
(O const-decl "finseq" finite_sequences nil)
(^ const-decl "finseq" finite_sequences 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 "[T, T -> boolean]" equalities nil)
(cycle? const-decl "bool" cycles nil)
(circuit? const-decl "bool" circuits nil)
(pre_circuit? const-decl "bool" circuits nil)
(w2 skolem-const-decl "prewalk[T]" cycles nil)
(w1 skolem-const-decl "prewalk[T]" cycles nil)
(last const-decl "T" seq_extras "structures/")
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(/= const-decl "boolean" notequal nil)
(add_first const-decl "finseq" seq_extras "structures/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cycle_prefix formula-decl nil cycles nil))
shostak))
(Pigeon_hole 0
(Pigeon_hole-1 nil 3507100929
("" (skosimp*)
(("" (lemma "seq_pigeon_hole[T,(vert(GF!1))]")
(("" (inst?)
(("1" (assert)
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst 2 "j!1")
(("1" (expand "finseq_appl") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (hide 2)
(("2" (typepred "x1!1")
(("2" (typepred "w!1")
(("2" (expand "walk?")
(("2" (flatten)
(("2" (expand "verts_in?") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Digraph type-eq-decl nil digraphs nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets 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 cycles nil)
(seq_pigeon_hole formula-decl nil seq_pigeon "structures/")
(NOT const-decl "[bool -> bool]" booleans nil)
(verts_in? const-decl "bool" walks nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(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)
(walk? const-decl "bool" walks nil)
(GF!1 skolem-const-decl "Digraph[T]" cycles nil)
(Walk type-eq-decl nil walks nil)
(w!1 skolem-const-decl "Walk[T](GF!1)" cycles nil))
nil)))
¤ Dauer der Verarbeitung: 0.40 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.
|
