|
(card_comp_transitive
(card_lt_transitive 0
(card_lt_transitive-1 nil 3316960965
("" (expand "card_lt")
(("" (lemma "injective_dichotomous")
(("" (prop)
(("" (skosimp*)
(("" (use "composition_injective[T3, T1, T2]")
(("" (inst? 2) nil nil)) nil))
nil))
nil))
nil))
nil)
((T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(injective_dichotomous formula-decl nil set_dichotomous "orders/")
(O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_lt const-decl "bool" card_comp nil))
shostak))
(card_lt_le_transitive 0
(card_lt_le_transitive-1 nil 3316961013
("" (expand* "card_lt" "card_le")
(("" (skosimp*)
(("" (use "composition_injective[T2, T3, T1]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
(f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_lt const-decl "bool" card_comp nil)
(card_le const-decl "bool" card_comp nil))
shostak))
(card_lt_eq_transitive 0
(card_lt_eq_transitive-1 nil 3316961037
("" (expand* "card_lt" "card_eq" "bijective?")
(("" (skosimp*)
(("" (use "composition_injective[T2, T3, T1]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(injective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_lt const-decl "bool" card_comp nil)
(bijective? const-decl "bool" functions nil)
(card_eq const-decl "bool" card_comp nil))
shostak))
(card_le_lt_transitive 0
(card_le_lt_transitive-1 nil 3316961078
("" (expand* "card_le" "card_lt")
(("" (skosimp*)
(("" (use "composition_injective[T3, T1, T2]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_le const-decl "bool" card_comp nil)
(card_lt const-decl "bool" card_comp nil))
shostak))
(card_eq_lt_transitive 0
(card_eq_lt_transitive-1 nil 3316961096
("" (expand* "card_eq" "card_lt" "bijective?")
(("" (skosimp*)
(("" (use "composition_injective[T3, T1, T2]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(injective? const-decl "bool" functions nil)
(f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_eq const-decl "bool" card_comp nil)
(bijective? const-decl "bool" functions nil)
(card_lt const-decl "bool" card_comp nil))
shostak))
(card_le_transitive 0
(card_le_transitive-1 nil 3316961118
("" (expand "card_le")
(("" (skosimp*)
(("" (use "composition_injective[T1, T2, T3]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_le const-decl "bool" card_comp nil))
shostak))
(card_le_eq_transitive 0
(card_le_eq_transitive-1 nil 3316961145
("" (expand* "card_le" "card_eq" "bijective?")
(("" (skosimp*)
(("" (use "composition_injective[T1, T2, T3]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(injective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_le const-decl "bool" card_comp nil)
(bijective? const-decl "bool" functions nil)
(card_eq const-decl "bool" card_comp nil))
shostak))
(card_eq_le_transitive 0
(card_eq_le_transitive-1 nil 3316961166
("" (expand* "card_eq" "card_le" "bijective?")
(("" (skosimp*)
(("" (use "composition_injective[T1, T2, T3]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(injective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_eq const-decl "bool" card_comp nil)
(bijective? const-decl "bool" functions nil)
(card_le const-decl "bool" card_comp nil))
shostak))
(card_eq_transitive 0
(card_eq_transitive-1 nil 3316961183
("" (expand "card_eq")
(("" (skosimp*)
(("" (use "composition_bijective[T1, T2, T3]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(composition_bijective judgement-tcc nil function_props nil)
(card_eq const-decl "bool" card_comp nil))
shostak))
(card_eq_ge_transitive 0
(card_eq_ge_transitive-1 nil 3316961212
("" (expand* "card_eq" "card_ge")
(("" (skosimp*)
(("" (use "bijective_inverse_exists[T1, T2]")
(("" (expand "exists1")
(("" (skosimp*)
(("" (use "bij_inv_is_bij_alt[T1, T2]")
(("" (expand "bijective?" -1)
(("" (flatten)
(("" (use "composition_injective[T3, T2, T1]")
(("" (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 "[T2 -> T1]" card_comp_transitive nil)
(inverse? const-decl "bool" function_inverse_def nil)
(O const-decl "T3" function_props nil)
(injective? const-decl "bool" functions nil)
(f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(card_eq const-decl "bool" card_comp nil)
(card_ge const-decl "bool" card_comp nil))
shostak))
(card_ge_eq_transitive 0
(card_ge_eq_transitive-1 nil 3316961287
("" (expand* "card_ge" "card_eq")
(("" (skosimp*)
(("" (use "bijective_inverse_exists[T2, T3]")
(("" (expand "exists1")
(("" (skosimp*)
(("" (use "bij_inv_is_bij_alt[T2, T3]")
(("" (expand "bijective?" -1)
(("" (flatten)
(("" (use "composition_injective[T3, T2, T1]")
(("" (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 "[T3 -> T2]" card_comp_transitive nil)
(inverse? const-decl "bool" function_inverse_def nil)
(O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(composition_injective judgement-tcc nil function_props nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(card_ge const-decl "bool" card_comp nil)
(card_eq const-decl "bool" card_comp nil))
shostak))
(card_ge_transitive 0
(card_ge_transitive-1 nil 3316961349
("" (expand "card_ge")
(("" (skosimp*)
(("" (use "composition_injective[T3, T2, T1]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
(f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_ge const-decl "bool" card_comp nil))
shostak))
(card_eq_gt_transitive 0
(card_eq_gt_transitive-1 nil 3316961376
("" (expand* "card_eq" "card_gt")
(("" (skosimp*)
(("" (use "bijective_inverse_exists[T1, T2]")
(("" (expand "exists1")
(("" (skosimp*)
(("" (use "bij_inv_is_bij_alt[T1, T2]")
(("" (expand "bijective?" -1)
(("" (flatten)
(("" (use "composition_injective[T2, T1, T3]")
(("" (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 "[T2 -> T1]" card_comp_transitive nil)
(inverse? const-decl "bool" function_inverse_def nil)
(O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(composition_injective judgement-tcc nil function_props nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(card_eq const-decl "bool" card_comp nil)
(card_gt const-decl "bool" card_comp nil))
shostak))
(card_ge_gt_transitive 0
(card_ge_gt_transitive-1 nil 3316961423
("" (expand* "card_ge" "card_gt")
(("" (skosimp*)
(("" (use "composition_injective[T2, T1, T3]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
(f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_ge const-decl "bool" card_comp nil)
(card_gt const-decl "bool" card_comp nil))
shostak))
(card_gt_eq_transitive 0
(card_gt_eq_transitive-1 nil 3316961447
("" (expand* "card_gt" "card_eq")
(("" (skosimp*)
(("" (use "bijective_inverse_exists[T2, T3]")
(("" (expand "exists1")
(("" (skosimp*)
(("" (use "bij_inv_is_bij_alt[T2, T3]")
(("" (expand "bijective?" -1)
(("" (flatten)
(("" (use "composition_injective[T1, T3, T2]")
(("" (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 "[T3 -> T2]" card_comp_transitive nil)
(inverse? const-decl "bool" function_inverse_def nil)
(O const-decl "T3" function_props nil)
(injective? const-decl "bool" functions nil)
(f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(card_gt const-decl "bool" card_comp nil)
(card_eq const-decl "bool" card_comp nil))
shostak))
(card_gt_ge_transitive 0
(card_gt_ge_transitive-1 nil 3316961503
("" (expand* "card_gt" "card_ge")
(("" (skosimp*)
(("" (use "composition_injective[T1, T3, T2]")
(("" (inst?) nil nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(f!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
(f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil card_comp_transitive nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_gt const-decl "bool" card_comp nil)
(card_ge const-decl "bool" card_comp nil))
shostak))
(card_gt_transitive 0
(card_gt_transitive-1 nil 3316961525
("" (expand "card_gt")
(("" (lemma "injective_dichotomous")
(("" (prop)
(("" (skosimp*)
(("" (use "composition_injective[T2, T1, T3]")
(("" (inst? 2) nil nil)) nil))
nil))
nil))
nil))
nil)
((T2 formal-type-decl nil card_comp_transitive nil)
(T1 formal-type-decl nil card_comp_transitive nil)
(injective_dichotomous formula-decl nil set_dichotomous "orders/")
(O const-decl "T3" function_props nil)
(f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
(f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
(injective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T3 formal-type-decl nil card_comp_transitive nil)
(composition_injective judgement-tcc nil function_props nil)
(card_gt const-decl "bool" card_comp nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
