Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: countable_set.prf Sprache: Lisp

Original von: PVS^©

(countable_set
(int_to_nat_TCC1 0
  (int_to_nat_TCC1-1 nil 3317054588 ("" (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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
(int_to_nat_TCC2 0
  (int_to_nat_TCC2-1 nil 3317054588 ("" (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)
    (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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(nat_to_int_TCC1 0
  (nat_to_int_TCC1-1 nil 3317054588 ("" (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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (even? const-decl "bool" integers nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil))
   nil))
(nat_to_int_TCC2 0
  (nat_to_int_TCC2-1 nil 3317054588
   ("" (skosimp)
    (("" (rewrite "even_or_odd")
      (("" (expand "odd?")
        (("" (skolem!)
          (("" (use "div_simple")
            (("" (iff)
              (("" (ground)
                (("" (inst + "-j!1 - 1") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((even_or_odd formula-decl nil naturalnumbers 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (div_simple formula-decl nil integer_props nil)
    (odd? const-decl "bool" integers 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))
   nil))
(int_to_nat_bijective 0
  (int_to_nat_bijective-1 nil 3317054588
   ("" (grind :if-match nil)
    (("" (inst + "nat_to_int(y!1)") (("" (grind) nil nil)) nil)) nil)
   ((nat_to_int const-decl "int" countable_set nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (even? const-decl "bool" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (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)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (int_to_nat const-decl "nat" countable_set nil))
   nil))
(nat_to_int_bijective 0
  (nat_to_int_bijective-1 nil 3317054588
   ("" (grind :if-match nil)
    (("" (inst + "int_to_nat(y!1)") (("" (grind) nil nil)) nil)) nil)
   ((int_to_nat const-decl "nat" countable_set nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (nat_to_int const-decl "int" countable_set nil)
    (even? const-decl "bool" integers nil))
   nil))
(countable_family_nat 0
  (countable_family_nat-1 nil 3317054743
   ("" (inst + "bit_encoding") (("" (assert) nil nil)) nil)
   ((encoding_bijection name-judgement
     "(bijective?[finite_set[nat], nat])" bits nil)
    (bit_encoding def-decl "nat" bits 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)
    (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))
   shostak))
(intset_to_natset_bijective 0
  (intset_to_natset_bijective-1 nil 3317054588
   ("" (lemma "int_to_nat_bijective")
    (("" (expand* "bijective?" "injective?" "surjective?")
      (("" (prop)
        (("1" (skosimp)
          (("1" (decompose-equality)
            (("1" (expand* "intset_to_natset" "image")
              (("1" (apply-extensionality :hide? t)
                (("1" (inst - "int_to_nat(x!1)")
                  (("1" (iff -)
                    (("1" (prop)
                      (("1" (skosimp*)
                        (("1" (inst-cp - "x!1" "x!3")
                          (("1" (inst-cp - "x!1" "x!2")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (smash)
                        (("1" (inst 2 "x!1") nil nil)
                         ("2" (inst + "x!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (inst + "image(nat_to_int, y!1)")
            (("2" (apply-extensionality :hide? t)
              (("2"
                (expand* "nat_to_int" "intset_to_natset" "image"
                 "int_to_nat")
                (("2" (smash)
                  (("1" (skosimp* t)
                    (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
                   ("2" (inst + "nat_to_int(x!1)")
                    (("1" (grind) nil nil)
                     ("2" (inst + "x!1") (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (int_to_nat_bijective name-judgement "(bijective?[int, nat])"
     countable_set nil)
    (bijective? const-decl "bool" functions nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (even? const-decl "bool" integers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (nnrrat_div_negrat_is_nprat application-judgement "nprat" rationals
     nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (y!1 skolem-const-decl "finite_set[nat]" countable_set nil)
    (x!1 skolem-const-decl "nat" countable_set nil)
    (nat_to_int const-decl "int" countable_set nil)
    (nat_to_int_bijective name-judgement "(bijective?[nat, int])"
     countable_set nil)
    (finite_image application-judgement "finite_set[int]" countable_set
     nil)
    (image const-decl "set[R]" function_image nil)
    (int_to_nat const-decl "nat" countable_set nil)
    (intset_to_natset const-decl "finite_set[nat]" countable_set 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)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (int_to_nat_bijective judgement-tcc nil countable_set nil))
   nil))
(countable_family_int 0
  (countable_family_int-1 nil 3317054966
   ("" (inst + "bit_encoding o intset_to_natset")
    (("" (assert) nil nil)) nil)
   ((intset_to_natset_bijective name-judgement
     "(bijective?[finite_set[int], finite_set[nat]])" countable_set
     nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (intset_to_natset const-decl "finite_set[nat]" countable_set nil)
    (bit_encoding def-decl "nat" bits nil)
    (O const-decl "T3" function_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (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)
    (encoding_bijection name-judgement
     "(bijective?[finite_set[nat], nat])" bits nil))
   shostak))
(tuple_to_natset_TCC1 0
  (tuple_to_natset_TCC1-1 nil 3317054588
   ("" (skolem!)
    (("" (expand "is_finite")
      ((""
        (inst + "2"
         "LAMBDA (x: ({i: nat | i = n!1`1 * 2 OR i = n!1`2 * 2 + 1})): rem(2)(x)")
        (("" (expand "injective?")
          (("" (skosimp :preds? t)
            (("" (rewrite "same_remainder")
              (("" (expand "divides") (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (same_remainder formula-decl nil modulo_arithmetic nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (divides const-decl "bool" divides nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
         modulo_arithmetic nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers
     nil))
   nil))
(countable_nat_tuple 0
  (countable_nat_tuple-1 nil 3317055072
   ("" (lemma "inj_inj_bij[[nat, nat], nat]")
    (("" (prop)
      (("1" (lemma "countable_family_nat")
        (("1" (expand "bijective?")
          (("1" (skosimp)
            (("1" (assert)
              (("1"
                (lemma
                 "composition_injective[[nat, nat], finite_set[nat], nat]"
                 ("f1" "tuple_to_natset" "f2" "f!1"))
                (("1" (inst?) nil nil)
                 ("2" (expand "injective?" 1)
                  (("2" (skosimp)
                    (("2" (decompose-equality)
                      (("2" (expand "tuple_to_natset")
                        (("2" (inst-cp - "2 * x1!1`1")
                          (("2" (inst - "1 + 2 * x1!1`2")
                            (("2" (assert)
                              (("2" (apply-extensionality) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (inst + "LAMBDA (n: nat): (n, n)")
        (("2" (expand "injective?" 1) (("2" (skosimp) nil nil)) nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers 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)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (O const-decl "T3" function_props nil)
    (composition_injective judgement-tcc nil function_props nil)
    (injective? const-decl "bool" functions nil)
    (tuple_to_natset const-decl "finite_set[nat]" countable_set nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (countable_family_nat formula-decl nil countable_set nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "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))
   shostak))
(tuple_to_intset_TCC1 0
  (tuple_to_intset_TCC1-1 nil 3317054588
   ("" (skolem!)
    (("" (expand "is_finite")
      ((""
        (inst + "2"
         "LAMBDA (x: ({i: int | i = n!1`1 * 2 OR i = n!1`2 * 2 + 1})): rem(2)(x)")
        (("" (expand "injective?")
          (("" (skosimp :preds? t)
            (("" (rewrite "same_remainder")
              (("" (expand "divides") (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (same_remainder formula-decl nil modulo_arithmetic nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (divides const-decl "bool" divides nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
         modulo_arithmetic nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers
     nil))
   nil))
(countable_int_tuple 0
  (countable_int_tuple-1 nil 3317055262
   ("" (lemma "inj_inj_bij[[int, int], nat]")
    (("" (prop)
      (("1" (lemma "countable_family_int")
        (("1" (expand "bijective?")
          (("1" (skosimp)
            (("1" (assert)
              (("1"
                (lemma
                 "composition_injective[[int, int], finite_set[int], nat]"
                 ("f1" "tuple_to_intset" "f2" "f!1"))
                (("1" (inst?) nil nil)
                 ("2" (expand "injective?" 1)
                  (("2" (skosimp)
                    (("2" (decompose-equality)
                      (("2" (expand "tuple_to_intset")
                        (("2" (inst-cp - "2 * x1!1`1")
                          (("2" (inst - "1 + 2 * x1!1`2")
                            (("2" (assert)
                              (("2" (apply-extensionality) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (inst + "LAMBDA (n: nat): (n, n)")
        (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers 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)
    (O const-decl "T3" function_props nil)
    (composition_injective judgement-tcc nil function_props nil)
    (injective? const-decl "bool" functions nil)
    (tuple_to_intset const-decl "finite_set[int]" countable_set nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (countable_family_int formula-decl nil countable_set nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "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))
   shostak))
(countable_rat 0
  (countable_rat-1 nil 3317055513
   ("" (lemma "inj_inj_bij[rat, nat]")
    (("" (prop)
      (("1" (lemma "countable_int_tuple")
        (("1" (expand "bijective?")
          (("1" (skosimp)
            (("1"
              (case "FORALL (r: rat): nonempty?[[int, int]]({t: [int, int] | t`2 /= 0 AND r = t`1 / t`2})")
              (("1" (assert)
                (("1"
                  (lemma "composition_injective[rat, [int, int], nat]"
                   ("f1"
                    "LAMBDA (r: rat): choose({t: [int, int] | t`2 /= 0 AND r = t`1 / t`2})"
                    "f2" "f!1"))
                  (("1" (inst? +) nil nil)
                   ("2" (expand "injective?" 1)
                    (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)
                   ("3" (propax) nil nil))
                  nil))
                nil)
               ("2" (skolem!)
                (("2" (expand* "nonempty?" "empty?" "member")
                  (("2" (lemma "rational_pred_ax" ("r" "r!1"))
                    (("2" (skolem!)
                      (("2" (inst - "(i!1, n0j!1)")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (inst + "LAMBDA (n: nat): n")
        (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (composition_injective judgement-tcc nil function_props nil)
    (injective? const-decl "bool" functions nil)
    (choose const-decl "(p)" sets nil)
    (O const-decl "T3" function_props nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (rational_pred_ax formula-decl nil rational_props nil)
    (countable_int_tuple formula-decl nil countable_set nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "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)
    (rat nonempty-type-eq-decl nil 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))
   shostak)))

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.