SSL inverse_clocks.prf   Interaktion und
PortierbarkeitLisp

(inverse_clocks
 (lower_Clocktime_exists 0
  (lower_Clocktime_exists-1 nil 3276601860
   ("" (skosimp*)
    (("" (lemma "axiom_of_archimedes")
      (("" (inst - "id(c!1(0)-t!1)*rate")
        (("" (skosimp*)
          (("" (case "i!1 >= 0")
            (("1" (inst + "-i!1")
              (("1" (lemma "drift_left")
                (("1" (inst - "-i!1" "0" "c!1")
                  (("1" (assert)
                    (("1" (div-by -3 "rate")
                      (("1" (expand "id") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "0")
              (("2" (use "pos_times_lt")
                (("2" (assert)
                  (("2" (expand "id") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((axiom_of_archimedes formula-decl nil real_props nil)
    (pos_times_lt formula-decl nil real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (both_sides_div_pos_lt1 formula-decl nil real_props nil)
    (times_div_cancel2 formula-decl nil extra_real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (drift_left formula-decl nil physical_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)
    (rho formal-const-decl "nonneg_real" inverse_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 "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (upper_Clocktime_exists 0
  (upper_Clocktime_exists-2 nil 3315959350
   ("" (skosimp*)
    (("" (lemma "axiom_of_archimedes")
      (("" (inst - "id(t!1-c!1(0))*rate")
        (("" (skosimp*)
          (("" (case "i!1 > 0")
            (("1" (inst + "i!1")
              (("1" (lemma "drift_left")
                (("1" (inst - "0" "i!1" "c!1")
                  (("1" (assert)
                    (("1" (div-by -3 "rate")
                      (("1" (expand "id") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "0")
              (("2" (use "neg_times_lt")
                (("2" (assert)
                  (("2" (expand "id") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((axiom_of_archimedes formula-decl nil real_props nil)
    (neg_times_lt formula-decl nil real_props nil)
    (both_sides_div_pos_lt1 formula-decl nil real_props nil)
    (times_div_cancel2 formula-decl nil extra_real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (drift_left formula-decl nil physical_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)
    (rho formal-const-decl "nonneg_real" inverse_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 "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil)
  (upper_Clocktime_exists-1 nil 3276602031
   ("" (skosimp*)
    (("" (lemma "axiom_of_archimedes")
      (("" (inst - "id(t!1-c!1(0))*id(1+rho)")
        (("" (skosimp*)
          (("" (case "i!1 > 0")
            (("1" (inst + "i!1")
              (("1" (lemma "drift_left")
                (("1" (inst - "0" "i!1" "c!1")
                  (("1" (assert)
                    (("1" (div-by -3 "id(1 + rho)")
                      (("1" (expand "id") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "0")
              (("2" (use "neg_times_lt")
                (("2" (assert)
                  (("2" (expand "id") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((drift_left formula-decl nil physical_clocks nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil))
   shostak))
 (past_ticks_max_set 0
  (past_ticks_max_set-2 nil 3399329805
   ("" (skosimp*)
    (("" (split +)
      (("1" (rewrite "nonempty_exists")
        (("1" (lemma "lower_Clocktime_exists")
          (("1" (inst - "c!1" "t!1")
            (("1" (skosimp*)
              (("1" (inst?)
                (("1" (expand "past_ticks") (("1" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand* "above_bounded" "upper_bound")
        (("2" (use "upper_Clocktime_exists")
          (("2" (skosimp*)
            (("2" (inst + "T!1")
              (("2" (skosimp* t)
                (("2" (expand "past_ticks")
                  (("2" (lemma "clock_nondecreasing_alt")
                    (("2" (inst - "z!1" "T!1" "c!1")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (use "sup_int_is_in_set")
        (("3" (rewrite "sup_int_in_set") nil nil)) nil))
      nil))
    nil)
   ((lower_Clocktime_exists formula-decl nil inverse_clocks nil)
    (c!1 skolem-const-decl "good_clock[rho]" inverse_clocks nil)
    (t!1 skolem-const-decl "real" inverse_clocks nil)
    (T!1 skolem-const-decl "int" inverse_clocks 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)
    (past_ticks const-decl "boolean" inverse_clocks 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 "nonneg_real" inverse_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 "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nonempty_exists formula-decl nil sets_lemmas nil)
    (upper_Clocktime_exists formula-decl nil inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (clock_nondecreasing_alt formula-decl nil physical_clocks nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (above_bounded const-decl "bool" bounded_reals "reals/")
    (upper_bound const-decl "bool" bound_defs "reals/")
    (sup_int_in_set formula-decl nil bounded_ints nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (sup_set type-eq-decl nil bounded_reals "reals/")
    (sup_int_is_in_set application-judgement "(SS)" bounded_ints nil)
    (sup_int_is_in_set judgement-tcc nil bounded_ints nil))
   nil)
  (past_ticks_max_set-1 nil 3399329765 ("" (judgement-tcc) nil nil) nil
   nil))
 (Clock_rewrite 0
  (Clock_rewrite-1 nil 3276295377
   ("" (skosimp*)
    (("" (expand* "C" "max")
      (("" (rewrite "sup_def")
        (("" (expand "least_upper_bound")
          (("" (split +)
            (("1" (expand "upper_bound")
              (("1" (skosimp* t)
                (("1" (expand "past_ticks")
                  (("1" (forward-chain "clock_nondecreasing_alt") nil
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (expand "upper_bound")
                (("2" (inst?)
                  (("2" (expand "past_ticks") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "T" bounded_reals "reals/")
    (C const-decl "int" inverse_clocks nil)
    (least_upper_bound const-decl "bool" bound_defs "reals/")
    (c!1 skolem-const-decl "good_clock[rho]" inverse_clocks nil)
    (T!1 skolem-const-decl "int" inverse_clocks nil)
    (upper_bound const-decl "bool" bound_defs "reals/")
    (clock_nondecreasing_alt formula-decl nil physical_clocks nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (past_ticks const-decl "boolean" inverse_clocks 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 "nonneg_real" inverse_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 "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sup_set type-eq-decl nil bounded_reals "reals/")
    (above_bounded const-decl "bool" bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sup_def formula-decl nil bounded_reals "reals/")
    (past_ticks_max_set application-judgement "max_set[int]"
     inverse_clocks nil))
   nil))
 (Clock_lower 0
  (Clock_lower-1 nil 3276451643
   ("" (skosimp*)
    (("" (expand* "C" "max")
      (("" (use "sup_int_in_set")
        (("" (expand* "in_set" "past_ticks") nil nil)) nil))
      nil))
    nil)
   ((max const-decl "T" bounded_reals "reals/")
    (C const-decl "int" inverse_clocks nil)
    (sup_int_is_in_set application-judgement "(SS)" bounded_ints nil)
    (in_set const-decl "bool" bounded_reals "reals/")
    (past_ticks_max_set application-judgement "max_set[int]"
     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)
    (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)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (setof type-eq-decl nil defined_types nil)
    (above_bounded const-decl "bool" bounded_reals "reals/")
    (sup_set type-eq-decl nil bounded_reals "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (>= const-decl "bool" reals 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 "nonneg_real" inverse_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)
    (past_ticks const-decl "boolean" inverse_clocks nil)
    (sup_int_in_set formula-decl nil bounded_ints nil))
   shostak))
 (Clock_upper 0
  (Clock_upper-1 nil 3276450834
   ("" (skosimp*)
    (("" (expand* "C" "max")
      (("" (invoke (typepred "%1") (! 1 r 1 2))
        (("" (expand "least_upper_bound")
          (("" (flatten)
            (("" (hide -2)
              (("" (expand "upper_bound")
                (("" (inst - "1 + sup(past_ticks(c!1)(t!1))")
                  (("1" (assert) nil nil)
                   ("2" (expand "past_ticks") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "T" bounded_reals "reals/")
    (C const-decl "int" inverse_clocks nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (c!1 skolem-const-decl "good_clock[rho]" inverse_clocks nil)
    (t!1 skolem-const-decl "real" inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (upper_bound const-decl "bool" bound_defs "reals/")
    (past_ticks const-decl "boolean" inverse_clocks 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 "nonneg_real" inverse_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 "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
     "reals/")
    (sup_set type-eq-decl nil bounded_reals "reals/")
    (above_bounded const-decl "bool" bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (least_upper_bound const-decl "bool" bound_defs "reals/")
    (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)
    (pred type-eq-decl nil defined_types 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sup_int_is_in_set application-judgement "(SS)" bounded_ints nil)
    (past_ticks_max_set application-judgement "max_set[int]"
     inverse_clocks nil))
   shostak))
 (Clock_nondecreasing 0
  (Clock_nondecreasing-1 nil 3276295641
   ("" (skosimp*)
    (("" (lemma "clock_nondecreasing")
      (("" (inst - "1+ C(c!1)(t2!1)" "C(c!1)(t1!1)" "c!1")
        (("" (assert)
          (("" (use "Clock_lower")
            (("" (use "Clock_upper") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rho formal-const-decl "nonneg_real" inverse_clocks 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)
    (clock_nondecreasing formula-decl nil physical_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Clock_upper formula-decl nil inverse_clocks nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (C const-decl "int" inverse_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)
    (> const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (alt_clock_edge 0
  (alt_clock_edge-1 nil 3356187762
   ("" (skosimp*)
    (("" (expand "clock_edge?")
      (("" (prop)
        (("1" (skosimp*)
          (("1" (replace*) (("1" (rewrite "Clock_rewrite") nil nil))
            nil))
          nil)
         ("2" (inst?) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((clock_edge? const-decl "bool" physical_clocks nil)
    (C const-decl "int" inverse_clocks nil)
    (Clock_rewrite 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)
    (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)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (>= const-decl "bool" reals 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 "nonneg_real" inverse_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))
   shostak))
 (conversion_left 0
  (conversion_left-1 nil 3399313032
   ("" (skosimp*)
    (("" (lemma "clock_increasing")
      (("" (inst - "T!1" "C(c!1)(t!1)" "c!1")
        (("" (use "Clock_lower") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((rho formal-const-decl "nonneg_real" inverse_clocks 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)
    (clock_increasing formula-decl nil physical_clocks nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (C const-decl "int" inverse_clocks 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" 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))
   nil))
 (conversion_left_alt 0
  (conversion_left_alt-1 nil 3400097352
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "clock_nondecreasing")
        (("1" (inst - "C(c!1)(t!1) + 1" "T!1 + 1" "c!1")
          (("1" (use "Clock_upper") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (lemma "clock_nondecreasing")
        (("2" (inst - "T!1 + 1" "C(c!1)(t!1)" "c!1")
          (("2" (use "Clock_lower") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (rate const-decl "posreal" physical_clocks nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil)
    (C const-decl "int" inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (Clock_upper formula-decl nil inverse_clocks nil)
    (clock_nondecreasing formula-decl nil physical_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" inverse_clocks nil)
    (Clock_lower formula-decl nil inverse_clocks nil))
   nil))
 (conversion_right 0
  (conversion_right-1 nil 3399313037
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "clock_nondecreasing")
        (("1" (inst - "T!1" "C(c!1)(t!1)" "c!1")
          (("1" (use "Clock_lower") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (lemma "clock_nondecreasing")
        (("2" (inst - "C(c!1)(t!1) + 1" "T!1" "c!1")
          (("2" (use "Clock_upper") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    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)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types 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)
    (C const-decl "int" inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (clock_nondecreasing formula-decl nil physical_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" inverse_clocks nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (Clock_upper formula-decl nil inverse_clocks nil))
   nil))
 (obs_bound 0
  (obs_bound-2 nil 3399314973
   ("" (expand "obs?")
    (("" (skosimp*)
      (("" (rewrite "conversion_right" :dir rl)
        (("" (rewrite "conversion_left_alt" :dir rl)
          (("" (rewrite "abs_max")
            (("" (rewrite "max_le") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (conversion_left_alt formula-decl nil inverse_clocks nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (max_le formula-decl nil minmax_ineq nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs nil)
    (rat_max application-judgement "{s: rat | s >= q AND s >= r}"
     real_defs nil)
    (abs_max formula-decl nil abs_props nil)
    (C const-decl "int" inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (rho formal-const-decl "nonneg_real" inverse_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)
    (<= const-decl "bool" reals 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (conversion_right formula-decl nil inverse_clocks nil)
    (obs? const-decl "bool" inverse_clocks nil))
   nil)
  (obs_bound-1 nil 3366976655
   ("" (skosimp*)
    (("" (expand "abs")
      (("" (lift-if)
        (("" (expand "obs?")
          (("" (prop)
            (("1" (lemma "clock_nondecreasing")
              (("1" (inst - "C(c!1)(t!1) + 1" "T!1 - X!1" "c!1")
                (("1" (assert)
                  (("1" (lemma "Clock_upper")
                    (("1" (inst - "c!1" "t!1") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (lemma "clock_nondecreasing")
              (("2" (inst - "T!1 + X!1" "C(c!1)(t!1)" "c!1")
                (("2" (assert)
                  (("2" (lemma "Clock_lower")
                    (("2" (inst - "c!1" "t!1") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_nondecreasing formula-decl nil physical_clocks nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil)
    (rate const-decl "posreal" physical_clocks nil))
   nil))
 (precision_conversion_sym 0
  (precision_conversion_sym-1 nil 3366739250
   ("" (skosimp*)
    (("" (use "skew_bound")
      (("" (assert)
        (("" (rewrite "obs_bound")
          (("" (use "Clock_lower")
            (("" (use "Clock_upper") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((skew_bound formula-decl nil physical_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" inverse_clocks nil)
    (nnreal type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (C const-decl "int" inverse_clocks 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" 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)
    (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (obs_bound formula-decl nil inverse_clocks nil)
    (Clock_upper formula-decl nil inverse_clocks nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (precision_conversion 0
  (precision_conversion-1 nil 3366740126
   ("" (skosimp*)
    (("" (use "precision_conversion_sym")
      (("" (prop)
        (("" (rewrite "abs_diff_commutes" +)
          (("" (rewrite "abs_diff_commutes")
            (("" (use "precision_conversion_sym")
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((precision_conversion_sym formula-decl nil inverse_clocks 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 "nonneg_real" inverse_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)
    (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)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (C const-decl "int" inverse_clocks nil)
    (abs_diff_commutes formula-decl nil abs_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (lower_accuracy_conversion 0
  (lower_accuracy_conversion-2 nil 3399215061
   ("" (skosimp*)
    (("" (rewrite "conversion_right" :dir rl)
      (("" (lemma "upper_offset")
        (("" (inst - "T!1" "1 + C(c!1)(t!1)" "X!1" "c!1")
          (("" (assert)
            (("" (use "Clock_upper")
              (("" (cross-mult) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (conversion_right 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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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 "nonneg_real" inverse_clocks nil)
    (rate const-decl "posreal" physical_clocks nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (C const-decl "int" inverse_clocks nil)
    (Clock_upper formula-decl nil inverse_clocks nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (drift const-decl "nonneg_real" physical_clocks nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (upper_offset formula-decl nil physical_clocks nil))
   nil))
 (upper_accuracy_conversion 0
  (upper_accuracy_conversion-2 nil 3399217261
   ("" (skosimp*)
    (("" (rewrite "conversion_right" :dir rl)
      (("" (lemma "lower_offset")
        (("" (inst - "T!1" "C(c!1)(t!1)" "X!1" "c!1")
          (("" (assert)
            (("" (use "Clock_lower")
              (("" (mult-by -1 "rate") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (conversion_right 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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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 "nonneg_real" inverse_clocks nil)
    (rate const-decl "posreal" physical_clocks nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (C const-decl "int" inverse_clocks nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (lower_offset formula-decl nil physical_clocks nil))
   nil)
  (upper_accuracy_conversion-1 nil 3399216258
   (";;; Proof for formula inverse_clocks.lower_offset_conversion_alt"
    (skosimp*)
    ((";;; Proof for formula inverse_clocks.lower_offset_conversion_alt"
      (rewrite "min_le")
      ((";;; Proof for formula inverse_clocks.lower_offset_conversion_alt"
        (flatten)
        ((";;; Proof for formula inverse_clocks.lower_offset_conversion_alt"
          (case "gamma!1 >= 0")
          (("1" (hide 1)
            (("1" (lemma "drift_right")
              (("1" (inst - "C(c!1)(t!1)" "T!1" "c!1")
                (("1" (prop)
                  (("1" (use "Clock_lower")
                    (("1" (mult-by 1 "rate") (("1" (assert) nil)))))
                   ("2" (lemma "Clock_nondecreasing")
                    (("2" (inst - "c!1" "t!1" "c!1(T!1)")
                      (("2" (assert)
                        (("2" (rewrite "Clock_rewrite")
                          nil)))))))))))))))
           ("2" (hide 3)
            (("2" (lemma "drift_left")
              (("2" (inst - "T!1" "C(c!1)(t!1)" "c!1")
                (("2" (prop)
                  (("1" (use "Clock_lower")
                    (("1" (div-by 2 "rate") (("1" (assert) nil)))))
                   ("2" (mult-by 2 "rate")
                    (("2" (assert) nil))))))))))))))))))
    "")
   nil nil)))