%% PVS Version 4.0 - CMU Common Lisp 19c (19C)
%% 19c (19C)
$$$time_triggered_system2.pvs
%% Lee Pike <leepike _at_ galois.com> 
%% July, 2007 

%% Accompanies the paper, "Modeling Time-Triggered Protocols and Verifying Their
%% Real-Time Schedules," (FMCAD, 2007).

%% <http://www.cs.indiana.edu/~lepike/pub_pages/fmcad.html>
%% PVS 4.0

time_triggered_system2: THEORY
 BEGIN

  proc, mess, state: TYPE+

  init_state: nonempty_pred[state]

  null: mess

  in_nbrs, out_nbrs: [proc -> setof[proc]]

  p, q, n: VAR proc

  s: VAR state

%% Definition
  channels_match: AXIOM in_nbrs(p)(q) IFF out_nbrs(q)(p)

  round: TYPE = nat

  r, i, j: VAR round

  msg(p): [state, (out_nbrs(p)) -> mess]

  inputs(p): TYPE = [(in_nbrs(p)) -> mess]

  trans(p): [state, inputs(p) -> state]

  global_state: TYPE = [proc -> state]

  gs1, gs2: VAR global_state

  global_init: TYPE = [proc -> (init_state)]

  ginit: VAR global_init

  ginit_cnst: global_init

  run(ginit)(r): RECURSIVE global_state =
    IF r = 0 THEN ginit
    ELSE LAMBDA p:
           trans(p)(s(p), (LAMBDA (q: (in_nbrs(p))): msg(q)(s(q), p)))
             WHERE s = run(ginit)(r - 1)
    ENDIF
     MEASURE r

  independent?(r): boolean

%% Untimed semantic axiom (Axiom 1)
  independent: AXIOM
    (NOT independent?(0)) AND
     (independent?(r) =>
       (FORALL (q: (out_nbrs(p))):
          msg(p)(run(ginit)(r)(p), q) = msg(p)(run(ginit)(r - 1)(p), q)))

  m: VAR mess

  clocktime: TYPE = int

  realtime: TYPE = real

  T, T1: VAR clocktime

  t, t1, t2: VAR realtime

  C(p, t): clocktime

  rho: {x: real | 0 <= x AND x < 1}

  sched(r)(p): clocktime

  D(r): clocktime

  P(r): {t: clocktime | t > 0}

  recv_win(r): {t: clocktime | t >= 0}

  Sigma(r): {t: clocktime | t >= 0}

  sched_skew(r): {t: clocktime | t >= 0}

  dur(r)(p): clocktime = sched(r + 1)(p) - sched(r)(p)

  nom_delay: {x: realtime | 0 < x}

  e_l: {x: realtime | 0 < x}

  e_u: {x: realtime | 0 < x}

  e: realtime = e_l + e_u;

  delay: TYPE =
        {x: realtime | nom_delay - e_l <= x AND x <= nom_delay + e_u}

  d: VAR delay

%% Schedule definitons %%%%%%%
  error_constraint: AXIOM e_l < nom_delay AND e_u < nom_delay

  sendtime(p, r): realtime

  sendtime_ax: AXIOM C(p, sendtime(p, r)) = sched(r)(p) + D(r)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% System Assumptions %%%%%%%%
  % Axiom 1
  drift_rate: AXIOM
    t1 >= t2 IMPLIES
     floor((1 - rho) * (t1 - t2)) <= C(p, t1) - C(p, t2) AND
      C(p, t1) - C(p, t2) <= ceiling((1 + rho) * (t1 - t2))

  monotone_clock: LEMMA t1 < t2 => C(p, t1) <= C(p, t2)

  % Axiom 2
  clock_sync: AXIOM
    (max(C(p, t), C(q, t)) >= min(sched(r)(p), sched(r)(q)) + D(r) AND
      min(C(p, t), C(q, t)) <= max(sched(r)(p), sched(r)(q)) + P(r))
     => abs(C(p, t) - C(q, t)) <= Sigma(r)

  sent(p, (q: (out_nbrs(p))), m, t): bool

  recv(q, (p: (in_nbrs(q))), m, t): bool

  % Axiom 3
  max_delay: AXIOM
    FORALL p, (q: (out_nbrs(p))), m, t:
      (EXISTS (d: delay): sent(p, q, m, t) => recv(q, p, m, t + d)) AND
       (EXISTS (d: delay): recv(q, p, m, t) => sent(p, q, m, t - d))

  % Axiom 4
  sched_sync: AXIOM abs(sched(r)(p) - sched(r)(q)) <= sched_skew(r)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Schedule Constraints %%%%%%
  constraint1: AXIOM P(r) < dur(r)(p)

  constraint2: AXIOM
    D(r) >= Sigma(r) + sched_skew(r) - floor((1 - rho) * (nom_delay - e_l))

  constraint3: AXIOM
    P(r) >
     D(r) + Sigma(r) + sched_skew(r) +
      ceiling((1 + rho) * (nom_delay + e_u))

  constraint4: AXIOM NOT independent?(r) => D(r) >= 0

  constraint5: AXIOM r > 0 => D(r) >= P(r - 1) - dur(r - 1)(p)

  constraint6: AXIOM
    recv_win(r) - 1 <=
     D(r) + floor((1 - rho) * (nom_delay - e_l)) - Sigma(r) - sched_skew(r)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  monotone_sched: LEMMA sched(i)(p) < sched(i + 1)(p)

  in_comp_phase(t, p, r): bool =
      LET T = C(p, t) IN sched(r)(p) + P(r) < T AND T < sched(r + 1)(p)

  comp_phase: LEMMA i < j => sched(i)(p) + P(i) < sched(j)(p)

  ttss(gs1)(p)(T): state

  rho_prop1: LEMMA (1 - rho) * d >= 0

  rho_prop2: LEMMA (1 + rho) * d >= 0

%% Semantic Axioms %%%%%%%%%%%
  % Axiom 3
  comm_phase1: AXIOM
    FORALL (q: (out_nbrs(p))):
      sent(p, q, m, sendtime(p, r))
        WHERE m = msg(p)(ttss(gs1)(p)(sched(r)(p) + D(r)), q)

  % Axiom 4
  comm_phase2: AXIOM
    FORALL (q: (out_nbrs(p))):
      sent(p, q, m, t) =>
       (EXISTS r:
          t = sendtime(p, r) AND
           m = msg(p)(ttss(gs1)(p)(sched(r)(p) + D(r)), q))

  constraint3_lemma: LEMMA
    P(i) > D(i) + Sigma(i) + sched_skew(i) + ceiling((1 + rho) * d)

  recv_win_open(t, p, r): bool =
      LET T = C(p, t) IN
        sched(r)(p) + recv_win(r) - 1 <= T AND T < sched(r)(p) + P(r)

  arrival_prop: LEMMA recv_win_open(sendtime(q, r) + d, p, r)

  recv_prop: LEMMA
    FORALL r, p, (q: (in_nbrs(p))):
      EXISTS (m: mess), (t: realtime):
        recv_win_open(t, p, r) AND recv(p, q, m, t)

  ttin(p)(T)((q: (in_nbrs(p)))): mess

  % Axiom 5
  ttin_ax: AXIOM
    sched(r)(p) + P(r) <= T AND T < sched(r + 1)(p) =>
     (FORALL (q: (in_nbrs(p))):
        ttin(p)(T)(q) =
         epsilon! (m):
           EXISTS t: recv_win_open(t, p, r) AND recv(p, q, m, t))

  % Axiom 6
  ttss_start: AXIOM
    ttss(ginit)(p)(sched(r)(p)) =
     IF r = 0 THEN ginit(p)
     ELSE trans(p)(ttss(ginit)(p)(T), ttin(p)(T))
            WHERE T = sched(r - 1)(p) + P(r - 1)
     ENDIF

  % Axiom 7
  ttss_comm: AXIOM
    sched(r)(p) <= T AND T <= sched(r)(p) + P(r) =>
     ttss(ginit)(p)(T) = ttss(ginit)(p)(sched(r)(p))

  gs(r): realtime

  % Axiom 8
  gs_ax: AXIOM
    (FORALL q: FORALL n: C(q, gs(r)) >= sched(r)(n)) AND
     (EXISTS p: FORALL n: C(p, gs(r)) = sched(r)(n))

  % Axiom 9
  ttss_comp: AXIOM
    (sched(r)(p) + P(r) <= T AND T < sched(r + 1)(p)) =>
     (ttss(ginit)(p)(T) = ttss(ginit)(p)(sched(r)(p)) OR
       ttss(ginit)(p)(T) = ttss(ginit)(p)(sched(r + 1)(p)))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  send_state: LEMMA
    FORALL r:
      (FORALL j: j <= r => ttss(ginit)(p)(sched(j)(p)) = run(ginit)(j)(p))
       =>
       IF independent?(r)
         THEN (ttss(ginit)(p)(sched(r)(p) + D(r)) = run(ginit)(r)(p) OR
                ttss(ginit)(p)(sched(r)(p) + D(r)) = run(ginit)(r - 1)(p))
       ELSE ttss(ginit)(p)(sched(r)(p) + D(r)) = run(ginit)(r)(p)
       ENDIF

  ttin_prop: LEMMA
    FORALL (q: (in_nbrs(p))):
      FORALL r:
        (FORALL j:
           j <= r => ttss(ginit)(q)(sched(j)(q)) = run(ginit)(j)(q))
         =>
         ttin(p)(sched(r)(p) + P(r))(q) =
          msg(q)(ttss(ginit)(q)(sched(r)(q)), p)

  Main_Lemma: LEMMA ttss(ginit)(p)(sched(r)(p)) = run(ginit)(r)(p)

  pre_comp_phase(t, p, r): bool =
      LET T = C(p, t) IN sched(r)(p) <= T AND T < sched(r)(p) + P(r)

  gs_pre_comp: LEMMA pre_comp_phase(gs(r), p, r)

  same_state_time: LEMMA
    pre_comp_phase(t, p, r) => ttss(ginit)(p)(C(p, t)) = run(ginit)(r)(p)

  Theorem_1: THEOREM ttss(ginit)(p)(C(p, gs(r))) = run(ginit)(r)(p)
 END time_triggered_system2

$$$time_triggered_system2.prf
(time_triggered_system2
 (init_state_TCC1 0
  (init_state_TCC1-1 nil 3322304665 3330685250
   ("" (inst + "LAMBDA (s: state): TRUE")
    (("" (use "state_nonempty") nil nil)) nil)
   unchecked
   ((state_nonempty formula-decl nil time_triggered_system2 nil)
    (TRUE const-decl "bool" booleans nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (state nonempty-type-decl nil time_triggered_system2 nil))
   14 10 t nil))
 (ginit_cnst_TCC1 0
  (ginit_cnst_TCC1-1 nil 3328265140 3330685250
   ("" (inst + "LAMBDA (p: proc): epsilon(init_state)")
    (("" (use "epsilon_ax[state]")
      (("" (split)
        (("1" (propax) nil nil)
         ("2" (use "init_state_TCC1") (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   unchecked
   ((epsilon_ax formula-decl nil epsilons nil)
    (init_state_TCC1 existence-tcc nil time_triggered_system2 nil)
    (epsilon const-decl "T" epsilons nil)
    (global_init type-eq-decl nil time_triggered_system2 nil)
    (init_state const-decl "nonempty_pred[state]"
     time_triggered_system2 nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (state nonempty-type-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   79 30 t nil))
 (run_TCC1 0
  (run_TCC1-1 nil 3321118094 3330685250 ("" (tcc)) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" 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)
    (round type-eq-decl nil time_triggered_system2 nil))
   62 60 nil nil))
 (run_TCC2 0
  (run_TCC2-1 nil 3321118094 3330685250 ("" (tcc)) unchecked nil 12 10
   nil nil))
 (run_TCC3 0
  (run_TCC3-1 nil 3321118094 3330685250
   ("" (skosimp*)
    (("" (use "channels_match") (("" (assert) nil nil)) nil)) nil)
   unchecked
   ((channels_match formula-decl nil time_triggered_system2 nil)
    (in_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   126 70 t shostak))
 (independent_TCC1 0
  (independent_TCC1-1 nil 3321118094 3330685250 ("" (tcc)) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" 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)
    (round type-eq-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (setof type-eq-decl nil defined_types nil)
    (out_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil))
   116 70 nil nil))
 (rho_TCC1 0
  (rho_TCC1-1 nil 3318164256 3330685251 ("" (inst + "1/2") nil nil)
   unchecked
   ((/ 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) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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))
   90 90 t shostak))
 (monotone_clock 0
  (monotone_clock-1 nil 3321786940 3330685251
   ("" (skosimp*)
    (("" (lemma "drift_rate")
      (("" (inst - "p!1" "t2!1" "t1!1")
        (("" (assert)
          (("" (flatten)
            ((""
              (case "floor(rho * t1!1 - rho * t2!1 + (t2!1 - t1!1)) >= 0")
              (("1" (assert) nil nil)
               ("2" (hide 2 -2 -1)
                (("2"
                  (case "rho * t1!1 - rho * t2!1 + (t2!1 - t1!1) = (1 - rho) * (t2!1 - t1!1)")
                  (("1" (lemma "pos_times_le")
                    (("1" (inst - "1 - rho" "t2!1 - t1!1")
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((drift_rate formula-decl nil time_triggered_system2 nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-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 "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pos_times_le formula-decl nil real_props nil)
    (realtime type-eq-decl nil time_triggered_system2 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)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   787 460 t nil))
 (P_TCC1 0
  (P_TCC1-1 nil 3320073551 3330685251
   ("" (inst + "LAMBDA (x: round): 1") nil nil) unchecked
   ((> const-decl "bool" reals nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 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))
   8 10 t shostak))
 (recv_win_TCC1 0
  (recv_win_TCC1-1 nil 3328373966 3330685251
   ("" (inst + "LAMBDA (r: round): 0") nil nil) unchecked
   ((clocktime type-eq-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 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))
   6 10 t nil))
 (nom_delay_TCC1 0
  (nom_delay_TCC1-1 nil 3318164256 3330685251 ("" (inst + "1") nil nil)
   unchecked
   ((< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (realtime type-eq-decl nil time_triggered_system2 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))
   16 20 t shostak))
 (constraint5_TCC1 0
  (constraint5_TCC1-1 nil 3319978161 3330685252 ("" (tcc)) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" 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)
    (round type-eq-decl nil time_triggered_system2 nil))
   90 60 t shostak))
 (monotone_sched 0
  (monotone_sched-1 nil 3319451473 3330685252
   ("" (skosimp*)
    (("" (use "constraint1")
      (("" (expand "dur") (("" (assert) nil nil)) nil)) nil))
    nil)
   unchecked
   ((constraint1 formula-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 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)
    (dur const-decl "clocktime" time_triggered_system2 nil))
   450 240 t shostak))
 (comp_phase 0
  (comp_phase-2 nil 3328163510 3330685253
   ("" (skosimp)
    ((""
      (case "forall (x:above(0)): sched(i!1)(p!1) + P(i!1) < sched(i!1+x)(p!1)")
      (("1" (inst - "j!1-i!1")
        (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
       ("2" (induct "x")
        (("1" (lemma "constraint1") (("1" (grind) nil nil)) nil)
         ("2" (skosimp)
          (("2" (lemma "monotone_sched")
            (("2" (inst - "i!1+ja!1" "p!1") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((P const-decl "{t: clocktime | t > 0}" time_triggered_system2 nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (monotone_sched formula-decl nil time_triggered_system2 nil)
    (constraint1 formula-decl nil time_triggered_system2 nil)
    (dur const-decl "clocktime" time_triggered_system2 nil)
    (above_induction formula-decl nil bounded_int_inductions nil)
    (pred type-eq-decl nil defined_types nil))
   1312 720 t nil)
  (comp_phase-1 nil 3318166106 3328163456
   ("" (skosimp)
    ((""
      (case "forall (x:above(0)): sched(i!1) + P(i!1) < sched(i!1+x)")
      (("1" (inst - "j!1-i!1")
        (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
       ("2" (induct "x")
        (("1" (lemma "constraint1") (("1" (grind) nil nil)) nil)
         ("2" (skosimp)
          (("2" (lemma "monotone_sched2")
            (("2" (inst - "i!1+ja!1" "i!1+ja!1+1")
              (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((monotone_sched formula-decl nil time_triggered_system2 nil)
    (P const-decl "{t: clocktime | t > 0}" time_triggered_system2 nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (constraint1 formula-decl nil time_triggered_system2 nil)
    (dur const-decl "clocktime" time_triggered_system2 nil)
    (above_induction formula-decl nil bounded_int_inductions nil)
    (pred type-eq-decl nil defined_types nil))
   105078 10050 t shostak))
 (max_delay_TCC1 0
  (max_delay_TCC1-1 nil 3318164256 3330685253
   ("" (skosimp*)
    (("" (use "channels_match") (("" (assert) nil nil)) nil)) nil)
   unchecked
   ((channels_match formula-decl nil time_triggered_system2 nil)
    (out_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   37 40 t shostak))
 (max_delay_TCC2 0
  (max_delay_TCC2-1 nil 3325428689 3330685254
   ("" (skosimp*)
    (("" (use "channels_match") (("" (assert) nil nil)) nil)) nil)
   unchecked
   ((channels_match formula-decl nil time_triggered_system2 nil)
    (out_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   79 50 t nil))
 (rho_prop1 0
  (rho_prop1-2 nil 3318172677 3330685254
   ("" (skosimp)
    (("" (use "pos_times_ge")
      (("" (use "error_constraint") (("" (ground) nil nil)) nil)) nil))
    nil)
   unchecked
   ((pos_times_ge formula-decl nil real_props nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (error_constraint formula-decl nil time_triggered_system2 nil))
   546 260 t nil)
  (rho_prop1-1 nil 3318172632 3318172645
   ("" (skosimp*) (("" (postpone) nil nil)) nil) unfinished nil 12737
   910 t shostak))
 (rho_prop2 0
  (rho_prop2-1 nil 3318172797 3330685255
   ("" (skosimp)
    (("" (use "pos_times_ge")
      (("" (use "error_constraint") (("" (ground) nil nil)) nil)) nil))
    nil)
   unchecked
   ((pos_times_ge formula-decl nil real_props nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (error_constraint formula-decl nil time_triggered_system2 nil))
   621 340 t nil))
 (constraint3_lemma 0
  (constraint3_lemma-1 nil 3318266271 3330685256
   ("" (skosimp)
    (("" (use "constraint3")
      (("" (lemma "both_sides_times_pos_le2")
        (("" (inst - "1+rho" "d!1" "nom_delay + e_u")
          (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   unchecked
   ((constraint3 formula-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 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)
    (> const-decl "bool" reals nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (both_sides_times_pos_le2 formula-decl nil real_props nil))
   1429 1020 t shostak))
 (arrival_prop 2
  (arrival_prop-4 "strictlyless proof" 3330685326 3330685705
   ("" (skosimp)
    (("" (expand "recv_win_open")
      (("" (use "constraint6")
        (("" (use "sendtime_ax")
          (("" (name "tt" "sendtime(q!1, r!1) + d!1")
            ((""
              (lemma "drift_rate" :subst
               ("p" "q!1" "t1" "tt" "t2" "tt-d!1"))
              (("" (lemma "rho_prop1" :subst ("d" "d!1"))
                (("" (lemma "rho_prop2" :subst ("d" "d!1"))
                  (("" (assert)
                    (("" (flatten)
                      (("" (use "constraint2")
                        ((""
                          (lemma "clock_sync" :subst
                           ("p" "p!1" "r" "r!1" "q" "q!1" "t" "tt"))
                          (("" (split)
                            (("1"
                              (lemma "constraint3_lemma" :subst
                               ("d" "d!1" "i" "r!1"))
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "sched_sync")
                                  (("1"
                                    (inst - "p!1" " q!1" " r!1")
                                    (("1"
                                      (split)
                                      (("1"
                                        (hide -2 -5 -6 -7)
                                        (("1"
                                          (name
                                           "t3"
                                           "sendtime(q!1, r!1)")
                                          (("1"
                                            (replace -1 :hide? t)
                                            (("1"
                                              (lemma "monotone_clock")
                                              (("1"
                                                (inst
                                                 -
                                                 "p!1"
                                                 "t3 + nom_delay - e_l"
                                                 "t3 + d!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma
                                                     "clock_sync")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "p!1"
                                                       "q!1"
                                                       "r!1"
                                                       "t3 + nom_delay - e_l")
                                                      (("1"
                                                        (split)
                                                        (("1"
                                                          (case
                                                           "-Sigma(r!1) <= C(p!1, nom_delay - e_l + t3) - C(q!1, nom_delay - e_l + t3)")
                                                          (("1"
                                                            (lemma
                                                             "drift_rate")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "q!1"
                                                               "t3 + nom_delay - e_l"
                                                               "t3")
                                                              (("1"
                                                                (split)
                                                                (("1"
                                                                  (case
                                                                   "floor((1 - rho) * (t3 + nom_delay - e_l - t3)) + C(q!1, t3) <= C(p!1, nom_delay - e_l + t3) + Sigma(r!1)")
                                                                  (("1"
                                                                    (case
                                                                     "sched(r!1)(q!1) + sched_skew(r!1) + D(r!1) + e_l * rho - nom_delay * rho + (nom_delay - e_l) - Sigma(r!1) - sched_skew(r!1) <= C(p!1, d!1 + t3)")
                                                                    (("1"
                                                                      (assert)
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (postpone)
                                                                        nil)))))
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (assert)
                                                                      nil)))))
                                                                 ("2"
                                                                  (use
                                                                   "error_constraint")
                                                                  (("2"
                                                                    (assert)
                                                                    nil)))))))))
                                                           ("2"
                                                            (expand
                                                             "abs")
                                                            (("2"
                                                              (lift-if)
                                                              (("2"
                                                                (assert)
                                                                nil)))))))
                                                         ("2"
                                                          (expand "t3")
                                                          (("2"
                                                            (hide 2)
                                                            (("2"
                                                              (lemma
                                                               "monotone_clock")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "q!1"
                                                                 "sendtime(q!1, r!1)"
                                                                 "sendtime(q!1, r!1) - e_l + nom_delay")
                                                                (("2"
                                                                  (split)
                                                                  (("1"
                                                                    (assert)
                                                                    nil)
                                                                   ("2"
                                                                    (use
                                                                     "error_constraint")
                                                                    (("2"
                                                                      (assert)
                                                                      nil)))))))))))))
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (expand
                                                             "t3")
                                                            (("3"
                                                              (use
                                                               "constraint3_lemma")
                                                              (("3"
                                                                (lemma
                                                                 "sched_sync")
                                                                (("3"
                                                                  (inst?)
                                                                  (("3"
                                                                    (case
                                                                     "C(p!1, sendtime(q!1, r!1) + d!1) <= P(r!1) + max(sched(r!1)(p!1), sched(r!1)(q!1))")
                                                                    (("1"
                                                                      (case
                                                                       "min(C(p!1, sendtime(q!1, r!1) - e_l + nom_delay),
                                        C(q!1, sendtime(q!1, r!1) - e_l + nom_delay)) <= C(p!1, sendtime(q!1, r!1) + d!1)")
                                                                      (("1"
                                                                        (assert)
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (typepred
                                                                           "d!1")
                                                                          (("2"
                                                                            (lemma
                                                                             "monotone_clock")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "sendtime(q!1, r!1) + d!1")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil)))))))))))))
                                                                     ("2"
                                                                      (hide
                                                                       -3
                                                                       -4
                                                                       -10
                                                                       2)
                                                                      (("2"
                                                                        (grind)
                                                                        nil)))))))))))))))))))))))))))))))))
                                       ("2"
                                        (expand "abs")
                                        (("2"
                                          (lift-if)
                                          (("2"
                                            (assert)
                                            nil)))))))))))))))
                             ("2" (hide 2) (("2" (assert) nil)))
                             ("3" (hide 2)
                              (("3"
                                (expand "tt")
                                (("3"
                                  (use "constraint3_lemma")
                                  (("3"
                                    (replace -8)
                                    (("3"
                                      (lemma "sched_sync")
                                      (("3"
                                        (inst - "p!1" "q!1" "r!1")
                                        (("3"
                                          (expand "abs")
                                          (("3"
                                            (assert)
                                            nil))))))))))))))))))))))))))))))))))))))))
    nil)
   unfinished nil 340474 39370 t nil)
  (arrival_prop-3 "strictlyless proof" 3330683779 3330685285
   ("" (skosimp)
    (("" (expand "recv_win_open")
      (("" (use "constraint6")
        (("" (use "sendtime_ax")
          (("" (name "tt" "sendtime(q!1, r!1) + d!1")
            ((""
              (lemma "drift_rate" :subst
               ("p" "q!1" "t1" "tt" "t2" "tt-d!1"))
              (("" (lemma "rho_prop1" :subst ("d" "d!1"))
                (("" (lemma "rho_prop2" :subst ("d" "d!1"))
                  (("" (assert)
                    (("" (flatten)
                      (("" (use "constraint2")
                        ((""
                          (lemma "clock_sync" :subst
                           ("p" "p!1" "r" "r!1" "q" "q!1" "t" "tt"))
                          (("" (split)
                            (("1"
                              (lemma "constraint3_lemma" :subst
                               ("d" "d!1" "i" "r!1"))
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "sched_sync")
                                  (("1"
                                    (inst - "p!1" " q!1" " r!1")
                                    (("1"
                                      (split)
                                      (("1"
                                        (hide -2 -5 -6 -7)
                                        (("1"
                                          (name
                                           "t3"
                                           "sendtime(q!1, r!1)")
                                          (("1"
                                            (replace -1 :hide? t)
                                            (("1"
                                              (lemma "monotone_clock")
                                              (("1"
                                                (inst
                                                 -
                                                 "p!1"
                                                 "t3 + nom_delay - e_l"
                                                 "t3 + d!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma
                                                     "clock_sync")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "p!1"
                                                       "q!1"
                                                       "r!1"
                                                       "t3 + nom_delay - e_l")
                                                      (("1"
                                                        (split)
                                                        (("1"
                                                          (case
                                                           "-Sigma(r!1) <=
                                                                                                                                                                                                                                                                        C(p!1, nom_delay - e_l + t3) - C(q!1, nom_delay - e_l + t3)")
                                                          (("1"
                                                            (lemma
                                                             "drift_rate")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "q!1"
                                                               "t3 + nom_delay - e_l"
                                                               "t3")
                                                              (("1"
                                                                (split)
                                                                (("1"
                                                                  (case
                                                                   "floor((1 - rho) * (t3 + nom_delay - e_l - t3)) + C(q!1, t3) <= C(p!1, nom_delay - e_l + t3) + Sigma(r!1)")
                                                                  (("1"
                                                                    (case
                                                                     "sched(r!1)(q!1) + sched_skew(r!1) + D(r!1) +
                                                 e_l * rho - nom_delay * rho + (nom_delay - e_l)
                                                 - Sigma(r!1)
                                                 - sched_skew(r!1)
                                                 <= C(p!1, d!1 + t3)")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (postpone)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (use
                                                                   "error_constraint")
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "abs")
                                                            (("2"
                                                              (lift-if)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand "t3")
                                                          (("2"
                                                            (hide 2)
                                                            (("2"
                                                              (lemma
                                                               "monotone_clock")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "q!1"
                                                                 "sendtime(q!1, r!1)"
                                                                 "sendtime(q!1, r!1) - e_l + nom_delay")
                                                                (("2"
                                                                  (split)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (use
                                                                     "error_constraint")
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (expand
                                                             "t3")
                                                            (("3"
                                                              (use
                                                               "constraint3_lemma")
                                                              (("3"
                                                                (lemma
                                                                 "sched_sync")
                                                                (("3"
                                                                  (inst?)
                                                                  (("3"
                                                                    (case
                                                                     "C(p!1, sendtime(q!1, r!1) + d!1) <= P(r!1) + max(sched(r!1)(p!1), sched(r!1)(q!1))")
                                                                    (("1"
                                                                      (case
                                                                       "min(C(p!1, sendtime(q!1, r!1) - e_l + nom_delay),
                         C(q!1, sendtime(q!1, r!1) - e_l + nom_delay)) <= C(p!1, sendtime(q!1, r!1) + d!1)")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (typepred
                                                                           "d!1")
                                                                          (("2"
                                                                            (lemma
                                                                             "monotone_clock")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "sendtime(q!1, r!1) + d!1")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -3
                                                                       -4
                                                                       -10
                                                                       2)
                                                                      (("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "abs")
                                        (("2"
                                          (lift-if)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2) (("2" (assert) nil nil))
                              nil)
                             ("3" (hide 2)
                              (("3"
                                (expand "tt")
                                (("3"
                                  (use "constraint3_lemma")
                                  (("3"
                                    (replace -8)
                                    (("3"
                                      (lemma "sched_sync")
                                      (("3"
                                        (inst - "p!1" "q!1" "r!1")
                                        (("3"
                                          (expand "abs")
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil 28647 24710 t shostak)
  (arrival_prop-2 nil 3330255354 3330686190
   ("" (skosimp)
    (("" (expand "recv_win_open")
      (("" (use "constraint6")
        (("" (use "sendtime_ax")
          (("" (name "tt" "sendtime(q!1, r!1) + d!1")
            ((""
              (lemma "drift_rate" :subst
               ("p" "q!1" "t1" "tt" "t2" "tt-d!1"))
              (("" (lemma "rho_prop1" :subst ("d" "d!1"))
                (("" (lemma "rho_prop2" :subst ("d" "d!1"))
                  (("" (assert)
                    (("" (flatten)
                      (("" (use "constraint2")
                        ((""
                          (lemma "clock_sync" :subst
                           ("p" "p!1" "r" "r!1" "q" "q!1" "t" "tt"))
                          (("" (split)
                            (("1"
                              (lemma "constraint3_lemma" :subst
                               ("d" "d!1" "i" "r!1"))
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "sched_sync")
                                  (("1"
                                    (inst - "p!1" " q!1" " r!1")
                                    (("1"
                                      (split)
                                      (("1"
                                        (hide -2 -5 -6 -7)
                                        (("1"
                                          (name
                                           "t3"
                                           "sendtime(q!1, r!1)")
                                          (("1"
                                            (replace -1 :hide? t)
                                            (("1"
                                              (lemma "monotone_clock")
                                              (("1"
                                                (inst
                                                 -
                                                 "p!1"
                                                 "t3 + nom_delay - e_l"
                                                 "t3 + d!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma
                                                     "clock_sync")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "p!1"
                                                       "q!1"
                                                       "r!1"
                                                       "t3 + nom_delay - e_l")
                                                      (("1"
                                                        (split)
                                                        (("1"
                                                          (case
                                                           "-Sigma(r!1) <=
                                                                                                                                                                                                                                                                        C(p!1, nom_delay - e_l + t3) - C(q!1, nom_delay - e_l + t3)")
                                                          (("1"
                                                            (lemma
                                                             "drift_rate")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "q!1"
                                                               "t3 + nom_delay - e_l"
                                                               "t3")
                                                              (("1"
                                                                (split)
                                                                (("1"
                                                                  (case
                                                                   "floor((1 - rho) * (t3 + nom_delay - e_l - t3)) + C(q!1, t3) <= C(p!1, nom_delay - e_l + t3) + Sigma(r!1)")
                                                                  (("1"
                                                                    (case
                                                                     "sched(r!1)(q!1) + sched_skew(r!1) + D(r!1) +
                              floor(e_l * rho - nom_delay * rho + (nom_delay - e_l))
                              - Sigma(r!1)
                              - sched_skew(r!1)
                              <= C(p!1, d!1 + t3)")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (use
                                                                   "error_constraint")
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "abs")
                                                            (("2"
                                                              (lift-if)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand "t3")
                                                          (("2"
                                                            (hide 2)
                                                            (("2"
                                                              (lemma
                                                               "monotone_clock")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "q!1"
                                                                 "sendtime(q!1, r!1)"
                                                                 "sendtime(q!1, r!1) - e_l + nom_delay")
                                                                (("2"
                                                                  (split)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (use
                                                                     "error_constraint")
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (expand
                                                             "t3")
                                                            (("3"
                                                              (use
                                                               "constraint3_lemma")
                                                              (("3"
                                                                (lemma
                                                                 "sched_sync")
                                                                (("3"
                                                                  (inst?)
                                                                  (("3"
                                                                    (case
                                                                     "C(p!1, sendtime(q!1, r!1) + d!1) <= P(r!1) + max(sched(r!1)(p!1), sched(r!1)(q!1))")
                                                                    (("1"
                                                                      (case
                                                                       "min(C(p!1, sendtime(q!1, r!1) - e_l + nom_delay),
                         C(q!1, sendtime(q!1, r!1) - e_l + nom_delay)) <= C(p!1, sendtime(q!1, r!1) + d!1)")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (typepred
                                                                           "d!1")
                                                                          (("2"
                                                                            (lemma
                                                                             "monotone_clock")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "sendtime(q!1, r!1) + d!1")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -3
                                                                       -4
                                                                       -10
                                                                       2)
                                                                      (("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "abs")
                                        (("2"
                                          (lift-if)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2) (("2" (assert) nil nil))
                              nil)
                             ("3" (hide 2)
                              (("3"
                                (expand "tt")
                                (("3"
                                  (use "constraint3_lemma")
                                  (("3"
                                    (replace -8)
                                    (("3"
                                      (lemma "sched_sync")
                                      (("3"
                                        (inst - "p!1" "q!1" "r!1")
                                        (("3"
                                          (expand "abs")
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished
   ((constraint6 formula-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 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)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (< const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sendtime const-decl "realtime" time_triggered_system2 nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (rho_prop1 formula-decl nil time_triggered_system2 nil)
    (constraint2 formula-decl nil time_triggered_system2 nil)
    (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (sched_skew const-decl "{t: clocktime | t >= 0}"
     time_triggered_system2 nil)
    (D const-decl "clocktime" time_triggered_system2 nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (integer nonempty-type-from-decl nil integers nil)
    (error_constraint formula-decl nil time_triggered_system2 nil)
    (C const-decl "clocktime" time_triggered_system2 nil)
    (Sigma const-decl "{t: clocktime | t >= 0}" time_triggered_system2
     nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (> const-decl "bool" reals nil)
    (P const-decl "{t: clocktime | t > 0}" time_triggered_system2 nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (monotone_clock formula-decl nil time_triggered_system2 nil)
    (sched_sync formula-decl nil time_triggered_system2 nil)
    (constraint3_lemma formula-decl nil time_triggered_system2 nil)
    (clock_sync formula-decl nil time_triggered_system2 nil)
    (rho_prop2 formula-decl nil time_triggered_system2 nil)
    (drift_rate formula-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (sendtime_ax formula-decl nil time_triggered_system2 nil)
    (recv_win_open const-decl "bool" time_triggered_system2 nil))
   59550 26650 t nil)
  (arrival_prop-1 nil 3330170478 3330686677
   ("" (skosimp)
    (("" (expand "recv_win_open")
      (("" (use "constraint6")
        (("" (use "sendtime_ax")
          (("" (name "tt" "sendtime(q!1, r!1) + d!1")
            ((""
              (lemma "drift_rate" :subst
               ("p" "q!1" "t1" "tt" "t2" "tt-d!1"))
              (("" (lemma "rho_prop1" :subst ("d" "d!1"))
                (("" (lemma "rho_prop2" :subst ("d" "d!1"))
                  (("" (assert)
                    (("" (flatten)
                      (("" (use "constraint2")
                        ((""
                          (lemma "clock_sync" :subst
                           ("p" "p!1" "r" "r!1" "q" "q!1" "t" "tt"))
                          (("" (split)
                            (("1"
                              (lemma "constraint3_lemma" :subst
                               ("d" "d!1" "i" "r!1"))
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "sched_sync")
                                  (("1"
                                    (inst - "p!1" " q!1" " r!1")
                                    (("1"
                                      (split)
                                      (("1"
                                        (hide -2 -5 -6 -7)
                                        (("1"
                                          (name
                                           "t3"
                                           "sendtime(q!1, r!1)")
                                          (("1"
                                            (replace -1 :hide? t)
                                            (("1"
                                              (lemma "monotone_clock")
                                              (("1"
                                                (inst
                                                 -
                                                 "p!1"
                                                 "t3 + nom_delay - e_l"
                                                 "t3 + d!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma
                                                     "clock_sync")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "p!1"
                                                       "q!1"
                                                       "r!1"
                                                       "t3 + nom_delay - e_l")
                                                      (("1"
                                                        (split)
                                                        (("1"
                                                          (expand
                                                           "abs")
                                                          (("1"
                                                            (lift-if)
                                                            (("1"
                                                              (case
                                                               "-Sigma(r!1) <
                                                                                                                                                                                                                                 C(p!1, nom_delay - e_l + t3) - C(q!1, nom_delay - e_l + t3)")
                                                              (("1"
                                                                (lemma
                                                                 "drift_rate")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "q!1"
                                                                   "t3 + nom_delay - e_l"
                                                                   "t3")
                                                                  (("1"
                                                                    (split)
                                                                    (("1"
                                                                      (case
                                                                       "floor((1 - rho) * (t3 + nom_delay - e_l - t3)) + C(q!1, t3) <= C(p!1, nom_delay - e_l + t3) + Sigma(r!1)")
                                                                      (("1"
                                                                        (grind-reals)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (use
                                                                       "error_constraint")
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand "t3")
                                                          (("2"
                                                            (hide 2)
                                                            (("2"
                                                              (lemma
                                                               "monotone_clock")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "q!1"
                                                                 "sendtime(q!1, r!1)"
                                                                 "sendtime(q!1, r!1) - e_l + nom_delay")
                                                                (("2"
                                                                  (split)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (use
                                                                     "error_constraint")
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (expand
                                                             "t3")
                                                            (("3"
                                                              (use
                                                               "constraint3_lemma")
                                                              (("3"
                                                                (lemma
                                                                 "sched_sync")
                                                                (("3"
                                                                  (postpone)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "abs")
                                        (("2" (grind-reals) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2) (("2" (assert) nil nil))
                              nil)
                             ("3" (hide 2)
                              (("3"
                                (expand "tt")
                                (("3"
                                  (use "constraint3_lemma")
                                  (("3"
                                    (replace -8)
                                    (("3"
                                      (lemma "sched_sync")
                                      (("3"
                                        (inst - "p!1" "q!1" "r!1")
                                        (("3"
                                          (expand "abs")
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil 407550 115980 t nil))
 (recv_prop 0
  (recv_prop-1 nil 3318267014 3330685285
   ("" (skosimp)
    (("" (lemma "comm_phase1")
      (("" (inst - _ "q!1" "r!1" "p!1")
        (("1" (inst - "epsilon! (g:global_init): true")
          (("1" (assert)
            (("1" (lemma "sendtime_ax")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (lemma "channels_match" ("p" "p!1" "q" "q!1"))
                    (("1" (assert)
                      (("1" (lemma "max_delay")
                        (("1" (inst?)
                          (("1" (flatten)
                            (("1" (assert)
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst?)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (lemma "arrival_prop")
                                      (("1" (inst?) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (use "channels_match" ("p" "p!1" "q" "q!1"))
            (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((comm_phase1 formula-decl nil time_triggered_system2 nil)
    (TRUE const-decl "bool" booleans nil)
    (epsilon const-decl "T" epsilons nil)
    (global_init type-eq-decl nil time_triggered_system2 nil)
    (init_state const-decl "nonempty_pred[state]"
     time_triggered_system2 nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (pred type-eq-decl nil defined_types nil)
    (global_state type-eq-decl nil time_triggered_system2 nil)
    (state nonempty-type-decl nil time_triggered_system2 nil)
    (sendtime_ax formula-decl nil time_triggered_system2 nil)
    (mess nonempty-type-decl nil time_triggered_system2 nil)
    (msg const-decl "[state, (out_nbrs(p)) -> mess]"
     time_triggered_system2 nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil)
    (ttss const-decl "state" time_triggered_system2 nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (D const-decl "clocktime" time_triggered_system2 nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (sendtime const-decl "realtime" time_triggered_system2 nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (arrival_prop formula-decl nil time_triggered_system2 nil)
    (max_delay formula-decl nil time_triggered_system2 nil)
    (channels_match formula-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (out_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (in_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil))
   499 400 t nil))
 (send_state_TCC1 0
  (send_state_TCC1-1 nil 3320664379 3330685286
   ("" (skosimp*)
    (("" (use "independent") (("" (prop) (("" (assert) nil nil)) nil))
      nil))
    nil)
   unchecked
   ((independent formula-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (global_init type-eq-decl nil time_triggered_system2 nil)
    (init_state const-decl "nonempty_pred[state]"
     time_triggered_system2 nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (state nonempty-type-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   275 240 t shostak))
 (send_state 0
  (send_state-1 nil 3320664498 3330685288
   ("" (skosimp*)
    (("" (use "independent")
      (("" (flatten)
        (("" (hide -1)
          (("" (case "D(r!1) >= 0")
            (("1" (inst-cp - "r!1")
              (("1" (assert)
                (("1" (lemma "ttss_comm")
                  (("1" (inst - "D(r!1) + sched(r!1)(p!1)" _ _ _)
                    (("1" (inst?)
                      (("1" (split)
                        (("1" (assert) nil nil)
                         ("2" (hide 2) (("2" (assert) nil nil)) nil)
                         ("3" (hide 2)
                          (("3" (use "constraint3")
                            (("3"
                              (case "Sigma(r!1) + (1 + rho) * (nom_delay + e_u) >= 0")
                              (("1" (assert) nil nil)
                               ("2"
                                (use "rho_prop2")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (use "error_constraint")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst-cp - "r!1")
              (("2" (assert)
                (("2" (split)
                  (("1" (flatten)
                    (("1" (lemma "ttss_comp")
                      (("1" (inst?)
                        (("1" (inst - "r!1 -1")
                          (("1" (inst - "r!1 - 1")
                            (("1" (assert)
                              (("1"
                                (split)
                                (("1" (assert) nil nil)
                                 ("2"
                                  (use "constraint5")
                                  (("2"
                                    (expand "dur")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil)
                           ("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (inst?)
                      (("2" (use "constraint4")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((independent formula-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (global_init type-eq-decl nil time_triggered_system2 nil)
    (init_state const-decl "nonempty_pred[state]"
     time_triggered_system2 nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (state nonempty-type-decl nil time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (ttss_comp formula-decl nil time_triggered_system2 nil)
    (constraint5 formula-decl nil time_triggered_system2 nil)
    (dur const-decl "clocktime" time_triggered_system2 nil)
    (constraint4 formula-decl nil time_triggered_system2 nil)
    (ttss_comm formula-decl nil time_triggered_system2 nil)
    (Sigma const-decl "{t: clocktime | t >= 0}" time_triggered_system2
     nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (error_constraint formula-decl nil time_triggered_system2 nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (rho_prop2 formula-decl nil time_triggered_system2 nil)
    (constraint3 formula-decl nil time_triggered_system2 nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (D const-decl "clocktime" time_triggered_system2 nil)
    (clocktime type-eq-decl nil time_triggered_system2 nil))
   2024 1720 t shostak))
 (ttin_prop_TCC1 0
  (ttin_prop_TCC1-1 nil 3318164256 3330685288
   ("" (skosimp*)
    (("" (use "channels_match") (("" (assert) nil nil)) nil)) nil)
   unchecked
   ((channels_match formula-decl nil time_triggered_system2 nil)
    (in_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil))
   28 20 t shostak))
 (ttin_prop 0
  (ttin_prop-2 nil 3328352709 3330685294
   ("" (skosimp*)
    (("" (use "ttin_ax")
      (("" (use "constraint1")
        (("" (ground)
          (("1" (inst?)
            (("1" (replace -1 :hide? t)
              (("1" (use "epsilon_ax[mess]")
                (("1" (ground)
                  (("1" (skosimp)
                    (("1" (use "max_delay")
                      (("1" (flatten)
                        (("1" (hide -1)
                          (("1" (assert)
                            (("1" (skosimp)
                              (("1"
                                (use "comm_phase2")
                                (("1"
                                  (split)
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (replace -1)
                                      (("1"
                                        (case-replace "r!1=r!2")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (use "constraint4")
                                            (("1"
                                              (split)
                                              (("1"
                                                (use "ttss_comm")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (use "constraint3")
                                                    (("1"
                                                      (lemma
                                                       "rho_prop2")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "(nom_delay + e_u)")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (lemma "independent")
                                                (("2"
                                                  (inst
                                                   -
                                                   _
                                                   "q!1"
                                                   "r!2")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (prop)
                                                        (("2"
                                                          (inst
                                                           -
                                                           "p!1")
                                                          (("1"
                                                            (use
                                                             "send_state")
                                                            (("1"
                                                              (inst?)
                                                              (("1"
                                                                (split)
                                                                (("1"
                                                                  (ground)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (assert)
                                                                  nil
                                                                  nil)
                                                                 ("3"
                                                                  (skosimp*)
                                                                  (("3"
                                                                    (hide
                                                                     2
                                                                     3)
                                                                    (("3"
                                                                      (reveal
                                                                       -1)
                                                                      (("3"
                                                                        (inst
                                                                         -
                                                                         "j!1")
                                                                        (("3"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (use
                                                             "channels_match")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide -2 -3 -5 -6 -7 -8 -9 2)
                                          (("2"
                                            (lemma "arrival_prop")
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (inst -1 "d!1" "p!1")
                                                (("2"
                                                  (replace

                                                   -2
                                                   :hide?

                                                   t
                                                   :dir
                                                   rl)
                                                  (("2"
                                                    (expand
                                                     "recv_win_open")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (case
                                                         "r!1<r!2")
                                                        (("1"
                                                          (case
                                                           "D(r!2) + floor(e_l * rho - nom_delay * rho + (nom_delay - e_l)) +
                                         sched(r!2)(p!1)
                                         - Sigma(r!2) >= sched(r!2)(p!1)")
                                                          (("1"
                                                            (lemma
                                                             "comp_phase")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "r!1"
                                                               "r!2"
                                                               "p!1")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (use
                                                             "constraint2")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (case
                                                           "D(r!1) + floor(e_l * rho - nom_delay * rho + (nom_delay - e_l)) +
                                         sched(r!1)(p!1)
                                         - Sigma(r!1) >= sched(r!1)(p!1)")
                                                          (("1"
                                                            (lemma
                                                             "comp_phase")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "r!2"
                                                               "r!1"
                                                               "p!1")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (use
                                                             "constraint2")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (use "recv_prop")
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (use "channels_match")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (use "channels_match")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (use "channels_match")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (use "recv_prop")
                      (("2" (assert)
                        (("2" (skosimp)
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (lemma "comp_phase")
            (("2" (inst - "r!1" "r!1+1" "p!1") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((ttin_ax formula-decl nil time_triggered_system2 nil)
    (P const-decl "{t: clocktime | t > 0}" time_triggered_system2 nil)
    (> const-decl "bool" reals nil)
    (sched const-decl "clocktime" time_triggered_system2 nil)
    (proc nonempty-type-decl nil time_triggered_system2 nil)
    (round type-eq-decl nil time_triggered_system2 nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (clocktime type-eq-decl nil time_triggered_system2 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)
    (max_delay formula-decl nil time_triggered_system2 nil)
    (out_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (epsilon const-decl "T" epsilons nil)
    (integer nonempty-type-from-decl nil integers nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rho const-decl "{x: real | 0 <= x AND x < 1}"
     time_triggered_system2 nil)
    (Sigma const-decl "{t: clocktime | t >= 0}" time_triggered_system2
     nil)
    (comp_phase formula-decl nil time_triggered_system2 nil)
    (constraint2 formula-decl nil time_triggered_system2 nil)
    (arrival_prop formula-decl nil time_triggered_system2 nil)
    (rho_prop2 formula-decl nil time_triggered_system2 nil)
    (constraint3 formula-decl nil time_triggered_system2 nil)
    (D const-decl "clocktime" time_triggered_system2 nil)
    (ttss_comm formula-decl nil time_triggered_system2 nil)
    (send_state formula-decl nil time_triggered_system2 nil)
    (independent formula-decl nil time_triggered_system2 nil)
    (constraint4 formula-decl nil time_triggered_system2 nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (global_init type-eq-decl nil time_triggered_system2 nil)
    (init_state const-decl "nonempty_pred[state]"
     time_triggered_system2 nil)
    (nonempty_pred type-eq-decl nil orders nil)
    (global_state type-eq-decl nil time_triggered_system2 nil)
    (state nonempty-type-decl nil time_triggered_system2 nil)
    (delay type-eq-decl nil time_triggered_system2 nil)
    (e_u const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (e_l const-decl "{x: realtime | 0 < x}" time_triggered_system2 nil)
    (nom_delay const-decl "{x: realtime | 0 < x}"
     time_triggered_system2 nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (comm_phase2 formula-decl nil time_triggered_system2 nil)
    (recv_prop formula-decl nil time_triggered_system2 nil)
    (recv const-decl "bool" time_triggered_system2 nil)
    (recv_win_open const-decl "bool" time_triggered_system2 nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (realtime type-eq-decl nil time_triggered_system2 nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (mess nonempty-type-decl nil time_triggered_system2 nil)
    (setof type-eq-decl nil defined_types nil)
    (in_nbrs const-decl "[proc -> setof[proc]]" time_triggered_system2
     nil)
    (constraint1 formula-decl nil time_triggered_system2 nil))
   6242 3810 t nil)
  (ttin_prop-1 nil 3318267064 3328352565
   ("" (skosimp*)
    (("" (use "ttin_ax")
      (("" (use "constraint1")
        (("" (ground)
          (("1" (inst?)
            (("1" (replace -1 :hide? t)
              (("1" (use "epsilon_ax[mess]")
                (("1" (ground)
                  (("1" (skosimp)
                    (("1" (use "max_delay")
                      (("1" (flatten)
                        (("1" (hide -1)
                          (("1" (assert)
                            (("1" (skosimp)
                              (("1"
                                (use "comm_phase2")
                                (("1"
                                  (split)
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (replace -1)
                                      (("1"
                                        (case-replace "r!1=r!2")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (use "constraint4")
                                            (("1"
                                              (split)
                                              (("1"
                                                (use "ttss_comm")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (use "constraint3")
                                                    (("1"
                                                      (lemma
                                                       "rho_prop2")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "(nom_delay + e_u)")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))