Quelle card_comp_set_transitive.prf Sprache: Lisp

(card_comp_set_transitive
(card_lt_transitive 0
  (card_lt_transitive-1 nil 3316966275
   ("" (expand "card_lt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop)
          (("" (skosimp*)
            (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
              (("" (inst? 2) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (O const-decl "T3" function_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_le_transitive 0
  (card_lt_le_transitive-1 nil 3316966326
   ("" (expand* "card_lt" "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S3!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_eq_transitive 0
  (card_lt_eq_transitive-1 nil 3316966361
   ("" (expand* "card_lt" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S3!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_le_lt_transitive 0
  (card_le_lt_transitive-1 nil 3316966385
   ("" (expand* "card_le" "card_lt")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_lt_transitive 0
  (card_eq_lt_transitive-1 nil 3316966409
   ("" (expand* "card_eq" "card_lt" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_le_transitive 0
  (card_le_transitive-1 nil 3316966440
   ("" (expand "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_le_eq_transitive 0
  (card_le_eq_transitive-1 nil 3316966458
   ("" (expand* "card_le" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_le_transitive 0
  (card_eq_le_transitive-1 nil 3316966499
   ("" (expand* "card_eq" "card_le" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_transitive 0
  (card_eq_transitive-1 nil 3316966568
   ("" (expand "card_eq")
    (("" (skosimp*)
      (("" (use "composition_bijective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_ge_transitive 0
  (card_eq_ge_transitive-1 nil 3316966605
   ("" (expand* "card_eq" "card_ge")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_eq_transitive 0
  (card_ge_eq_transitive-1 nil 3316966787
   ("" (expand* "card_ge" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S2!1), (S3!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S2!1), (S3!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_transitive 0
  (card_ge_transitive-1 nil 3316966978
   ("" (expand "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_gt_transitive 0
  (card_eq_gt_transitive-1 nil 3316967003
   ("" (expand* "card_eq" "card_gt")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_gt_transitive 0
  (card_ge_gt_transitive-1 nil 3316967051
   ("" (expand* "card_ge" "card_gt")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_eq_transitive 0
  (card_gt_eq_transitive-1 nil 3316967073
   ("" (expand* "card_gt" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S2!1), (S3!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S2!1), (S3!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S1!1), (S3!1), (S2!1)]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_ge_transitive 0
  (card_gt_ge_transitive-1 nil 3316967127
   ("" (expand* "card_gt" "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S3!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_transitive 0
  (card_gt_transitive-1 nil 3316967160
   ("" (expand "card_gt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop)
          (("" (skosimp*)
            (("" (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
              (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (O const-decl "T3" function_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.