%Patch files loaded: patch2 version 1.2.2.36

$$$a2.pvs
equivker[V, W: TYPE]: THEORY
 BEGIN
  x, y: VAR V
  f: VAR [V -> W]

 ker(f): (equivalence?[V]) = (LAMBDA x, y: f(x) = f(y))
 END equivker

EquivPO [V:TYPE]:THEORY
  BEGIN
  E1,E2:VAR (equivalence?[V])
  x,y:VAR V
  <=(E1,E2):bool = (forall x,y:E1(x,y) IMPLIES E2(x,y))
  END EquivPO

function_Image   [ D, R :TYPE ]
		: THEORY

  BEGIN

  f:VAR [D -> R]
  Image(f):set[R]= {y: R | (EXISTS (x:D): y = f(x))}
  
  END function_Image


universal_algebra  [ V1,V2,V3:TYPE+ ]
		: THEORY

  BEGIN

  IMPORTING equivker,EquivPO,function_Image
  
  f:VAR [V1->V3]
  g:VAR [V1->V2]
  h:VAR [V2->V3]

  hExists: CLAIM (EXISTS h: h o g = f) IFF ker(g)<=ker(f)
  gExists: CLAIM (EXISTS g: h o g = f) IFF subset?(Image(f),Image(h))
  

END universal_algebra



block_comp  [M,C,Mp,Cp:TYPE+  ]
		: THEORY

  BEGIN

  IMPORTING  universal_algebra
  
  REQ:VAR [M->C]
  SOF_REQ:VAR [Mp->Cp]
  AbstM:VAR [M->Mp]
  AbstC:VAR [C->Cp]
  AbstCp:VAR [Cp->C]


% Question 1(a) - Complete the following theorem statement and prove it.
% uncomment and fill in the necessary and sufficent conditions

  exists_SOF_REQ: THEOREM 
(EXISTS SOF_REQ: SOF_REQ o AbstM=AbstC o REQ) 
%IFF ???????????




% Question 1(b) Add necessary definitions and prove result required from
% the assignment 
% NOTE:  Both "IN" and "O" are PVS keywords so you must use other names for 
% these such as "IN1" and "O1".


% existsSOF: THEOREM
% 	Your theorem goes here!!!

  END block_comp


sentrip:THEORY
BEGIN
  k_PressSP: int = 2450; k_deadBand: int = 50
  KDB:int = k_deadBand;  KHPSP:int = k_PressSP

  Trip:TYPE = {Tripped, NotTripped}

  f_PressTrip(Pressure:real,f_PressTripS1:Trip):Trip = TABLE
  | Pressure<=k_PressSP-k_deadBand                       | NotTripped  ||
  | k_PressSP-k_deadBand<Pressure&Pressure<k_PressSP   |f_PressTripS1||
  | Pressure>=k_PressSP                                 |Tripped      ||
  ENDTABLE

  AItype:TYPE = real

  PTRIP(PRES:AItype,PREV:bool):bool = TABLE
  |[PRES<=KHPSP-KDB|KHPSP-KDB<PRES & PRES<KHPSP|PRES>=KHPSP]|
  | FALSE           | PREV                       | TRUE     ||
  ENDTABLE

% Abstraction Functions
  Trip2bool(TripVal:Trip):bool = TABLE
  |[TripVal=Tripped|TripVal=NotTripped]|
  |  TRUE          |  FALSE           ||
  ENDTABLE

  bool2Trip(x:bool):Trip = TABLE
  |[ x=TRUE		| x=FALSE	]|
  |  Tripped		| NotTripped 	||
  ENDTABLE

  real2AItype(x:real):AItype = floor(x)


  % You cannot prove this theorem with the above definitions
  Sentrip1:THEOREM
  (FORALL (Pressure:real,f_PressTripS1:Trip):
  f_PressTrip(Pressure,f_PressTripS1) = 
	bool2Trip(PTRIP(real2AItype(Pressure),Trip2bool(f_PressTripS1))))

  % Question 1(c)
  % State and prove a theorem here that says that there does not exists a 
  % function to implement the requirements as defined above.

  % Q1c:THEOREM

END sentrip


modular_SenLock [K:posreal]
		: THEORY

  BEGIN

  IMPORTING TimerGeneral[K]

  t:VAR clock

  ldelay:VAR posreal
  sensor,reset:VAR PRED[clock]

% SRS (Requirements) - fixed  version of Sensor lock  function

 SenLock(sensor,reset,ldelay)(t): RECURSIVE bool = COND
    init(t) -> true,
    NOT init(t) AND Held_For(sensor,ldelay)(t) -> true,
    NOT init(t) AND NOT Held_For(sensor,ldelay)(t) 
      AND reset(t) AND sensor(t)->SenLock(sensor,reset,ldelay)(pre(t)),
    NOT init(t) AND NOT Held_For(sensor,ldelay)(t) 
      AND reset(t) AND NOT sensor(t)-> false,
    NOT init(t) AND NOT Held_For(sensor,ldelay)(t) AND 
      NOT reset(t) ->SenLock(sensor,reset,ldelay)(pre(t))
    ENDCOND
    MEASURE rank(t)



  Lock_State: TYPE = {Good, Bad, lock}  
  SDD_State: TYPE = [#  Elock: Lock_State, lLockDly: clock #]

  %Question 2(a)
  %Fill in your definitions below for a version of ELOCK that makes use
  % of the TimerUpdate function to update lLockDly


  ELOCK(sensor,reset,ldelay)(t): % RECURSIVE 
SDD_State 
%
%= 
%
%  COND
%
%	Your COND or TABLE goes here!
%
%  ENDCOND
%  MEASURE rank(t)


% Question 2(b) Prove the theorem below theorem below.
% Put any additional lemmas you need here to prove the main result.





% Main theorem

  SensorLock_Block: THEOREM
  SenLock(sensor,reset,ldelay)(t) = 
	lock?(Elock(ELOCK(sensor,reset,ldelay)(t)))



% Are we having fun yet?

  END modular_SenLock



$$$a2.prf
(|equivker| (|ker_TCC1| "" (SUBTYPE-TCC) NIL NIL))
(|EquivPO|)
(|function_Image|)
(|universal_algebra|
 (|hExists| "" (SKOLEM!)
  (("" (BDDSIMP)
    (("1" (AUTO-REWRITE-DEFS :ALWAYS? T)
      (("1" (ASSERT)
        (("1" (SKOLEM!)
          (("1" (SKOLEM!)
            (("1" (DECOMPOSE-EQUALITY)
              (("1" (INST-CP - "x!1")
                (("1" (INST - "y!1") (("1" (GRIND) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (EXPAND* "ker" "<=")
      (("2" (INST + "lambda (v2:V2):f!1(epsilon! (v1:V1):g!1(v1)=v2)")
        (("2" (GRIND)
          (("2" (APPLY-EXTENSIONALITY :HIDE? T)
            (("2" (INST?)
              (("2" (SPLIT)
                (("1" (PROPAX) NIL NIL)
                 ("2" (LEMMA "epsilon_ax[V1]")
                  (("2" (INST?)
                    (("2" (SPLIT)
                      (("1" (BETA) (("1" (PROPAX) NIL NIL)) NIL)
                       ("2" (INST + "x!1")
                        (("2" (BETA) (("2" (PROPAX) NIL NIL)) NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|gExists| "" (SKOLEM!)
  (("" (BDDSIMP)
    (("1" (SKOLEM!)
      (("1" (AUTO-REWRITE-DEFS :ALWAYS? T)
        (("1" (ASSERT)
          (("1" (EXPAND "o")
            (("1" (DECOMPOSE-EQUALITY)
              (("1" (SKOLEM!)
                (("1" (FLATTEN)
                  (("1" (SKOLEM!)
                    (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (AUTO-REWRITE-DEFS :ALWAYS? T)
      (("2" (ASSERT)
        (("2" (INST + "lambda (v1:V1):(epsilon!(v2:V2):h!1(v2)=f!1(v1))")
          (("2" (ASSERT)
            (("2" (APPLY-EXTENSIONALITY :HIDE? T)
              (("2" (INST?)
                (("2" (SPLIT)
                  (("1" (SKOLEM!)
                    (("1" (LEMMA "epsilon_ax[V2]")
                      (("1" (INST?)
                        (("1" (SPLIT)
                          (("1" (BETA) (("1" (PROPAX) NIL NIL)) NIL)
                           ("2" (INST?)
                            (("2" (BETA) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (INST?) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|block_comp| (|exists_SOF_REQ| "" (POSTPONE) NIL NIL))
(|sentrip| (|f_PressTrip_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|f_PressTrip_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (PTRIP_TCC1 "" (COND-DISJOINT-TCC) NIL NIL)
 (PTRIP_TCC2 "" (COND-COVERAGE-TCC) NIL NIL)
 (|Trip2bool_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|Trip2bool_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|bool2Trip_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|bool2Trip_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|Sentrip1| "" (GRIND) NIL NIL))
(|modular_SenLock| (|SenLock_TCC1| "" (TERMINATION-TCC) NIL NIL)
 (|SenLock_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|SenLock_TCC3| "" (COND-DISJOINT-TCC) NIL NIL)
 (|SenLock_TCC4| "" (COND-COVERAGE-TCC) NIL NIL))


$$$Clocks.pvs
Clocks[ K: posreal ]: THEORY

BEGIN

non_neg: TYPE = { x: real | x>=0 } CONTAINING 0

time: TYPE = non_neg

t: VAR time
n: VAR nat

clock: TYPE = { t: time | EXISTS(n: nat): t=n*K } CONTAINING 0

x: VAR clock

init(x): bool = (x=0)

noninit_elem: TYPE ={ x | not init(x) }

y: VAR noninit_elem

pre(y): clock = y - K

next(x): noninit_elem = x + K

rank(x): nat = x/K

  %------------------
  %  induction rules
  %------------------

clock_induct : LEMMA
        FORALL (P : pred[clock]) : 
            (FORALL x, n : rank(x) = n implies P(x))
        implies
            (FORALL x : P(x))

% The general clock induction proposition

clock_induction: PROPOSITION
  FORALL (P: pred[clock]):
    (FORALL (t: clock): init(t)
      IMPLIES P(t)) AND
    (FORALL (t: noninit_elem): P(pre(t))
      IMPLIES P(t))
      IMPLIES (FORALL (t: clock): P(t))


clock_strong_induction: PROPOSITION
  FORALL (P: pred[clock]):
    (FORALL (x:clock): 
    (FORALL (z:clock): z < x IMPLIES P(z)) IMPLIES P(x))
      IMPLIES (FORALL (t: clock): P(t))

END Clocks






$$$Clocks.prf
(|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|pre_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SKOLEM-TYPEPRED)
    (("" (SPLIT)
      (("1" (GRIND)
        (("1" (DELETE -3)
          (("1" (CASE "n!1>0")
            (("1" (ASSERT)
              (("1" (LEMMA "both_sides_times_pos_ge1")
                (("1" (INST -1 "K" "n!1-1" "0")
                  (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (INST 1 "n!1-1")
        (("1" (ASSERT) NIL NIL)
         ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|next_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SPLIT)
    (("1" (SKOLEM-TYPEPRED)
      (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL)
     ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|rank_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SKOLEM-TYPEPRED)
    (("" (REPLACE -3 *)
      (("" (LEMMA "times_div2")
        (("" (INST - "K" "n!1" "K")
          (("" (REPLACE - + RL)
            (("" (LEMMA "div_cancel2")
              (("" (INST?) (("" (REPLACE - +) (("" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|clock_induct| "" (SKOSIMP)
  (("" (SKOLEM!)
    (("" (INST -1 "x!1" "rank(x!1)")
      (("" (BDDSIMP) (("" (PROPAX) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|clock_induction| "" (SKOSIMP)
  (("" (LEMMA "clock_induct" ("P" "P!1"))
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (DELETE 2)
        (("2" (INDUCT "n")
          (("1" (SKOSIMP)
            (("1" (INST -2 "x!1")
              (("1" (GRIND)
                (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K"))
                  (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP*)
            (("2" (ASSERT)
              (("2" (GROUND)
                (("2" (INST -1 "pre(x!1)")
                  (("1" (INST -4 "x!1")
                    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
                   ("2" (GRIND) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|clock_strong_induction| "" (LEMMA "clock_induction")
  (("" (SKOSIMP*)
    ((""
      (INST -1
       "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))")
      (("" (BETA)
        (("" (SPLIT)
          (("1" (INST -1 "t!1")
            (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (SKOSIMP*)
            (("2" (INST -3 0) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL))
              NIL))
            NIL)
           ("3" (SKOSIMP*)
            (("3" (INST -3 "m!1")
              (("3" (ASSERT)
                (("3" (SKOSIMP)
                  (("3" (INST -1 "z!1")
                    (("3" (BDDSIMP)
                      (("3" (HIDE 2 3 4)
                        (("3" (TYPEPRED "m!1" "z!1" "t!2" "K")
                          (("3" (GRIND)
                            (("3" (HIDE -10 -5 -7 -9)
                              (("3" (HIDE -4 -5 -6)
                                (("3" (BOTH-SIDES "/" "K" -5)
                                  (("3" (BOTH-SIDES "/" "K" -6)
                                    (("3" (BOTH-SIDES "/" "K" 2)
                                      (("3" (GRIND) NIL NIL)) NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$Held_For.pvs
Held_For_Rec  [K:posreal] : THEORY
  BEGIN
  IMPORTING Clocks[K]
 
  t, t_now: VAR clock
  duration:VAR time
  P: VAR pred[clock]

  heldfor(P, t, t_now, duration): 
    RECURSIVE bool =
        IF P(t) THEN 
          IF (t_now - t >= duration) THEN TRUE
          ELSIF init(t) THEN FALSE
          ELSE heldfor(P,pre(t),t_now,duration)
          ENDIF
        ELSE FALSE
        ENDIF
        MEASURE rank(t)
 
  Held_For_Rec(P, duration): pred[clock] =
    (LAMBDA (t:clock): heldfor(P,t,t,duration))
 
  t1,t2:VAR clock

   le_inner_clockvar: lemma 
       forall (x:{y: posreal|(t1<y) & (y<t1+K)}): t2<=x => t2<=t1

   ge_inner_clockvar: lemma 
       forall (x:{y: posreal|(t1<y) & (y<t1+K)}): t2>=x => t2>=t1+K  

END Held_For_Rec

Held_For  [K:posreal] : THEORY
  BEGIN
  IMPORTING Clocks[K]
 
  t, t_now,t_n,t_j: VAR clock
  duration:VAR time
  P: VAR pred[clock]

  Held_For(P, duration): pred[clock]=
	(LAMBDA (t_n):EXISTS(t_j):(t_n-t_j>=duration) and FORALL(t:clock|t>=t_j&t<=t_n):P(t))
	
END Held_For









$$$Held_For.prf
(|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|pre_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SKOLEM-TYPEPRED)
    (("" (SPLIT)
      (("1" (GRIND)
        (("1" (DELETE -3)
          (("1" (CASE "n!1>0")
            (("1" (ASSERT)
              (("1" (LEMMA "both_sides_times_pos_ge1")
                (("1" (INST -1 "K" "n!1-1" "0")
                  (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (INST 1 "n!1-1")
        (("1" (ASSERT) NIL NIL)
         ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|next_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SPLIT)
    (("1" (SKOLEM-TYPEPRED)
      (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL)
     ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|clock_induct| "" (SKOSIMP)
  (("" (SKOLEM!)
    (("" (INST -1 "x!1" "rank(x!1)") (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|clock_induction| "" (SKOSIMP)
  (("" (LEMMA "clock_induct" ("P" "P!1"))
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (DELETE 2)
        (("2" (INDUCT "n")
          (("1" (SKOSIMP)
            (("1" (INST -2 "x!1")
              (("1" (GRIND)
                (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K"))
                  (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP*)
            (("2" (ASSERT)
              (("2" (GROUND)
                (("2" (INST -1 "pre(x!1)")
                  (("1" (INST -4 "x!1")
                    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
                   ("2" (GRIND) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|clock_strong_induction| "" (LEMMA "clock_induction")
  (("" (SKOSIMP*)
    ((""
      (INST -1
       "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))")
      (("" (BETA)
        (("" (SPLIT)
          (("1" (INST -1 "t!1")
            (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (SKOSIMP*)
            (("2" (INST -3 0)
              (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
            NIL)
           ("3" (SKOSIMP*)
            (("3" (INST -3 "m!1")
              (("3" (ASSERT)
                (("3" (SKOSIMP)
                  (("3" (INST -1 "z!1")
                    (("3" (GRIND)
                      (("3" (HIDE 2 3 4)
                        (("3" (TYPEPRED "m!1" "z!1" "t!2" "K")
                          (("3" (BOTH-SIDES "/" "K" -7)
                            (("1" (BOTH-SIDES "/" "K" -9)
                              (("1"
                                (BOTH-SIDES "/" "K" -10)
                                (("1"
                                  (BOTH-SIDES "/" "K" 2)
                                  (("1" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|Held_For_Rec| (|heldfor_TCC1| "" (TERMINATION-TCC) NIL NIL)
 (|le_inner_clockvar| "" (GRIND)
  (("" (CASE "floor(n!2)<=n!1")
    (("1" (GRIND)
      (("1" (CASE "floor(n!2)=n!2")
        (("1" (GRIND)
          (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL)
     ("2" (GRIND)
      (("2" (BOTH-SIDES "/" "K" -11)
        (("2" (GRIND)
          (("2" (BOTH-SIDES "/" "K" -9)
            (("2" (GRIND)
              (("2" (CASE "n!1 * K / K=n!1")
                (("1" (REPLACE -1 -10 LR)
                  (("1" (CASE "n!2* K / K=n!2")
                    (("1" (REPLACE -1 -13 LR)
                      (("1" (GRIND)
                        (("1" (BOTH-SIDES "/" "K" -12)
                          (("1" (CASE "(K + n!1 * K) / K=n!1+1")
                            (("1" (REPLACE -1 -13 LR)
                              (("1" (GRIND) NIL NIL)) NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (GRIND) NIL NIL))
                    NIL))
                  NIL)
                 ("2" (GRIND) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|ge_inner_clockvar| "" (GRIND)
  (("" (CASE "floor(n!2)>=n!1+1")
    (("1" (GRIND)
      (("1" (CASE "floor(n!2)=n!2")
        (("1" (GRIND)
          (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL)
     ("2" (GRIND)
      (("2" (BOTH-SIDES "/" "K" -11)
        (("2" (GRIND)
          (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|Held_For|)
(|DelayedTrip| (|TimerUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|TimerUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|TimerUpdate_TCC3| "" (SKOSIMP)
  (("" (INST 2 "0") (("" (GRIND) NIL NIL)) NIL)) NIL)
 (|TimerUpdate_TCC4| "" (COND-COVERAGE-TCC) NIL NIL)
 (|TimerUpdate_TCC5| "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|Timer_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|Timer_TCC3| "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer_Lemma2| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer_Lemma3| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer_Lemma4| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (SKOSIMP)
      (("2" (INST -1 "P!1" "t_h!1" "timeout!1")
        (("2" (BDDSIMP)
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
           ("3" (ASSERT)
            (("3" (EXPAND "Timer" -4) (("3" (GRIND) NIL NIL)) NIL))
            NIL)
           ("4"
            (CASE "timeout!1 - (t_h!1 - t!1)>0 OR timeout!1 - (t_h!1 - t!1)<=0")
            (("1" (BDDSIMP)
              (("1" (LEMMA "Timer_Lemma2")
                (("1" (INST -1 "P!1" "pre(t!1)" "timeout!1")
                  (("1" (GRIND) NIL NIL)) NIL))
                NIL)
               ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL)
           ("5" (GRIND) NIL NIL)
           ("6" (CASE "t!1<=t_h!1-timeout!1 OR t!1>t_h!1-timeout!1")
            (("1" (BDDSIMP)
              (("1" (HIDE -5) (("1" (GRIND) NIL NIL)) NIL)
               ("2" (CASE "t!1>floor((t_h!1 - timeout!1) / K) * K")
                (("1" (HIDE -6)
                  (("1" (GRIND)
                    (("1" (HIDE -2 -3 -4 -5)
                      (("1" (HIDE 2 3)
                        (("1" (GRIND)
                          (("1" (TYPEPRED "t!1")
                            (("1" (GRIND)
                              (("1"
                                (BOTH-SIDES "/" "K" -4)
                                (("1"
                                  (BOTH-SIDES "/" "K" 2)
                                  (("1" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (ASSERT)
                  (("2"
                    (CASE "t_h!1 - timeout!1>floor((t_h!1 - timeout!1) / K) * K")
                    (("1" (HIDE -6) (("1" (GRIND) NIL NIL)) NIL)
                     ("2" (HIDE -1 -2 -3 -4 -5)
                      (("2" (HIDE 2 3 4 5)
                        (("2" (BOTH-SIDES "/" "K" 1)
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General1| "" (SKOSIMP)
  (("" (EXPAND "Held_For")
    (("" (SKOSIMP)
      ((""
        (CASE "FORALL (t: clock[K] | NOT init(t)& t >= t_j!1 & t <= t!1 ):Timer(P!1,timeout!1)(pre(t))>=timeout!1-(t!1-t) AND P!1(t)")
        (("1" (INST -1 "t!1")
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
         ("2" (BDDSIMP)
          (("1" (HIDE 1)
            (("1" (REVEAL 1)
              (("1" (HIDE 2)
                (("1" (INDUCT "t" 1 "clock_induction")
                  (("1" (TYPEPRED "t!2") (("1" (PROPAX) NIL NIL)) NIL)
                   ("2" (TYPEPRED "t!2") (("2" (PROPAX) NIL NIL)) NIL)
                   ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL)
                   ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
                   ("7" (GRIND) NIL NIL)
                   ("8" (SKOSIMP)
                    (("8" (BDDSIMP)
                      (("1" (INST -5 "t!2") (("1" (GRIND) NIL NIL))
                        NIL)
                       ("2" (EXPAND "init")
                        (("2" (REPLACE -1 * LR)
                          (("2" (EXPAND "pre")
                            (("2" (CASE "t!2>t_j!1 OR t!2=t_j!1")
                              (("1"
                                (BDDSIMP)
                                (("1"
                                  (CASE "t_j!1=0")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (ASSERT)
                                    (("2"
                                      (SIMPLIFY)
                                      (("2"
                                        (HIDE 3)
                                        (("2"
                                          (GRIND)
                                          (("2"
                                            (TYPEPRED "t_j!1")
                                            (("2"
                                              (GRIND)
                                              (("2"
                                                (CASE "K>n!1*K")
                                                (("1"
                                                  (GRIND)
                                                  (("1"
                                                    (BOTH-SIDES
                                                     "/"
                                                     "K"
                                                     -1)
                                                    (("1"
                                                      (BOTH-SIDES
                                                       "/"
                                                       "K"
                                                       1)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (GRIND)
                                                      (("2"
                                                        (BOTH-SIDES
                                                         "*"
                                                         "K"
                                                         1)
                                                        (("2"
                                                          (GRIND)
                                                          NIL
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2"
                                  (CASE "timeout!1 - (t!1 - t!2)<=0")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (HIDE 3)
                                    (("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("3" (INST -6 "t!2") (("3" (GRIND) NIL NIL))
                        NIL)
                       ("4" (CASE "NOT init(pre(t!2))")
                        (("1" (GRIND) NIL NIL)
                         ("2" (EXPAND "Timer" 2)
                          (("2" (ASSERT)
                            (("2" (EXPAND "TimerUpdate")
                              (("2"
                                (ASSERT)
                                (("2"
                                  (EXPAND "init")
                                  (("2"
                                    (EXPAND "pre")
                                    (("2"
                                      (EXPAND "next")
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("5" (INST -4 "t!2") (("5" (GRIND) NIL NIL))
                        NIL)
                       ("6" (HIDE 3) (("6" (GRIND) NIL NIL)) NIL)
                       ("7" (INST -4 "t!2") (("7" (GRIND) NIL NIL))
                        NIL)
                       ("8" (CASE "t!2=t_j!1 OR t!2>t_j!1")
                        (("1" (BDDSIMP)
                          (("1" (REPLACE -1 * LR)
                            (("1" (CASE "timeout!1 - (t!1 - t_j!1)<=0")
                              (("1" (GRIND) NIL NIL)
                               ("2"
                                (HIDE 4)
                                (("2" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (HIDE 3)
                            (("2" (GRIND)
                              (("2"
                                (TYPEPRED "t!2")
                                (("2"
                                  (TYPEPRED "t_j!1")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (BOTH-SIDES "/" "K" 2)
                                      (("2"
                                        (BOTH-SIDES "/" "K" -7)
                                        (("2"
                                          (BOTH-SIDES "/" "K" -8)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (GRIND) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General2| "" (SKOLEM!)
  (("" (BDDSIMP)
    (("" (EXPAND "Held_For")
      (("" (INST 1 "floor((t!1-timeout!1)/K)*K")
        (("1"
          (CASE "FORALL (t_h: clock[K] | t_h >= floor((t!1 - timeout!1) / K) * K & t_h <= t!1 & NOT init(t_h)): P!1(t_h) AND Timer(P!1,timeout!1)(pre(t_h))>=timeout!1-(t!1-t_h) IMPLIES  FORALL (t: clock[K] | t >= floor((t!1 - timeout!1) / K) * K & t <= t_h): P!1(t)")
          (("1" (INST -1 "t!1")
            (("1" (BDDSIMP)
              (("1"
                (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                (("1" (GRIND) NIL NIL)
                 ("2" (HIDE 2)
                  (("2" (NAME-REPLACE "y!1" "t!1-timeout!1")
                    (("2" (HIDE -2 -3)
                      (("2" (GRIND)
                        (("2" (BOTH-SIDES "/" "K")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (GRIND) NIL NIL))
              NIL)
             ("2" (HIDE 2)
              (("2"
                (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                (("1" (GRIND) NIL NIL)
                 ("2" (HIDE -2 -1)
                  (("2" (GRIND)
                    (("2" (HIDE 2)
                      (("2" (BOTH-SIDES "/" "K")
                        (("2"
                          (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE 2)
            (("2" (HIDE -2)
              (("2" (INDUCT "t_h" 1 "clock_induction")
                (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
                 ("3" (GRIND) NIL NIL) ("4" (SKOSIMP) NIL NIL)
                 ("5" (SKOSIMP)
                  (("5" (BDDSIMP)
                    (("1" (CASE "t!2=K")
                      (("1" (REPLACE -1 * LR)
                        (("1" (REPLACE -1 * RL)
                          (("1" (REPLACE -1 * LR)
                            (("1"
                              (CASE "timeout!1 - (t!1 - K)<=0 OR timeout!1 - (t!1 - K)>0")
                              (("1"
                                (BDDSIMP)
                                (("1"
                                  (CASE
                                   "floor((t!1 - timeout!1) / K) * K>=K")
                                  (("1"
                                    (SKOSIMP)
                                    (("1"
                                      (TYPEPRED "t!3")
                                      (("1"
                                        (CASE "t!3>=K")
                                        (("1"
                                          (HIDE -13)
                                          (("1" (GRIND) NIL NIL))
                                          NIL)
                                         ("2"
                                          (HIDE -12)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (HIDE -7)
                                    (("2"
                                      (CASE "t!1-timeout!1>=K")
                                      (("1"
                                        (HIDE 2 3)
                                        (("1"
                                          (NAME-REPLACE
                                           "y!1"
                                           "t!1-timeout!1")
                                          (("1"
                                            (GRIND)
                                            (("1"
                                              (BOTH-SIDES "/" "K")
                                              (("1"
                                                (GRIND)
                                                (("1"
                                                  (BOTH-SIDES
                                                   "/"
                                                   "K"
                                                   -1)
                                                  (("1"
                                                    (NAME-REPLACE
                                                     "z!1"
                                                     "y!1/K")
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (ASSERT)
                                                (("2"
                                                  (BOTH-SIDES
                                                   "*"
                                                   "K"
                                                   -1)
                                                  (("2"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2"
                                  (SKOSIMP)
                                  (("2"
                                    (CASE "t!3=K or t!3=0")
                                    (("1"
                                      (BDDSIMP)
                                      (("1" (ASSERT) NIL NIL)
                                       ("2"
                                        (ASSERT)
                                        (("2" (GRIND) NIL NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (TYPEPRED "t!3")
                                      (("2"
                                        (BDDSIMP)
                                        (("2"
                                          (CASE "t!3<t!2 OR t!3=t!2")
                                          (("1"
                                            (BDDSIMP)
                                            (("1"
                                              (REPLACE -7 * LR)
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (GRIND)
                                                  (("1"
                                                    (BOTH-SIDES
                                                     "/"
                                                     "K"
                                                     -2)
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (BOTH-SIDES
                                                         "/"
                                                         "K"
                                                         -2)
                                                        (("1"
                                                          (GRIND)
                                                          NIL
                                                          NIL)
                                                         ("2"
                                                          (ASSERT)
                                                          (("2"
                                                            (GRIND)
                                                            (("2"
                                                              (BOTH-SIDES
                                                               "/"
                                                               "K"
                                                               -2)
                                                              (("1"
                                                                (GRIND)
                                                                NIL
                                                                NIL)
                                                               ("2"
                                                                (HIDE
                                                                 -4
                                                                 -5
                                                                 -6
                                                                 -7)
                                                                (("2"
                                                                  (ASSERT)
                                                                  (("2"
                                                                    (CASE
                                                                     "n!1=1")
                                                                    (("1"
                                                                      (GRIND)
                                                                      NIL
                                                                      NIL)
                                                                     ("2"
                                                                      (CASE
                                                                       "n!1<1")
                                                                      (("1"
                                                                        (GRIND)
                                                                        NIL
                                                                        NIL)
                                                                       ("2"
                                                                        (BOTH-SIDES
                                                                         "*"
                                                                         "K"
                                                                         1)
                                                                        (("2"
                                                                          (GRIND)
                                                                          NIL
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2" (GRIND) NIL NIL))
                                            NIL)
                                           ("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (GRIND) NIL NIL))
                      NIL)
                     ("2" (SKOSIMP)
                      (("2" (CASE "t!3<=pre(t!2) OR t!3>pre(t!2)")
                        (("1" (BDDSIMP)
                          (("1" (INST -2 "t!3") NIL NIL)
                           ("2" (ASSERT)
                            (("2" (TYPEPRED "t!3")
                              (("2"
                                (CASE "t!3=t!2")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (TYPEPRED "t!2")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (HIDE -1 -2 -3 -4 -5 -6)
                                      (("2"
                                        (CASE "n!2<=n!1")
                                        (("1"
                                          (CASE "n!2>n!1-1")
                                          (("1" (GRIND) NIL NIL)
                                           ("2"
                                            (BOTH-SIDES "*" "K" 1)
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL)
                                         ("2"
                                          (BOTH-SIDES "*" "K" 1)
                                          (("2"
                                            (ASSERT)
                                            (("2"
                                              (GRIND)
                                              (("2"
                                                (BOTH-SIDES "/" "K" -1)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL)
                     ("3"
                      (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)>0 OR timeout!1 - (t!1 - t!2)<0")
                      (("1" (BDDSIMP)
                        (("1" (CASE "t!2=t!1-timeout!1")
                          (("1" (REPLACE -1 * LR)
                            (("1" (REPLACE -1 * RL)
                              (("1"
                                (REPLACE -1 * LR)
                                (("1"
                                  (REPLACE -1 * RL)
                                  (("1"
                                    (ASSERT)
                                    (("1" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("2" (LEMMA "Timer_Lemma2")
                          (("2" (INST -1 "P!1" "pre(t!2)" "timeout!1")
                            (("2" (BDDSIMP)
                              (("1"
                                (EXPAND "Timer" -6)
                                (("1" (GRIND) NIL NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("3" (HIDE -5 -6 1 2)
                          (("3" (CASE "t!2<t!1-timeout!1")
                            (("1" (SKOSIMP)
                              (("1"
                                (CASE
                                 "t!2<=floor((t!1 - timeout!1) / K) * K")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (HIDE 2)
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (TYPEPRED "t!2")
                                      (("2"
                                        (GRIND)
                                        (("2"
                                          (CASE
                                           "n!1<=floor((t!1 - timeout!1) / K)")
                                          (("1"
                                            (GRIND)
                                            (("1"
                                              (BOTH-SIDES "/" "K" 1)
                                              (("1"
                                                (BOTH-SIDES "/" "K" 2)
                                                (("1" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL)
                                           ("2"
                                            (CASE
                                             "n!1<(t!1 - timeout!1) / K")
                                            (("1" (GRIND) NIL NIL)
                                             ("2"
                                              (HIDE 2 3 4)
                                              (("2"
                                                (BOTH-SIDES "*" "K" 1)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2"
                        (CASE "t!2 > floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K")
                        (("1" (BDDSIMP)
                          (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL)
                           ("2" (GRIND) NIL NIL))
                          NIL)
                         ("2" (GRIND) NIL NIL))
                        NIL))
                      NIL)
                     ("4"
                      (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)<0 OR timeout!1 - (t!1 - t!2)>0")
                      (("1" (BDDSIMP)
                        (("1" (CASE "t!2=t!1-timeout!1")
                          (("1" (REPLACE -1 * LR)
                            (("1" (REPLACE -1 * RL)
                              (("1"
                                (HIDE -6)
                                (("1"
                                  (CASE
                                   "floor((t!1 - timeout!1) / K) * K=t!2")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (CASE
                                     "floor((t!1 - timeout!1) / K) * K=floor((t!2)/K)*K")
                                    (("1"
                                      (CASE "t!2=floor((t!2) / K) * K")
                                      (("1" (GRIND) NIL NIL)
                                       ("2"
                                        (ASSERT)
                                        (("2"
                                          (HIDE 2 3 4 5)
                                          (("2"
                                            (TYPEPRED "t!2")
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("2" (CASE "t!2<t!1-timeout!1")
                          (("1" (HIDE -2)
                            (("1"
                              (CASE "t!2<= floor((t!1 - timeout!1) / K) * K")
                              (("1" (GRIND) NIL NIL)
                               ("2"
                                (HIDE 2 3 4)
                                (("2"
                                  (TYPEPRED "t!2")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (CASE
                                       "n!1<= floor((t!1 - timeout!1) / K) ")
                                      (("1"
                                        (BOTH-SIDES "/" "K" 2)
                                        (("1"
                                          (HIDE -8)
                                          (("1" (GRIND) NIL NIL))
                                          NIL))
                                        NIL)
                                       ("2"
                                        (HIDE -8)
                                        (("2"
                                          (HIDE 2 3)
                                          (("2"
                                            (BOTH-SIDES "/" "K" -4)
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("3" (LEMMA "Timer_Lemma2")
                          (("3" (INST -1 "P!1" "pre(t!2)" "timeout!1")
                            (("3" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL)
                       ("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("5" (ASSERT)
                      (("5" (HIDE -4) (("5" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("6"
                      (CASE "t!2 > floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K")
                      (("1" (BDDSIMP)
                        (("1" (HIDE -5)
                          (("1" (HIDE 2 3)
                            (("1" (TYPEPRED "t!2")
                              (("1"
                                (GRIND)
                                (("1"
                                  (CASE
                                   "n!1>=floor((t!1 - timeout!1) / K)+1")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (GRIND)
                                      (("1"
                                        (BOTH-SIDES "/" "K" 2)
                                        (("1" (GRIND) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (HIDE 2 3)
                                    (("2"
                                      (HIDE -5 -6)
                                      (("2"
                                        (BOTH-SIDES "/" "K" -4)
                                        (("2" (GRIND) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL))
                        NIL)
                       ("2" (ASSERT)
                        (("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (BDDSIMP)
          (("1" (INST 1 "floor((t!1 - timeout!1) / K)")
            (("1" (CASE "t!1>=timeout!1")
              (("1" (HIDE -3)
                (("1" (GRIND)
                  (("1" (CASE "t!1-timeout!1>=0")
                    (("1" (GRIND)
                      (("1" (BOTH-SIDES "/" "K" -1)
                        (("1" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (LEMMA "Timer_Lemma4")
                (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1")
                  (("2" (BDDSIMP)
                    (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)
                     ("4" (ASSERT) NIL NIL)
                     ("5"
                      (CASE "t!1-timeout!1>= floor((t!1 - timeout!1) / K) * K")
                      (("1" (ASSERT) NIL NIL)
                       ("2" (HIDE 2 3 4)
                        (("2" (HIDE -2)
                          (("2" (GRIND)
                            (("2" (NAME-REPLACE "y!1" "t!1-timeout!1")
                              (("2"
                                (GRIND)
                                (("2"
                                  (BOTH-SIDES "/" "K" 1)
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (LEMMA "Timer_Lemma4")
            (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1")
              (("2" (BDDSIMP)
                (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL)
                 ("2" (ASSERT)
                  (("2" (CASE "(t!1-timeout!1)/K>=0")
                    (("1" (NAME-REPLACE "y!1" "(t!1-timeout!1)/K")
                      (("1" (HIDE -4)
                        (("1" (GRIND)
                          (("1" (BOTH-SIDES "/" "K" 1)
                            (("1" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (ASSERT)
                      (("2" (HIDE -3)
                        (("2" (GRIND)
                          (("2" (CASE "t!1-timeout!1>=0")
                            (("1" (GRIND)
                              (("1"
                                (BOTH-SIDES "/" "K" -1)
                                (("1" (GRIND) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL)
                 ("5"
                  (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (HIDE 2 3)
                    (("2" (BOTH-SIDES "/" "K" 1)
                      (("2"
                        (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K")
                        (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (LEMMA "Timer_General1")
      (("2" (LEMMA "Timer_General2")
        (("2" (SKOSIMP)
          (("2" (INST -1 "P!1" "timeout!1" "t!1")
            (("2" (INST - "P!1" "timeout!1" "t!1")
              (("2" (TYPEPRED "t!1")
                (("2" (ASSERT)
                  (("2" (HIDE -5)
                    (("2"
                      (CASE "(P!1(t!1) AND Timer(P!1, timeout!1)(pre(t!1)) >= timeout!1) IFF Held_For(P!1, timeout!1)(t!1)")
                      (("1" (GRIND) NIL NIL)
                       ("2" (HIDE 3) (("2" (BDDSIMP) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|DelayedTrip_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|DelayedTrip_SRS_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (SDD_TCC1 "" (TERMINATION-TCC) NIL NIL)
 (SDD_TCC2 "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer2_lemma| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOLEM-TYPEPRED)
    (("2" (BDDSIMP)
      (("2" (SKOSIMP)
        (("2" (SKOSIMP)
          (("2" (INST -3 "P!1" "timeout1!1" "timeout2!1")
            (("2" (EXPAND "SDD" 2)
              (("2" (EXPAND "Timer" 2)
                (("2" (ASSERT)
                  (("2" (LEMMA "Timer1_is_Timer")
                    (("2"
                      (INST - "P!1" "pre(t!1)" "timeout1!1"
                       "timeout2!1")
                      (("2" (REPLACE -1 * RL)
                        (("2" (REPLACE -4 * RL)
                          (("2" (LEMMA "Timer_General")
                            (("2" (INST?)
                              (("2"
                                (LIFT-IF)
                                (("2"
                                  (SPLIT)
                                  (("1" (FLATTEN) NIL NIL)
                                   ("2"
                                    (FLATTEN)
                                    (("2"
                                      (REPLACE -1 * RL)
                                      (("2" (PROPAX) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Final_lemma2| "" (LEMMA "Timer1_is_Timer")
  (("" (SKOLEM-TYPEPRED)
    (("" (INST?)
      (("" (REPLACE -7 * RL)
        (("" (LEMMA "Timer_General")
          (("" (INST?)
            (("" (LIFT-IF)
              (("" (SPLIT)
                (("1" (FLATTEN) NIL NIL)
                 ("2" (FLATTEN)
                  (("2" (REPLACE -1 *)
                    (("2" (LEMMA "Timer2_lemma")
                      (("2" (INST?)
                        (("2" (REPLACE -1 * RL)
                          (("2" (LEMMA "Timer_General")
                            (("2"
                              (INST -1
                               "LAMBDA (x: clock[K]): NOT Held_For(P!1, timeout1!1)(x)"
                               "t!1" "timeout2!1")
                              (("2"
                                (LIFT-IF)
                                (("2"
                                  (SPLIT)
                                  (("1" (FLATTEN) NIL NIL)
                                   ("2"
                                    (HIDE -2 -3)
                                    (("2"
                                      (FLATTEN)
                                      (("2"
                                        (BETA)
                                        (("2"
                                          (HIDE -2 -3 -4 -5 -6 -7 -8)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (GOAL "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (SKOSIMP)
      (("2" (INST -1 "timeout1!1" "timeout2!1")
        (("2" (LEMMA "Final_lemma2")
          (("2" (INST -1 "PP" "timeout1!1" "timeout2!1" "t!1")
            (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$TimerGeneral.pvs
TimerGeneral  [K:posreal] : THEORY

  BEGIN
  IMPORTING Held_For[K]

  t, t_h: VAR clock
  P:var pred[clock]

  timeout : var posreal%time

  CurrentP:var bool
  previous:var clock

TimerUpdate(CurrentP,timeout,previous):clock= TABLE
		%------------------------------------%
		|[previous<timeout|previous>=timeout]|
%----------------------------------------------------%
|CurrentP	|next(previous)	  |previous	    ||
%----------------------------------------------------%
|NOT CurrentP   |0		  |0		    ||
%----------------------------------------------------%
ENDTABLE

Timer(P,timeout)(t):RECURSIVE clock= TABLE
%--------------------------------------------------------------------------------%
|[init(t)		     |	 			NOT init(t)	     ]|
%--------------------------------------------------------------------------------%
|TimerUpdate(P(t),timeout,0) | TimerUpdate(P(t),timeout,Timer(P,timeout)(pre(t)))||
%--------------------------------------------------------------------------------%
ENDTABLE
MEASURE rank(t)

Timer_Lemma2: lemma 
Timer(P,timeout)(t)>0 IMPLIES P(t)


Timer_Lemma3: lemma
Timer(P,timeout)(t)>=timeout IMPLIES t>=0

Timer_Lemma4: lemma
t >= floor((t_h - timeout) / K) * K & t <= t_h AND P(t) AND NOT init(t) AND Timer(P,timeout)(pre(t))>=timeout-(t_h-t) IMPLIES t>=timeout-(t_h-t)

Timer_General1: THEOREM
FORALL(t|NOT init(t)): Held_For(P,timeout)(t) IMPLIES P(t) AND Timer(P,timeout)(pre(t))>=timeout

Timer_General2: THEOREM
FORALL(t|NOT init(t)):  P(t) AND Timer(P,timeout)(pre(t))>=timeout IMPLIES Held_For(P,timeout)(t) 

Timer_General: THEOREM
IF init(t) THEN  FALSE ELSE P(t) AND Timer(P,timeout)(pre(t))>=timeout ENDIF = Held_For(P,timeout)(t)

END TimerGeneral

$$$TimerGeneral.prf
(|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|pre_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SKOLEM-TYPEPRED)
    (("" (SPLIT)
      (("1" (GRIND)
        (("1" (DELETE -3)
          (("1" (CASE "n!1>0")
            (("1" (ASSERT)
              (("1" (LEMMA "both_sides_times_pos_ge1")
                (("1" (INST -1 "K" "n!1-1" "0")
                  (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (INST 1 "n!1-1")
        (("1" (ASSERT) NIL NIL)
         ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|next_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (SPLIT)
    (("1" (SKOLEM-TYPEPRED)
      (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL)
     ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|clock_induct| "" (SKOSIMP)
  (("" (SKOLEM!)
    (("" (INST -1 "x!1" "rank(x!1)") (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|clock_induction| "" (SKOSIMP)
  (("" (LEMMA "clock_induct" ("P" "P!1"))
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (DELETE 2)
        (("2" (INDUCT "n")
          (("1" (SKOSIMP)
            (("1" (INST -2 "x!1")
              (("1" (GRIND)
                (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K"))
                  (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP*)
            (("2" (ASSERT)
              (("2" (GROUND)
                (("2" (INST -1 "pre(x!1)")
                  (("1" (INST -4 "x!1")
                    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
                   ("2" (GRIND) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|clock_strong_induction| "" (LEMMA "clock_induction")
  (("" (SKOSIMP*)
    ((""
      (INST -1
       "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))")
      (("" (BETA)
        (("" (SPLIT)
          (("1" (INST -1 "t!1")
            (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (SKOSIMP*)
            (("2" (INST -3 0)
              (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
            NIL)
           ("3" (SKOSIMP*)
            (("3" (INST -3 "m!1")
              (("3" (ASSERT)
                (("3" (SKOSIMP)
                  (("3" (INST -1 "z!1")
                    (("3" (GRIND)
                      (("3" (HIDE 2 3 4)
                        (("3" (TYPEPRED "m!1" "z!1" "t!2" "K")
                          (("3" (BOTH-SIDES "/" "K" -7)
                            (("1" (BOTH-SIDES "/" "K" -9)
                              (("1"
                                (BOTH-SIDES "/" "K" -10)
                                (("1"
                                  (BOTH-SIDES "/" "K" 2)
                                  (("1" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|Held_For| (|heldfor_TCC1| "" (TERMINATION-TCC) NIL NIL)
 (|le_inner_clockvar| "" (GRIND)
  (("" (CASE "floor(n!2)<=n!1")
    (("1" (GRIND)
      (("1" (CASE "floor(n!2)=n!2")
        (("1" (GRIND)
          (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL)
     ("2" (GRIND)
      (("2" (BOTH-SIDES "/" "K" -11)
        (("2" (GRIND)
          (("2" (BOTH-SIDES "/" "K" -9)
            (("2" (GRIND)
              (("2" (CASE "n!1 * K / K=n!1")
                (("1" (REPLACE -1 -10 LR)
                  (("1" (CASE "n!2* K / K=n!2")
                    (("1" (REPLACE -1 -13 LR)
                      (("1" (GRIND)
                        (("1" (BOTH-SIDES "/" "K" -12)
                          (("1" (CASE "(K + n!1 * K) / K=n!1+1")
                            (("1" (REPLACE -1 -13 LR)
                              (("1" (GRIND) NIL NIL)) NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (GRIND) NIL NIL))
                    NIL))
                  NIL)
                 ("2" (GRIND) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|ge_inner_clockvar| "" (GRIND)
  (("" (CASE "floor(n!2)>=n!1+1")
    (("1" (GRIND)
      (("1" (CASE "floor(n!2)=n!2")
        (("1" (GRIND)
          (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL)
     ("2" (GRIND)
      (("2" (BOTH-SIDES "/" "K" -11)
        (("2" (GRIND)
          (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))
(|Held_For2|)
(|TimerGeneral| (|TimerUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|TimerUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|TimerUpdate_TCC3| "" (SKOSIMP)
  (("" (INST 2 "0") (("" (GRIND) NIL NIL)) NIL)) NIL)
 (|TimerUpdate_TCC4| "" (COND-COVERAGE-TCC) NIL NIL)
 (|TimerUpdate_TCC5| "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|Timer_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|Timer_TCC3| "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer_Lemma2| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer_Lemma3| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer_Lemma4| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (SKOSIMP)
      (("2" (INST -1 "P!1" "t_h!1" "timeout!1")
        (("2" (BDDSIMP)
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
           ("3" (ASSERT)
            (("3" (EXPAND "Timer" -4) (("3" (GRIND) NIL NIL)) NIL))
            NIL)
           ("4"
            (CASE "timeout!1 - (t_h!1 - t!1)>0 OR timeout!1 - (t_h!1 - t!1)<=0")
            (("1" (BDDSIMP)
              (("1" (LEMMA "Timer_Lemma2")
                (("1" (INST -1 "P!1" "pre(t!1)" "timeout!1")
                  (("1" (GRIND) NIL NIL)) NIL))
                NIL)
               ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL)
           ("5" (GRIND) NIL NIL)
           ("6" (CASE "t!1<=t_h!1-timeout!1 OR t!1>t_h!1-timeout!1")
            (("1" (BDDSIMP)
              (("1" (HIDE -5) (("1" (GRIND) NIL NIL)) NIL)
               ("2" (CASE "t!1>floor((t_h!1 - timeout!1) / K) * K")
                (("1" (HIDE -6)
                  (("1" (GRIND)
                    (("1" (HIDE -2 -3 -4 -5)
                      (("1" (HIDE 2 3)
                        (("1" (GRIND)
                          (("1" (TYPEPRED "t!1")
                            (("1" (GRIND)
                              (("1"
                                (BOTH-SIDES "/" "K" -4)
                                (("1"
                                  (BOTH-SIDES "/" "K" 2)
                                  (("1" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (ASSERT)
                  (("2"
                    (CASE "t_h!1 - timeout!1>floor((t_h!1 - timeout!1) / K) * K")
                    (("1" (HIDE -6) (("1" (GRIND) NIL NIL)) NIL)
                     ("2" (HIDE -1 -2 -3 -4 -5)
                      (("2" (HIDE 2 3 4 5)
                        (("2" (BOTH-SIDES "/" "K" 1)
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General1| "" (SKOSIMP)
  (("" (EXPAND "Held_For")
    (("" (SKOSIMP)
      ((""
        (CASE "FORALL (t: clock[K] | NOT init(t)& t >= t_j!1 & t <= t!1 ):Timer(P!1,timeout!1)(pre(t))>=timeout!1-(t!1-t) AND P!1(t)")
        (("1" (INST -1 "t!1")
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
         ("2" (BDDSIMP)
          (("1" (HIDE 1)
            (("1" (REVEAL 1)
              (("1" (HIDE 2)
                (("1" (INDUCT "t" 1 "clock_induction")
                  (("1" (TYPEPRED "t!2") (("1" (PROPAX) NIL NIL)) NIL)
                   ("2" (TYPEPRED "t!2") (("2" (PROPAX) NIL NIL)) NIL)
                   ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL)
                   ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
                   ("7" (GRIND) NIL NIL)
                   ("8" (SKOSIMP)
                    (("8" (BDDSIMP)
                      (("1" (INST -5 "t!2") (("1" (GRIND) NIL NIL))
                        NIL)
                       ("2" (EXPAND "init")
                        (("2" (REPLACE -1 * LR)
                          (("2" (EXPAND "pre")
                            (("2" (CASE "t!2>t_j!1 OR t!2=t_j!1")
                              (("1"
                                (BDDSIMP)
                                (("1"
                                  (CASE "t_j!1=0")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (ASSERT)
                                    (("2"
                                      (SIMPLIFY)
                                      (("2"
                                        (HIDE 3)
                                        (("2"
                                          (GRIND)
                                          (("2"
                                            (TYPEPRED "t_j!1")
                                            (("2"
                                              (GRIND)
                                              (("2"
                                                (CASE "K>n!1*K")
                                                (("1"
                                                  (GRIND)
                                                  (("1"
                                                    (BOTH-SIDES
                                                     "/"
                                                     "K"
                                                     -1)
                                                    (("1"
                                                      (BOTH-SIDES
                                                       "/"
                                                       "K"
                                                       1)
                                                      (("1"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (GRIND)
                                                      (("2"
                                                        (BOTH-SIDES
                                                         "*"
                                                         "K"
                                                         1)
                                                        (("2"
                                                          (GRIND)
                                                          NIL
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2"
                                  (CASE "timeout!1 - (t!1 - t!2)<=0")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (HIDE 3)
                                    (("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("3" (INST -6 "t!2") (("3" (GRIND) NIL NIL))
                        NIL)
                       ("4" (CASE "NOT init(pre(t!2))")
                        (("1" (GRIND) NIL NIL)
                         ("2" (EXPAND "Timer" 2)
                          (("2" (ASSERT)
                            (("2" (EXPAND "TimerUpdate")
                              (("2"
                                (ASSERT)
                                (("2"
                                  (EXPAND "init")
                                  (("2"
                                    (EXPAND "pre")
                                    (("2"
                                      (EXPAND "next")
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("5" (INST -4 "t!2") (("5" (GRIND) NIL NIL))
                        NIL)
                       ("6" (HIDE 3) (("6" (GRIND) NIL NIL)) NIL)
                       ("7" (INST -4 "t!2") (("7" (GRIND) NIL NIL))
                        NIL)
                       ("8" (CASE "t!2=t_j!1 OR t!2>t_j!1")
                        (("1" (BDDSIMP)
                          (("1" (REPLACE -1 * LR)
                            (("1" (CASE "timeout!1 - (t!1 - t_j!1)<=0")
                              (("1" (GRIND) NIL NIL)
                               ("2"
                                (HIDE 4)
                                (("2" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (HIDE 3)
                            (("2" (GRIND)
                              (("2"
                                (TYPEPRED "t!2")
                                (("2"
                                  (TYPEPRED "t_j!1")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (BOTH-SIDES "/" "K" 2)
                                      (("2"
                                        (BOTH-SIDES "/" "K" -7)
                                        (("2"
                                          (BOTH-SIDES "/" "K" -8)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (GRIND) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General2| "" (SKOLEM!)
  (("" (BDDSIMP)
    (("" (EXPAND "Held_For")
      (("" (INST 1 "floor((t!1-timeout!1)/K)*K")
        (("1"
          (CASE "FORALL (t_h: clock[K] | t_h >= floor((t!1 - timeout!1) / K) * K & t_h <= t!1 & NOT init(t_h)): P!1(t_h) AND Timer(P!1,timeout!1)(pre(t_h))>=timeout!1-(t!1-t_h) IMPLIES  FORALL (t: clock[K] | t >= floor((t!1 - timeout!1) / K) * K & t <= t_h): P!1(t)")
          (("1" (INST -1 "t!1")
            (("1" (BDDSIMP)
              (("1"
                (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                (("1" (GRIND) NIL NIL)
                 ("2" (HIDE 2)
                  (("2" (NAME-REPLACE "y!1" "t!1-timeout!1")
                    (("2" (HIDE -2 -3)
                      (("2" (GRIND)
                        (("2" (BOTH-SIDES "/" "K")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (GRIND) NIL NIL))
              NIL)
             ("2" (HIDE 2)
              (("2"
                (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                (("1" (GRIND) NIL NIL)
                 ("2" (HIDE -2 -1)
                  (("2" (GRIND)
                    (("2" (HIDE 2)
                      (("2" (BOTH-SIDES "/" "K")
                        (("2"
                          (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K")
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE 2)
            (("2" (HIDE -2)
              (("2" (INDUCT "t_h" 1 "clock_induction")
                (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
                 ("3" (GRIND) NIL NIL) ("4" (SKOSIMP) NIL NIL)
                 ("5" (SKOSIMP)
                  (("5" (BDDSIMP)
                    (("1" (CASE "t!2=K")
                      (("1" (REPLACE -1 * LR)
                        (("1" (REPLACE -1 * RL)
                          (("1" (REPLACE -1 * LR)
                            (("1"
                              (CASE "timeout!1 - (t!1 - K)<=0 OR timeout!1 - (t!1 - K)>0")
                              (("1"
                                (BDDSIMP)
                                (("1"
                                  (CASE
                                   "floor((t!1 - timeout!1) / K) * K>=K")
                                  (("1"
                                    (SKOSIMP)
                                    (("1"
                                      (TYPEPRED "t!3")
                                      (("1"
                                        (CASE "t!3>=K")
                                        (("1"
                                          (HIDE -13)
                                          (("1" (GRIND) NIL NIL))
                                          NIL)
                                         ("2"
                                          (HIDE -12)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (HIDE -7)
                                    (("2"
                                      (CASE "t!1-timeout!1>=K")
                                      (("1"
                                        (HIDE 2 3)
                                        (("1"
                                          (NAME-REPLACE
                                           "y!1"
                                           "t!1-timeout!1")
                                          (("1"
                                            (GRIND)
                                            (("1"
                                              (BOTH-SIDES "/" "K")
                                              (("1"
                                                (GRIND)
                                                (("1"
                                                  (BOTH-SIDES
                                                   "/"
                                                   "K"
                                                   -1)
                                                  (("1"
                                                    (NAME-REPLACE
                                                     "z!1"
                                                     "y!1/K")
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (ASSERT)
                                                (("2"
                                                  (BOTH-SIDES
                                                   "*"
                                                   "K"
                                                   -1)
                                                  (("2"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL)
                                 ("2"
                                  (SKOSIMP)
                                  (("2"
                                    (CASE "t!3=K or t!3=0")
                                    (("1"
                                      (BDDSIMP)
                                      (("1" (ASSERT) NIL NIL)
                                       ("2"
                                        (ASSERT)
                                        (("2" (GRIND) NIL NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (TYPEPRED "t!3")
                                      (("2"
                                        (BDDSIMP)
                                        (("2"
                                          (CASE "t!3<t!2 OR t!3=t!2")
                                          (("1"
                                            (BDDSIMP)
                                            (("1"
                                              (REPLACE -7 * LR)
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (GRIND)
                                                  (("1"
                                                    (BOTH-SIDES
                                                     "/"
                                                     "K"
                                                     -2)
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (BOTH-SIDES
                                                         "/"
                                                         "K"
                                                         -2)
                                                        (("1"
                                                          (GRIND)
                                                          NIL
                                                          NIL)
                                                         ("2"
                                                          (ASSERT)
                                                          (("2"
                                                            (GRIND)
                                                            (("2"
                                                              (BOTH-SIDES
                                                               "/"
                                                               "K"
                                                               -2)
                                                              (("1"
                                                                (GRIND)
                                                                NIL
                                                                NIL)
                                                               ("2"
                                                                (HIDE
                                                                 -4
                                                                 -5
                                                                 -6
                                                                 -7)
                                                                (("2"
                                                                  (ASSERT)
                                                                  (("2"
                                                                    (CASE
                                                                     "n!1=1")
                                                                    (("1"
                                                                      (GRIND)
                                                                      NIL
                                                                      NIL)
                                                                     ("2"
                                                                      (CASE
                                                                       "n!1<1")
                                                                      (("1"
                                                                        (GRIND)
                                                                        NIL
                                                                        NIL)
                                                                       ("2"
                                                                        (BOTH-SIDES
                                                                         "*"
                                                                         "K"
                                                                         1)
                                                                        (("2"
                                                                          (GRIND)
                                                                          NIL
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2" (GRIND) NIL NIL))
                                            NIL)
                                           ("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (GRIND) NIL NIL))
                      NIL)
                     ("2" (SKOSIMP)
                      (("2" (CASE "t!3<=pre(t!2) OR t!3>pre(t!2)")
                        (("1" (BDDSIMP)
                          (("1" (INST -2 "t!3") NIL NIL)
                           ("2" (ASSERT)
                            (("2" (TYPEPRED "t!3")
                              (("2"
                                (CASE "t!3=t!2")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (TYPEPRED "t!2")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (HIDE -1 -2 -3 -4 -5 -6)
                                      (("2"
                                        (CASE "n!2<=n!1")
                                        (("1"
                                          (CASE "n!2>n!1-1")
                                          (("1" (GRIND) NIL NIL)
                                           ("2"
                                            (BOTH-SIDES "*" "K" 1)
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL)
                                         ("2"
                                          (BOTH-SIDES "*" "K" 1)
                                          (("2"
                                            (ASSERT)
                                            (("2"
                                              (GRIND)
                                              (("2"
                                                (BOTH-SIDES "/" "K" -1)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL)
                     ("3"
                      (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)>0 OR timeout!1 - (t!1 - t!2)<0")
                      (("1" (BDDSIMP)
                        (("1" (CASE "t!2=t!1-timeout!1")
                          (("1" (REPLACE -1 * LR)
                            (("1" (REPLACE -1 * RL)
                              (("1"
                                (REPLACE -1 * LR)
                                (("1"
                                  (REPLACE -1 * RL)
                                  (("1"
                                    (ASSERT)
                                    (("1" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("2" (LEMMA "Timer_Lemma2")
                          (("2" (INST -1 "P!1" "pre(t!2)" "timeout!1")
                            (("2" (BDDSIMP)
                              (("1"
                                (EXPAND "Timer" -6)
                                (("1" (GRIND) NIL NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("3" (HIDE -5 -6 1 2)
                          (("3" (CASE "t!2<t!1-timeout!1")
                            (("1" (SKOSIMP)
                              (("1"
                                (CASE
                                 "t!2<=floor((t!1 - timeout!1) / K) * K")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (HIDE 2)
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (TYPEPRED "t!2")
                                      (("2"
                                        (GRIND)
                                        (("2"
                                          (CASE
                                           "n!1<=floor((t!1 - timeout!1) / K)")
                                          (("1"
                                            (GRIND)
                                            (("1"
                                              (BOTH-SIDES "/" "K" 1)
                                              (("1"
                                                (BOTH-SIDES "/" "K" 2)
                                                (("1" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL)
                                           ("2"
                                            (CASE
                                             "n!1<(t!1 - timeout!1) / K")
                                            (("1" (GRIND) NIL NIL)
                                             ("2"
                                              (HIDE 2 3 4)
                                              (("2"
                                                (BOTH-SIDES "*" "K" 1)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2"
                        (CASE "t!2 > floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K")
                        (("1" (BDDSIMP)
                          (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL)
                           ("2" (GRIND) NIL NIL))
                          NIL)
                         ("2" (GRIND) NIL NIL))
                        NIL))
                      NIL)
                     ("4"
                      (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)<0 OR timeout!1 - (t!1 - t!2)>0")
                      (("1" (BDDSIMP)
                        (("1" (CASE "t!2=t!1-timeout!1")
                          (("1" (REPLACE -1 * LR)
                            (("1" (REPLACE -1 * RL)
                              (("1"
                                (HIDE -6)
                                (("1"
                                  (CASE
                                   "floor((t!1 - timeout!1) / K) * K=t!2")
                                  (("1" (GRIND) NIL NIL)
                                   ("2"
                                    (CASE
                                     "floor((t!1 - timeout!1) / K) * K=floor((t!2)/K)*K")
                                    (("1"
                                      (CASE "t!2=floor((t!2) / K) * K")
                                      (("1" (GRIND) NIL NIL)
                                       ("2"
                                        (ASSERT)
                                        (("2"
                                          (HIDE 2 3 4 5)
                                          (("2"
                                            (TYPEPRED "t!2")
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("2" (CASE "t!2<t!1-timeout!1")
                          (("1" (HIDE -2)
                            (("1"
                              (CASE "t!2<= floor((t!1 - timeout!1) / K) * K")
                              (("1" (GRIND) NIL NIL)
                               ("2"
                                (HIDE 2 3 4)
                                (("2"
                                  (TYPEPRED "t!2")
                                  (("2"
                                    (GRIND)
                                    (("2"
                                      (CASE
                                       "n!1<= floor((t!1 - timeout!1) / K) ")
                                      (("1"
                                        (BOTH-SIDES "/" "K" 2)
                                        (("1"
                                          (HIDE -8)
                                          (("1" (GRIND) NIL NIL))
                                          NIL))
                                        NIL)
                                       ("2"
                                        (HIDE -8)
                                        (("2"
                                          (HIDE 2 3)
                                          (("2"
                                            (BOTH-SIDES "/" "K" -4)
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL)
                         ("3" (LEMMA "Timer_Lemma2")
                          (("3" (INST -1 "P!1" "pre(t!2)" "timeout!1")
                            (("3" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL)
                       ("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("5" (ASSERT)
                      (("5" (HIDE -4) (("5" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("6"
                      (CASE "t!2 > floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K")
                      (("1" (BDDSIMP)
                        (("1" (HIDE -5)
                          (("1" (HIDE 2 3)
                            (("1" (TYPEPRED "t!2")
                              (("1"
                                (GRIND)
                                (("1"
                                  (CASE
                                   "n!1>=floor((t!1 - timeout!1) / K)+1")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (GRIND)
                                      (("1"
                                        (BOTH-SIDES "/" "K" 2)
                                        (("1" (GRIND) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (HIDE 2 3)
                                    (("2"
                                      (HIDE -5 -6)
                                      (("2"
                                        (BOTH-SIDES "/" "K" -4)
                                        (("2" (GRIND) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL))
                        NIL)
                       ("2" (ASSERT)
                        (("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (BDDSIMP)
          (("1" (INST 1 "floor((t!1 - timeout!1) / K)")
            (("1" (CASE "t!1>=timeout!1")
              (("1" (HIDE -3)
                (("1" (GRIND)
                  (("1" (CASE "t!1-timeout!1>=0")
                    (("1" (GRIND)
                      (("1" (BOTH-SIDES "/" "K" -1)
                        (("1" (GRIND) NIL NIL)) NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (LEMMA "Timer_Lemma4")
                (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1")
                  (("2" (BDDSIMP)
                    (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)
                     ("4" (ASSERT) NIL NIL)
                     ("5"
                      (CASE "t!1-timeout!1>= floor((t!1 - timeout!1) / K) * K")
                      (("1" (ASSERT) NIL NIL)
                       ("2" (HIDE 2 3 4)
                        (("2" (HIDE -2)
                          (("2" (GRIND)
                            (("2" (NAME-REPLACE "y!1" "t!1-timeout!1")
                              (("2"
                                (GRIND)
                                (("2"
                                  (BOTH-SIDES "/" "K" 1)
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (LEMMA "Timer_Lemma4")
            (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1")
              (("2" (BDDSIMP)
                (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL)
                 ("2" (ASSERT)
                  (("2" (CASE "(t!1-timeout!1)/K>=0")
                    (("1" (NAME-REPLACE "y!1" "(t!1-timeout!1)/K")
                      (("1" (HIDE -4)
                        (("1" (GRIND)
                          (("1" (BOTH-SIDES "/" "K" 1)
                            (("1" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (ASSERT)
                      (("2" (HIDE -3)
                        (("2" (GRIND)
                          (("2" (CASE "t!1-timeout!1>=0")
                            (("1" (GRIND)
                              (("1"
                                (BOTH-SIDES "/" "K" -1)
                                (("1" (GRIND) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL)
                 ("5"
                  (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (HIDE 2 3)
                    (("2" (BOTH-SIDES "/" "K" 1)
                      (("2"
                        (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K")
                        (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Timer_General| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (LEMMA "Timer_General1")
      (("2" (LEMMA "Timer_General2")
        (("2" (SKOSIMP)
          (("2" (INST -1 "P!1" "timeout!1" "t!1")
            (("2" (INST - "P!1" "timeout!1" "t!1")
              (("2" (TYPEPRED "t!1")
                (("2" (ASSERT)
                  (("2" (HIDE -5)
                    (("2"
                      (CASE "(P!1(t!1) AND Timer(P!1, timeout!1)(pre(t!1)) >= timeout!1) IFF Held_For(P!1, timeout!1)(t!1)")
                      (("1" (GRIND) NIL NIL)
                       ("2" (HIDE 3) (("2" (BDDSIMP) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|TimerGeneral_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|TimerGeneral_SRS_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (SDD_TCC1 "" (TERMINATION-TCC) NIL NIL)
 (SDD_TCC2 "" (COND-DISJOINT-TCC) NIL NIL)
 (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
 (|Timer2_lemma| "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOLEM-TYPEPRED)
    (("2" (BDDSIMP)
      (("2" (SKOSIMP)
        (("2" (SKOSIMP)
          (("2" (INST -3 "P!1" "timeout1!1" "timeout2!1")
            (("2" (EXPAND "SDD" 2)
              (("2" (EXPAND "Timer" 2)
                (("2" (ASSERT)
                  (("2" (LEMMA "Timer1_is_Timer")
                    (("2"
                      (INST - "P!1" "pre(t!1)" "timeout1!1"
                       "timeout2!1")
                      (("2" (REPLACE -1 * RL)
                        (("2" (REPLACE -4 * RL)
                          (("2" (LEMMA "Timer_General")
                            (("2" (INST?)
                              (("2"
                                (LIFT-IF)
                                (("2"
                                  (SPLIT)
                                  (("1" (FLATTEN) NIL NIL)
                                   ("2"
                                    (FLATTEN)
                                    (("2"
                                      (REPLACE -1 * RL)
                                      (("2" (PROPAX) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|Final_lemma2| "" (LEMMA "Timer1_is_Timer")
  (("" (SKOLEM-TYPEPRED)
    (("" (INST?)
      (("" (REPLACE -7 * RL)
        (("" (LEMMA "Timer_General")
          (("" (INST?)
            (("" (LIFT-IF)
              (("" (SPLIT)
                (("1" (FLATTEN) NIL NIL)
                 ("2" (FLATTEN)
                  (("2" (REPLACE -1 *)
                    (("2" (LEMMA "Timer2_lemma")
                      (("2" (INST?)
                        (("2" (REPLACE -1 * RL)
                          (("2" (LEMMA "Timer_General")
                            (("2"
                              (INST -1
                               "LAMBDA (x: clock[K]): NOT Held_For(P!1, timeout1!1)(x)"
                               "t!1" "timeout2!1")
                              (("2"
                                (LIFT-IF)
                                (("2"
                                  (SPLIT)
                                  (("1" (FLATTEN) NIL NIL)
                                   ("2"
                                    (HIDE -2 -3)
                                    (("2"
                                      (FLATTEN)
                                      (("2"
                                        (BETA)
                                        (("2"
                                          (HIDE -2 -3 -4 -5 -6 -7 -8)
                                          (("2" (GRIND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (GOAL "" (INDUCT "t" 1 "clock_induction")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP)
    (("2" (SKOSIMP)
      (("2" (INST -1 "timeout1!1" "timeout2!1")
        (("2" (LEMMA "Final_lemma2")
          (("2" (INST -1 "PP" "timeout1!1" "timeout2!1" "t!1")
            (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))