Quelle  booleans_are_finite.prf

(booleans_are_finite
 (bool_is_finite_type 0
  (bool_is_finite_type-1 nil 3318701065
   ("" (expand "is_finite_type")
    (("" (inst + 2 "LAMBDA (b: bool): IF b THEN 1 ELSE 0 ENDIF")
      (("" (grind) nil nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (injective? const-decl "bool" functions nil)
    (is_finite_type const-decl "bool" finite_sets nil))
   shostak))
 (implies_is_total_order 0
  (implies_is_total_order-1 nil 3318695078 ("" (judgement-tcc) nil nil)
   ((reflexive? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (preorder? const-decl "bool" orders nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil))
   nil))
 (IMP_finite_types_TCC1 0
  (IMP_finite_types_TCC1-1 nil 3318695078
   ("" (rewrite "bool_is_finite_type") nil nil)
   ((bool_is_finite_type formula-decl nil booleans_are_finite nil))
   nil)))