(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)))