Quelle interval_clocks.prf
Sprache: Lisp
(interval_clocksnil 3381399668 ("" (expand "T" ) (("" (propax) nil nil )) nil )"int" interval_clocks nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"int" integers nil ))nil 3381399683"" (expand "T" ) (("" (propax) nil nil )) nil )"int" interval_clocks nil )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil ))nil 3399129068"" (skosimp*)"" (expand "adjustment_lower_bound?" )"" (expand "t" )"" (inst?)"" (lemma "drift_right" )"" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)" )"" (rewrite "T_def" )"" (rewrite "drift" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"bool" interval_clocks nil )"(total_order?[real])" nil )"posint" 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 booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" interval_clocks 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 )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" physical_clocks nil )nil physical_clocks nil )nil interval_clocks nil )"nonneg_real" physical_clocks nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"posreal" nil )"int" integers nil )"nnreal" nil )"odd_int" integers nil )nil interval_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )nil physical_clocks nil )"real" interval_clocks nil ))nil ))nil 3399129088"" (skosimp*)"" (expand "adjustment_upper_bound?" )"" (expand "t" )"" (inst?)"" (lemma "drift_left" )"" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)" )"" (rewrite "T_def" )"" (rewrite "drift" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" nil )"bool" interval_clocks nil )"(total_order?[real])" nil )"posint" 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 booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" interval_clocks 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 )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" physical_clocks nil )nil physical_clocks nil )nil interval_clocks nil )"nonneg_real" physical_clocks nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"int" integers nil )"nnreal" nil )"odd_int" integers nil )nil interval_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )nil physical_clocks nil )"real" interval_clocks nil ))nil ))nil 3399129148"" (skosimp*)"" (expand "abs" )"" (lift-if)"" (rewrite "handover_precision_lower" )"" (use "handover_precision_upper" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"int" integers nil )"posint" nil )nil interval_clocks 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 booleans nil )"bool" reals nil )nil naturalnumbers 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 )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"nnreal" interval_clocks nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )nil interval_clocks nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"odd_int" integersnil )"real" reals nil )"even_int" integersnil )"real" reals nil )"posreal" nil )"posreal" nil )"nnreal" nil )nil interval_clocks nil )"real" reals nil ))nil ))"" 3381397883"" (skosimp*)"" (expand "peer_precision?" )"" (expand "t" )"" (inst?)"" (lemma "skew_bound_1" )"" "T(j!1)" "T1!1" "T1!1 + X!1" "P" "ic1!1(j!1)" "ic2!1(j!1)" "pi!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" interval_clocks 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 booleans nil )"bool" reals nil )nil naturalnumbers nil )"int" integers nil )"int" interval_clocks nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" interval_clocks 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 )nil real_types nil )nil real_types nil )"posreal" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )nil physical_clocks nil )nil interval_clocks nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"nnreal" nil )"nnreal" interval_clocks nil )nil real_types nil )nil physical_clocks nil )"real" interval_clocks nil ))nil 3315403635"" (skosimp*)"" (expand "peer_precision?" )"" (inst?)"" (rewrite "T_def" )"" (lemma "proper_separation" )"" "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)" "0" "pi_0" )"" (assert )"" (hide 2 -1)"" case "%1 <= ADJ" ) (assert )) (! 1 r))"" (hide 2 -3)"" (expand "ADJ" )"" (rewrite "floor_monotone" )"" (hide 2)"" (cancel)"" case "%1 <= %2" ) (assert ))"" "" "" "" rewrite "max_le" )"" rewrite "max_le" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" physical_clocks nil )nil physical_clocks nil )nil floor_ceiling_ineq nil )nil minmax_ineq nil )"nonneg_real" physical_clocks nil ))nil )nil 3294485333"" (skosimp*)"" (lemma "proper_separation" )"" "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)" "0" "delta_0" )"" (assert )"" (prop)"1" (expand "peer_precision?" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 -1)"2" (invoke (then (case "%1 <=ADJ" ) (assert )) (! 1 r))"2" (hide 2 -3)"2" (expand "ADJ" )"2" (rewrite "floor_monotone" )"2" (hide 2)"2" (div-by 1 "id(1 + rho)" )"2" (expand "id" )"2" (move-terms 1 l 2)"2" assert )"2" case "%1 <= %2" ) (assert ))"2" "2" "drift" )"2" rewrite "max_le" )"2" rewrite "max_le" )"2" rewrite "T_def" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil physical_clocks nil )"nonneg_real" physical_clocks nil )nil floor_ceiling_ineq nil ))nil ))nil 3365507387"" (skosimp*)"" (use "handover_precision_lower" )"" (assert )"" (lemma "nonoverlap_basis" )"" "T1!1" "T1!1 + X!1" _ "ic1!1(j!1)" "ic2!1(1 + j!1)" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil interval_clocks nil )nil interval_clocks nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )"bool" reals nil )nil real_types 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 naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )"posreal" nil )"real" reals nil )"int" integers nil )"even_int" integersnil )"posint" nil )"int" integers nil )"nnreal" nil )nil physical_clocks nil )"posnat" interval_clocks nil )nil integers nil )nil integers nil )"nonneg_real" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"int" interval_clocks nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3315403714"" (skosimp*)"" (lemma "proper_separation" )"" "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1 + 1)" "0" "drift * P + pi_0 + alpha_l" )"" (assert )"" (prop)"1" (forward-chain "handover_precision_lower" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 -1)"2" (invoke (then (case "%1 <= ADJ" ) (assert )) (! 1 r))"2" (hide 2 -3)"2" (expand "ADJ" )"2" (rewrite "floor_monotone" )"2" (hide 2)"2" (expand "id" )"2" (cancel)"2" (isolate 1 l 1)"2" assert )"2" "2" "rate" )"2" case "%1 <= 0" )"1" "drift" )"1" (assert ) nil nil ))nil )"2" "2" rewrite "max_le" )"2" rewrite "max_le" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil floor_ceiling_ineq nil )nil minmax_ineq nil )"nonneg_real" physical_clocks nil )nil physical_clocks nil )"posreal" physical_clocks nil ))nil )nil 3294485363"" (skosimp*)"" (lemma "proper_separation" )"" "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1 + 1)" "0" "drift * P + delta_0 + epsilon_l" )"" (assert )"" (prop)"1" (forward-chain "handover_precision_lower" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 -1)"2" (invoke (then (case "%1 <= ADJ" ) (assert )) (! 1 r))"2" (hide 2 -3)"2" (expand "ADJ" )"2" (rewrite "floor_monotone" )"2" (hide 2)"2" (div-by 1 "id(1 + rho)" )"2" (expand "id" )"2" (move-terms 1 l (2 3))"2" assert )"2" case "%1 <= 0" ) (! 1 l 1 2))"1" "drift" )"1" (assert ) nil nil ))nil )"2" "2" rewrite "max_le" )"2" rewrite "max_le" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil physical_clocks nil )"nonneg_real" physical_clocks nil )nil floor_ceiling_ineq nil ))nil ))nil 3365507440"" (skosimp*)"" (use "handover_precision_upper" )"" (assert )"" (lemma "nonoverlap_basis" )"" "T1!1" "T1!1 + X!1" _ "ic2!1(1 + j!1)" "ic1!1(j!1)" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil interval_clocks nil )nil interval_clocks nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )"bool" reals nil )nil real_types 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 naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )"posreal" nil )"real" reals nil )"int" integers nil )"posreal" nil )"even_int" integersnil )"posint" nil )"int" integers nil )"nnreal" nil )nil physical_clocks nil )"posnat" interval_clocks nil )nil integers nil )nil integers nil )"nonneg_real" physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"int" interval_clocks nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3294485393"" (skosimp*)"" (lemma "proper_separation" )"" "T(j!1 + 1)" "T1!1" "T2!1" "ic2!1(j!1 + 1)" "ic1!1(j!1)" "0" "drift * P + pi_0 + alpha_u" )"" (assert )"" (prop)"1" (forward-chain "handover_precision_upper" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 -1)"2" (invoke (then (case "%1 <= ADJ" ) (assert )) (! 1 r))"2" (hide 2 -3)"2" (expand "ADJ" )"2" (rewrite "floor_monotone" )"2" (hide 2)"2" (expand "id" )"2" (isolate 1 l 1)"2" (assert )"2" "2" "rate" )"2" case "%1 <= 0" ) (! 1 l 1))"1" "drift" )"1" (assert ) nil nil ))nil )"2" "2" rewrite "max_le" )"2" rewrite "max_le" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil floor_ceiling_ineq nil )nil minmax_ineq nil )"nonneg_real" physical_clocks nil )nil physical_clocks nil )"posreal" physical_clocks nil ))nil ))"" 3400004207"" (skosimp*)"" (use "handover_precision_lower" )"" (assert )"" (use "nonoverlap_basis" )"" (rewrite "T_def" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil interval_clocks nil )nil interval_clocks nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )"bool" reals nil )nil real_types 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 naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )"posreal" nil )"int" integers nil )"real" reals nil )"odd_int" integersnil )"nnreal" nil )"even_int" integersnil )"posint" nil )"int" integers nil )nil physical_clocks nil )"int" interval_clocks nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" physical_clocks nil )nil integers nil )nil integers nil )"posnat" interval_clocks nil )"even_int" integersnil )nil interval_clocks nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil )"" 3400004192"" (skosimp*) (("" (postpone) nil nil )) nil ) nil shostak)nil 3294485429"" (skosimp*)"" (rewrite "T_def" )"" (use "nonoverlap_lower" )"" (rewrite "T_def" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" physical_clocks nil )nil physical_clocks nil ))nil ))nil 3399233072"" (induct "j" )"1" (assert )"1" (skosimp*)"1" (expand "lower_accuracy_bound?" )"1" (skosimp*)"1" (inst -2 0) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "lower_accuracy_bound?" -2)"2" (skosimp*)"2" (inst - "alpha!1" "ic1!1" "p!1" 0)"2" (prop)"1" (replace -5 :dir rl)"1" (expand "adjustment_lower_bound?" )"1" (inst - "j!1" )"1" (inst - "1 + j!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "lower_accuracy_bound?" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval_clocks nil )"posint" nil )"(total_order?[real])" nil )"posint" nil )"real" reals nil )"posreal" nil )nil naturalnumbers nil )"real" interval_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" interval_clocks nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"bool" interval_clocks nil )"[bool, bool -> bool]" booleans nil )nil interval_clocks nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types 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 defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil 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 booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil )nil 3399232999"" (skosimp*) (("" (postpone) nil nil )) nil ) nil shostak))nil 3399237520"" (induct "j" )"1" (assert )"1" (expand "upper_accuracy_bound?" )"1" (skosimp*) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "upper_accuracy_bound?" -2)"2" (skosimp*)"2" (inst - "alpha!1" "ic1!1" "p!1" 0)"2" (prop)"1" (replace -5 :dir rl)"1" (expand "adjustment_upper_bound?" )"1" (inst - "j!1" )"1" (inst - "1 + j!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "upper_accuracy_bound?" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval_clocks nil )"posint" nil )"(total_order?[real])" nil )"real" reals nil )"posint" nil )"posreal" nil )nil naturalnumbers nil )"real" interval_clocks nil )"posnat" interval_clocks nil )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"bool" interval_clocks nil )"[bool, bool -> bool]" booleans nil )nil interval_clocks nil )nil physical_clocks nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" physical_clocks nil )"nnreal" interval_clocks nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types 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 defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil 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 booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil )nil 3399233266"" (expand "upper_accuracy_bound?" )"" (skosimp*)"" (lemma "upper_adjustment" )"" (inst - "ic1!1" "j!1" "p!1" )"" (assert )"" (expand "t" )"" (inst - "T(j!1)" "j!1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" physical_clocks nil )nil physical_clocks nil ))nil )))quality 96%
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
