Quelle bits.prf
Sprache: Lisp
(bitsnil 3316868811"" (skosimp)"" (use "every_nonempty_set_has_least" )"" (hide 2) (("" (grind) nil nil )) nil )) nil ))nil )nil bounded_nats"orders/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"nat" bits nil )"set[nat]" bits nil )"bool" sets nil )set type-eq-decl nil sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"posnat" exp2 nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )nil application-judgement "above(n)" exp2 nil )"(strict_total_order?[real])" real_props nil ))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" nil )nil minmax_orders "orders/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"bool" relations nil )"R" restrict nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders "orders/" )"set[nat]" bits nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"int" integers nil )"(total_order?[real])" nil )nil application-judgement "above(n)" exp2 nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nat" bits nil )"nat" bits nil )"bool" minmax_orders "orders/" )"bool" bounded_orders "orders/" ))nil )nil 3316868576"" (skosimp)"" (use "bounding_bits_has_least" ) (("" (assert ) nil nil )) nil ))nil )nil nil ))nil 3316868576"" (skosimp*) (("" (grind) nil nil )) nil )nil application-judgement "above(n)" exp2 nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"int" integers nil ))nil ))nil 3508504937"" (skosimp)"" (use "bounding_bits_has_least" ) (("" (assert ) nil nil )) nil ))nil )nil bits nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil )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 )nil minmax_orders "orders/" )"bool" relations nil )set type-eq-decl nil sets nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"bool" bounded_orders "orders/" ))nil ))nil 3508504990"" (skosimp)"" "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 )"bool" reals nil )"R" restrict nil )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )nil defined_types nil )"set[nat]" bits nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"posint" exponentiation nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )nil exp2 nil ))nil )nil 3316868576 ("" (termination-tcc) nil nil )nil nil ))nil 3316869847"" (skosimp)"" (use "non_empty_finite_has_greatest" )"" (expand "bit_decoding" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil minmax_orders"orders/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"nat" bits nil )"bool" reals nil )"R" restrict nil )"bool" orders nil )nil defined_types nil )"finite_set" bits nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"non_empty_finite_set[nat]" bits nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil application-judgement "above(n)" exp2 nil ))nil 3316868576"" (skosimp)"" (forward-chain "bit_decoding_has_greatest" ) nil nil )) nil )nil bits nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil ))nil ))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" )"" "lesseq" "bounding_bits(j!1)" "least(lesseq)(bounding_bits(j!1)) - 1" )"1" expand "restrict" )"1" (assert ) nil nil ))nil )"2" expand "bounding_bits" "2" assert )"2" "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)" )"2" "1" "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)" )"1" assert )"1" "+" "exp2(least[nat](restrict[[real, real], [nat, nat], boolean](<=))(bounding_bits(j!1)) - 1)" "1" assert )"1" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" expand *"greatest?" "upper_bound?" )"1" "greatest(lesseq)(bit_decoding(j!1))" )"1" expand "restrict" "1" expand "restrict" "1" "exp2_def" )"1" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" "greatest(lesseq)(bit_decoding(j!1))" )"1" "both_sides_expt_gt1_lt" )"1" "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" "bit_decoding_TCC3" )"2" assert )"2" "least(lesseq)(bounding_bits(j!1)) - 1" )"2" expand "bit_decoding" "2" expand "emptyset" )"2" 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 )"bool" reals nil )"R" restrict nil )"finite_set" bits nil )nil finite_sets nil )"bool" finite_sets nil )"bool" minmax_orders "orders/" )nil defined_types nil )set type-eq-decl nil sets nil ) (> const-decl "bool" reals nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil integers nil )nil integers nil )"posnat" exp2 nil )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )nil naturalnumbers nil )nil bits nil )"bool" sets nil )"(nonempty?)" sets nil )"set[nat]" bits nil )"nat" bits nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"(strict_total_order?[real])" real_props nil )"bool" bounded_orders "orders/" )nil exp2 nil )nil real_types nil )nil real_types nil )"posint" exponentiation nil )nil exponentiation nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"odd_int" integers nil )"set" sets nil )nil minmax_orders "orders/" )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )nil bits nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )nil bits nil ))nil )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" )"" "lesseq" "bounding_bits(j!1)" "least(lesseq)(bounding_bits(j!1)) - 1" )"1" expand "restrict" )"1" (assert ) nil nil ))nil )"2" expand "bounding_bits" "2" assert )"2" "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)" )"2" "1" "j!1 - exp2(least[nat](lesseq)(bounding_bits(j!1)) - 1)" )"1" assert )"1" "+" "exp2(least[nat](restrict[[real, real], [nat, nat], boolean](<=))(bounding_bits(j!1)) - 1)" "1" assert )"1" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" expand *"greatest?" "upper_bound?" )"1" "1" "greatest(lesseq)(bit_decoding(j!1))" )"1" expand "restrict" "1" expand "restrict" "1" "exp2_def" )"1" "greatest(lesseq)(bit_decoding(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" "greatest(lesseq)(bit_decoding(j!1))" )"1" "both_sides_expt_gt1_lt" )"1" "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" "bit_decoding_TCC3" )"2" assert )"2" "least(lesseq)(bounding_bits(j!1)) - 1" )"2" expand "bit_decoding" "2" expand "emptyset" )"2" 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 finite_sets nil )"bool" finite_sets nil )"bool" minmax_orders "orders/" )set type-eq-decl nil sets nil )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" sets nil )"(nonempty?)" sets nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"bool" bounded_orders "orders/" )"set" sets nil )nil minmax_orders "orders/" ))nil 3316868576"" (skosimp)"" (forward-chain "bounding_bits_has_least" ) nil nil )) nil )nil bits nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil ))nil ))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 )"" "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" "1" replace -1)"1" "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)" )"1" assert )"1" replace -5)"1" "1" "least(lesseq)(bounding_bits(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" expand *"least?" "lower_bound?" )"1" expand "restrict" "1" expand "bounding_bits" "1" "least(lesseq)(bounding_bits(j!1)) - 1" )"1" assert )nil nil )"2" expand "bounding_bits" "2" "exp2_n" )"2" "least(lesseq)(bounding_bits(j!1)) - 1" )"2" "least(lesseq)(bounding_bits(j!1))" )"2" expand "least?" )"2" expand "bounding_bits" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )nil bits nil )"(strict_total_order?[real])" real_props nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"non_empty_finite_set[nat]" bits nil )nil bits nil )"posnat" exp2 nil )nil integers nil )nil integers nil )"odd_int" integers nil )nil sets_lemmas nil )"non_empty_finite_set[nat]" bits nil )"bool" orders nil )nil bounded_orders "orders/" )nil minmax_orders "orders/" )nil defined_types nil )"bool" relations nil )"bool" sets nil )"(singleton?)" sets nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_orders "orders/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )nil exp2 nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" bits nil )nil total_lattices "orders/" )"(total_order?[real])" nil )nil bits nil )nil bits nil )"int" integers nil )nil application-judgement "above(n)" exp2 nil )nil naturalnumbers nil )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"[T, T -> boolean]" equalities nil )"bool" minmax_orders "orders/" )"set[nat]" bits nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders "orders/" )"bool" finite_sets nil )nil finite_sets nil )"finite_set" bits nil )"R" restrict nil )"bool" reals nil )nil bits nil ))nil )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 )"" "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" "1" replace -1)"1" "j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)" )"1" assert )"1" replace -5)"1" "1" "least(lesseq)(bounding_bits(j!1 - exp2(least(lesseq)(bounding_bits(j!1)) - 1)))" )"1" expand *"least?" "lower_bound?" )"1" "1" expand "restrict" "1" expand "bounding_bits" "1" "least(lesseq)(bounding_bits(j!1)) - 1" )"1" assert )nil nil )"2" expand "bounding_bits" "2" "exp2_n" )"2" "least(lesseq)(bounding_bits(j!1)) - 1" )"2" "least(lesseq)(bounding_bits(j!1))" )"2" expand "least?" )"2" "2" expand "bounding_bits" "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" "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 )"bool" orders nil )nil bounded_orders "orders/" )nil minmax_orders "orders/" )"bool" relations nil )"bool" sets nil )"(singleton?)" sets nil )"bool" bounded_orders "orders/" )nil total_lattices "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )set type-eq-decl nil sets nil )"bool" minmax_orders "orders/" )"bool" finite_sets nil )nil finite_sets nil ))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" )"" "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 )"set" sets nil )"(nonempty?)" sets nil )nil bits nil )nil bits nil )"(total_order?[real])" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"R" restrict nil )"set[nat]" bits nil )"nat" bits nil )"(strict_total_order?[real])" real_props nil )nil bits nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )nil bits nil )"int" integers nil )nil application-judgement "above(n)" exp2 nil )nil naturalnumbers nil )"posnat" exp2 nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"finite_set" bits nil )nil finite_sets nil )"bool" finite_sets nil )"bool" sets nil ) (set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )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" )"" "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 )"set" sets nil )"(nonempty?)" sets nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )nil finite_sets nil )"bool" finite_sets nil )"bool" sets nil )set type-eq-decl nil sets nil ))nil 3316868576"" (skosimp) (("" (use "non_empty_finite_has_greatest" ) nil nil ))nil )"finite_set[nat]" bits nil )"bool" reals nil )"R" restrict nil )"bool" orders nil )nil defined_types nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )nil minmax_orders"orders/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil ))nil ))nil 3316868576"" (skosimp)"" (forward-chain "bit_encoding_TCC1" )"" (use "card_remove" )"" (use "greatest_member" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil bits nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"int" integers nil )"finite_set[nat]" bits nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )nil defined_types nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"R" restrict nil )"bool" reals nil )nil finite_sets nil ))nil ))nil 3316907428"" (measure-induct+ "card(S)" ("S" ))"" (skolem!)"" (expand "bit_encoding" +)"" (lift-if)"" (ground)"1" (expand * "empty?" "member" )"1" (inst - "x!2" ) (("1" (assert ) nil nil )) nil )) nil )"2" (forward-chain "bit_encoding_TCC2" )"2" (forward-chain "bit_encoding_TCC1" )"2" (inst - "remove(greatest(lesseq)(x!1), x!1)" )"2" (inst - "x!2" )"1" (assert ) nil nil )"2" (expand * "remove" "member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil bits nil )"R" restrict nil )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"set" sets nil )"(strict_total_order?[real])" real_props nil )"(x!1)" bits nil )"finite_set[nat]" bits nil )nil bits nil )"bool" sets nil )"bool" sets nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"finite_set[nat]" bits nil )"posint" nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"nat" bits nil )"posnat" exp2 nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3316907588"" (measure-induct+ "card(S)" ("S" ))"1" (expand "bit_encoding" +)"1" (rewrite "exp2_sum" )"1" (expand "exp2" 1 :occurrence 2)"1" (expand "exp2" 1 :occurrence 2)"1" (case "empty?(remove(greatest(lesseq)(x!1), x!1))" )"1" (expand "bit_encoding" +) (("1" (assert ) nil nil ))nil )"2" (inst - "remove(greatest(lesseq)(x!1), x!1)" )"2" (prop)"1" (lemma "exp2_def" )"1" (inst-cp - "greatest(lesseq)(x!1)" )"1" "1 + greatest(lesseq)(remove(greatest(lesseq)(x!1), x!1))" )"1" (lemma "both_sides_expt_gt1_le" )"1" "2" "1 + greatest(lesseq)(remove(greatest(lesseq)(x!1), x!1))" "greatest(lesseq)(x!1)" )"1" (assert )"1" "remove_greatest" )"1" expand "nonempty?" )"1" (propax) nil nil ))nil )"2" "non_empty_finite_bounded_above" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "bit_encoding_TCC2" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "bit_encoding_member2_TCC1" ) nil nil ))nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " bits nil )"finite_set[nat]" bits nil )"set" sets nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"posint" exponentiation nil )"bool" sets nil )"bool" non_empty_bounded_sets"orders/" )nil bounded_integers "orders/" )nil real_types nil )nil real_types nil )"posint" nil )nil exp2 nil )nil bits nil )"non_empty_finite_set[nat]" bits nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"int" integers nil )nil exp2 nil )"bool" reals nil )"R" restrict nil )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posnat" exp2 nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" bits nil )"posint" nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3316868576"" (skolem!)"" (use "bit_decoding_TCC3" )"" (assert )"" (expand "bit_encoding" -) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil bits nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " bits nil )"finite_set[nat]" bits nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil ))nil ))nil 3316908262"" (skolem!)"" (use "bit_encoding_member3_TCC1" )"" (assert )"" "least(lesseq)(bounding_bits(bit_encoding(S!1)))" )"" (expand * "least?" "lower_bound?" )"" (flatten)"" (expand "bounding_bits" -1 :occurrence 1)"" (expand "restrict" -2 :occurrence 1)"" (use "bit_encoding_member2" )"" (assert )"" (inst - "greatest(lesseq)(S!1) + 1" )"1" (lemma "bit_encoding_member1" )"1" (inst - "S!1" "greatest(lesseq)(S!1)" )"1" (lemma "exp2_lt" )"1" "greatest(lesseq)(S!1)" "least(lesseq)(bounding_bits(bit_encoding(S!1)))" )"1" (assert ) nil nil ))nil ))nil )"2" (use "greatest_member" ) nil nil ))nil ))nil )"2" (expand "bounding_bits" 1)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil bits nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"set[nat]" bits nil )"nat" bits nil )nil defined_types nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )"R" restrict nil )"bool" reals nil )nil bits nil )"even_int" integersnil )"posint" nil )"posint" nil )nil application-judgement "above(n)" exp2 nil )"non_empty_finite_set[nat]" bits nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )nil exp2 nil )nil bits nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_orders "orders/" )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"int" integers nil ))nil 3316868576"" (skolem!)"" (use "bit_decoding_max1_TCC1" )"" (assert )"" (expand "bit_encoding" 1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil bits nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " bits nil )"finite_set[nat]" bits nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3316909101"" (skolem!)"" (use "bit_decoding_max2" )"" (use "bit_encoding_member3" )"" (assert )"" (expand "bit_encoding" 1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil bits nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"int" integers nil )nil application-judgement "above(n)" exp2 nil )"finite_set[nat]" bits nil )"(LAMBDA (S: set[nat]): " bits nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"posint" nil )nil bits nil ))nil 3316909141"" (skolem!)"" (expand * "bit_encoding" "bit_decoding" )"" (smash) (("" (rewrite "emptyset_is_empty?[nat]" ) nil nil ))nil ))nil ))nil )"finite_set" bits nil )"non_empty_finite_set[nat]" bits nil )"int" integers nil )"finite_set[nat]" bits nil )"finite_set" finite_sets nil )nil application-judgement "above(n)" exp2 nil )"nat" bits nil )nil sets_lemmas nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[real])" nil )"(total_order?[S])" nil )"finite_set[nat]" bits nil )"posint" nil ))nil 3316909203"" (skolem!)"" (expand "bit_decoding" :occurrence 1)"" (lift-if)"" (ground)"1" (expand "bit_encoding" -) (("1" (assert ) nil nil )) nil )"2" (use "bit_encoding_member3" )"2" (replace -1)"2" (lemma "bit_encoding_member1" )"2" (inst - "S!1" "greatest(lesseq)(S!1)" )"1" (assert )"1" (use "remove_add_member[nat]" )"1" (prop)"1" (replace -1)"1" (expand "bit_encoding" 2 :occurrence 1)"1" (propax) nil nil )) nil ))nil )"2" (forward-chain "bit_decoding_max3" )"2" (use "bit_encoding_member2" )"2" (expand "exp2" -1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (use "greatest_member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil application-judgement "above(n)" exp2 nil )"int" integers nil )"finite_set" bits nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " bits nil )"finite_set[nat]" bits nil )"(total_order?[S])" nil )"(total_order?[real])" nil )"non_empty_finite_set[nat]" bits nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"finite_set" finite_sets nil )"finite_set[nat]" bits nil )"posint" nil )"nat" bits nil )"bool" reals nil )"R" restrict nil )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )nil defined_types nil )nil sets_lemmas nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" exp2 nil )"(total_order?[real])" nil )nil bits nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )"odd_int" integersnil )"even_int" integersnil )nil bits nil )nil bits nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil bits nil ))nil 3316909396"" (induct "n" :name "NAT_induction" )"" (skosimp)"" (expand "bit_encoding" +)"" (lift-if)"" (ground)"1" (expand "bit_decoding" -1) (("1" (assert ) nil nil ))nil )"2" "j!1 - exp2(greatest(lesseq)(bit_decoding(j!1)))" )"1" (assert )"1" (expand "bit_decoding" 2 :occurrence 2)"1" (assert )"1" (use "bit_decoding_max2" )"1" (assert )"1" (use "non_empty_finite_has_greatest" )"1" (replace -2 2 :dir rl)"1" (use "remove_add_member[nat]" )"1" assert )"1" "bit_decoding_max3" )"1" "+" "exp2(greatest(lesseq)(bit_decoding(j!1)))" "1" assert )"1" rewrite "exp2_n" -1 :dir rl)"1" replace -4 -1)"1" assert )"1" "least(lesseq)(bounding_bits(j!1))" )"1" expand "least?" )"1" "1" expand "bounding_bits" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "bit_decoding_max1" )"2" (assert )"2" (expand "bit_decoding" 3)"2" (rewrite "emptyset_is_empty?[nat]" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" bits nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" exp2 nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"R" restrict nil )"bool" reals nil )nil bits nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " nil )"(LAMBDA (S: set[nat]): " bits nil )nil minmax_orders"orders/" )"bool" orders nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil sets_lemmas nil )nil bits nil )"set[nat]" bits nil )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"{t: (S) | least?(t, S, <=)}" minmax_orders"orders/" )nil exp2 nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"finite_set[nat]" bits nil )"(strict_total_order?[real])" real_props nil )"set" sets nil )nil sets_lemmas nil )"finite_set" finite_sets nil )nil bits nil )"int" integers nil )"non_empty_finite_set[nat]" bits nil )nil application-judgement "above(n)" exp2 nil )"(total_order?[real])" nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"finite_set[nat]" bits nil )"posint" nil )nil naturalnumbers nil )"finite_set" bits nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3316909662"" (measure-induct+ "card(S)" ("S" ))"" (use "decoding_encoding_empty" )"" (prop)"1" (expand "bit_encoding" +)"1" (expand "bit_decoding" +)"1" (ground)"1" (rewrite "emptyset_is_empty?[nat]" ) nil nil )) nil ))nil ))nil )"2" (apply-extensionality :hide? t)"2" (iff)"2" (prop)"1" "total_order_restrict[real, nat]" "R" "reals.<=" ))"1" (lemma "non_empty_finite_has_greatest" )"1" "bit_decoding(bit_encoding(x!1))" "lesseq" )"1" (inst - "x!1" "lesseq" )"1" (use "decoding_encoding_remove" )"1" "remove(greatest(lesseq)(x!1), x!1)" )"1" (ground)"1" (replace -1)"1" "1" expand * "remove" "member" )"1" "x!2" )"1" assert )"1" "1" "greatest_member" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "card_remove" )"2" "greatest_member" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "total_order_restrict[real, nat]" "R" "reals.<=" ))"2" (use "non_empty_finite_has_greatest" )"2" (inst - "remove(greatest(lesseq)(x!1), x!1)" )"2" (use "bit_encoding_TCC2" )"2" (assert )"2" (replace -5 -1 :dir rl)"2" (use "decoding_encoding_remove" )"2" (replace -1 :dir rl)"2" "decoding_encoding_max" )"2" "2" expand * "remove" "member" )"2" "x!2" )"2" "2" assert )"2" "2" "greatest_member" )"2" "lesseq" "bit_decoding(bit_encoding(x!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 ))nil ))nil ))nil )nil bits nil )nil minmax_orders"orders/" )"finite_set[nat]" bits nil )"{t: (S) | greatest?(t, S, <=)}" minmax_orders"orders/" )"bool" minmax_orders "orders/" )"bool" minmax_orders "orders/" )"set" sets nil )nil finite_sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )nil bits nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )"R" restrict nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"bool" reals nil )"bool" orders nil )nil restrict_order_props nil )"(total_order?[real])" nil )nil bits nil )nil bits nil )"finite_set[nat]" bits nil )"finite_set" finite_sets nil )"finite_set[nat]" bits nil )nil sets_lemmas nil )"int" integers nil )nil application-judgement "above(n)" exp2 nil )"finite_set" bits nil )"nat" bits nil )nil naturalnumbers nil )"bool" reals nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3316868576"" (lemma "encoding_decoding" )"" (lemma "decoding_encoding" )"" (use "left_right_bij[finite_set, nat]" )"" (expand * "right_inverse?" "left_inverse?" )"" (ground) nil nil )) nil ))nil ))nil ))nil )nil bits nil )"bool" function_inverse_def nil )"bool" function_inverse_def nil )"finite_set" bits nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil function_inverse_def nil )nil bits nil ))nil ))nil 3316868576"" (lemma "encoding_decoding" )"" (lemma "decoding_encoding" )"" (use "left_right_bij[nat, finite_set]" )"" (expand * "right_inverse?" "left_inverse?" )"" (ground) nil nil )) nil ))nil ))nil ))nil )nil bits nil )"bool" function_inverse_def nil )"(bijective?[finite_set[nat], nat])" bits nil )"bool" function_inverse_def nil )"nat" bits nil )"finite_set" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil function_inverse_def nil )nil bits nil ))nil ))nil 3316910617"" (apply-extensionality :hide? t)"" (use "function_inverse[nat, finite_set].bijective_inverse" )"" (use "decoding_encoding" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil function_inverse nil )"bool" functions nil )nil bits nil )"(bijective?[nat, finite_set[nat]])" bits nil )"(bijective?[finite_set, nat])" bits nil )"{x: nat | f(x) = y}" bits nil )"(bijective?[finite_set[nat], nat])" bits nil )"nat" bits nil )"D" function_inverse nil )"finite_set" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3316910643"" (apply-extensionality :hide? t)"" (use "function_inverse[finite_set, nat].bijective_inverse" )"" (use "encoding_decoding" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil function_inverse nil )"bool" functions nil )nil bits nil )"(bijective?[finite_set[nat], nat])" bits nil )"(bijective?[nat, finite_set])" bits nil )"{x: finite_set[nat] | f(x) = y}" bits nil )"(bijective?[nat, finite_set[nat]])" bits nil )"finite_set" bits nil )"D" function_inverse nil )"nat" bits nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.60 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
