Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
trig_values.pvs
Sprache: Unknown
|
(imputations
(subset_core_I 0
(subset_core_I-1 nil 3450693734
("" (expand "subset?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "setI")
(("" (expand "core")
(("" (split)
(("1" (flatten) nil nil)
("2" (flatten)
(("2" (skosimp)
(("2" (inst - "singleton(i!1)")
(("2" (expand "tot")
(("2" (rewrite "sum_singleton") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((setI const-decl "set_vect" imputations nil)
(tot const-decl "real" coalition_fun nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(restrict const-decl "R" restrict nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(number nonempty-type-decl nil numbers nil)
(sum_singleton formula-decl nil finite_sets_sum "finite_sets/")
(real_plus_real_is_real application-judgement "real" reals nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(powset type-eq-decl nil coalition_fun nil)
(N formal-const-decl "players_set" imputations nil)
(players_set nonempty-type-eq-decl nil players_set nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil imputations nil)
(core const-decl "set_vect" imputations nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
shostak))
(subset_I_PI 0
(subset_I_PI-1 nil 3450686942 ("" (grind) nil nil)
((N formal-const-decl "players_set" imputations nil)
(players_set nonempty-type-eq-decl nil players_set nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil imputations nil)
(fullN const-decl "powset" coalition_fun nil)
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(tot const-decl "real" coalition_fun nil)
(setPI const-decl "set_vect" imputations nil)
(setI const-decl "set_vect" imputations nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
shostak))
(subset_PI_FP 0
(subset_PI_FP-1 nil 3450686723 ("" (grind) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(N formal-const-decl "players_set" imputations nil)
(players_set nonempty-type-eq-decl nil players_set nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil imputations nil)
(fullN const-decl "powset" coalition_fun nil)
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(tot const-decl "real" coalition_fun nil)
(setPI const-decl "set_vect" imputations nil)
(setFP const-decl "set_vect" imputations nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
shostak)))
[ zur Elbe Produktseite wechseln0.22Quellennavigators
Analyse erneut starten
]
|
|
