%Patch files loaded: patch2 version 1.2.2.36 $$$DelayTrip2.pvs DelayedTrip2 [K:posreal] : THEORY BEGIN IMPORTING TimerGeneral[K] t: VAR clock P:var pred[clock] timeout,timeout1,timeout2 : var posreal%time timed_real: TYPE=[clock->real] Power,Pressure: timed_real PT, DSP: posreal CurrentP:var bool previous:var clock Relay_State: TYPE = {OPEN, CLOSED} SDD_State: TYPE = [# Relay: Relay_State, Timer1: clock, Timer2:clock #] PP(t):bool=Power(t)>=PT AND Pressure(t)>=DSP DelayedTrip_SRS(P,t,timeout1,timeout2): RECURSIVE bool= IF init(t) THEN FALSE ELSE TABLE |Held_For(P,timeout1)(t) | TRUE || |Held_For(NOT Held_For(P,timeout1),timeout2)(t) | FALSE || |NOT Held_For(P,timeout1)(t) & (NOT Held_For(NOT Held_For(P,timeout1),timeout2)(t)) | DelayedTrip_SRS(P,pre(t),timeout1,timeout2)|| ENDTABLE ENDIF MEASURE rank(t) S:VAR SDD_State RelayUpdate(timeout1,timeout2,CurrentP,S):Relay_State = TABLE |CurrentP & (Timer1(S) >= timeout1) |OPEN || |NOT (CurrentP& Timer1(S)>=timeout1) & Timer2(S)>=timeout2 |CLOSED|| | NOT(CurrentP& Timer1(S)>=timeout1) & NOT( Timer2(S)>=timeout2) |Relay(S)|| ENDTABLE SDD(P,timeout1,timeout2)(t):RECURSIVE SDD_State = IF init(t) THEN (# Relay := CLOSED, Timer1:=TimerUpdate(P(t),timeout1,0), Timer2:=TimerUpdate(TRUE,timeout2,0) #) ELSE (# Relay:=RelayUpdate(timeout1,timeout2,P(t),SDD(P,timeout1,timeout2)(pre(t))), Timer1:=TimerUpdate(P(t),timeout1, Timer1(SDD(P,timeout1,timeout2)(pre(t)))), Timer2:=TimerUpdate( NOT (P(t)& (Timer1(SDD(P,timeout1,timeout2)(pre(t)))>=timeout1)), timeout2, Timer2(SDD(P,timeout1,timeout2)(pre(t)))) #) ENDIF MEASURE rank(t) Timer1_is_Timer: LEMMA Timer(P,timeout1)(t)=Timer1(SDD(P,timeout1,timeout2)(t)) Timer2_Timer: lemma Timer(NOT Held_For(P,timeout1),timeout2)(t)= Timer2(SDD(P,timeout1,timeout2)(t)) DelayedTrip_Block :THEOREM DelayedTrip_SRS(PP,t,timeout1,timeout2)=OPEN?(Relay(SDD(PP,timeout1,timeout2)(t))) END DelayedTrip2 $$$DelayTrip2.prf (|DelayedTrip2| (|DelayedTrip_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|DelayedTrip_SRS_TCC2| "" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (BDDSIMP) (("" (EXPAND "Held_For") (("" (SKOLEM-TYPEPRED) (("" (SKOLEM-TYPEPRED) (("" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (INST -14 "t!1") (("1" (INST -16 "t!1") (("1" (INST + "t_j!1") (("1" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (REVEAL -2) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|DelayedTrip_SRS_TCC3| "" (COND-COVERAGE-TCC) NIL NIL) (|RelayUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|RelayUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (SDD_TCC1 "" (SUBTYPE-TCC) NIL NIL) (SDD_TCC2 "" (TERMINATION-TCC) NIL NIL) (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (FLATTEN) (("2" (SKOLEM-TYPEPRED) (("2" (SKOLEM-TYPEPRED) (("2" (EXPAND "Timer" 2) (("2" (EXPAND "SDD" 2) (("2" (INST?) (("2" (REPLACE -8 + RL) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer2_Timer| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (FLATTEN) (("2" (SKOLEM-TYPEPRED) (("2" (SKOLEM-TYPEPRED) (("2" (EXPAND "Timer" +) (("2" (EXPAND "SDD" +) (("2" (INST?) (("2" (REPLACE -8 + RL) (("2" (LEMMA "Timer1_is_Timer") (("2" (INST?) (("2" (REPLACE - + RL) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE - +) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|DelayedTrip_Block| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (FLATTEN) (("2" (EXPAND "DelayedTrip_SRS" +) (("2" (SKOLEM-TYPEPRED) (("2" (SKOLEM-TYPEPRED) (("2" (EXPAND "SDD" +) (("2" (EXPAND "RelayUpdate" +) (("2" (INST?) (("2" (LEMMA "Timer1_is_Timer") (("2" (INST?) (("2" (REPLACE - + RL :HIDE? T) (("2" (LEMMA "Timer2_Timer") (("2" (INST?) (("2" (REPLACE - + RL :HIDE? T) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF -1) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE - + LR :HIDE? T) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF -1) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (BETA) (("2" (REPLACE - + LR :HIDE? T) (("2" (LIFT-IF) (("2" (SIMPLIFY) (("2" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 t2<=t1 ge_inner_clockvar: lemma forall (x:{y: posreal|(t1=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!3pre(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 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 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]| %----------------------------------------------------% |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!3pre(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 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 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))