| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 113 kB |
|
SSL circuits.prfSprache: 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil circuits 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) (eq_circuit? const-decl "bool" circuits nil) (eq_prewalk? const-decl "bool" walks nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (x!1 skolem-const-decl "below[w2`length]" circuits nil) (w2 skolem-const-decl "prewalk[T]" circuits nil) (int_plus_int_is_int application-judgement "int" integers nil) (empty_seq const-decl "finseq" finite_sequences nil) (x!1 skolem-const-decl "below[w2`length]" circuits nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (O const-decl "finseq" finite_sequences nil) (x!1 skolem-const-decl "below[w2`length]" circuits nil) (w1 skolem-const-decl "prewalk[T]" circuits nil) (i skolem-const-decl "posnat" circuits nil) (reord_prewalk const-decl "prewalk" walks nil) (rest const-decl "finseq" seq_extras "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (pre_circuit? const-decl "bool" circuits nil) (circuit? const-decl "bool" circuits 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (empty_o_seq formula-decl nil seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (equal_rest_equal_circuit formula-decl nil circuits nil) (eq_circuit_length formula-decl nil circuits nil)) shostak)) (eq_circuit_edges 0 (eq_circuit_edges-1 nil 3581720334 ("" (auto-rewrite "finseq_appl") (("" (skeep) (("" (lemma "eq_circuit_length") (("" (inst -1 "G" "w1" "w2") (("" (assert) (("" (lemma "eq_circuit_position") (("" (inst -1 "G" "w1" "w2") (("" (assert) (("" (skeep) (("" (expand* "eq_circuit?" "circuit?" "pre_circuit?") (("" (flatten) (("" (assert) (("" (hide -3 -6 -9) (("" (case-replace "w1 = w2") (("" (case "i > length(w1) - 1 OR i = length(w1) - 1") (("1" (hide 2) (("1" (split) (("1" (expand "^" -2 1) (("1" (assert) nil nil)) nil) ("2" (replaces -1) (("2" (expand "o" -1) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (expand* "^" "min" "empty_seq") (("2" (decompose-equality -1) (("2" (decompose-equality -1) (("2" (inst -1 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (decompose-equality 4) (("2" (iff) (("2" (prop) (("1" (expand "edges_of") (("1" (skeep) (("1" (assert) (("1" (typepred "i!1") (("1" (case "i!1 < i") (("1" (inst 1 "length(w1) - i + i!1 - 1") (("1" (expand* "^" "min" "o") (("1" (decompose-equality -5) (("1" (decompose-equality -1) (("1" (inst-cp -1 "length(w1) - i + i!1") (("1" (assert) (("1" (inst -1 "length(w1) - i + i!1 - 1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand* "^" "min" "o") (("2" (decompose-equality -4) (("2" (decompose-equality -1) (("2" (inst 2 "i!1 - i") (("1" (inst-cp -1 "i!1 - i") (("1" (assert) (("1" (inst -1 "i!1 - i + 1") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "edges_of") (("2" (skeep) (("2" (assert) (("2" (typepred "i!1") (("2" (expand* "^" "min" "o") (("2" (decompose-equality -4) (("2" (decompose-equality -1) (("2" (case "i!1 < w1`length - i - 1") (("1" (inst-cp -2 "i!1") (("1" (inst -2 "i!1 + 1") (("1" (assert) (("1" (inst 1 "i!1 + i") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst-cp -1 "i!1") (("2" (inst -1 "i!1 + 1") (("2" (assert) (("2" (case-replace "i!1 = w1`length - 1 - i") (("1" (assert) (("1" (hide -1 1) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst 3 "1 - w1`length + i!1 + i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil circuits 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) (eq_circuit_position formula-decl nil circuits nil) (circuit? const-decl "bool" circuits nil) (pre_circuit? const-decl "bool" circuits nil) (eq_circuit? const-decl "bool" circuits 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (w2 skolem-const-decl "prewalk[T]" circuits nil) (i!1 skolem-const-decl "below(length(w1) - 1)" circuits nil) (i skolem-const-decl "below[length(w1)]" circuits nil) (w1 skolem-const-decl "prewalk[T]" circuits nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (edges_of const-decl "finite_set[edgetype[T]]" walks nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (O const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (eq_circuit_length formula-decl nil circuits nil)) shostak)) (commuted_circuit_TCC1 0 (commuted_circuit_TCC1-1 nil 3582567742 ("" (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) (pre_circuit? const-decl "bool" circuits nil) (circuit? const-decl "bool" circuits nil)) nil)) (commuted_circuit_TCC2 0 (commuted_circuit_TCC2-1 nil 3582567742 ("" (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) (< 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) (real_ge_is_total_order name-judgement "(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_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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (commuted_circuit 0 (commuted_circuit-1 nil 3582569158 ("" (auto-rewrite "finseq_appl") (("" (skeep) (("" (typepred "i") (("" (case "i = 0 OR i = w`length - 1") (("1" (split) (("1" (replaces -1) (("1" (hide -1) (("1" (expand "^" 1 2) (("1" (rewrite "seq_o_empty") (("1" (case-replace "w ^ (0, w`length - 1) = w") (("1" (hide -1 2) (("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) ("2" (replaces -1) (("2" (hide -1) (("2" (case-replace "w ^ (w`length - 1, w`length - 1) o w ^ (1, w`length - 1) = w") (("2" (hide 2) (("2" (expand* "circuit?" "pre_circuit?") (("2" (flatten) (("2" (hide -1) (("2" (decompose-equality 1) (("1" (expand* "o" "^" "min" "empty_seq") nil nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand* "o" "^" "min" "empty_seq") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "circuit?") (("2" (flatten) (("2" (split) (("1" (expand "pre_circuit?") (("1" (flatten) (("1" (split) (("1" (lemma "walk_o") (("1" (inst -1 "G" "w ^ (i, w`length - 1)" "w ^ (0, i)") (("1" (rewrite "walk?_caret") (("1" (rewrite "walk?_caret") (("1" (expand "^" -1 (1 2 3 7)) (("1" (expand "min") (("1" (assert) (("1" (case-replace "w ^ (0, i) ^ (1, i) = w ^ (1, i)") (("1" (hide -1 -3 -4 2) (("1" (decompose-equality) (("1" (expand* "^" "min" "empty_seq") nil nil) ("2" (decompose-equality) (("2" (typepred "x!1") (("2" (expand* "^" "min" "empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand* "^" "min") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2 -3) (("2" (expand "^" 1 (5 6)) (("2" (expand "o" 1 3) (("2" (expand "min") (("2" (expand "o") (("2" (expand "^") (("2" (expand "min") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "o") (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (O const-decl "finseq" finite_sequences nil) (pre_circuit? const-decl "bool" circuits nil) (circuit? const-decl "bool" circuits nil) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (seq_o_empty formula-decl nil seq_extras "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (walk_o formula-decl nil walks nil) (walk?_caret formula-decl nil walks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs 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) (i skolem-const-decl "below[w`length]" circuits nil) (w skolem-const-decl "prewalk[T]" circuits nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil circuits nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil)) shostak)) (commuted_circuit_is_eq 0 (commuted_circuit_is_eq-1 nil 3582567599 ("" (auto-rewrite "finseq_appl") (("" (skeep) (("" (expand "eq_circuit?") (("" (prop) (("1" (rewrite "commuted_circuit") nil nil) ("2" (expand "eq_prewalk?") (("2" (flatten) (("2" (typepred "i") (("2" (case "i = 0 or i = length(w) - 1") (("1" (split) (("1" (replaces -1) (("1" (hide -1 2) (("1" (expand "circuit?") (("1" (flatten) (("1" (hide -1) (("1" (decompose-equality) (("1" (expand* "rest" "o" "^" "min" "empty_seq") nil nil) ("2" (decompose-equality) (("2" (typepred "x!1") (("2" (expand* "rest" "o" "^" "min" "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (expand "circuit?") (("2" (flatten) (("2" (hide -1 -2 2) (("2" (decompose-equality) (("1" (expand* "rest" "o" "^" "min" "empty_seq") nil nil) ("2" (decompose-equality) (("2" (expand* "rest" "o" "^" "min" "empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide 3) (("2" (expand "circuit?") (("2" (flatten) (("2" (hide -2) (("2" (inst 3 "i") (("1" (expand "reord_prewalk") (("1" (expand "rest") (("1" (expand "o" 3 1) (("1" (expand "^" 3 (1 2)) (("1" (expand "min") (("1" (assert) (("1" (expand "o" 3 2) (("1" (expand "^" 3 (4 5)) (("1" (expand "min") (("1" (expand "^" 3 6) (("1" (expand "min") (("1" (decompose-equality 3) (("1" (expand* "o" "^" "min" "empty_seq") nil nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand* "o" "^" "min" "empty_seq") (("2" (lift-if) (("2" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (commuted_circuit formula-decl nil circuits nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers 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) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs nil) (circuit? const-decl "bool" circuits nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences 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) (w skolem-const-decl "prewalk[T]" circuits nil) (i skolem-const-decl "below[w`length]" circuits nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (reord_prewalk const-decl "prewalk" walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (eq_prewalk? const-decl "bool" walks nil) (eq_circuit? const-decl "bool" circuits nil)) shostak)))
¤ Dauer der Verarbeitung: 0.90 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26