| products/sources/formale Sprachen/PVS/digraphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Merge.thy Sprache: LispUntersuchung PVS© |
|
||||||
|
(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.65 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
