| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ints/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 15 kB |
|
Quelle circuits.prf Sprache: Lisp |
|||||||||
|
(circuits
(pre_circuit?_TCC1 0 (pre_circuit?_TCC1-1 nil 3560614114 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil circuits 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)) nil)) (pre_circuit?_TCC2 0 (pre_circuit?_TCC2-1 nil 3560614114 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil circuits 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)) nil)) (eq_circuit?_TCC1 0 (eq_circuit?_TCC1-1 nil 3563142575 ("" (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) (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) (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 circuits 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) (rest const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (eq_circuit?_TCC2 0 (eq_circuit?_TCC2-1 nil 3563142575 ("" (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) (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) (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 circuits 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) (rest const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (eq_circuit_length 0 (eq_circuit_length-1 nil 3579518251 ("" (skeep) (("" (expand "eq_circuit?") (("" (flatten) (("" (lemma "eq_prewalk_length") (("" (inst -1 "rest(w1)" "rest(w2)") (("" (assert) (("" (hide -4) (("" (expand "circuit?") (("" (flatten) (("" (hide -2 -4) (("" (expand* "rest" "^" "min") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_circuit? const-decl "bool" circuits nil) (T formal-type-decl nil circuits nil) (eq_prewalk_length formula-decl nil walks nil) (circuit? const-decl "bool" circuits 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) (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) (rest const-decl "finseq" seq_extras "structures/") (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (eq_circuit_reflexive 0 (eq_circuit_reflexive-1 nil 3582581994 ("" (skeep) (("" (expand "eq_circuit?") (("" (assert) (("" (hide -1) (("" (lemma "eq_relation_eq_prewalk") (("" (expand "equivalence?") (("" (flatten) (("" (hide -2 -3) (("" (expand "reflexive?") (("" (inst -1 "rest(w)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_circuit? const-decl "bool" circuits nil) (equivalence? const-decl "bool" relations 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) (rest const-decl "finseq" seq_extras "structures/") (reflexive? const-decl "bool" relations nil) (eq_relation_eq_prewalk formula-decl nil walks nil) (T formal-type-decl nil circuits nil)) shostak)) (eq_circuit_symmetric 0 (eq_circuit_symmetric-1 nil 3563539116 ("" (skeep) (("" (expand "eq_circuit?") (("" (flatten) (("" (assert) (("" (hide -1 -2) (("" (lemma "eq_relation_eq_prewalk") (("" (expand "equivalence?") (("" (flatten) (("" (hide -1 -3) (("" (expand "symmetric?") (("" (inst -1 "rest(w1)" "rest(w2)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_circuit? const-decl "bool" circuits nil) (T formal-type-decl nil circuits nil) (eq_relation_eq_prewalk formula-decl nil walks nil) (symmetric? const-decl "bool" relations nil) (rest const-decl "finseq" seq_extras "structures/") (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (equivalence? const-decl "bool" relations nil)) shostak)) (loop_is_circuit 0 (loop_is_circuit-1 nil 3560698741 ("" (skeep) (("" (expand* "loop?" "circuit?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((circuit? const-decl "bool" circuits nil) (loop? const-decl "bool" circuits nil)) shostak)) (equal_rest_equal_circuit 0 (equal_rest_equal_circuit-1 nil 3578694276 ("" (skeep) (("" (decompose-equality 1) (("1" (hide -1 -2) (("1" (grind) nil nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand* "circuit?" "pre_circuit?" "finseq_appl") (("2" (flatten) (("2" (hide -2 -5) (("2" (expand "rest") (("2" (expand "^") (("2" (grind) (("2" (decompose-equality -6) (("2" (case "x!1 = 0") (("1" (inst -2 " w2`length - 2") (("1" (assert) nil nil)) nil) ("2" (hide -3 -5) (("2" (inst -1 "x!1 - 1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil circuits nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" 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 "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans 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) (w1 skolem-const-decl "prewalk[T]" circuits nil) (x!1 skolem-const-decl "below[w1`length]" circuits nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (circuit? const-decl "bool" circuits nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (pre_circuit? const-decl "bool" circuits 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)) shostak)) (equal_eq_circuit 0 (equal_eq_circuit-1 nil 3578330066 ("" (lemma "equal_rest_equal_circuit") (("" (skeep) (("" (inst -1 "G" "w1" "w2") (("" (expand "eq_circuit?") (("" (flatten) (("" (hide -4) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_circuit? const-decl "bool" circuits 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) (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 circuits nil) (equal_rest_equal_circuit formula-decl nil circuits nil)) shostak)) (circuit_equal_fisrt_TCC1 0 (circuit_equal_fisrt_TCC1-1 nil 3578740546 ("" (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) (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 circuits 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) (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)) (circuit_equal_fisrt_TCC2 0 (circuit_equal_fisrt_TCC2-1 nil 3578740546 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil circuits nil) (rest const-decl "finseq" seq_extras "structures/") (O const-decl "finseq" finite_sequences 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (circuit_equal_fisrt_TCC3 0 (circuit_equal_fisrt_TCC3-1 nil 3578740546 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil circuits nil) (rest const-decl "finseq" seq_extras "structures/") (O const-decl "finseq" finite_sequences 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (circuit_equal_fisrt 0 (circuit_equal_fisrt-1 nil 3578740547 ("" (skeep) (("" (expand "circuit?") (("" (expand "pre_circuit?") (("" (flatten) (("" (hide -1 -4 -7) (("" (expand "finseq_appl") (("" (expand "o ") (("" (case "rest(w2)`length > 0") (("1" (assert) (("1" (expand "rest" -6) (("1" (expand* "^" "min") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand* "rest" "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circuit? const-decl "bool" circuits nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (prewalk type-eq-decl nil walks nil) (rest const-decl "finseq" seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil circuits nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (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) (O const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (pre_circuit? const-decl "bool" circuits nil)) shostak)) (comp_circuit_inter_TCC1 0 (comp_circuit_inter_TCC1-1 nil 3578757841 ("" (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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil circuits 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)) (comp_circuit_inter 0 (comp_circuit_inter-1 nil 3578757843 ("" (skeep) (("" (expand "circuit?") (("" (expand "pre_circuit?") (("" (flatten) (("" (hide -1 -3) (("" (expand "finseq_appl") (("" (expand "o ") (("" (case "rest(w2)`length > 0") (("1" (assert) (("1" (hide -1) (("1" (expand "rest") (("1" (expand "^") (("1" (expand "min") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst -3 "w1`seq(0)") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (split) (("1" (inst 1 "0") nil nil) ("2" (inst 1 "w2`length - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "rest") (("2" (expand "^") (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circuit? const-decl "bool" circuits nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (prewalk type-eq-decl nil walks nil) (rest const-decl "finseq" seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil circuits nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (verts_of const-decl "finite_set[T]" walks nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_intersection2 application-judgement "finite_set[T]" circuits 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) (O const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (pre_circuit? const-decl "bool" circuits nil)) shostak)) (eq_circuit_position_TCC1 0 (eq_circuit_position_TCC1-1 nil 3582720412 ("" (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_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (T formal-type-decl nil circuits 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) (rest const-decl "finseq" seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (reord_prewalk const-decl "prewalk" walks nil) (eq_prewalk? const-decl "bool" walks nil) (eq_circuit? const-decl "bool" circuits nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (eq_circuit_position 0 (eq_circuit_position-1 nil 3582720425 ("" (auto-rewrite "finseq_appl") (("" (skeep) (("" (lemma "eq_circuit_length") (("" (inst -1 "G" "w1" "w2") (("" (assert) (("" (expand "eq_circuit?") (("" (flatten) (("" (expand "eq_prewalk?") (("" (split) (("1" (case-replace "w1 = w2") (("1" (hide -1 -2) (("1" (expand* "circuit?" "pre_circuit?") (("1" (flatten) (("1" (hide -1) (("1" (assert) (("1" (inst 1 "length(w2) - 1") (("1" (expand "^" 1 1) (("1" (rewrite "empty_o_seq") (("1" (decompose-equality 1) (("1" (expand* "^" "min") nil nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "equal_rest_equal_circuit") (("2" (inst -1 "G" "w1" "w2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand* "reord_prewalk" "rest") (("2" (expand "^" -1 4) (("2" (expand "min") (("2" (expand* "circuit?" "pre_circuit?") (("2" (flatten) (("2" (hide -3 -6) (("2" (assert) (("2" (case "i > length(w1) - 1") (("1" (expand "^" -2 3) (("1" (assert) (("1" (rewrite "empty_o_seq") (("1" (case-replace "(w1 ^ (1, w1`length - 1)) ^ (0, i - 1) = w1 ^ (1, w1`length - 1)") (("1" (hide -1) (("1" (inst 1 "length(w1) - 1") (("1" (expand "^" 1 1) (("1" (rewrite "empty_o_seq") (("1" (decompose-equality 1) (("1" (hide -2) (("1" (expand* "^" "min") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "^" 1) (("2" (expand "^" -3) (("2" (decompose-equality -3) (("1" (case-replace "x!1 = 0") (("1" (inst -2 "length(w2) - 2") (("1" (assert) nil nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil) ("2" (inst -1 "x!1 - 1") (("1" (assert) nil nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 -6 -7 2) (("2" (decompose-equality) (("1" (expand* "^" "min") nil nil) ("2" (decompose-equality) (("2" (expand* "^" "min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "(w1 ^ (1, w1`length - 1)) ^ (i, w1`length - 2) = w1 ^ (i + 1, w1`length - 1)") (("1" (hide -1) (("1" (case-replace "(w1 ^ (1, w1`length - 1)) ^ (0, i - 1) = w1 ^ (1, i)") (("1" (hide -1) (("1" (case "i = length(w1) - 1") (("1" (replace -1) (("1" (expand "^" -2 2) (("1" (rewrite "empty_o_seq") (("1" (inst 2 "i") (("1" (replaces -1) (("1" (expand "^" 2 1) (("1" (rewrite "empty_o_seq") (("1" (hide 1) (("1" (decompose-equality 1) (("1" (hide -1) (("1" (expand* "^" "min") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand* "^" "min") (("2" (decompose-equality -1) (("1" (typepred "x!1") (("1" (case "x!1 = 0") (("1" (inst -3 "length(w2) - 2") (("1" (assert) nil nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil) ("2" (inst -2 "x!1 - 1") (("1" (assert) nil nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 3 "i") (("1" (decompose-equality 3) (("1" (hide -1) (("1" (expand* "o" "^" "min" "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "o" -2) (("2" (decompose-equality) (("2" (hide -1) (("2" (decompose-equality) (("1" (expand "^" -1) (("1" (expand "min") (("1" (case-replace "x!1 = 0") (("1" (expand* "o" "^" "min" "empty_seq") (("1" (inst -2 "length(w2) - 2") (("1" (assert) nil nil) ("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -1 "x!1 - 1") (("1" (assert) (("1" (expand* "o" "^" "min" "empty_seq") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand* "^" "min" "empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (decompose-equality 1) (("1" (expand* "^" "min" "empty_seq") nil nil) ("2" (decompose-equality 1) (("2" (expand* "^" "min" "empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (decompose-equality 1) (("1" (expand* "^" "min" "empty_seq") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand* "^" "min" "empty_seq") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28