Quelle clock_minmax.prf
Sprache: Lisp
(clock_minmaxnil 3389336991"" (skosimp*)"" (expand "clock_min" )"" (typepred "min(image(t_at(T!1), participant!1))" )"" (hide -2)"" (rewrite "image" -)"" (expand "t_at" )"" (skosimp*)"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" clock_minmax nil )"(nonempty?[R])" clock_minmaxnil )"non_empty_finite_set[real]" clock_minmax nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nonneg_real" clock_minmax nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )set type-eq-decl nil sets nil )"set[R]" function_image nil )"real" clock_minmax nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )min const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" "finite_sets/" ))nil 3389337114"" (skosimp*)"" (expand "clock_max" )"" (typepred "max(image(t_at(T!1), participant!1))" )"" (hide -2)"" (rewrite "image" -)"" (expand "t_at" )"" (skosimp*)"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" clock_minmax nil )"(nonempty?[R])" clock_minmaxnil )"non_empty_finite_set[real]" clock_minmax nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nonneg_real" clock_minmax nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )set type-eq-decl nil sets nil )"set[R]" function_image nil )"real" clock_minmax nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" ))nil 3389337201"" (skosimp*)"" (expand "clock_min" )"" (typepred "min(image(t_at(T!1), participant!1))" )"" (hide -1)"" (inst?)"" (assert )"" (rewrite "image" )"" (expand "t_at" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" clock_minmax nil )"(nonempty?[R])" clock_minmaxnil )"non_empty_finite_set[real]" clock_minmax nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nonneg_real" clock_minmax nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )set type-eq-decl nil sets nil )"set[R]" function_image nil )"real" clock_minmax nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )min const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" "finite_sets/" ))nil 3389337260"" (skosimp*)"" (expand "clock_max" )"" (invoke (typepred "%1" ) (! 1 r))"" (hide -1)"" (inst?)"" (assert )"" (hide 2)"" (expand * "image" "t_at" ) (("" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" clock_minmax nil )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )"real" clock_minmax nil )"set[R]" function_image nil )set type-eq-decl nil sets nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nonneg_real" clock_minmax nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"non_empty_finite_set[real]" clock_minmax nil )"(nonempty?[R])" clock_minmaxnil ))nil 3389336989"" (skosimp*)"" (prop)"1" (use "clock_min_witness" )"1" (skosimp*)"1" (replace -2 :hide? t)"1" (use "clock_min_is_min" )"1" (typepred "c!1" )"1" (inst - "T!1" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "clock_min_witness" )"2" (inst - "T!1" _)"2" (inst?)"2" (skosimp*)"2" (replace -2 :hide? t)"2" (use "clock_min_is_min" )"2" (typepred "c!1" )"2" (inst - "T!1" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil clock_minmax nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"int" integers nil )"odd_int" integers nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nonneg_real" clock_minmax nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )nil clock_minmax nil ))nil ))nil 3389336989"" (skosimp*)"" (prop)"1" (lemma "clock_max_witness" )"1" (inst - "T!1" _)"1" (inst?)"1" (skosimp*)"1" (replace -2 :hide? t)"1" (lemma "clock_max_is_max" )"1" (inst - "1 + T!1" _ _)"1" (inst?)"1" (typepred "c!1" )"1" (inst - "T!1" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "clock_max_witness" )"2" (skosimp*)"2" (replace -2 :hide? t)"2" (lemma "clock_max_is_max" )"2" (inst - "T!1" _ _)"2" (inst?)"2" (typepred "c!1" )"2" (inst - "T!1" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil clock_minmax nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"int" integers nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nonneg_real" clock_minmax nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil clock_minmax nil )"int" integers nil )"odd_int" integers nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
