|
(virtual_clocks
(VC_j 0
(VC_j-1 nil 3400104336
("" (skosimp*)
(("" (expand "VC") (("" (rewrite "index_rewrite") nil nil)) nil))
nil)
((VC const-decl "int" virtual_clocks nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(index_rewrite formula-decl nil event_sequences nil))
nil))
(observable_peers 0
(observable_peers-1 nil 3399253525
("" (expand "self_adjustment?")
(("" (skosimp*)
(("" (expand "obs?")
(("" (prop)
(("1" (forward-chain "index_le")
(("1" (expand "earliest_adjustment?")
(("1" (inst?)
(("1"
(invoke (then (case "%1 <= %2") (assert)) (! 1 l)
(! -2 l))
(("1" (rewrite "clock_nondecreasing") nil nil)) nil))
nil))
nil))
nil)
("2" (use "lt_index")
(("2" (expand "latest_adjustment?")
(("2" (inst?)
(("2" (rewrite "T_def") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((earliest_adjustment? const-decl "bool" virtual_clocks nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(rate const-decl "posreal" physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T const-decl "int" interval_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(clock_nondecreasing formula-decl nil physical_clocks nil)
(index_of const-decl "nat" event_sequences nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(index_le formula-decl nil event_sequences nil)
(latest_adjustment? const-decl "bool" virtual_clocks nil)
(T_def formula-decl nil interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(lt_index formula-decl nil event_sequences nil)
(obs? const-decl "bool" inverse_clocks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(self_adjustment? const-decl "bool" virtual_clocks nil))
nil))
(observable_master 0
(observable_master-1 nil 3399253550
("" (skosimp*)
(("" (expand* "self_adjustment?" "cross_adjustment?" "obs?")
(("" (prop)
(("1" (lemma "index_le")
(("1" (inst - "es2!1" _)
(("1" (inst?)
(("1" (expand "earliest_cross_adjustment?")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (lemma "lt_index")
(("2" (inst - "es1!1" _)
(("2" (inst?)
(("2" (expand "latest_adjustment?")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cross_adjustment? const-decl "bool" virtual_clocks nil)
(obs? const-decl "bool" inverse_clocks nil)
(self_adjustment? const-decl "bool" virtual_clocks nil)
(lt_index formula-decl nil event_sequences nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(latest_adjustment? const-decl "bool" virtual_clocks nil)
(index_le formula-decl nil event_sequences nil)
(index_of const-decl "nat" event_sequences nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(earliest_cross_adjustment? const-decl "bool" virtual_clocks nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(observable_slave 0
(observable_slave-1 nil 3399253567
("" (skosimp*)
(("" (expand* "self_adjustment?" "cross_adjustment?" "obs?")
(("" (prop)
(("1" (lemma "index_le")
(("1" (inst - "es2!1" _)
(("1" (inst?)
(("1" (expand "earliest_adjustment?")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (lemma "lt_index")
(("2" (inst - "es1!1" _)
(("2" (inst?)
(("2" (expand "latest_cross_adjustment?")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cross_adjustment? const-decl "bool" virtual_clocks nil)
(obs? const-decl "bool" inverse_clocks nil)
(self_adjustment? const-decl "bool" virtual_clocks nil)
(lt_index formula-decl nil event_sequences nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(latest_cross_adjustment? const-decl "bool" virtual_clocks nil)
(index_le formula-decl nil event_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(index_of const-decl "nat" event_sequences nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(earliest_adjustment? const-decl "bool" virtual_clocks nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(adjustment_nonoverlap 0
(adjustment_nonoverlap-1 nil 3400105725
("" (expand "nonoverlap?")
(("" (skosimp*)
(("" (expand "latest_cross_adjustment?")
(("" (inst?)
(("" (expand "earliest_cross_adjustment?")
(("" (inst?)
(("" (rewrite "T_def")
((""
(invoke (then (case "%1 <= %2") (assert)) (! -1 r)
(! -2 l))
(("" (rewrite "clock_nondecreasing") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T const-decl "int" interval_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(clock_nondecreasing formula-decl nil physical_clocks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(T_def formula-decl nil interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(earliest_cross_adjustment? const-decl "bool" virtual_clocks nil)
(latest_cross_adjustment? const-decl "bool" virtual_clocks nil)
(nonoverlap? const-decl "bool" event_sequences nil))
nil))
(VC_precision_0 1
(VC_precision_0-2 "" 3399314721
("" (skosimp*)
(("" (expand "VC")
(("" (replace*)
(("" (expand "Pi")
(("" (lemma "precision_conversion")
(("" (assert)
((""
(inst - "T(index_of(es1!1)(t1!1))" "P + A!1" _ _ _ _)
(("" (inst?)
(("" (assert)
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (expand "obs?")
(("" (prop)
(("1"
(expand "peer_precision?")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(expand "abs")
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "peers_le") nil nil)
("3" (rewrite "lt_peers") nil nil)
("4"
(swap-rel -6)
(("4"
(replace*)
(("4" (rewrite "peers_le") nil nil))
nil))
nil)
("5"
(swap-rel -6)
(("5"
(replace*)
(("5" (rewrite "lt_peers") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak)
(VC_precision_0-1 nil 3399253349
("" (skosimp*)
(("" (expand "VC")
(("" (replace*)
(("" (expand "Pi")
(("" (lemma "precision_conversion")
(("" (assert)
((""
(inst - "T(index_of(es1!1)(t1!1))" "P + A!1" _ _ _ _)
(("" (inst?)
(("" (assert)
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand* "peer_precision?" "t")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(expand "abs")
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (use "observable_peers")
(("2" (assert) nil nil)) nil)
("3" (swap-rel -6)
(("3"
(replace*)
(("3"
(use "observable_peers")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((VC const-decl "int" virtual_clocks nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(Pi const-decl "int" virtual_clocks nil)
(nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(<= const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(observable_peers formula-decl nil virtual_clocks nil)
(t const-decl "real" interval_clocks nil)
(peer_precision? const-decl "bool" interval_clocks nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(index_of const-decl "nat" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T const-decl "int" interval_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(precision_conversion formula-decl nil inverse_clocks nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(VC_precision_1 0
(VC_precision_1-1 nil 3399253439
("" (skosimp*)
(("" (expand "VC")
(("" (replace*)
(("" (lemma "observable_master")
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (hide -3 -5)
(("" (lemma "observable_slave")
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (hide -4 -5)
(("" (expand "compatible?")
((""
(flatten)
((""
(lemma "handover_precision")
((""
(inst?)
((""
(inst?)
((""
(prop)
((""
(use "precision_conversion")
((""
(expand "Pi")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((VC const-decl "int" virtual_clocks nil)
(observable_master formula-decl nil virtual_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(compatible? const-decl "bool" interval_clocks nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(handover_precision formula-decl nil interval_clocks nil)
(index_of const-decl "nat" event_sequences nil)
(precision_conversion formula-decl nil inverse_clocks nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(T const-decl "int" interval_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
(Pi const-decl "int" virtual_clocks nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(observable_slave formula-decl nil virtual_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(VC_precision_sym 0
(VC_precision_sym-1 nil 3399253457
("" (skosimp*)
(("" (rewrite "VC_precision_1")
(("" (expand "compatible?")
(("" (rewrite "VC_precision_0")
(("" (use "nonoverlap_index_bound") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((VC_precision_1 formula-decl nil virtual_clocks nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(rate const-decl "posreal" physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(VC_precision_0 formula-decl nil virtual_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nonoverlap_index_bound formula-decl nil event_sequences nil)
(compatible? const-decl "bool" interval_clocks nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(VC_precision 0
(VC_precision-1 nil 3399253472
("" (skosimp*)
(("" (rewrite "VC_precision_sym")
(("" (rewrite "abs_diff_commutes")
(("" (rewrite "max_commutative")
(("" (rewrite "VC_precision_sym") nil nil)) nil))
nil))
nil))
nil)
((VC_precision_sym formula-decl nil virtual_clocks nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(rate const-decl "posreal" physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max_commutative formula-decl nil minmax_ineq nil)
(abs_diff_commutes formula-decl nil abs_props nil)
(VC const-decl "int" virtual_clocks nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(index_upper_bound 0
(index_upper_bound-1 nil 3399253758
("" (skosimp*)
(("" (cross-mult)
(("" (use "lower_interval_accuracy")
(("" (prop)
(("" (expand "earliest_adjustment?")
(("" (forward-chain "index_le")
(("" (inst?)
(("" (invoke (name-replace "K" "%1") (! 1 l 1))
(("" (lemma "drift_right")
(("" (inst - "T(K) - A!1" "T(K)" "ic!1(K)")
(("" (expand "t") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(t const-decl "real" interval_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(index_of const-decl "nat" event_sequences nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(index_le formula-decl nil event_sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(T const-decl "int" interval_clocks nil)
(drift_right formula-decl nil physical_clocks nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(earliest_adjustment? const-decl "bool" virtual_clocks nil)
(lower_interval_accuracy formula-decl nil interval_clocks nil))
nil))
(VC_lower_accuracy 0
(VC_lower_accuracy-1 nil 3399253775
("" (skosimp*)
(("" (expand "VC")
(("" (forward-chain "index_upper_bound")
(("" (mult-by -1 "au!1")
(("" (lemma "upper_interval_accuracy")
(("" (inst?)
(("" (inst - "index_of(es!1)(t1!1)" "P * rate + au!1")
(("" (prop)
(("" (forward-chain "index_le")
(("" (expand* "earliest_adjustment?" "id")
(("" (inst?)
(("" (lemma "lower_accuracy_conversion")
(("" (inst - _ _ _ "t1!1")
(("" (inst?)
((""
(assert)
((""
(cross-mult (-1 1))
((""
(expand* "t" "T")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(VC const-decl "int" virtual_clocks nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(index_of const-decl "nat" event_sequences nil)
(t const-decl "real" interval_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(earliest_adjustment? const-decl "bool" virtual_clocks nil)
(lower_accuracy_conversion formula-decl nil inverse_clocks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(T const-decl "int" interval_clocks nil)
(times_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div2 formula-decl nil real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(C const-decl "int" inverse_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(index_le formula-decl nil event_sequences nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(upper_interval_accuracy formula-decl nil interval_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(index_upper_bound formula-decl nil virtual_clocks nil))
nil))
(VC_upper_accuracy 0
(VC_upper_accuracy-1 nil 3399253790
("" (skosimp*)
(("" (expand "VC")
(("" (forward-chain "index_upper_bound")
(("" (mult-by -1 "al!1")
(("" (expand* "earliest_adjustment?" "id")
(("" (inst?)
(("" (lemma "lower_interval_accuracy")
(("" (inst?)
((""
(inst - "index_of(es!1)(t1!1)" "P / rate - al!1")
(("" (prop)
(("" (forward-chain "index_le")
(("" (lemma "upper_accuracy_conversion")
(("" (inst - _ _ _ "t1!1")
(("" (inst?)
((""
(assert)
((""
(div-by (-1 1) "rate")
((""
(expand* "t" "T")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(VC const-decl "int" virtual_clocks nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(index_of const-decl "nat" event_sequences nil)
(t const-decl "real" interval_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(upper_accuracy_conversion formula-decl nil inverse_clocks nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(T const-decl "int" interval_clocks nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(C const-decl "int" inverse_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(index_le formula-decl nil event_sequences nil)
(lower_interval_accuracy formula-decl nil interval_clocks nil)
(earliest_adjustment? const-decl "bool" virtual_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(T0 formal-const-decl "int" virtual_clocks nil)
(P formal-const-decl "posnat" virtual_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" virtual_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(event_sequence type-eq-decl nil event_sequences nil)
(unbounded? const-decl "bool" event_sequences nil)
(increasing? const-decl "bool" event_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(index_upper_bound formula-decl nil virtual_clocks nil))
nil)))
¤ Dauer der Verarbeitung: 0.63 Sekunden
(vorverarbeitet)
¤
|
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.
|
