| products/sources/formale sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: bits.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(bits
(bounding_bits_has_least 0 (bounding_bits_has_least-1 nil 3316868811 ("" (skosimp) (("" (use "every_nonempty_set_has_least") (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil) ((every_nonempty_set_has_least judgement-tcc nil bounded_nats "orders/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (n!1 skolem-const-decl "nat" bits nil) (bounding_bits const-decl "set[nat]" bits nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (exp2 def-decl "posnat" exp2 nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "above(n)" exp2 nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (bit_decoding_TCC1 0 (bit_decoding_TCC1-2 nil 3508504742 ("" (skosimp*) (("" (use "least_def" ("t" "1 + bit!1")) (("" (expand* "least?" "lower_bound?" "restrict") (("" (ground) (("" (inst - "bit!1") (("1" (assert) nil nil) ("2" (expand "bounding_bits" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (least_def formula-decl nil minmax_orders "orders/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders "orders/") (bounding_bits const-decl "set[nat]" bits nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nil application-judgement "above(n)" exp2 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) (bit!1 skolem-const-decl "nat" bits nil) (n!1 skolem-const-decl "nat" bits nil) (least? const-decl "bool" minmax_orders "orders/") (lower_bound? const-decl "bool" bounded_orders "orders/")) nil) (bit_decoding_TCC1-1 nil 3316868576 ("" (skosimp) (("" (use "bounding_bits_has_least") (("" (assert) nil nil)) nil)) nil) nil nil)) (bit_decoding_TCC2 0 (bit_decoding_TCC2-1 nil 3316868576 ("" (skosimp*) (("" (grind) nil nil)) nil) ((nil application-judgement "above(n)" exp2 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) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (bit_decoding_TCC3 0 (bit_decoding_TCC3-2 nil 3508504937 ("" (skosimp) (("" (use "bounding_bits_has_least") (("" (assert) nil nil)) nil)) nil) ((bounding_bits_has_least formula-decl nil bits nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (real_le_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)) nil) (bit_decoding_TCC3-1 nil 3316868576 ("" (skosimp*) (("" (use "least_def" ("t" "1 + bit!1")) (("" (expand* "least?" "lower_bound?" "restrict") (("" (ground) (("" (inst - "bit!1") (("1" (assert) nil nil) ("2" (expand "bounding_bits" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_def formula-decl nil minmax_orders "orders/") (antisymmetric? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (lower_bound? const-decl "bool" bounded_orders "orders/")) nil)) (bit_decoding_TCC4 0 (bit_decoding_TCC4-2 nil 3508504990 ("" (skosimp) (("" (typepred "least[nat](restrict[[real, real], [nat, nat], boolean](<=))(bounding_bits(n!1))") (("" (expand "least?") (("" (expand "bounding_bits" -1 :occurrence 1) (("" (rewrite "exp2_def" -1) (("" (lemma "expt_x0" ("x" "2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (has_least? const-decl "bool" minmax_orders "orders/") (pred type-eq-decl nil defined_types nil) (bounding_bits const-decl "set[nat]" bits nil) (set type-eq-decl nil sets nil) (nat nonempty-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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (expt_x0 formula-decl nil exponentiation 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) (posint_exp application-judgement "posint" exponentiation nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (exp2_def formula-decl nil exp2 nil)) nil) (bit_decoding_TCC4-1 nil 3316868576 ("" (termination-tcc) nil nil) nil nil)) (bit_decoding_has_greatest 0 (bit_decoding_has_greatest-1 nil 3316869847 ("" (skosimp) (("" (use "non_empty_finite_has_greatest") (("" (expand "bit_decoding") (("" (assert) nil nil)) nil)) nil)) nil) ((non_empty_finite_has_greatest formula-decl nil minmax_orders "orders/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (n!1 skolem-const-decl "nat" bits nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (bit_decoding def-decl "finite_set" bits nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonempty_add_finite application-judgement "non_empty_finite_set[nat]" bits 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) (nil application-judgement "above(n)" exp2 nil)) shostak)) (bit_decoding_max1_TCC1 0 (bit_decoding_max1_TCC1-1 nil 3316868576 ("" (skosimp) (("" (forward-chain "bit_decoding_has_greatest") nil nil)) nil) ((bit_decoding_has_greatest formula-decl nil bits nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (bit_decoding_max1 0 (bit_decoding_max1-2 nil 3508505373 ("" (lemma "bit_decoding_max1_TCC1") (("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (inst-cp -3 "j!1") (("" (assert) (("" (use "bit_decoding_TCC4") (("" (use "bit_decoding_TCC3") (("" (assert) (("" (typepred "greatest(lesseq)(bit_decoding(j!1))") (("" (expand "greatest?") (("" (expand "bit_decoding" -1 :occurrence 1) (("" (expand* "add" "member") (("" (lemma "least_le") (("" (inst - "lesseq" "bounding_bits(j!1)" "least(lesseq)(bounding_bits(j!1)) - 1") (("1" (expand "restrict") (("1" (assert) nil nil)) nil) ("2" (expand "bounding_bits" 1 :occurrence 1) (("2" (assert) (("2" (inst - "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)") (("2" (ground) (("1" (inst - "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)") (("1" (assert) (("1" (both-sides "+" "exp2(least[nat](restrict[[real, real], [nat, nat], boolean](<=))(bounding_bits(j!1)) - 1)" -1) (("1" (assert) (("1" (typepred "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (expand* "greatest?" "upper_bound?") (("1" (inst - "greatest(lesseq)(bit_decoding(j!1))") (("1" (expand "restrict" -2 :occurrence 1) (("1" (expand "restrict" -5 :occurrence 1) (("1" (lemma "exp2_def") (("1" (inst-cp - "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (inst - "greatest(lesseq)(bit_decoding(j!1))") (("1" (lemma "both_sides_expt_gt1_lt") (("1" (inst - "2" "greatest(lesseq)(bit_decoding(j!1))" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "bit_decoding_TCC3") (("2" (assert) (("2" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("2" (expand "bit_decoding" -2 :occurrence 1) (("2" (expand "emptyset") (("2" (propax) 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) ((<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (bit_decoding def-decl "finite_set" bits nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (has_greatest? const-decl "bool" minmax_orders "orders/") (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (exp2 def-decl "posnat" exp2 nil) (greatest? const-decl "bool" minmax_orders "orders/") (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders "orders/") (NAT_induction formula-decl nil naturalnumbers nil) (bit_decoding_TCC4 subtype-tcc nil bits nil) (member const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (bounding_bits const-decl "set[nat]" bits nil) (j!1 skolem-const-decl "nat" bits nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upper_bound? const-decl "bool" bounded_orders "orders/") (exp2_def formula-decl nil exp2 nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posint_exp application-judgement "posint" exponentiation nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (both_sides_plus_ge1 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (emptyset const-decl "set" sets nil) (least_le formula-decl nil minmax_orders "orders/") (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (bit_decoding_TCC3 subtype-tcc nil bits nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nil application-judgement "above(n)" exp2 nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bit_decoding_max1_TCC1 subtype-tcc nil bits nil)) nil) (bit_decoding_max1-1 nil 3316869877 ("" (lemma "bit_decoding_max1_TCC1") (("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (inst-cp -3 "j!1") (("" (assert) (("" (use "bit_decoding_TCC2") (("" (use "bit_decoding_TCC1") (("" (assert) (("" (typepred "greatest(lesseq)(bit_decoding(j!1))") (("" (expand "greatest?") (("" (flatten) (("" (expand "bit_decoding" -1 :occurrence 1) (("" (expand* "add" "member") (("" (lemma "least_le") (("" (inst - "lesseq" "bounding_bits(j!1)" "least(lesseq)(bounding_bits(j!1)) - 1") (("1" (expand "restrict") (("1" (assert) nil nil)) nil) ("2" (expand "bounding_bits" 1 :occurrence 1) (("2" (assert) (("2" (inst - "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)") (("2" (ground) (("1" (inst - "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)") (("1" (assert) (("1" (both-sides "+" "exp2(least[nat](restrict[[real, real], [nat, nat], boolean](<=))(bounding_bits(j!1)) - 1)" -1) (("1" (assert) (("1" (typepred "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (expand* "greatest?" "upper_bound?") (("1" (flatten) (("1" (inst - "greatest(lesseq)(bit_decoding(j!1))") (("1" (expand "restrict" -2 :occurrence 1) (("1" (expand "restrict" -5 :occurrence 1) (("1" (lemma "exp2_def") (("1" (inst-cp - "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (inst - "greatest(lesseq)(bit_decoding(j!1))") (("1" (lemma "both_sides_expt_gt1_lt") (("1" (inst - "2" "greatest(lesseq)(bit_decoding(j!1))" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "bit_decoding_TCC3") (("2" (assert) (("2" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("2" (expand "bit_decoding" -2 :occurrence 1) (("2" (expand "emptyset") (("2" (propax) 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) ((finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (has_greatest? const-decl "bool" minmax_orders "orders/") (set type-eq-decl nil sets nil) (greatest? const-decl "bool" minmax_orders "orders/") (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders "orders/") (member const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (upper_bound? const-decl "bool" bounded_orders "orders/") (emptyset const-decl "set" sets nil) (least_le formula-decl nil minmax_orders "orders/")) shostak)) (bit_decoding_max2_TCC1 0 (bit_decoding_max2_TCC1-1 nil 3316868576 ("" (skosimp) (("" (forward-chain "bounding_bits_has_least") nil nil)) nil) ((bounding_bits_has_least formula-decl nil bits nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (bit_decoding_max2 0 (bit_decoding_max2-2 nil 3508505405 ("" (lemma "bit_decoding_max2_TCC1") (("" (lemma "bit_decoding_max1_TCC1") (("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (expand "bit_decoding" +) (("" (ground) (("" (use "bit_decoding_TCC3") (("" (use "bit_decoding_TCC4") (("" (use "bit_decoding_TCC1") (("" (assert :quant-simp? t) (("" (assert) (("" (case-replace "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) = 0") (("1" (expand "bit_decoding" +) (("1" (rewrite "singleton_as_add" :dir rl) (("1" (rewrite "greatest_equals_lub") (("1" (rewrite "lub_singleton") nil nil)) nil)) nil)) nil) ("2" (use "greatest_add") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (inst - "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("1" (assert) (("1" (replace -5) (("1" (hide -1 -5) (("1" (typepred "least(lesseq)(bounding_bits(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1))) (("1" (expand* "least?" "lower_bound?") (("1" (expand "restrict" -2 :occurrence 1) (("1" (expand "bounding_bits" -1 :occurrence 1) (("1" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("1" (assert) nil nil) ("2" (expand "bounding_bits" 1 :occurrence 1) (("2" (lemma "exp2_n") (("2" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("2" (typepred "least(lesseq)(bounding_bits(j!1))") (("2" (expand "least?") (("2" (expand "bounding_bits" -1 :occurrence 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -6 "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bit_decoding_max1_TCC1 subtype-tcc nil bits nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonempty_add_finite application-judgement "non_empty_finite_set[nat]" bits nil) (bit_decoding_TCC4 subtype-tcc nil bits nil) (exp2 def-decl "posnat" exp2 nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (singleton_as_add formula-decl nil sets_lemmas nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" bits nil) (partial_order? const-decl "bool" orders nil) (lub_singleton formula-decl nil bounded_orders "orders/") (greatest_equals_lub formula-decl nil minmax_orders "orders/") (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lower_bound? const-decl "bool" bounded_orders "orders/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (exp2_n formula-decl nil exp2 nil) (NOT const-decl "[bool -> bool]" booleans nil) (j!1 skolem-const-decl "nat" bits nil) (greatest_add formula-decl nil total_lattices "orders/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bit_decoding_TCC1 subtype-tcc nil bits nil) (bit_decoding_TCC3 subtype-tcc nil bits nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "above(n)" exp2 nil) (NAT_induction formula-decl nil naturalnumbers nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders "orders/") (greatest? const-decl "bool" minmax_orders "orders/") (= const-decl "[T, T -> boolean]" equalities nil) (has_least? const-decl "bool" minmax_orders "orders/") (bounding_bits const-decl "set[nat]" bits nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders "orders/") (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (bit_decoding def-decl "finite_set" bits nil) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil) (bit_decoding_max2_TCC1 subtype-tcc nil bits nil)) nil) (bit_decoding_max2-1 nil 3316870891 ("" (lemma "bit_decoding_max2_TCC1") (("" (lemma "bit_decoding_max1_TCC1") (("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (expand "bit_decoding" +) (("" (ground) (("" (use "bit_decoding_TCC1") (("" (use "bit_decoding_TCC2") (("" (use "bit_decoding_TCC3") (("" (assert :quant-simp? t) (("" (assert) (("" (case-replace "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1) = 0") (("1" (expand "bit_decoding" +) (("1" (rewrite "singleton_as_add" :dir rl) (("1" (rewrite "greatest_equals_lub") (("1" (rewrite "lub_singleton") nil nil)) nil)) nil)) nil) ("2" (use "greatest_add") (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (inst - "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("1" (assert) (("1" (replace -5) (("1" (hide -1 -5) (("1" (typepred "least(lesseq)(bounding_bits(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1))) (("1" (expand* "least?" "lower_bound?") (("1" (flatten) (("1" (expand "restrict" -2 :occurrence 1) (("1" (expand "bounding_bits" -1 :occurrence 1) (("1" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("1" (assert) nil nil) ("2" (expand "bounding_bits" 1 :occurrence 1) (("2" (lemma "exp2_n") (("2" (inst - "least(lesseq)(bounding_bits(j!1)) - 1") (("2" (typepred "least(lesseq)(bounding_bits(j!1))") (("2" (expand "least?") (("2" (flatten) (("2" (expand "bounding_bits" -1 :occurrence 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -6 "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partial_order? const-decl "bool" orders nil) (lub_singleton formula-decl nil bounded_orders "orders/") (greatest_equals_lub formula-decl nil minmax_orders "orders/") (antisymmetric? const-decl "bool" relations nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (lower_bound? const-decl "bool" bounded_orders "orders/") (greatest_add formula-decl nil total_lattices "orders/") (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders "orders/") (greatest? const-decl "bool" minmax_orders "orders/") (has_least? const-decl "bool" minmax_orders "orders/") (set type-eq-decl nil sets nil) (has_greatest? const-decl "bool" minmax_orders "orders/") (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil)) shostak)) (bit_decoding_max3 0 (bit_decoding_max3-2 nil 3508505431 ("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (expand "bit_decoding" -2) (("" (expand* "emptyset" "member") (("" (prop) (("" (expand* "add" "member") (("" (use "bit_decoding_max2") (("" (use "bit_decoding_max1") (("" (assert) (("" (forward-chain "bit_decoding_TCC3") (("" (forward-chain "bit_decoding_TCC4") (("" (inst - "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("" (assert) (("" (inst - "m!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (bit_decoding_max1 formula-decl nil bits nil) (bit_decoding_TCC3 subtype-tcc nil bits nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (restrict const-decl "R" restrict nil) (bounding_bits const-decl "set[nat]" bits nil) (j!1 skolem-const-decl "nat" bits nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bit_decoding_TCC4 subtype-tcc nil bits nil) (real_le_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) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (bit_decoding_max2 formula-decl nil bits nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "above(n)" exp2 nil) (NAT_induction formula-decl nil naturalnumbers nil) (exp2 def-decl "posnat" exp2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (bit_decoding def-decl "finite_set" bits nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil) (bit_decoding_max3-1 nil 3316907107 ("" (induct "n" :name "NAT_induction") (("" (skosimp*) (("" (expand "bit_decoding" -2) (("" (expand* "emptyset" "member") (("" (prop) (("" (expand* "add" "member") (("" (use "bit_decoding_max2") (("" (use "bit_decoding_max1") (("" (assert) (("" (forward-chain "bit_decoding_TCC1") (("" (forward-chain "bit_decoding_TCC2") (("" (inst - "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)") (("" (assert) (("" (inst - "m!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (has_least? const-decl "bool" minmax_orders "orders/") (least? const-decl "bool" minmax_orders "orders/") (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders "orders/") (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)) shostak)) (bit_encoding_TCC1 0 (bit_encoding_TCC1-1 nil 3316868576 ("" (skosimp) (("" (use "non_empty_finite_has_greatest") nil nil)) nil) ((S!1 skolem-const-decl "finite_set[nat]" bits nil) (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.93 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
