Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 412


Synopsis:        Slow proofs and typechecking problem
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jan  4 11:20:07 2000
Originator:      Bruno Dutertre
Organization:    sdl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------DEF11F3F21E0131D32F94669
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  
  In theory sporadic_tasks, there used to be two functions B. 
  That was OK with the previous version of PVS. With the new one, 
  I get an error message:
  
  B does not uniquely resolve - one of:
  
    sporadic_tasks.B : [priority -> nat],
  
    sporadic_tasks.B : [task[nbtasks] -> nat]
  
  
  I've changed the name of one of these in the attached dump.
  
  
  There's also a serious performance degradation in some of 
  the proofs:
  
  On December 8:
      process_time_K..............................proved - incomplete
  [O](0.61 s)
      max_process_time_K..........................proved - incomplete
  [O](1.19 s)
  
  Today:
      process_time_K.............................proved - incomplete
  [O](14.78 s)
      max_process_time_K.........................proved - incomplete
  [O](21.61 s)
  
  
  Bruno
  --------------DEF11F3F21E0131D32F94669
  Content-Type: text/plain; charset=us-ascii;
   name="prioceiling.dmp"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="prioceiling.dmp"
  
  %Patch files loaded: patch2 version 1.2.2.38
  
  $$$sporadic_tasks.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Sporadic tasks                                         %
  %   - tasks are in [0..nbtask-1]                          %
  %   - prio(i): priority of task i                         %
  %   - jobs are pairs (i, n) where i is a task, n is nat   %
  %   - prio of a job = prio of its task                    %
  %                                                         %
  %   C(i): max length of jobs of task i                    %
  %   T(i): min delay between two successive jobs of i      %
  %   D(i): dealine for each job of i                       %
  %                                                         %
  %   B(p): upper bound on blocking time for jobs of        %
  %         priority >= p                                   %
  %                                                         %
  %   dispatch(j): start of job j                           %
  %   prog(j): program for job j                            %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  sporadic_tasks [ 
  	nbtasks: posnat,
  	(IMPORTING programs, tasks_and_jobs[nbtasks])
  
  	prio: [task -> priority],
  	C, T, D: [task -> posnat],
  	B: [priority -> nat],
  	dispatch: [job -> nat],
  	prog: [job -> prog] ]: THEORY
  
    BEGIN
  
    ASSUMING
  
    i: VAR task		% below(nbtask)
    n, m: VAR nat
    p: VAR priority
    j: VAR job		% [task, nat]
    s: VAR semaphore  
  
    prio(i, n): priority = prio(i)
  
    good_dispatch: ASSUMPTION dispatch(i, n) + T(i) <= dispatch(i, n + 1)
  
    bound_length: ASSUMPTION length(prog(i, n)) <= C(i)
  
    blocking: ASSUMPTION prio(j) < p IMPLIES max_cs(prog(j), p) <= B(p)
  
    good_ceiling: ASSUMPTION
        member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
  
    good_programs: ASSUMPTION  well_behaved(prog(j))
  
    IMPORTING fsets_sum
  
    cpu_usage: ASSUMPTION sum(fullset[task], lambda i: C(i)/T(i)) < 1
  
    topprio_is_used: ASSUMPTION EXISTS i: prio(i) = maxprio - 1
  
    ENDASSUMING
  
  
    IMPORTING traces[job, prio, dispatch, prog], ceiling_equations, schedules3
  
  
    u: VAR trace
    t, t1, t2: VAR nat
  
  
    %-----------------------------------------
    %  Properties of dispatch, blocking, etc.
    %-----------------------------------------
  
    dispatch_delay: LEMMA dispatch(i, n + m) - dispatch(i, m) >= n * T(i)
  
    increasing_dispatch: LEMMA 
       n <  m IMPLIES dispatch(i, n) + T(i) <= dispatch(i, m)
  
    blocking_bound: LEMMA blocking(u, p, t) <= B(p)
  
    process_time_bound: LEMMA process_time(sch(u), t1, t2, j) <= C(j`1)
  
    finished_prop: LEMMA 
  	process_time(sch(u), t1, t2, j) = C(j`1) IMPLIES finished(u, j, t2)
  
  
    %----------------------------------------------------------------
    %  Set of jobs of priority >= p AND dispatched between t1 and t2 
    %-----------------------------------------------------------------
  
    K(p, t1, t2): set[job] = { j | prio(j) >= p AND t1 <= dispatch(j) AND dispa
 tch(j) < t2 }
  
    L(i, t1, t2): set[job] = { j | j`1 = i AND t1 <= dispatch(j) AND dispatch(j
 ) < t2 }
  
    A(p): set[task] = { i | prio(i) >= p }
  
    partition_K: LEMMA partition(K(p, t1, t2))(A(p), lambda i: L(i, t1, t2))
  
    A_nonempty: JUDGEMENT A(p) HAS_TYPE non_empty_finite_set[task]
  
  
    %-------------------------------
    %  The sets L and K are finite
    %-------------------------------
  
    injection_prop: LEMMA t1 <= t2 AND n = ceiling((t2 - t1) / T(i)) 
  	IMPLIES EXISTS (h: [(L(i, t1, t2)) -> below(n)]): injective?(h)
  
    L_finite: JUDGEMENT L(i, t1, t2) HAS_TYPE finite_set[job]
  
    card_L: LEMMA t1 <= t2 IMPLIES card(L(i, t1, t2)) <= ceiling((t2 - t1)/ T(i
 ))
  
    K_finite: JUDGEMENT K(p, t1, t2) HAS_TYPE finite_set[job]
  
    bound_L: LEMMA L(i, t1, t2)(j) IMPLIES process_time(sch(u), t1, t2, j) <= C
 (i)
  
    finished_L: LEMMA
        L(i, t1, t2)(j) AND process_time(sch(u), t1, t2, j) = C(i) 	
  	IMPLIES finished(u, j, t2)
  
    process_time_L: LEMMA
       t1 <= t2 IMPLIES 
  	process_time(sch(u), t1, t2, L(i, t1, t2)) <= C(i) * ceiling((t2 - t1)/
  T(i))
  	
    max_process_time_L: LEMMA
       t1 <= t2 AND member(j, L(i, t1, t2)) AND 
  	process_time(sch(u), t1, t2, L(i, t1, t2)) = C(i) * ceiling((t2 - t1)/ 
 T(i))
  	   IMPLIES finished(u, j, t2)
  
  
    process_time_K: LEMMA
       t1 <= t2 IMPLIES 
  	process_time(sch(u), t1, t2, K(p, t1, t2)) <=
  		 sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
  
    max_process_time_K: LEMMA
       t1 < t2 AND member(j, K(p, t1, t2)) AND 
  	 process_time(sch(u), t1, t2, K(p, t1, t2)) = 
  	   sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
  		IMPLIES  finished(u, j, t2)
  
  
    %--------------------------------------------------------------
    %  Quiet time: time t such that all jobs of priority >= p 
    %    started before t are finished at t
    %---------------------------------------------------------------
  
    quiet(u, p, t): bool = 
        FORALL j: dispatch(j) < t AND prio(j) >= p IMPLIES finished(u, j, t)
  
    not_busy_quiet: LEMMA not busy(u, p, t) IMPLIES quiet(u, p, t)
  
    quiet_step: LEMMA
  	quiet(u, p, t) AND not busy(u, p, t) IMPLIES quiet(u, p, t+1)
  
    zero_is_quiet: LEMMA quiet(u, p, 0)
  
    busy_interval: LEMMA
        quiet(u, p, t1) AND t1 <= t2 IMPLIES
  	process_time(sch(u), t1, t2, K(p, t1, t2)) = process_time(sch(u), t1, t
 2, K(p))
  
    busy_interval2: LEMMA
        quiet(u, p, t1) AND t1 <= t2 IMPLIES
  	process_time(sch(u), t1, t2, K(p)) <= 
  		sum(A(p), lambda i: C(i) * ceiling((t2 - t1)/T(i)))
  
  
  
    %-----------------------------------------------------------------
    %  - M(p): smallest solution of the equation
    %  B_p + sum_{prio(i) <= p} C_i * ceiling(x / T_i)  = x
    %----------------------------------------------------------------
  
    x: VAR posreal
    d: VAR posnat
  
    bound(x, p): bool =
  	sum(A(p), lambda i: C(i) * ceiling(x / T(i))) + B(p) = x
  	
    partial_cpu_usage: LEMMA  sum(A(p), lambda i: C(i)/T(i)) < 1
  
    smallest_bound: LEMMA
  	EXISTS d: bound(d, p) AND (FORALL x: bound(x, p) IMPLIES d <= x)
  
    M(p): { d | bound(d, p) AND FORALL x: bound(x, p) IMPLIES d <= x }
  
    solution_prop: LEMMA 
  	sum(A(p), lambda i: C(i) * ceiling(M(p)/T(i))) = M(p) - B(p)
  
  
  
    %----------------
    %  Busy periods
    %----------------
  
    busy_period(u, p, t1, t2): bool =
  	t1 < t2 AND busy(u, p, t1) AND quiet(u, p, t1) AND quiet(u, p, t2) AND 
  	  FORALL t: t1 < t AND t < t2 IMPLIES not quiet(u, p, t)
  
    busy_period_prop: LEMMA
  	busy_period(u, p, t1, t2) AND t1 <= t AND t < t2 IMPLIES busy(u, p, t)
  
  
    %----------------------------------------
    %  Bound on the length of busy periods
    %----------------------------------------
  
    critical_interval: PROPOSITION
  	quiet(u, p, t1) IMPLIES
  	    EXISTS t2: t1 < t2 AND t2 <= t1 + M(p) AND quiet(u, p, t2)
  
    delay_to_quiet_time: LEMMA
  	 FORALL t: EXISTS t2: quiet(u, p, t2) AND t < t2 AND t2 <= t + M(p)
  
  
    busy_period_length: LEMMA
        busy_period(u, p, t1, t2) IMPLIES t2 - t1 <= M(p)
  
    job_in_busy_period: LEMMA
        prio(j) = p IMPLIES
           EXISTS t1, t2: t1 <= dispatch(j) AND dispatch(j) < t2 AND busy_perio
 d(u, p, t1, t2)
  
  
    %---------------------------
    %  First termination bound
    %---------------------------
  
    termination1: PROPOSITION
  	prio(j) = p IMPLIES finished(u, j, dispatch(j) + M(p))
  
  
  
    %------------------------------------------------------
    %  First schedulability criterion: M(prio(i)) <= D(i) 
    %------------------------------------------------------
  
    deadline(j): nat = dispatch(j) + D(j`1)
  
    schedulability1: PROPOSITION
          (FORALL i: M(prio(i)) <= D(i)) IMPLIES
  	    (FORALL u, j: finished(u, j, deadline(j)))
  
  
    %------------------------------------------------------
    %  Schedulability criterion in the more standard case
    %  - one task per priority
    %  - deadline before period
    %------------------------------------------------------
  
    l, l1, l2: VAR task
  
    M: VAR posnat
  
    H(i): set[task] = { l | prio(l) > prio(i) }
  
    J(i): set[task] = { l | prio(l) = prio(i) }
  
    BB(i): nat = B(prio(i))
  
    schedulability_criterion: PROPOSITION
          (FORALL l1, l2: prio(l1) = prio(l2) IMPLIES l1 = l2)
      AND (FORALL i: D(i) <= T(i))
      AND (FORALL i:
   	   EXISTS M:
  	     sum(H(i), lambda l: C(l) * ceiling(M / T(l))) + BB(i) + C(i) = M 
               AND M <= D(i))
  	IMPLIES (FORALL u, j: finished(u, j, deadline(j)))
  
  
    END sporadic_tasks
  
  
  $$$sporadic_tasks.prf
  (|sporadic_tasks|
   (|IMP_traces_TCC1| "" (LEMMA "good_ceiling") (("" (PROPAX) NIL NIL))
    NIL)
   (|IMP_traces_TCC2| "" (LEMMA "good_programs") (("" (PROPAX) NIL NIL))
    NIL)
   (|dispatch_delay| "" (SKOLEM + ("i!1" "m!1" _))
    (("" (INDUCT-AND-SIMPLIFY "n")
      (("" (USE "good_dispatch") (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|increasing_dispatch| "" (SKOSIMP)
    (("" (USE "dispatch_delay" ("m" "n!1" "n" "m!1 - n!1"))
      (("1"
        (USE "both_sides_times_pos_le1"
             ("pz" "T(i!1)" "x" "n!1 + 1" "y" "m!1"))
        (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT) NIL NIL))
      NIL))
    NIL)
   (|blocking_bound| "" (SKOLEM!)
    (("" (EXPAND "blocking")
      (("" (AUTO-REWRITE "blocking" "blocker_prio2")
        (("" (SMASH) NIL NIL)) NIL))
      NIL))
    NIL)
   (|process_time_bound| "" (SKOLEM!)
    (("" (CASE "t1!1 <= t2!1")
      (("1" (REWRITE "process_time2")
        (("1" (USE "bound_length" ("n" "j!1`2")) (("1" (ASSERT) NIL NIL))
          NIL))
        NIL)
       ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL)
   (|finished_prop| "" (SKOSIMP)
    (("" (CASE "t1!1 <= t2!1")
      (("1" (REWRITE "process_time2")
        (("1" (REWRITE "finished_equiv")
          (("1" (USE "bound_length" ("n" "j!1`2"))
            (("1" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL)
       ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL)
   (|partition_K| "" (GRIND)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
    NIL)
   (|A_nonempty| "" (SKOLEM!)
    (("" (LEMMA "topprio_is_used")
      (("" (GRIND :IF-MATCH NIL)
        (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|injection_prop| "" (SKOSIMP)
    ((""
      (INST +
       "lambda (j: (L(i!1, t1!1, t2!1))): floor((dispatch(j) - t1!1)/T(i!1))")
      (("1" (GRIND)
        (("1" (APPLY-EXTENSIONALITY :HIDE? T)
          (("1" (DELETE -2 -3 -5 -6 -7 -8)
            (("1" (AUTO-REWRITE "div_simp")
              (("1"
                (USE "increasing_dispatch" ("n" "x1!1`2" "m" "x2!1`2"))
                (("1"
                  (USE "increasing_dispatch" ("n" "x2!1`2" "m" "x1!1`2"))
                  (("1" (CASE-REPLACE "(i!1, x1!1`2) = x1!1")
                    (("1" (CASE-REPLACE "(i!1, x2!1`2) = x2!1")
                      (("1" (DELETE -1 -2)
                        (("1" (GROUND)
                          (("1"
                            (USE "both_sides_div_pos_le1"
                                 ("pz"
                                  "T(i!1)"
                                  "x"
                                  "T(i!1) + dispatch(x2!1)"
                                  "y"
                                  "dispatch(x1!1)"))
                            (("1" (REWRITE "div_distributes" -1 :DIR RL)
                              (("1" (ASSERT) NIL NIL)) NIL))
                            NIL)
                           ("2"
                            (USE "both_sides_div_pos_le1"
                                 ("pz"
                                  "T(i!1)"
                                  "x"
                                  "T(i!1) + dispatch(x1!1)"
                                  "y"
                                  "dispatch(x2!1)"))
                            (("2" (REWRITE "div_distributes" -1 :DIR RL)
                              (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (ASSERT) NIL NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (SKOLEM-TYPEPRED)
        (("2" (EXPAND "L")
          (("2" (GROUND)
            (("1" (USE "pos_div_ge" ("x" "dispatch(j!1) - t1!1"))
              (("1" (ASSERT) NIL NIL)) NIL)
             ("2"
              (USE "both_sides_div_pos_lt1"
                   ("pz" "T(i!1)" "x" "dispatch(j!1) - t1!1" "y"
                    "t2!1 - t1!1"))
              (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|L_finite| "" (SKOLEM!)
    (("" (CASE "t1!1 <= t2!1")
      (("1" (ASSERT)
        (("1" (EXPAND "is_finite")
          (("1" (NAME "n!1" "ceiling((t2!1 - t1!1) / T(i!1))")
            (("1" (USE "pos_div_ge")
              (("1" (ASSERT)
                (("1" (USE "injection_prop" ("n" "n!1"))
                  (("1" (ASSERT)
                    (("1" (SKOLEM!) (("1" (INST + "n!1" "h!1") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (ASSERT)
        (("2" (CASE-REPLACE "L(i!1, t1!1, t2!1) = emptyset")
          (("1" (ASSERT) NIL NIL)
           ("2" (DELETE 3)
            (("2" (AUTO-REWRITE "L" "emptyset")
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|card_L| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "card_def")
        ((""
          (NAME-REPLACE "n!1" "ceiling((t2!1 - t1!1) / T(i!1))" :HIDE?
           NIL)
          (("" (USE "pos_div_ge")
            (("" (ASSERT)
              (("" (REWRITE "Card_injection")
                (("" (USE "injection_prop" ("n" "n!1"))
                  (("" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|K_finite| "" (SKOLEM!)
    (("" (USE "partition_K")
      (("" (EXPAND "partition")
        (("" (GROUND)
          (("" (REPLACE*) (("" (REWRITE "union_is_finite") NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|bound_L| "" (EXPAND "L")
    (("" (SKOSIMP)
      (("" (REPLACE -1 + RL)
        (("" (REWRITE "process_time_bound") NIL NIL)) NIL))
      NIL))
    NIL)
   (|finished_L| "" (EXPAND "L")
    (("" (SKOSIMP)
      (("" (REPLACE -1 - RL)
        (("" (FORWARD-CHAIN "finished_prop") NIL NIL)) NIL))
      NIL))
    NIL)
   (|process_time_L| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "process_time_finite_set")
        (("" (USE "sum_bound[job]" ("N" "C(i!1)"))
          (("" (AUTO-REWRITE "bound_L" "card_L")
            (("" (GROUND)
              ((""
                (USE "both_sides_times_pos_le2"
                     ("x" "card(L(i!1, t1!1, t2!1))" "y"
                      "ceiling((t2!1 - t1!1) / T(i!1))" "pz" "C(i!1)"))
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_process_time_L| "" (SKOSIMP)
    (("" (REWRITE "process_time_finite_set")
      (("" (AUTO-REWRITE "bound_L" "member")
        ((""
          (CASE-REPLACE
           "ceiling((t2!1 - t1!1) / T(i!1)) = card(L(i!1, t1!1, t2!1))")
          (("1" (DELETE -1)
            (("1" (USE "sum_max_bound[job]" ("N" "C(i!1)"))
              (("1" (GROUND)
                (("1" (INST?)
                  (("1" (FORWARD-CHAIN "finished_L") NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (DELETE -2 2)
            (("2" (USE "sum_bound[job]" ("N" "C(i!1)"))
              (("2" (GROUND)
                (("2"
                  (USE "both_sides_times_pos_lt2"
                       ("pz" "C(i!1)" "x" "card(L(i!1, t1!1, t2!1))" "y"
                        "ceiling((t2!1 - t1!1) / T(i!1))"))
                  (("2" (ASSERT)
                    (("2" (USE "card_L") (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_K| (:NEW-GROUND? T) "" (SKOSIMP)
    (("" (USE "partition_K")
      (("" (USE "process_time_partition[task, job]")
        (("" (GROUND)
          (("" (REPLACE*)
            (("" (DELETE -1 -2)
              (("" (AUTO-REWRITE "process_time_L")
                (("" (REWRITE "sum_le") NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_process_time_K| "" (SKOSIMP)
    (("" (USE "partition_K")
      (("" (USE "process_time_partition[task, job]")
        (("" (GROUND)
          (("" (REPLACE*)
            (("" (DELETE -1 -2)
              (("" (USE "equal_sum_le[task]")
                ((""
                  (AUTO-REWRITE "process_time_L" "A" "K" "L" "member"
                                "prio")
                  (("" (GROUND)
                    (("" (DELETE -4)
                      (("" (REDUCE :IF-MATCH NIL)
                        (("" (INST - "j!1`1")
                          (("" (USE "max_process_time_L")
                            (("" (GROUND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|not_busy_quiet| "" (SKOSIMP)
    (("" (AUTO-REWRITE "busy" "quiet" "ready_equiv" "finished_equiv")
      (("" (REDUCE) NIL NIL)) NIL))
    NIL)
   (|quiet_step| "" (EXPAND "quiet")
    (("" (SKOSIMP*)
      (("" (INST?)
        (("" (GROUND)
          (("1" (USE "finished_stable" ("t2" "1+t!1"))
            (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (EXPAND "busy")
            (("2" (INST?)
              (("2" (USE "ready_at_dispatch") (("2" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|zero_is_quiet| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL)
   (|busy_interval| "" (SKOSIMP)
    ((""
      (USE "process_time_partition3"
           ("E" "K(p!1)" "E1"
            "{ j | prio(j) >= p!1 AND dispatch(j) < t1!1 }" "E2"
            "K(p!1, t1!1, t2!1)" "E3"
            "{ j | prio(j) >= p!1 AND t2!1 <= dispatch(j) }"))
      (("" (GROUND)
        (("1"
          (CASE "process_time(sch(u!1), t1!1, t2!1, {j: job | prio(j) >= p!1 AN
 D dispatch(j) < t1!1}) = 0 AND process_time(sch(u!1), t1!1, t2!1, {j: job | pr
 io(j) >= p!1 AND t2!1 <= dispatch(j)}) = 0")
          (("1" (GROUND) NIL NIL)
           ("2" (DELETE -1 2)
            (("2" (GROUND)
              (("1"
                (AUTO-REWRITE "active_prop" "finished_equiv"
                              "ready_equiv")
                (("1" (REWRITE "zero_process_time")
                  (("1" (SKOSIMP)
                    (("1" (FORWARD-CHAIN "active_ready")
                      (("1" (EXPAND "quiet")
                        (("1" (INST?)
                          (("1" (ASSERT)
                            (("1" (ASSERT)
                              (("1"
                                (USE "pc_increasing"
                                     ("t1" "t1!1" "t2" "t!1"))
                                (("1" (ASSERT) NIL NIL)) NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (AUTO-REWRITE "active_prop" "ready_equiv")
                (("2" (REWRITE "zero_process_time")
                  (("2" (SKOSIMP)
                    (("2" (FORWARD-CHAIN "active_ready")
                      (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE -1 -2 2)
          (("2" (GRIND)
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|busy_interval2| "" (SKOSIMP)
    (("" (REWRITE "busy_interval" :DIR RL)
      (("" (REWRITE "process_time_K") NIL NIL)) NIL))
    NIL)
   (|partial_cpu_usage| "" (SKOLEM!)
    (("" (LEMMA "cpu_usage")
      (("" (USE "sum_subset[task]" ("A" "A(p!1)" "B" "fullset[task]"))
        (("" (ASSERT)
          (("" (DELETE -1 2) (("" (GRIND :EXCLUDE ("A")) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|smallest_bound| "" (SKOLEM!)
    (("" (EXPAND "bound")
      (("" (USE "partial_cpu_usage")
        (("" (USE "smallest_int_solution[task]" ("B1" "B(p!1)"))
          (("" (ASSERT) (("" (EXPAND* "G" "F") NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (M_TCC1 ""
    (INST +
     "lambda p: epsilon! d: bound(d, p) AND (FORALL (x: posreal): bound(x, p) I
 MPLIES d <= x)")
    (("" (SKOLEM!)
      (("" (USE "epsilon_ax[posnat]")
        (("" (AUTO-REWRITE "smallest_bound") (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|solution_prop| "" (SKOLEM!)
    (("" (TYPEPRED "M(p!1)")
      (("" (DELETE -3)
        (("" (EXPAND "bound") (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|busy_period_prop| "" (EXPAND "busy_period")
    (("" (SKOSIMP)
      (("" (FORWARD-CHAIN "not_busy_quiet")
        (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|critical_interval| "" (SKOSIMP)
    (("" (CASE "busy(u!1, p!1, t1!1, t1!1+M(p!1))")
      (("1" (AUTO-REWRITE "solution_prop")
        (("1" (USE "busy_time2")
          (("1" (USE "busy_interval2")
            (("1" (ASSERT)
              (("1" (USE "blocking_bound")
                (("1" (INST + "M(p!1) + t1!1")
                  (("1" (ASSERT)
                    (("1" (EXPAND "quiet")
                      (("1" (SKOSIMP)
                        (("1" (AUTO-REWRITE "member" "K" "busy_interval")
                          (("1"
                            (USE "max_process_time_K"
                                 ("t1" "t1!1" "t2" "M(p!1) + t1!1"))
                            (("1" (GROUND)
                              (("1" (ASSERT)
                                (("1"
                                  (INST?)
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (USE
                                       "finished_stable"
                                       ("t1"
                                        "t1!1"
                                        "t2"
                                        "M(p!1) + t1!1"))
                                      (("1" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (CASE "busy(u!1, p!1, t1!1)")
        (("1" (ASSERT)
          (("1" (EXPAND "busy" +)
            (("1" (SKOSIMP)
              (("1" (INST + "t!1")
                (("1" (ASSERT)
                  (("1" (AUTO-REWRITE "not_busy_quiet")
                    (("1" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2)
          (("2" (INST + "t1!1+1")
            (("2" (GROUND)
              (("2" (FORWARD-CHAIN "quiet_step") (("2" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|delay_to_quiet_time| "" (SKOSIMP)
    (("" (USE "wf_nat")
      (("" (EXPAND "well_founded?")
        ((""
          (INST - "{ n | EXISTS t: t + n = t!1 AND quiet(u!1, p!1, t) }")
          (("" (GROUND)
            (("1" (SKOSIMP* :PREDS? T)
              (("1" (ASSERT)
                (("1" (FORWARD-CHAIN "critical_interval")
                  (("1" (SKOSIMP)
                    (("1" (INST + "t2!1")
                      (("1" (GROUND)
                        (("1" (INST - "t!1 - t2!1")
                          (("1" (ASSERT) NIL NIL)
                           ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (AUTO-REWRITE "zero_is_quiet")
              (("2" (INST + "t!1")
                (("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|busy_period_length| "" (EXPAND "busy_period")
    (("" (SKOSIMP)
      (("" (FORWARD-CHAIN "critical_interval")
        (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|job_in_busy_period| "" (SKOSIMP)
    (("" (LEMMA "wf_nat")
      (("" (EXPAND "well_founded?")
        ((""
          (INST-CP -
           "{ n | EXISTS t: t = dispatch(j!1) - n AND quiet(u!1, p!1, t) }")
          (("" (REDUCE :IF-MATCH NIL)
            (("1" (DELETE -1)
              (("1"
                (INST -
                 "{ t | dispatch(j!1) < t AND quiet(u!1, p!1, t) }")
                (("1" (REDUCE :IF-MATCH NIL)
                  (("1" (INST + "t!1" "y!2")
                    (("1" (ASSERT)
                      (("1" (EXPAND "busy_period")
                        (("1" (GROUND)
                          (("1" (CASE-REPLACE "t!1 = dispatch(j!1)")
                            (("1" (EXPAND "busy")
                              (("1" (INST?)
                                (("1"
                                  (AUTO-REWRITE "ready_at_dispatch")
                                  (("1" (ASSERT) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (REPLACE -3 - RL)
                              (("2" (FORWARD-CHAIN "quiet_step")
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (INST -7 "y!1 - 1")
                                    (("1" (ASSERT) NIL NIL)
                                     ("2"
                                      (INST + "1+t!1")
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (SKOSIMP)
                            (("2" (CASE "t!2 <= dispatch(j!1)")
                              (("1" (ASSERT)
                                (("1"
                                  (INST -10 "dispatch(j!1) - t!2")
                                  (("1" (ASSERT) NIL NIL)
                                   ("2"
                                    (INST? +)
                                    (("2" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (ASSERT)
                                (("2" (INST - "t!2") NIL NIL)) NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (DELETE -1 -2 -3 -4 2)
                    (("2"
                      (USE "delay_to_quiet_time" ("t" "dispatch(j!1)"))
                      (("2" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 -2 2)
              (("2" (AUTO-REWRITE "zero_is_quiet")
                (("2" (INST + "dispatch(j!1)")
                  (("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|termination1| "" (SKOSIMP)
    (("" (USE "delay_to_quiet_time")
      (("" (SKOSIMP)
        (("" (EXPAND "quiet")
          (("" (INST?)
            (("" (ASSERT)
              ((""
                (USE "finished_stable" ("t2" "M(p!1) + dispatch(j!1)"))
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|schedulability1| "" (SKOSIMP*)
    (("" (INST - "j!1`1")
      (("" (USE "termination1")
        (("" (ASSERT)
          (("" (AUTO-REWRITE "prio")
            (("" (ASSERT)
              (("" (USE "finished_stable" ("t2" "deadline(j!1)"))
                (("" (AUTO-REWRITE "deadline") (("" (ASSERT) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|schedulability_criterion| "" (SKOSIMP)
    (("" (REWRITE "schedulability1")
      (("" (DELETE 2)
        (("" (SKOLEM!)
          (("" (INST? -3)
            (("" (SKOSIMP)
              (("" (CASE "bound(M!1, prio(i!1))")
                (("1" (DELETE -2 -3 -4)
                  (("1" (TYPEPRED "M(prio(i!1))")
                    (("1" (INST - "M!1") (("1" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL)
                 ("2" (DELETE 2)
                  (("2" (EXPAND* "B" "bound")
                    (("2"
                      (CASE-REPLACE "A(prio(i!1)) = add(i!1, H(i!1))")
                      (("1"
                        (AUTO-REWRITE "sum_add" "member" "H" "div_simp")
                        (("1" (ASSERT)
                          (("1"
                            (CASE-REPLACE "ceiling(M!1 / T(i!1)) = 1")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (DELETE -1 -2 -4 2)
                              (("2" (INST?)
                                (("2"
                                  (USE
                                   "both_sides_div_pos_le1"
                                   ("pz"
                                    "T(i!1)"
                                    "x"
                                    "M!1"
                                    "y"
                                    "T(i!1)"))
                                  (("2"
                                    (ASSERT)
                                    (("2"
                                      (TYPEPRED "ceiling(M!1 / T(i!1))")
                                      (("2" (ASSERT :FLUSH? T) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (DELETE -2 -3 -4 2)
                        (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                          (("2" (GRIND) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$indexed_partitions.pvs
  indexed_partitions [T, U: TYPE ] : THEORY
  
    BEGIN
  
    A, B, C: VAR set[T]
    X, Y, Z: VAR set[U]
  
    F: VAR [T -> set[U]]
    
    a, b, c: VAR T
    x, y, z: VAR U
  
  
    %--------------------------------------------------------
    %  Union and intersection of a family F(a) for a in  A
    %--------------------------------------------------------
  
    union(A, F): set[U] = { x | EXISTS (a: (A)): F(a)(x) }
  
    inter(A, F): set[U] = { x | FORALL (a: (A)): F(a)(x) }
  
  
    union_upper_bound: LEMMA FORALL (a: (A)): subset?(F(a), union(A, F))
  
    inter_lower_bound: LEMMA FORALL (a: (A)): subset?(inter(A, F), F(a))
  
    union_least_upper_bound: LEMMA
  	subset?(union(A, F), X) IFF FORALL (a: (A)): subset?(F(a), X)
  
    inter_least_upper_bound: LEMMA
  	subset?(X, inter(A, F)) IFF FORALL (a: (A)): subset?(X, F(a))
  
  
    union_emptyset: LEMMA union(emptyset, F) = emptyset
  
    union_empty: LEMMA empty?(A) IMPLIES empty?(union(A, F))
  
    inter_emptyset: LEMMA inter(emptyset, F) = fullset
  
  
    %----------------------------------------
    %  Finiteness of union and intersection
    %----------------------------------------
  
    IMPORTING finite_sets@finite_sets_inductions
   
    G: VAR [T -> finite_set[U]]
    D: VAR finite_set[T]
    E: VAR (nonempty?[T])
  
    finite_inter: LEMMA 
  	(EXISTS (a: (A)): is_finite(F(a))) IMPLIES is_finite(inter(A, F))
  
    inter_is_finite: JUDGEMENT inter(E, G) HAS_TYPE finite_set[U]
  
    union_is_finite: JUDGEMENT union(D, G) HAS_TYPE finite_set[U]
  
  
  
    %--------------
    %  Partitions
    %-------------- 
  
    partition(X)(A, F): bool = 
  	X = union(A, F) AND FORALL (a, b: (A)): a = b OR disjoint?(F(a), F(b))
  
    END indexed_partitions
  
  $$$indexed_partitions.prf
  (|indexed_partitions| (|union_upper_bound| "" (GRIND) NIL NIL)
   (|inter_lower_bound| "" (GRIND) NIL NIL)
   (|union_least_upper_bound| "" (GRIND) NIL NIL)
   (|inter_least_upper_bound| "" (GRIND) NIL NIL)
   (|union_emptyset| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|union_empty| "" (GRIND) NIL NIL)
   (|inter_emptyset| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|finite_inter| "" (SKOSIMP*)
    (("" (USE "inter_lower_bound")
      (("" (FORWARD-CHAIN "finite_subset") NIL NIL)) NIL))
    NIL)
   (|inter_is_finite| "" (SKOLEM-TYPEPRED)
    (("" (REWRITE "finite_inter") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|union_is_finite| "" (SKOLEM + (_ "G!1"))
    (("" (AUTO-REWRITE "nonempty?" "union_emptyset" "finite_union[U]")
      (("" (INDUCT "D" :NAME "finite_set_induction_rest[T]")
        (("1" (ASSERT) NIL NIL)
         ("2" (SKOSIMP)
          (("2"
            (CASE-REPLACE
             "union(SS!1, G!1) = union(G!1(choose(SS!1)), union(rest(SS!1), G!1
 ))")
            (("1" (ASSERT) NIL NIL)
             ("2" (DELETE -1 2)
              (("2" (AUTO-REWRITE "union" "rest" "remove" "member")
                (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$sum_indexed_partitions.pvs
  sum_indexed_partitions  [T, U: TYPE] : THEORY
  
    BEGIN
  
    IMPORTING indexed_partitions, sum_sequences, fsets_sum
  
    F: VAR [T -> set[U]]
    A: VAR finite_set[T]
    X: VAR set[U]
    u: VAR [nat -> U]
    i: VAR T
    t1, t2: VAR nat
  
    sum_partition: LEMMA
       partition(X)(A, F) IMPLIES 
  	sum(u, t1, t2, X) = sum(A, lambda i: sum(u, t1, t2, F(i)))
  
    END sum_indexed_partitions
  
  $$$sum_indexed_partitions.prf
  (|sum_indexed_partitions|
   (|sum_partition_TCC1| "" (ASSUMING-TCC) NIL NIL)
   (|sum_partition_TCC2| "" (ASSUMING-TCC) NIL NIL)
   (|sum_partition| "" (SKOLEM + (_ "F!1" _ "t1!1" "t2!1" "u!1"))
    ((""
      (AUTO-REWRITE "sum_emptyset" "sum" "partition" "nonempty?"
                    "union_emptyset" "union_upper_bound")
      (("" (INDUCT "A" :NAME "finite_set_induction_rest[T]")
        (("1" (REDUCE)
          (("1" (REWRITE "sum_emptyset[T, real, 0, +]") NIL NIL)) NIL)
         ("2" (SKOSIMP*)
          (("2" (INST - "difference(X!1, F!1(choose(SS!1)))")
            (("2" (GROUND)
              (("1" (REWRITE "sum_diff_subset")
                (("1" (ASSERT) NIL NIL)
                 ("2" (DELETE -1 2)
                  (("2" (GRIND :EXCLUDE ("choose")) NIL NIL)) NIL))
                NIL)
               ("2" (DELETE 2)
                (("2" (GROUND)
                  (("1" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("1" (GRIND :EXCLUDE "choose") NIL NIL)) NIL)
                   ("2" (AUTO-REWRITE "rest" "remove" "member")
                    (("2" (REDUCE) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$schedules2.pvs
  schedules2  [ index, job: TYPE ]: THEORY
  
    BEGIN
  
    IMPORTING schedules, sum_indexed_partitions
  
    sch: VAR schedule[job]
    t1, t2: VAR nat
    E: VAR set[job]
    A: VAR finite_set[index]
    F: VAR [index -> set[job]] 
    i: VAR index
  
    process_time_partition: LEMMA
         partition(E)(A, F) IMPLIES
  	  process_time(sch, t1, t2, E) = sum(A, lambda i: process_time(sch, t1,
  t2, F(i)))
  
    END schedules2
  
  $$$schedules2.prf
  (|schedules2| (|process_time_partition_TCC1| "" (ASSUMING-TCC) NIL NIL)
   (|process_time_partition_TCC2| "" (ASSUMING-TCC) NIL NIL)
   (|process_time_partition| "" (SKOSIMP)
    (("" (EXPAND "process_time")
      (("" (REWRITE "sum_partition")
        (("" (DELETE 2)
          (("" (GRIND)
            (("" (DELETE -)
              (("" (APPLY-EXTENSIONALITY :HIDE? T)
                (("" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$schedules3.pvs
  schedules3 [job: TYPE] : THEORY
  
    BEGIN
  
    IMPORTING schedules2
  
    sch: VAR schedule[job]
    t1, t2: VAR nat
    A: VAR finite_set[job]
    j: VAR job
    
    process_time_finite_set: LEMMA
       process_time(sch, t1, t2, A) = sum(A, lambda j: process_time(sch, t1, t2
 , j))
  
    END schedules3
  
  $$$schedules3.prf
  (|schedules3|
   (|process_time_finite_set_TCC1| "" (ASSUMING-TCC) NIL NIL)
   (|process_time_finite_set_TCC2| "" (ASSUMING-TCC) NIL NIL)
   (|process_time_finite_set| "" (SKOLEM!)
    (("" (EXPAND "process_time" 1 2)
      (("" (REWRITE "process_time_partition")
        (("" (DELETE 2)
          (("" (GRIND)
            (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$fsets_minmax.pvs
  %---------------------------------------------------
  % Minimum/Maximum of a function over a finite set
  %---------------------------------------------------
  
  fsets_minmax [T:TYPE] : THEORY
  
    BEGIN
  
    IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
  
    S: VAR finite_set[T]
    A, B: VAR non_empty_finite_set[T]
  
    t: VAR T
    f, g: VAR [T -> real]
    x, y: VAR real
  
  
    %---------------------------------------
    %  x is the minimum of f(t) for t in S
    %--------------------------------------
  
    minimum(S, f, x): bool =
       (EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): x <= f(t))
  
    unique_minimum: LEMMA 
        minimum(S, f, x) AND minimum(S, f, y) IMPLIES x = y
  
    minimum_exists: LEMMA EXISTS x: minimum(A, f, x)
  	
    min(A, f): { x | minimum(A, f, x) }
  
    min_prop1: LEMMA FORALL (t: (A)): min(A, f) <= f(t)
  
    min_prop2: LEMMA EXISTS (t: (A)): min(A, f) = f(t)
  
    min_def: LEMMA
       min(A, f) = x IFF (EXISTS (t: (A)): x = f(t))
  		   AND (FORALL (t: (A)): x <= f(t)) 
  
  
    min_nnreal:  JUDGEMENT min(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real
    min_npreal:  JUDGEMENT min(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real
    min_posreal: JUDGEMENT min(A, (f: [T -> posreal]))     HAS_TYPE posreal
    min_negreal: JUDGEMENT min(A, (f: [T -> negreal]))     HAS_TYPE negreal
   
    min_rat:    JUDGEMENT min(A, (f: [T -> rat]))        HAS_TYPE rat
    min_nnrat:  JUDGEMENT min(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat
    min_nprat:  JUDGEMENT min(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat
    min_posrat: JUDGEMENT min(A, (f: [T -> posrat]))     HAS_TYPE posrat
    min_negrat: JUDGEMENT min(A, (f: [T -> negrat]))     HAS_TYPE negrat
  
    min_int:    JUDGEMENT min(A, (f: [T -> int]))        HAS_TYPE int
    min_nat:    JUDGEMENT min(A, (f: [T -> nat]))        HAS_TYPE nat
    min_npint:  JUDGEMENT min(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int
    min_posnat: JUDGEMENT min(A, (f: [T -> posnat]))     HAS_TYPE posnat
    min_negint: JUDGEMENT min(A, (f: [T -> negint]))     HAS_TYPE negint
  
  
    %---------------------------------------
    %  x is the maximum of f(t) for t in S
    %--------------------------------------
  
    maximum(S, f, x): bool =
       (EXISTS (t: (S)): x = f(t)) AND (FORALL (t: (S)): f(t) <= x)
  
    unique_maximum: LEMMA 
        maximum(S, f, x) AND maximum(S, f, y) IMPLIES x = y
  
    maximum_exists: LEMMA EXISTS x: maximum(A, f, x)
  	
    max(A, f): { x | maximum(A, f, x) }
  
    max_prop1: LEMMA FORALL (t: (A)): f(t) <= max(A, f) 
  
    max_prop2: LEMMA EXISTS (t: (A)): max(A, f) = f(t)
  
    max_def: LEMMA
       max(A, f) = x IFF (EXISTS (t: (A)): x = f(t))
  		   AND (FORALL (t: (A)): f(t) <= x) 
  
  
    max_nnreal:  JUDGEMENT max(A, (f: [T -> nonneg_real])) HAS_TYPE nonneg_real
    max_npreal:  JUDGEMENT max(A, (f: [T -> nonpos_real])) HAS_TYPE nonpos_real
    max_posreal: JUDGEMENT max(A, (f: [T -> posreal]))     HAS_TYPE posreal
    max_negreal: JUDGEMENT max(A, (f: [T -> negreal]))     HAS_TYPE negreal
   
    max_rat:    JUDGEMENT max(A, (f: [T -> rat]))        HAS_TYPE rat
    max_nnrat:  JUDGEMENT max(A, (f: [T -> nonneg_rat])) HAS_TYPE nonneg_rat
    max_nprat:  JUDGEMENT max(A, (f: [T -> nonpos_rat])) HAS_TYPE nonpos_rat
    max_posrat: JUDGEMENT max(A, (f: [T -> posrat]))     HAS_TYPE posrat
    max_negrat: JUDGEMENT max(A, (f: [T -> negrat]))     HAS_TYPE negrat
  
    max_int:    JUDGEMENT max(A, (f: [T -> int]))        HAS_TYPE int
    max_nat:    JUDGEMENT max(A, (f: [T -> nat]))        HAS_TYPE nat
    max_npint:  JUDGEMENT max(A, (f: [T -> nonpos_int])) HAS_TYPE nonpos_int
    max_posnat: JUDGEMENT max(A, (f: [T -> posnat]))     HAS_TYPE posnat
    max_negint: JUDGEMENT max(A, (f: [T -> negint]))     HAS_TYPE negint
  
    END fsets_minmax
  
  $$$fsets_minmax.prf
  (|fsets_minmax|
   (|unique_minimum| "" (SKOLEM!)
    (("" (GRIND :IF-MATCH NIL)
      (("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|minimum_exists| "" (SKOLEM + (_ "f!1"))
    (("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
      (("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL))
        NIL)
       ("2" (SKOSIMP*)
        (("2" (INST + "min(x!1, f!1(e!1))")
          (("2" (GRIND :IF-MATCH NIL)
            (("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL)
             ("4" (INST? + :IF-MATCH ALL) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|min_TCC1| "" (INST + "lambda A, f: epsilon! x: minimum(A, f, x)")
    (("" (SKOLEM!)
      (("" (USE "epsilon_ax[real]")
        (("" (AUTO-REWRITE "minimum_exists") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 )
      NIL))
    NIL)
   (|min_prop1| "" (SKOLEM!)
    (("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|min_prop2| "" (SKOLEM!)
    (("" (TYPEPRED "min(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|min_def| "" (SKOLEM!)
    (("" (REWRITE "minimum" :DIR RL)
      (("" (GROUND)
        (("" (TYPEPRED "min(A!1, f!1)")
          (("" (USE "unique_minimum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|min_nnreal| "" (SKOLEM!)
    (("" (USE "min_prop2") (("" (REDUCE) NIL NIL)) NIL)) NIL)
   (|min_npreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_posreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_negreal| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_rat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_nnrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_nprat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_posrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_negrat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_int| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_nat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_npint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_posnat| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|min_negint| "" (SKOLEM!) (("" (USE "min_prop2") (("" (REDUCE) NIL)))))
   (|unique_maximum| "" (SKOLEM!)
    (("" (GRIND :IF-MATCH NIL)
      (("" (INST - "t!2") (("" (INST - "t!1") (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|maximum_exists| "" (SKOLEM + (_ "f!1"))
    (("" (INDUCT "A" :NAME "nonempty_finite_set_induct[T]")
      (("1" (SKOLEM!) (("1" (INST + "f!1(e!1)") (("1" (GRIND) NIL NIL)) NIL))
        NIL)
       ("2" (SKOSIMP*)
        (("2" (INST + "max(x!1, f!1(e!1))")
          (("2" (GRIND :IF-MATCH NIL)
            (("1" (INST? :IF-MATCH ALL) (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (INST?) NIL NIL) ("3" (INST? + :IF-MATCH ALL) NIL NIL)
             ("4" (INST? + :IF-MATCH ALL) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_TCC1| "" (INST + "lambda A, f: epsilon! x: maximum(A, f, x)")
    (("" (AUTO-REWRITE "maximum_exists")
      (("" (SKOLEM!) (("" (USE "epsilon_ax[real]") (("" (ASSERT) NIL NIL)) NIL)
 )
        NIL))
      NIL))
    NIL)
   (|max_prop1| "" (SKOLEM!)
    (("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|max_prop2| "" (SKOLEM!)
    (("" (TYPEPRED "max(A!1, f!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|max_def| "" (SKOLEM!)
    (("" (REWRITE "maximum" :DIR RL)
      (("" (GROUND)
        (("" (TYPEPRED "max(A!1, f!1)")
          (("" (USE "unique_maximum") (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|max_nnreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_npreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_posreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_negreal| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_rat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_nnrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_nprat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_posrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_negrat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_int| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_nat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_npint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_posnat| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL)))))
   (|max_negint| "" (SKOLEM!) (("" (USE "max_prop2") (("" (REDUCE) NIL))))))
  
  
  $$$ceiling_equations.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %   Equations of the form                %
  %                                        %
  %   Sum C_i * ceiling(x/T_i) + B = x     %
  %                                        % 
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  ceiling_equations[U: TYPE] : THEORY
  
    BEGIN
  
    IMPORTING fsets_sum[U], fsets_minmax[U]
  
  %% IMPORTING fsets_sum, fsets_minmax sould work but judgements are not visibl
 e
  
    i: VAR U
    A: VAR finite_set[U]
    E: VAR non_empty_finite_set[U]
    C, T: VAR [U -> posreal]
    B: VAR nonneg_real
    x, y: VAR nonneg_real
    c, z, w: VAR posreal
    n, m: VAR nat
   
  
    %----------------------------------
    %  F(C, T, x): a term in the sum
    %----------------------------------
  
    F(C, T, x)(i): nonneg_real = C(i) * ceiling(x / T(i))
    
    low_F1: LEMMA x * (C(i) / T(i)) <= F(C, T, x)(i)
  
    low_F2: LEMMA C(i) <= F(C, T, z)(i)
  
    high_F: LEMMA F(C, T, x)(i) < C(i) + x * (C(i) / T(i))
  
    increasing_F: LEMMA x <= y IMPLIES F(C, T, x)(i) <= F(C, T, y)(i)
    
    increasing_F2: LEMMA x <= y IMPLIES 
  	F(C, T, x)(i) = F(C, T, y)(i) OR F(C, T, x)(i) + C(i) <= F(C, T, y)(i)
    
    F_zero: LEMMA F(C, T, 0)(i) = 0
  
    F_posreal: JUDGEMENT F(C, T, z) HAS_TYPE [U -> posreal]
  
  
  
    %-------------------------------------
    %  G(A, C, T, x): the sum for i in A
    %-------------------------------------
  
    G(A, C, T, x): nonneg_real = sum(A, F(C, T, x))
  
    low_G1: LEMMA x * sum(A, lambda i: C(i)/T(i)) <= G(A, C, T, x)
  
    low_G2: LEMMA sum(A, C) <= G(A, C, T, z)
  
    high_G1: LEMMA G(A, C, T, x) <= x * sum(A, lambda i: C(i)/T(i)) + sum(A, C)
  
    high_G2: LEMMA not empty?(A) IMPLIES 
  	G(A, C, T, x) < x * sum(A, lambda i: C(i)/T(i)) + sum(A, C)
  
    increasing_G: LEMMA x <= y IMPLIES G(A, C, T, x) <= G(A, C, T, y)
  
    increasing_G2: LEMMA
  	 x <= y IMPLIES G(A, C, T, x) = G(A, C, T, y) 
        OR (EXISTS i: A(i) AND G(A, C, T, x) + C(i) <= G(A, C, T, y))
  
    G_zero: LEMMA G(A, C, T, 0) = 0
  
    G_empty: LEMMA empty?(A) IMPLIES G(A, C, T, x) = 0
  
    G_posreal: JUDGEMENT G(E, C, T, z) HAS_TYPE posreal
  
  
  
    %---------------------------------
    %  u(0) = B + sum(E, C)
    %  u(n+1) = B + G(E, C, T, u(n))
    %---------------------------------
  
    u(E, B, C, T)(n): RECURSIVE posreal = 
        IF n=0 THEN B + sum(E, C) ELSE B + G(E, C, T, u(E, B, C, T)(n - 1)) END
 IF
      MEASURE n
  
    increasing_u1: LEMMA u(E, B, C, T)(n) <= u(E, B, C, T)(n + 1)
  
    increasing_u2: LEMMA 
  	u(E, B, C, T)(n) = u(E, B, C, T)(n+1) 
       OR EXISTS i: E(i) AND u(E, B, C, T)(n) + C(i) <= u(E, B, C, T)(n + 1)
  
    increasing_u3: LEMMA n <= m IMPLIES u(E, B, C, T)(n) <= u(E, B, C, T)(m)
  
    fixed_point: LEMMA (EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n))
  	  OR (EXISTS c: FORALL n: u(E, B, C, T)(n) >= n * c + B + sum(E, C))
  
  
    least_fixed_point: LEMMA
         B + G(E, C, T, z) = z IMPLIES FORALL n: u(E, B, C, T)(n) <= z
  
    fixed_point_prop: LEMMA
         z < u(E, B, C, T)(n) IMPLIES z < B + G(E, C, T, z) 
    
    
  
    %--------------------------
    %  Existence of solutions
    %--------------------------
  
    upper_bound1: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES 
  	 EXISTS z: G(E, C, T, z) + B <= z
  
    upper_bound2: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES 
  	 EXISTS z: FORALL n: u(E, B, C, T)(n) <= z
  
    fixed_point_exists: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES 
  	 EXISTS n: u(E, B, C, T)(n + 1) = u(E, B, C, T)(n)
  
  
    %--------------------
    %   Main results 
    %--------------------
  
    solution_exists: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES EXISTS z: G(E, C, T, z) + B = z
  
    smallest_solution: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
  	 EXISTS z: G(E, C, T, z) + B = z 
  		   AND FORALL w: G(E, C, T, w) + B = w IMPLIES z <= w
  
    smallest_solution2: LEMMA
        sum(E, lambda i: C(i)/T(i)) < 1 IMPLIES
  	 EXISTS z: G(E, C, T, z) + B = z AND 
  	    (FORALL w: G(E, C, T, w) + B <= w IMPLIES z <= w)
  
  
    %---------------------------------------------------
    %  Case when C(i) and T(i) are posnat and B is nat
    %---------------------------------------------------
  
    C1, T1: VAR [U -> posnat]
    B1: VAR nat
    q: VAR posnat
  
    integer_solution: LEMMA
        sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES EXISTS q: G(E, C1, T1, q) + B
 1 = q
  
    smallest_int_solution: LEMMA
        sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES
  	EXISTS q: G(E, C1, T1, q) + B1 = q
  		   AND FORALL w: G(E, C1, T1, w) + B1 = w IMPLIES q <= w
  
    smallest_int_solution2: LEMMA
        sum(E, lambda i: C1(i)/T1(i)) < 1 IMPLIES
  	EXISTS q: G(E, C1, T1, q) + B1 = q 
  		AND (FORALL w: G(E, C1, T1, w) + B1 <= w IMPLIES q <= w)
  
    END ceiling_equations
  
  
  $$$ceiling_equations.prf
  (|ceiling_equations|
   (|low_F1| "" (EXPAND "F")
    (("" (SKOLEM!)
      (("" (USE "both_sides_times_pos_le1" ("pz" "C!1(i!1)" "x" "x!1/T!1(i!1)" 
 "y" "ceiling(x!1 / T!1(i!1))"))
        (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|low_F2| "" (EXPAND "F")
    (("" (SKOLEM!)
      (("" (USE "both_sides_times_pos_le2" ("pz" "C!1(i!1)" "x" "1" "y" "ceilin
 g(z!1 / T!1(i!1))"))
        (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|high_F| "" (EXPAND "F")
    (("" (SKOLEM!)
      ((""
        (USE "both_sides_times_pos_lt1"
             ("pz" "C!1(i!1)" "x" "ceiling(x!1/T!1(i!1))" "y" "1 + x!1 / T!1(i!
 1)"))
        (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|increasing_F| "" (EXPAND "F")
    (("" (SKOSIMP)
      (("" (REWRITE "both_sides_times_pos_le2")
        (("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL))
  NIL)) NIL))
      NIL))
    NIL)
   (|increasing_F2| "" (EXPAND "F")
    (("" (SKOSIMP)
      (("" (REWRITE "both_sides_times2")
        ((""
          (USE "both_sides_times_pos_le2"
               ("pz" "C!1(i!1)" "x" "1 + ceiling(x!1 / T!1(i!1))" "y" "ceiling(
 y!1 / T!1(i!1))"))
          (("" (USE "both_sides_div_pos_le1" ("y" "y!1")) (("" (ASSERT) NIL NIL
 )) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|F_zero| "" (GRIND) NIL NIL)
   (|F_posreal| "" (EXPAND "F")
    (("" (SKOLEM!) (("" (REWRITE "pos_times_gt") (("" (ASSERT) NIL NIL)) NIL)) 
 NIL)) NIL)
   (|low_G1| "" (EXPAND "G")
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "low_F1" "sum_mult")
        (("" (USE "sum_le" ("f" "lambda i: x!1 * (C!1(i) / T!1(i))" "g" "F(C!1,
  T!1, x!1)"))
          (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|low_G2| "" (SKOLEM!)
    (("" (EXPAND "G") (("" (REWRITE "sum_le") (("" (SKOLEM!) (("" (REWRITE "low
 _F2") NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|high_G1| "" (EXPAND "G")
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "sum_mult")
        (("" (USE "sum_le" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: x!1 * (C!1(i)
  / T!1(i)) + C!1(i)"))
          (("" (GROUND)
            (("1" (REWRITE "sum_distributive" :DIR RL) NIL NIL)
             ("2" (SKOLEM!) (("2" (USE "high_F") (("2" (ASSERT) NIL NIL)) NIL))
  NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|high_G2| "" (EXPAND "G")
    (("" (SKOSIMP)
      (("" (ASSERT)
        (("" (AUTO-REWRITE "sum_mult" "high_F")
          (("" (USE "sum_lt" ("f" "F(C!1, T!1, x!1)" "g" "lambda i: C!1(i) + x!
 1 * (C!1(i) / T!1(i))"))
            (("" (ASSERT) (("" (REWRITE "sum_distributive" :DIR RL) NIL NIL)) N
 IL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|increasing_G| "" (AUTO-REWRITE "G" "sum_le" "increasing_F") (("" (REDUCE) 
 NIL NIL)) NIL)
   (|increasing_G2| "" (SKOSIMP)
    (("" (EXPAND "G")
      (("" (REWRITE "sum_f_g")
        (("" (DELETE 2)
          (("" (SKOLEM!)
            (("" (USE "increasing_F2")
              (("" (GROUND)
                (("" (INST?)
                  (("" (ASSERT)
                    ((""
                      (USE "sum_update"
                           ("f" "F(C!1, T!1, x!1)" "t" "x!2" "c" "C!1(x!2) + F(
 C!1, T!1, x!1)(x!2)"))
                      (("" (ASSERT)
                        ((""
                          (USE "sum_le"
                               ("f" "F(C!1, T!1, x!1) WITH [(x!2) := F(C!1, T!1
 , x!1)(x!2) + C!1(x!2)]" "g"
                                "F(C!1, T!1, y!1)"))
                          (("" (GROUND)
                            (("" (DELETE -1 2 3)
                              (("" (AUTO-REWRITE "increasing_F") (("" (REDUCE) 
 NIL NIL)) NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|G_zero| "" (EXPAND "G")
    (("" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (SKOLEM!) (("" (REWRITE "F_ze
 ro") NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|G_empty| "" (EXPAND "G")
    (("" (SKOSIMP)
      (("" (REWRITE "emptyset_is_empty?") (("" (REPLACE*) (("" (REWRITE "sum_em
 ptyset") NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|G_posreal| "" (SKOLEM!) (("" (EXPAND "G") (("" (ASSERT) NIL NIL)) NIL)) NI
 L)
   (|u_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|u_TCC2| "" (TERMINATION-TCC) NIL NIL)
   (|increasing_u1| "" (INDUCT-AND-REWRITE "n" 1 "u")
    (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
     ("2"
      (USE "increasing_G"
           ("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "G(E!1, C!1, T!1, u(E!1, B!1, 
 C!1, T!1)(j!1)) + B!1"))
      (("2" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|increasing_u2| "" (SKOSIMP)
    (("" (AUTO-REWRITE "u")
      (("" (CASE-REPLACE "n!1 = 0")
        (("1" (ASSERT)
          (("1" (CASE "EXISTS c: c <= sum(E!1, C!1) AND G(E!1, C!1, T!1, c) = s
 um(E!1, C!1)")
            (("1" (SKOSIMP)
              (("1" (USE "increasing_G2" ("x" "c!1" "y" "sum(E!1, C!1) + B!1"))
  (("1" (REDUCE) NIL NIL)) NIL))
              NIL)
             ("2" (DELETE -1 2 3)
              (("2" (INST + "min(sum(E!1, C!1), min(E!1, T!1))")
                (("2" (AUTO-REWRITE "G" "F" "div_simp")
                  (("2" (GROUND)
                    (("2" (REWRITE "sum_f_g")
                      (("2" (DELETE 2)
                        (("2" (SKOLEM!)
                          (("2" (CASE-REPLACE "ceiling(min(sum(E!1, C!1), min(E
 !1, T!1)) / T!1(x!1)) = 1")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (DELETE 2)
                              (("2" (USE "min_prop1" ("A" "E!1" "f" "T!1"))
                                (("2"
                                  (USE "both_sides_div_pos_le1"
                                       ("x" "min(sum(E!1, C!1), min(E!1, T!1))"
  "y" "T!1(x!1)" "pz"
                                        "T!1(x!1)"))
                                  (("2" (ASSERT)
                                    (("2" (TYPEPRED "ceiling(min(sum(E!1, C!1),
  min(E!1, T!1)) / T!1(x!1))")
                                      (("2" (ASSERT :FLUSH? T) NIL NIL)) NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (ASSERT)
          (("2" (USE "increasing_G2" ("x" "u(E!1, B!1, C!1, T!1)(n!1 - 1)" "y" 
 "u(E!1, B!1, C!1, T!1)(n!1)"))
            (("2" (REWRITE "increasing_u1") (("2" (REDUCE) NIL NIL)) NIL)) NIL)
 )
          NIL))
        NIL))
      NIL))
    NIL)
   (|increasing_u3| "" (SKOSIMP)
    (("" (CASE "FORALL n: u(E!1, B!1, C!1, T!1)(n!1) <= u(E!1, B!1, C!1, T!1)(n
 !1 + n)")
      (("1" (ASSERT) (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)) 
 NIL)
       ("2" (DELETE -1 2)
        (("2" (INDUCT "n")
          (("1" (ASSERT) NIL NIL)
           ("2" (SKOSIMP) (("2" (USE "increasing_u1" ("n" "n!1 + j!1")) (("2" (
 ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|fixed_point| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (INST 2 "min(E!1, C!1)")
        (("" (INDUCT "n" 2)
          (("1" (AUTO-REWRITE "u") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (SKOSIMP)
            (("2" (USE "increasing_u2")
              (("2" (GROUND)
                (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (SKOSIMP) (("2" (USE "min_prop1") (("2" (ASSERT) NIL NIL)
 ) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|least_fixed_point| "" (SKOSIMP)
    (("" (INDUCT-AND-REWRITE "n" 1 "u")
      (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|fixed_point_prop| "" (SKOLEM + ("B!1" "C!1" "E!1" "T!1" _ "z!1"))
    (("" (INDUCT-AND-REWRITE "n" 1 "u")
      (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (USE "increasing_G" ("x" "u(E!1, B!1, C!1, T!1)(j!1)" "y" "z!1")) (
 ("2" (GROUND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|upper_bound1| "" (SKOSIMP)
    (("" (CASE "EXISTS x: x * sum(E!1, lambda i: C!1(i)/T!1(i)) + sum(E!1, C!1)
  + B!1 = x")
      (("1" (SKOLEM!)
        (("1" (ASSERT) (("1" (INST + "x!1") (("1" (USE "high_G1") (("1" (ASSERT
 ) NIL NIL)) NIL)) NIL)) NIL))
        NIL)
       ("2" (DELETE 2)
        (("2" (NAME-REPLACE "a!1" "sum(E!1, LAMBDA (i: U): C!1(i) / T!1(i))")
          (("2" (ASSERT)
            (("2" (INST + "(sum(E!1, C!1) + B!1) / (1 - a!1)")
              (("1" (USE "div_cancel2" ("x" "sum(E!1, C!1) + B!1" "n0z" "1 - a!
 1")) (("1" (ASSERT) NIL NIL))
                NIL)
               ("2" (REWRITE "pos_div_ge") (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|upper_bound2| "" (SKOSIMP)
    (("" (USE "upper_bound1" ("B" "B!1"))
      (("" (ASSERT)
        (("" (SKOLEM!)
          (("" (INST?)
            (("" (INDUCT-AND-REWRITE "n" 1 "u")
              (("1" (USE "low_G2") (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (USE "increasing_G" ("y" "z!1")) (("2" (ASSERT) NIL NIL)) N
 IL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|fixed_point_exists| "" (SKOSIMP)
    (("" (USE "fixed_point")
      (("" (GROUND)
        (("" (USE "upper_bound2")
          (("" (ASSERT)
            (("" (SKOSIMP*)
              (("" (DELETE -3 1)
                (("" (CASE "EXISTS n: (z!1 - B!1)/c!1 < n")
                  (("1" (SKOLEM!)
                    (("1" (REWRITE "div_mult_pos_lt1")
                      (("1" (INST - "n!1") (("1" (INST - "n!1") (("1" (ASSERT) 
 NIL NIL)) NIL)) NIL)) NIL))
                    NIL)
                   ("2" (DELETE -)
                    (("2" (LEMMA "axiom_of_archimedes" ("x" "(z!1 - B!1) / c!1"
 ))
                      (("2" (SKOLEM!)
                        (("2" (CASE "i!1 < 0")
                          (("1" (INST + "0") (("1" (ASSERT) NIL NIL)) NIL)
                           ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|solution_exists| "" (SKOSIMP)
    (("" (USE "fixed_point_exists" ("B" "B!1"))
      (("" (AUTO-REWRITE "u")
        (("" (ASSERT) (("" (SKOLEM!) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL))
  NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|smallest_solution| "" (SKOSIMP)
    (("" (USE "fixed_point_exists" ("B" "B!1"))
      (("" (AUTO-REWRITE "u")
        (("" (ASSERT)
          (("" (SKOLEM!)
            (("" (INST?)
              (("" (GROUND)
                (("" (SKOSIMP) (("" (USE "least_fixed_point") (("" (ASSERT) (("
 " (INST?) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|smallest_solution2| "" (SKOSIMP)
    (("" (USE "fixed_point_exists" ("B" "B!1"))
      (("" (AUTO-REWRITE "u")
        (("" (ASSERT)
          (("" (SKOLEM!)
            (("" (INST?)
              (("" (GROUND)
                (("" (SKOSIMP)
                  (("" (USE "fixed_point_prop" ("z" "w!1" "n" "n!1")) (("" (ASS
 ERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|integer_solution| "" (SKOSIMP)
    (("" (USE "solution_exists" ("B" "B1!1"))
      (("" (ASSERT)
        (("" (SKOLEM!)
          (("" (INST?) (("" (EXPAND "G") (("" (EXPAND "F") (("" (ASSERT) NIL NI
 L)) NIL)) NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|smallest_int_solution| "" (SKOSIMP)
    (("" (USE "smallest_solution" ("B" "B1!1"))
      (("" (ASSERT)
        (("" (SKOSIMP)
          (("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (
 ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|smallest_int_solution2| "" (SKOSIMP)
    (("" (USE "smallest_solution2" ("B" "B1!1"))
      (("" (ASSERT)
        (("" (SKOSIMP)
          (("" (INST? +) (("1" (GROUND) NIL NIL) ("2" (EXPAND* "G" "F") (("2" (
 ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$sum_partitions.pvs
  sum_partitions  [ T: TYPE] : THEORY
  
    BEGIN
  
    IMPORTING sum_sequences[T]
  
    A, B, C, D, X: VAR set[T]
  
    u: VAR [nat -> T]
  
    t, t1, t2, n: VAR nat
  
    
    partition2(X)(A, B): bool = disjoint?(A, B) AND X = union(A, B)
  
    partition3(X)(A, B, C): bool = 
      disjoint?(A, B) AND partition2(X)(union(A, B), C)
  
    partition4(X)(A, B, C, D): bool=
      disjoint?(A, B) AND disjoint?(C, D) AND 
  	partition2(X)(union(A, B), union(C, D))
  
  
  
    sum_partition2: LEMMA 
       partition2(X)(A, B) IMPLIES 
  	sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B)
  
    sum_partition3: LEMMA
       partition3(X)(A, B, C) IMPLIES 
  	sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) + sum(u, t1, 
 t2, C)
  
    sum_partition4: LEMMA
       partition4(X)(A, B, C, D) IMPLIES 
  	sum(u, t1, t2, X) = sum(u, t1, t2, A) + sum(u, t1, t2, B) 
  			  + sum(u, t1, t2, C) + sum(u, t1, t2, D)
  
    END sum_partitions
  
  $$$sum_partitions.prf
  (|sum_partitions|
   (|sum_partition2| "" (AUTO-REWRITE "partition2" "sum_disj_union")
    (("" (REDUCE) NIL NIL)) NIL)
   (|sum_partition3| ""
    (AUTO-REWRITE "partition3" "partition2" "sum_disj_union")
    (("" (REDUCE) NIL NIL)) NIL)
   (|sum_partition4| ""
    (AUTO-REWRITE "partition4" "partition2" "sum_disj_union")
    (("" (REDUCE) NIL NIL)) NIL))
  
  
  $$$sum_sequences.pvs
  sum_sequences [ T: TYPE] : THEORY
  
    BEGIN
  
    u, u1, u2: VAR [nat -> T]
    t, t1, t2, t3, n: VAR nat
    E, E1, E2: VAR set[T]
  
    %------------------------------------------------------------------------
    %  sum(u, t1, t2, E) = card { t | t1 <= t < t2 AND u(t) belongs to E }
    %------------------------------------------------------------------------
  
    sum(u, t1, t2, E): RECURSIVE nat =
       IF t2 <= t1 THEN 0 
  	ELSIF E(u(t2-1)) THEN 1 + sum(u, t1, t2-1, E) 
           ELSE sum(u, t1, t2-1, E) ENDIF
      MEASURE max(t2 - t1, 0)
  
  
    %% Auxiliary lemmas for inductive proofs
  
    sum_init: LEMMA sum(u, t, t, E) = 0
  
    sum_step: LEMMA 
       sum(u, t, t + n + 1, E) = 
  	IF E(u(t + n)) THEN 1 + sum(u, t, t + n, E) ELSE sum(u, t, t + n, E) EN
 DIF
  
  
    %-----------------------
    %  Bounds & splitting
    %-----------------------
  
    max_sum: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, E) <= t2 - t1
  
    sum_zero: LEMMA 
       sum(u, t1, t2, E) = 0 IFF FORALL t: t1 <= t AND t < t2 IMPLIES not E(u(t
 ))
  
    sum_full: LEMMA
       sum(u, t1, t2, E) = t2 - t1 IFF
  	t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES E(u(t))
  
    sum_split: LEMMA
        t1 <= t AND t <= t2 IMPLIES 
  	 sum(u, t1, t, E) + sum(u, t, t2, E) = sum(u, t1, t2, E)
  
    sum_increasing: LEMMA
        t1 <= t2 AND t2 <= t3 IMPLIES sum(u, t1, t2, E) <= sum(u, t1, t3, E)
  
    equal_sums: LEMMA
        (FORALL (t | t1 <= t AND t < t2): E(u1(t)) IFF E(u2(t)))
  	  IMPLIES sum(u1, t1, t2, E) = sum(u2, t1, t2, E)
  
  
    %-------------------------
    %  sum for various sets
    %-------------------------
  
    sum_emptyset: LEMMA sum(u, t1, t2, emptyset) = 0
  
    sum_fullset: LEMMA t1 <= t2 IMPLIES sum(u, t1, t2, fullset) = t2 - t1
  
    sum_disj_union: LEMMA disjoint?(E1, E2) IMPLIES
  	sum(u, t1, t2, union(E1, E2)) = sum(u, t1, t2, E1) + sum(u, t1, t2, E2)
  
    sum_diff_subset: LEMMA subset?(E1, E2) IMPLIES
  	sum(u, t1, t2, difference(E2, E1)) = sum(u, t1, t2, E2) - sum(u, t1, t2
 , E1)
  
    sum_union_inter: LEMMA 
  	sum(u, t1, t2, union(E1, E2)) + sum(u, t1, t2, intersection(E1, E2)) = 
  		sum(u, t1, t2, E1) + sum(u, t1, t2, E2)
  
    sum_complement: LEMMA
  	t1 <= t2 IMPLIES sum(u, t1, t2, complement(E)) = t2 - t1 - sum(u, t1, t
 2, E)
  	
  
    sum_subset: LEMMA subset?(E1, E2) IMPLIES sum(u, t1, t2, E1) <= sum(u, t1, 
 t2, E2)
  
    sum_union1: LEMMA sum(u, t1, t2, E1) <= sum(u, t1, t2, union(E1, E2))
  
    sum_union2: LEMMA sum(u, t1, t2, E2) <= sum(u, t1, t2, union(E1, E2))
 	
  
    sum_inter1: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E1
 )
  
    sum_inter2: LEMMA sum(u, t1, t2, intersection(E1, E2)) <= sum(u, t1, t2, E2
 )
  
    END sum_sequences
  
  $$$sum_sequences.prf
  (|sum_sequences| (|sum_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_TCC2| "" (SUBTYP
 E-TCC) NIL NIL)
   (|sum_TCC3| "" (TERMINATION-TCC) NIL NIL) (|sum_TCC4| "" (SUBTYPE-TCC) NIL N
 IL)
   (|sum_init| "" (GRIND) NIL NIL) (|sum_step| "" (GRIND) NIL NIL)
   (|max_sum| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, E!1) <= n")
        (("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE -1 2)
          (("2" (INDUCT-AND-SIMPLIFY "n" 1 :DEFS NIL :REWRITES ("sum_init" ("su
 m_step"))) NIL
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_zero| "" (SKOLEM!)
    (("" (CASE "t2!1 < t1!1")
      (("1" (GRIND) NIL NIL)
       ("2" (ASSERT)
        (("2"
          (CASE "FORALL n: sum(u!1, t1!1, t1!1 + n, E!1) = 0 IFF (FORALL t: t <
 n IMPLIES not E!1(u!1(t1!1 + t)))")
          (("1" (INST - "t2!1 - t1!1")
            (("1" (REDUCE :IF-MATCH NIL)
              (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("2" (DELETE 2 3)
            (("2"
              (INDUCT-AND-SIMPLIFY "n" :IF-MATCH BEST :DEFS NIL :REWRITES
               ("sum_init" ("sum_step")))
              NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_full| "" (SKOLEM!)
    (("" (CASE "t2!1 < t1!1")
      (("1" (GRIND) NIL NIL)
       ("2" (ASSERT)
        (("2"
          (CASE "FORALL n: sum(u!1, t1!1, t1!1 + n, E!1) = n IFF (FORALL t: t <
 n IMPLIES E!1(u!1(t1!1 + t)))")
          (("1" (INST - "t2!1 - t1!1")
            (("1" (REDUCE :IF-MATCH NIL)
              (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("2" (DELETE 2 3)
            (("2" (AUTO-REWRITE "sum_init" "sum_step")
              (("2" (INDUCT "n")
                (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)
                 ("3" (SKOSIMP)
                  (("3" (CASE "E!1(u!1(t1!1 + j!1))")
                    (("1" (ASSERT)
                      (("1" (GROUND)
                        (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) 
 NIL)) NIL)
                         ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) 
 NIL)) NIL))
                        NIL))
                      NIL)
                     ("2" (DELETE -)
                      (("2" (ASSERT)
                        (("2" (USE "max_sum")
                          (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL))
  NIL)) NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_split| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: sum(u!1, t1!1, t!1, E!1) + sum(u!1, t!1, t!1 + n, E!1) =
  sum(u!1, t1!1, t!1 + n, E!1)")
      (("1" (INST - "t2!1 - t!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL
 )) NIL)
       ("2" (DELETE 2)
        (("2" (INDUCT-AND-REWRITE "n" 1 "sum_init")
          (("2" (USE "sum_step" ("t" "t!1" "n" "j!1"))
            (("2" (USE "sum_step" ("t" "t1!1" "n" "j!1 + t!1 - t1!1")) (("2" (S
 MASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_increasing| "" (SKOSIMP)
    (("" (USE "sum_split" ("t2" "t3!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)
   (|equal_sums| "" (SKOSIMP)
    (("" (CASE "t2!1 <= t1!1")
      (("1" (ASSERT) (("1" (EXPAND "sum") (("1" (PROPAX) NIL NIL)) NIL)) NIL)
       ("2" (ASSERT)
        (("2"
          (CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES sum(u1!1, t1!1, t1!1 + n, E
 !1) = sum(u2!1, t1!1, t1!1 + n, E!1)")
          (("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE 2 3)
            (("2" (AUTO-REWRITE "sum_init")
              (("2" (INDUCT "n")
                (("1" (ASSERT) NIL NIL)
                 ("2" (SKOSIMP)
                  (("2" (ASSERT)
                    (("2" (USE "sum_step")
                      (("2" (USE "sum_step" ("u" "u2!1"))
                        (("2" (INST?) (("2" (SMASH) NIL NIL)) NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_emptyset| "" (SKOLEM!) (("" (REWRITE "sum_zero") (("" (GRIND) NIL NIL)
 ) NIL)) NIL)
   (|sum_fullset| "" (SKOSIMP) (("" (REWRITE "sum_full") (("" (GRIND) NIL NIL))
  NIL)) NIL)
   (|sum_disj_union| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) = sum(u!1, t1!
 1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
      (("1" (INST - "t2!1 - t1!1")
        (("1" (ASSERT) NIL NIL)
         ("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
 )
        NIL)
       ("2" (DELETE 2)
        (("2"
          (INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
 ) :THEORIES
           ("sets[T]"))
          NIL NIL))
        NIL))
      NIL))
    NIL)
   (|sum_diff_subset| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, difference(E2!1, E1!1)) = sum(u!1
 , t1!1, t1!1+n, E2!1) - sum(u!1, t1!1, t1!1+n, E1!1)")
      (("1" (INST - "t2!1 - t1!1")
        (("1" (ASSERT) NIL NIL)
         ("2" (ASSERT) (("2" (EXPAND "sum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)
 )
        NIL)
       ("2" (DELETE 2)
        (("2"
          (INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_step")
 ) :THEORIES
           ("sets[T]"))
          NIL NIL))
        NIL))
      NIL))
    NIL)
   (|sum_union_inter| "" (SKOLEM!)
    (("" (CASE "t2!1 <= t1!1")
      (("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT)
        (("2"
          (CASE "FORALL n: sum(u!1, t1!1, t1!1+n, intersection(E1!1, E2!1)) + s
 um(u!1, t1!1, t1!1+n, union(E1!1, E2!1)) = 
  sum(u!1, t1!1, t1!1+n, E1!1) + sum(u!1, t1!1, t1!1+n, E2!1)")
          (("1" (INST - "t2!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE 2 3)
            (("2"
              (INDUCT-AND-SIMPLIFY "n" :DEFS NIL :REWRITES ("sum_init" ("sum_st
 ep")) :THEORIES
               ("sets[T]"))
              NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_complement| "" (SKOSIMP)
    (("" (AUTO-REWRITE "sum_fullset")
      (("" (ASSERT)
        (("" (USE "sum_disj_union" ("E1" "E!1" "E2" "complement(E!1)"))
          (("" (GROUND)
            (("1" (CASE-REPLACE "union(E!1, complement(E!1)) = fullset")
              (("1" (ASSERT) NIL NIL)
               ("2" (DELETE -1 -2 2)
                (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) N
 IL)) NIL))
              NIL)
             ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_subset| "" (SKOSIMP)
    (("" (CASE "t2!1 <= t1!1")
      (("1" (AUTO-REWRITE "sum") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT)
        (("2" (USE "sum_diff_subset" ("E2" "E2!1")) (("2" (ASSERT) (("2" (ASSER
 T) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_union1| "" (SKOLEM!)
    (("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
 L)) NIL)
   (|sum_union2| "" (SKOLEM!)
    (("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
 L)) NIL)
   (|sum_inter1| "" (SKOLEM!)
    (("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
 L)) NIL)
   (|sum_inter2| "" (SKOLEM!)
    (("" (REWRITE "sum_subset") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NI
 L)) NIL))
  
  
  $$$some_or_none_adt.pvs
  %%% ADT file generated from some_or_none
  
  some_or_none_adt[T: TYPE]: THEORY
   BEGIN
  
    some_or_none: TYPE
  
    none?, some?: [some_or_none -> boolean]
  
    none: (none?)
  
    some: [T -> (some?)]
  
    the_one: [(some?) -> T]
  
    ord(x: some_or_none): upto(1) =
        CASES x OF none: 0, some(some1_var): 1 ENDCASES
  
      some_or_none_none_extensionality: AXIOM
      FORALL (none?_var: (none?), (none?_var2: (none?))): none?_var = none?_var
 2;
  
    some_or_none_some_extensionality: AXIOM
      FORALL (some?_var: (some?), (some?_var2: (some?))):
        the_one(some?_var) = the_one(some?_var2) IMPLIES some?_var = some?_var2
 ;
  
    some_or_none_some_eta: AXIOM
      FORALL (some?_var: (some?)): some(the_one(some?_var)) = some?_var;
  
    some_or_none_the_one_some: AXIOM
      FORALL (some1_var: T): the_one(some(some1_var)) = some1_var;
  
    some_or_none_inclusive: AXIOM
      FORALL (some_or_none_var: some_or_none):
        none?(some_or_none_var) OR some?(some_or_none_var);
  
    some_or_none_induction: AXIOM
      FORALL (p: [some_or_none -> boolean]):
        (p(none) AND (FORALL (some1_var: T): p(some(some1_var)))) IMPLIES
         (FORALL (some_or_none_var: some_or_none): p(some_or_none_var));
  
    every(p: PRED[T])(a: some_or_none):  boolean =
        CASES a OF none: TRUE, some(some1_var): p(some1_var) ENDCASES;
  
      every(p: PRED[T], (a: some_or_none)):  boolean =
        CASES a OF none: TRUE, some(some1_var): p(some1_var) ENDCASES;
  
      some(p: PRED[T])(a: some_or_none):  boolean =
        CASES a OF none: FALSE, some(some1_var): p(some1_var) ENDCASES;
  
      some(p: PRED[T], (a: some_or_none)):  boolean =
        CASES a OF none: FALSE, some(some1_var): p(some1_var) ENDCASES;
  
      subterm(x, y: some_or_none):  boolean = x = y;
  
      <<(x, y: some_or_none):  boolean = FALSE;
  
      some_or_none_well_founded: AXIOM well_founded?[some_or_none](<<);
  
    reduce_nat(none?_fun: nat, (some?_fun: [T -> nat])):  [some_or_none -> nat]
  =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun, some(some1_var): some?_fun(some1_var)
            ENDCASES;
  
      REDUCE_nat(none?_fun: [some_or_none -> nat],
                 (some?_fun: [[T, some_or_none] -> nat])):
       [some_or_none -> nat] =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun(some_or_none_adtvar),
               some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
            ENDCASES;
  
      reduce_ordinal(none?_fun: ordinal, (some?_fun: [T -> ordinal])):
      [some_or_none -> ordinal] =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun, some(some1_var): some?_fun(some1_var)
            ENDCASES;
  
      REDUCE_ordinal(none?_fun: [some_or_none -> ordinal],
                     (some?_fun: [[T, some_or_none] -> ordinal])):
       [some_or_none -> ordinal] =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun(some_or_none_adtvar),
               some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
            ENDCASES;
   END some_or_none_adt
  
  some_or_none_adt_map[T: TYPE, T1: TYPE]: THEORY
   BEGIN
  
    IMPORTING some_or_none_adt
  
    map(f: [T -> T1])(a: some_or_none[T]):  some_or_none[T1] =
        CASES a OF none: none, some(some1_var): some(f(some1_var)) ENDCASES;
  
      map(f: [T -> T1], (a: some_or_none[T])):  some_or_none[T1] =
        CASES a OF none: none, some(some1_var): some(f(some1_var)) ENDCASES;
   END some_or_none_adt_map
  
  some_or_none_adt_reduce[T: TYPE, range: TYPE]: THEORY
   BEGIN
  
    IMPORTING some_or_none_adt[T]
  
    reduce(none?_fun: range, (some?_fun: [T -> range])):
    [some_or_none -> range] =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun, some(some1_var): some?_fun(some1_var)
            ENDCASES;
  
      REDUCE(none?_fun: [some_or_none -> range],
             (some?_fun: [[T, some_or_none] -> range])):
       [some_or_none -> range] =
        LAMBDA (some_or_none_adtvar: some_or_none):
          CASES some_or_none_adtvar
            OF none: none?_fun(some_or_none_adtvar),
               some(some1_var): some?_fun(some1_var, some_or_none_adtvar)
            ENDCASES;
   END some_or_none_adt_reduce
  $$$some_or_none.pvs
  some_or_none[T: TYPE] : DATATYPE
    BEGIN
     none: none?
     some(the_one: T): some?
    END some_or_none
  
  $$$schedules.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Schedules: mapping from nat to idle or some job j   %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  schedules [ job: TYPE] : THEORY
  
    BEGIN
  
    IMPORTING some_or_none[job], sum_sequences, sum_partitions
  
    schedule: TYPE = [nat -> some_or_none[job]]
  
  
    sch, sch1, sch2: VAR schedule
  
    t, t1, t2, t3: VAR nat
  
    j, k: VAR job
  
    E, E1, E2, E3, E4: VAR set[job]
  
    x: VAR some_or_none[job]
  
  
    %-------------------------------------------------------------------------
    %  active(sch, j, t): j is the job active at time t in sch
    %  idle(sch, t): no job is active at time t
    %
    %  process_time(sch, t1, t2, E): time allocated to a job of E in [t1, t2[
    %    = card { u | t1 <= u < t2 AND active_job at time u belongs to E }
    %
    %  idle_time(sch, t1, t2): idle time in [t1, t2[
    %    = card { u | t1 <= u < t2 AND no job is active at time u }
    %-------------------------------------------------------------------------
    
    active(sch, j, t): bool = sch(t) = some(j)
  
    idle(sch, t): bool = sch(t) = none
  
    idle_time(sch, t1, t2): nat = sum(sch, t1, t2, none?)
  
    process_time(sch, t1, t2, E): nat = sum(sch, t1, t2, { x | some?(x) AND E(t
 he_one(x)) })
  
  
  
    %---------------
    %  Properties
    %---------------
  
    unique_active: LEMMA active(sch, j, t) AND active(sch, k, t) IMPLIES j = k
  
    idle_equiv: LEMMA idle(sch, t) IFF NOT EXISTS j: active(sch, j, t)
  
    total_cpu: LEMMA 
       t1 <= t2 IMPLIES 
  	process_time(sch, t1, t2, fullset) + idle_time(sch, t1, t2) = t2 - t1
  
    max_idle_time: LEMMA t1 <= t2 IMPLIES idle_time(sch, t1, t2) <= t2 - t1
  
    zero_idle_time: LEMMA
       idle_time(sch, t1, t2) = 0 IFF
  	FORALL t: t1 <= t AND t < t2 IMPLIES not idle(sch, t)
  
    idle_interval: LEMMA
       idle_time(sch, t1, t2) = t2 - t1 IFF 
  	t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES idle(sch, t)
  
    split_idle_time: LEMMA
  	t1 <= t2 AND t2 <= t3 IMPLIES
  	   idle_time(sch, t1, t2) + idle_time(sch, t2, t3) = idle_time(sch, t1,
  t3)
  
    increasing_idle_time: LEMMA
  	t1 <= t2 AND t2 <= t3 IMPLIES 
  	   idle_time(sch, t1, t2) <= idle_time(sch, t1, t3)
  
    equal_idle_time: LEMMA
  	(FORALL t: t1 <= t AND t < t2 IMPLIES (idle(sch1, t) IFF idle(sch2, t))
 )
  	   IMPLIES idle_time(sch1, t1, t2) = idle_time(sch2, t1, t2)
  
  
  
  
    %------------------------------
    %  Properties of process_time
    %------------------------------
  
    max_process_time: LEMMA t1 <= t2 IMPLIES process_time(sch, t1, t2, E) <= t2
  - t1
  
    zero_process_time: LEMMA 
       process_time(sch, t1, t2, E) = 0 IFF
  	FORALL t, j: t1 <= t AND t < t2 AND active(sch, j, t) IMPLIES not E(j)
  
    busy_interval: LEMMA
       process_time(sch, t1, t2, E) = t2 - t1 IFF 
  	t1 <= t2 AND FORALL t: t1 <= t AND t < t2 IMPLIES 
  				EXISTS j: active(sch, j, t) AND E(j)
  
    split_process_time: LEMMA
  	t1 <= t2 AND t2 <= t3 IMPLIES
  	   process_time(sch, t1, t2, E) + 
  	       process_time(sch, t2, t3, E) = process_time(sch, t1, t3, E)
  
    increasing_process_time: LEMMA
  	t1 <= t2 AND t2 <= t3 IMPLIES 
  	   process_time(sch, t1, t2, E) <= process_time(sch, t1, t3, E)
  
    equal_process_time: LEMMA
  	(FORALL t, j: t1 <= t AND t < t2 AND E(j) IMPLIES 
  		(active(sch1, j, t) IFF active(sch2, j, t)))
  	   IMPLIES process_time(sch1, t1, t2, E) = process_time(sch2, t1, t2, E
 )
  
  
    %-----------------------------------------
    %  Process time for various sets of jobs
    %-----------------------------------------
  
    process_time_emptyset: LEMMA process_time(sch, t1, t2, emptyset) = 0
  
    process_time_subset: LEMMA
  	subset?(E1, E2) IMPLIES process_time(sch, t1, t2, E1) <= process_time(s
 ch, t1, t2, E2)
  
    process_time_partition2: LEMMA
  	partition2(E)(E1, E2) IMPLIES 
  	    process_time(sch, t1, t2, E) = 
  		process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2)
  
    process_time_partition3: LEMMA
  	partition3(E)(E1, E2, E3) IMPLIES 
  	    process_time(sch, t1, t2, E) = 
  		process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) +
  		process_time(sch, t1, t2, E3)
  		
    process_time_partition4: LEMMA
  	partition4(E)(E1, E2, E3, E4) IMPLIES 
  	    process_time(sch, t1, t2, E) = 
  		process_time(sch, t1, t2, E1) + process_time(sch, t1, t2, E2) +
  		process_time(sch, t1, t2, E3) + process_time(sch, t1, t2, E4)
  		
  
  
  
    %--------------------------------------
    %  Abbreviations for sums from 0 to t
    %   and for sums over singleton sets
    %--------------------------------------
  
    process_time(sch, t, E): nat = process_time(sch, 0, t, E)
  
    process_time(sch, t1, t2, j): nat = process_time(sch, t1, t2, singleton(j))
  
    process_time(sch, t, j): nat = process_time(sch, t, singleton(j))
  
    idle_time(sch, t): nat = idle_time(sch, 0, t)
  
  
  
    total_cpu2: LEMMA process_time(sch, t, fullset) + idle_time(sch, t) = t
  
    process_time_equiv1: LEMMA
       t1 <= t2 IMPLIES 
  	process_time(sch, t1, t2, E) = process_time(sch, t2, E) - process_time(
 sch, t1, E)
  
    process_time_equiv2: LEMMA
       t1 <= t2 IMPLIES
  	process_time(sch, t1, t2, j) = process_time(sch, t2, j) - process_time(
 sch, t1, j)
  
    idle_time_equiv: LEMMA
       t1 <= t2 IMPLIES idle_time(sch, t1, t2) = idle_time(sch, t2) - idle_time
 (sch, t1)
  
  
  
  
    %-----------------------------------------
    %  Next value of process_time(sch, t, j)
    %-----------------------------------------
  
    process_time_init: LEMMA process_time(sch, 0, j) = 0
  
    process_time_step: LEMMA 
       process_time(sch, t+1, j) = IF active(sch, j, t) THEN 1 + process_time(s
 ch, t, j) 
  						      ELSE process_time(sch, t,
  j) ENDIF
  
  
    process_time_init2: LEMMA process_time(sch, t, t, j) = 0
  
    process_time_step2: LEMMA t1 <= t2 IMPLIES 
  	process_time(sch, t1, t2 +1, j) = 
  	   IF active(sch, j, t2) THEN 1 + process_time(sch, t1, t2, j) 
  				 ELSE process_time(sch, t1, t2, j) ENDIF
  
  
  
  
    %--------------------------------------------------
    %  Schedule constructed from act(j, t) predicate
    %--------------------------------------------------
  
    act: VAR { p: [job, nat -> bool] | FORALL j, k, t: p(j, t) AND p(k, t) => j
  = k }
  
    sched(act): schedule = 
       lambda t: IF EXISTS j: act(j, t) THEN some(epsilon! j: act(j, t)) ELSE n
 one ENDIF
  
  
    schedule_from_act1: LEMMA active(sched(act), j, t) IFF act(j, t)
  
    schedule_from_act2: LEMMA idle(sched(act), t) IFF NOT EXISTS j: act(j, t)
  
    END schedules
  
  $$$schedules.prf
  (|schedules|
   (|unique_active| "" (EXPAND "active")
    (("" (SKOSIMP)
      (("" (ASSERT)
        (("" (CASE "the_one(some(j!1)) = k!1")
          (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
 )
          NIL))
        NIL))
      NIL))
    NIL)
   (|idle_equiv| "" (GRIND)
    (("" (INST + "the_one(sch!1(t!1))")
      (("" (ASSERT) (("" (REPLACE-ETA "sch!1(t!1)" "(some?)") NIL NIL)) NIL))
      NIL))
    NIL)
   (|total_cpu| "" (EXPAND* "process_time" "idle_time" "fullset")
    (("" (SKOSIMP)
      (("" (CASE-REPLACE "{ x | some?(x) } = complement(none?)")
        (("1" (REWRITE "sum_complement") (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2)
          (("2" (AUTO-REWRITE "complement" "member")
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_idle_time| "" (EXPAND "idle_time")
    (("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL)
   (|zero_idle_time| "" (EXPAND* "idle_time" "idle")
    (("" (SKOLEM!)
      (("" (REWRITE "sum_zero")
        (("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL))
      NIL))
    NIL)
   (|idle_interval| "" (EXPAND* "idle_time" "idle")
    (("" (SKOLEM!)
      (("" (REWRITE "sum_full")
        (("" (APPLY (THEN (SMASH) (SKOSIMP) (INST?) (ASSERT))) NIL NIL)) NIL))
      NIL))
    NIL)
   (|split_idle_time| "" (EXPAND "idle_time")
    (("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL)
   (|increasing_idle_time| "" (EXPAND "idle_time")
    (("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL)
   (|equal_idle_time| "" (EXPAND* "idle_time" "idle")
    (("" (SKOSIMP)
      (("" (REWRITE "equal_sums")
        (("" (APPLY (THEN (SKOSIMP) (INST?) (SMASH))) NIL NIL)) NIL))
      NIL))
    NIL)
   (|max_process_time| "" (EXPAND "process_time")
    (("" (SKOSIMP) (("" (REWRITE "max_sum") NIL NIL)) NIL)) NIL)
   (|zero_process_time| "" (EXPAND* "process_time" "active")
    (("" (SKOLEM!)
      (("" (REWRITE "sum_zero")
        (("" (AUTO-REWRITE "some_or_none_some_eta")
          (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|busy_interval| "" (EXPAND* "process_time" "active")
    (("" (SKOLEM!)
      (("" (REWRITE "sum_full")
        (("" (AUTO-REWRITE "some_or_none_some_eta")
          (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE))) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|split_process_time| "" (EXPAND "process_time")
    (("" (SKOSIMP) (("" (REWRITE "sum_split") NIL NIL)) NIL)) NIL)
   (|increasing_process_time| "" (EXPAND "process_time")
    (("" (SKOSIMP) (("" (REWRITE "sum_increasing") NIL NIL)) NIL)) NIL)
   (|equal_process_time| "" (EXPAND* "process_time" "active")
    (("" (SKOSIMP)
      (("" (REWRITE "equal_sums")
        (("" (AUTO-REWRITE "some_or_none_some_eta")
          (("" (DELETE 2)
            (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REDUCE :POLARITY? T))) NI
 L
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_emptyset| "" (SKOLEM!)
    (("" (AUTO-REWRITE "emptyset" "sum_emptyset" "process_time")
      (("" (ASSERT)
        (("" (CASE-REPLACE "{ x | FALSE } = emptyset")
          (("1" (ASSERT) NIL NIL)
           ("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_subset| "" (EXPAND "process_time")
    (("" (SKOSIMP)
      (("" (REWRITE "sum_subset")
        (("" (DELETE 2)
          (("" (GRIND :REWRITES ("some_or_none_some_eta")) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_partition2| "" (SKOSIMP)
    (("" (EXPAND "process_time")
      (("" (REWRITE "sum_partition2")
        (("" (DELETE 2)
          (("" (GRIND)
            (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_partition3| "" (SKOSIMP)
    (("" (EXPAND "process_time")
      (("" (REWRITE "sum_partition3")
        (("" (DELETE 2)
          (("" (GRIND)
            (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_partition4| "" (SKOSIMP)
    (("" (EXPAND "process_time")
      (("" (REWRITE "sum_partition4")
        (("" (DELETE 2)
          (("" (GRIND)
            (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|total_cpu2| "" (EXPAND* "process_time" "idle_time")
    (("" (SKOSIMP) (("" (USE "total_cpu") (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|process_time_equiv1| "" (EXPAND "process_time" 1 2)
    (("" (EXPAND "process_time" 1 3)
      (("" (SKOSIMP)
        (("" (USE "split_process_time" ("t1" "0" "t2" "t1!1" "t3" "t2!1"))
          (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_equiv2| "" (EXPAND "process_time")
    (("" (SKOSIMP) (("" (REWRITE "process_time_equiv1") NIL NIL)) NIL)) NIL)
   (|idle_time_equiv| "" (EXPAND "idle_time" 1 2)
    (("" (EXPAND "idle_time" 1 3)
      (("" (SKOSIMP)
        (("" (USE "split_idle_time" ("t1" "0")) (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_init| "" (GRIND) NIL NIL)
   (|process_time_step| "" (GRIND)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
   (|process_time_init2| "" (GRIND) NIL NIL)
   (|process_time_step2| "" (GRIND)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
   (|sched_TCC1| "" (EXISTENCE-TCC) NIL NIL)
   (|schedule_from_act1| "" (SKOLEM-TYPEPRED)
    (("" (EXPAND* "sched" "active")
      (("" (CASE "EXISTS j: true")
        (("1" (SMASH)
          (("1" (USE "epsilon_ax[job]")
            (("1" (GROUND)
              (("1"
                (CASE "the_one(some(epsilon! (j: job): act!1(j, t!1))) = j!1")
                (("1" (ASSERT) NIL NIL)
                 ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
                 ("3" (PROPAX) NIL NIL))
                NIL))
              NIL))
            NIL)
           ("2" (USE "epsilon_ax[job]")
            (("2" (GROUND)
              (("2" (INST - "j!1" "epsilon! j: act!1(j, t!1)" "t!1")
                (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("3" (INST? +) NIL NIL))
          NIL)
         ("2" (INST + "j!1") NIL NIL))
        NIL))
      NIL))
    NIL)
   (|schedule_from_act2| "" (EXPAND* "idle" "sched")
    (("" (SKOLEM!) (("" (SMASH) NIL NIL)) NIL)) NIL))
  
  
  $$$precedence.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%
  %  order between jobs    %
  %%%%%%%%%%%%%%%%%%%%%%%%%%
  
  precedence [ (IMPORTING basic_types) 
        job: TYPE, 
        prio: [job -> priority],
        dispatch: [job -> nat] 
     ] : THEORY
  
    BEGIN
  
    j, k: VAR job  
  
    A: VAR (nonempty?[job])
  
    precedes(j, k): bool =
       prio(j) > prio(k) OR prio(j) = prio(k) AND dispatch(j) <= dispatch(k)
  
    topjob_exists: LEMMA
       EXISTS (j: (A)): FORALL (k: (A)): precedes(j, k)
  
    top(A): { j | A(j) AND FORALL (k: (A)): precedes(j, k) }
  
    topjob_maxprio: LEMMA FORALL (k: (A)): prio(k) <= prio(top(A))
  
    topjob_dispatch: LEMMA 
  	FORALL (k: (A)): prio(k) = prio(top(A)) IMPLIES dispatch(top(A)) <= dis
 patch(k)
  
    END precedence
  
  $$$precedence.prf
  (|precedence|
   (|topjob_exists| "" (LEMMA "wf_nat")
    (("" (EXPAND "well_founded?")
      (("" (SKOSIMP*)
        (("" (INST-CP - "{ n:nat | EXISTS j: A!1(j) AND prio(j) = maxprio - n }
 ")
          (("" (GROUND)
            (("1" (SKOSIMP* :PREDS? T)
              (("1" (INST -4 "{ t:nat | EXISTS j: A!1(j) AND prio(j) = maxprio 
 - y!1 AND dispatch(j) = t }")
                (("1" (GROUND)
                  (("1" (SKOSIMP* :PREDS? T)
                    (("1" (EXPAND "precedes")
                      (("1" (INST + "j!2")
                        (("1" (SKOSIMP)
                          (("1" (ASSERT)
                            (("1" (CASE "prio(j!2) = prio(k!1)")
                              (("1" (ASSERT)
                                (("1" (INST - "dispatch(k!1)") (("1" (ASSERT) N
 IL NIL) ("2" (INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)
                               ("2" (DELETE 3)
                                (("2" (INST -7 "maxprio - prio(k!1)")
                                  (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (
 INST + "k!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (INST + "dispatch(j!1)") (("2" (DELETE 2) (("2" (INST?)
  (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (TYPEPRED "A!1")
                (("2" (GRIND :IF-MATCH NIL)
                  (("2" (INST + "maxprio - prio(x!1)") (("1" (INST?) (("1" (ASS
 ERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|top_TCC1| "" (INST + "lambda A: epsilon! (j: (A)): FORALL (k: (A)): preced
 es(j, k)")
    (("1" (SKOLEM!)
      (("1" (USE "epsilon_ax[(A!1)]")
        (("1" (GROUND) (("1" (REWRITE "topjob_exists") NIL NIL)) NIL) ("2" (DEL
 ETE 2) (("2" (TYPEPRED "A!1") (("2" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL)
     ("2" (GRIND) NIL NIL))
    NIL)
   (|topjob_maxprio| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL N
 IL)) NIL)) NIL)
   (|topjob_dispatch| "" (SKOLEM!) (("" (TYPEPRED "top(A!1)") (("" (GRIND) NIL 
 NIL)) NIL)) NIL))
  
  
  $$$priority_ceiling.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Priority ceiling scheduler   %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  priority_ceiling [ (IMPORTING programs)
  	job: TYPE,
  	prio: [job -> priority],
  	dispatch: [job -> nat],
  	prog: [job -> prog] ] : THEORY
  
    BEGIN
  
    ASSUMING
  
    j: VAR job 
    s: VAR semaphore
  
    good_ceiling: ASSUMPTION
        member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
  
    good_programs: ASSUMPTION  well_behaved(prog(j))
  
    ENDASSUMING
  
  
    j1, j2, k: VAR job
    p: VAR priority
    n, m, t, t1, t2: VAR nat
  
    cmd: VAR command
  
    IMPORTING precedence[job, prio, dispatch]
    
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Resource management state:                         %
    %  - for each job j:                                  %
    %      alloc(j) = set of semaphores held by j         %
    %    request(j) = set of semaphores j is waiting for  %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    rsrc_state: TYPE = [# alloc, request: [job -> rsrc_set] #]
  
    r, r1, r2: VAR rsrc_state
  
  
    %------------------------------------------------------------------
    %  Blocking rules:
    %  - a blocker of j is a job that owns an s of ceiling >= prio(j)
    %  - j is blocked if it has pending requests and blockers
    %------------------------------------------------------------------
   
    blk(r, j): set[job] = 
       { k | k /= j AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= prio(j) 
 }
  
    blocked(r, j): bool = not empty?(blk(r, j)) AND not empty?(r`request(j))
  
  
  
    %---------------------------------------------------
    %  Allocation request: P(s) by j
    %  - allocates s to j if j has no blocker
    %  - otherwise s is recorded as a pending request
    %   (and j becomes blocked)
    %---------------------------------------------------
    
    alloc_step(r, j, s): rsrc_state =
       IF empty?(blk(r, j)) THEN 
  	r WITH [ `alloc(j) := add(s, r`alloc(j)) ]
       ELSE
  	r WITH [ `request(j) := add(s, r`request(j)) ]
       ENDIF
  
  
    %-------------------------------------------------
    %  Release request: V(s) by j
    %  - removes s from alloc(j)
    %   (no effect if j does not own s)
    %-------------------------------------------------
  
    release_step(r, j, s): rsrc_state =
       r WITH [ `alloc(j) := remove(s, r`alloc(j)) ]
  
  
    %---------------------------------------------
    %  Wakeup(r, j): grant j's pending requests
    %---------------------------------------------
  
    wakeup(r, j): rsrc_state =
       r WITH [ `alloc(j) := union(r`alloc(j), r`request(j)),
  	      `request(j) := emptyset ]
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Scheduler state:                         %
    %  - rsrc: resource state                   %
    %  - for each job j:                        %
    %       pc(j) = program counter for job j   %
    %  - time: global time counter              %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    sch_state: TYPE = [# 
  	rsrc: rsrc_state,
  	pc: [j:job -> pc(prog(j))], 
  	time: nat #]
  
    q, q1, q2: VAR sch_state
  
  
    %--------------------------------------------------------------------
    %  Selection of active job in state q:
    %  - finished(q, j): job j is completed
    %  - ready(q, j)   : j is ready to execute
    %  - topjob(q, j)  : j has highest precedence among the ready jobs
    %  - eligible(q, j): j can be active in state q
    % ==> either j is a topjob and is not blocked
    %     or j is blocking a topjob k
    %--------------------------------------------------------------------
  
    finished(q, j): bool = complete(prog(j), q`pc(j))
   
    ready(q, j): bool = dispatch(j) <= q`time AND not finished(q, j)
  
    topjob(q, j): bool =
       ready(q, j) AND (FORALL k: ready(q, k) IMPLIES precedes(j, k))
  
    eligible(q, j): bool =
         topjob(q, j) AND not blocked(q`rsrc, j)
      OR (EXISTS k: topjob(q, k) AND blocked(q`rsrc, k) AND 
  		member(j, blk(q`rsrc, k)))
  
  
  
    %---------------------------------------------------
    %  Execution of a step by job j (requires j ready)
    %  - update rsrc state
    %  - increment j's pc
    %  - increment time counter
    %---------------------------------------------------
  
    run_step(r, j, cmd): rsrc_state =
        CASES cmd OF
  	 P(s): alloc_step(wakeup(r, j), j, s),
  	 V(s): release_step(wakeup(r, j), j, s),
  	 Step: wakeup(r, j)
        ENDCASES 
  
  
    step(q, (j | ready(q, j))): sch_state =
  	(# rsrc := run_step(q`rsrc, j, cmd(prog(j), q`pc(j))),
             pc   := q`pc WITH [(j) := q`pc(j) + 1],
  	   time := q`time +1 #)
  
  
  
    %-----------------------------
    %  idle_step: no job active
    %-----------------------------
  
    idle(q): bool = not EXISTS j: eligible(q, j)
  
    idle_step(q): sch_state = q WITH [time := q`time + 1]
  
  
  
  
    %------------------------------
    %  Existence of eligible jobs
    %------------------------------
  
    topjob_maxprio: LEMMA topjob(q, j) AND ready(q, k) IMPLIES prio(k) <= prio(
 j)
  
    topjob_dispatch: LEMMA topjob(q, j) AND ready(q, k) AND prio(k) = prio(j)
  	IMPLIES dispatch(j) <= dispatch(k)
  
    topjob_exists: LEMMA 
  	(EXISTS j: ready(q, j)) IMPLIES (EXISTS j: topjob(q, j))
  
    eligible_exists: LEMMA 
  	(EXISTS j: ready(q, j)) IMPLIES (EXISTS j: eligible(q, j))
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Invariant for type correctness         %
    %   ensures that eligible jobs are ready  %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    P(q): bool = 
          (FORALL j: 
  	   union(q`rsrc`alloc(j), q`rsrc`request(j)) = needs(prog(j), q`pc(j)))
      AND (FORALL j: q`time <= dispatch(j) IMPLIES q`pc(j) = 0)
  
  
    %-------------------
    %  Invariance of P
    %-------------------
  
    alloc_P: LEMMA
       union(alloc_step(r, j, s)`alloc(k), alloc_step(r, j, s)`request(k)) =
  	IF j=k THEN add(s, union(r`alloc(k), r`request(k))) 
  	       ELSE union(r`alloc(k), r`request(k)) ENDIF
  
    wakeup_P: LEMMA 
       union(wakeup(r, j)`alloc(k), wakeup(r, j)`request(k)) = 
  	union(r`alloc(k), r`request(k))
  
    release_P: LEMMA
       union(release_step(r, j, s)`alloc(k), release_step(r, j, s)`request(k)) 
 =
  	IF j=k THEN union(remove(s, r`alloc(k)), r`request(k))
  	       ELSE union(r`alloc(k), r`request(k)) ENDIF
  
  
    step_P: LEMMA P(q) AND ready(q, j) IMPLIES P(step(q, j))
  
    idle_P: LEMMA P(q) IMPLIES P(idle_step(q))
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Good states: satisfy P  %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    good_state: NONEMPTY_TYPE = (P)
  
    g, g1, g2: VAR good_state
  
  
    %----------------------------------------------------
    %  Any job eligible in a good state is ready
    %----------------------------------------------------
  
    good_prop: LEMMA
       needs(prog(j), g`pc(j)) = union(g`rsrc`alloc(j), g`rsrc`request(j))
  
    alloc_not_ready: LEMMA 
       not ready(g, j) IMPLIES empty?(g`rsrc`alloc(j))
  
    alloc_before_dispatch: LEMMA
       g`time <= dispatch(j) IMPLIES empty?(g`rsrc`alloc(j))
  
    request_not_ready: LEMMA 
       not ready(g, j) IMPLIES empty?(g`rsrc`request(j))
  
    request_before_dispatch: LEMMA 
       g`time <= dispatch(j) IMPLIES empty?(g`rsrc`request(j))
  
    eligible_ready: LEMMA eligible(g, j) IMPLIES ready(g, j)
  
  
    %-------------------------------------------
    %  Ceiling of allocated/requested resource
    %  is higher than job priority
    %-------------------------------------------
  
    alloc_prop1: LEMMA subset?(g`rsrc`alloc(j), resources(prog(j)))
    
    ceiling_prop1: LEMMA member(s, g`rsrc`alloc(j)) IMPLIES prio(j) <= ceil(s)
  
  
    alloc_prop2: LEMMA subset?(g`rsrc`request(j), resources(prog(j)))
  
    ceiling_prop2: LEMMA member(s, g`rsrc`request(j)) IMPLIES prio(j) <= ceil(s
 )
  
  
    idle_equiv: LEMMA  idle(g) IFF not EXISTS j: ready(g, j)
  	
    prio_blocker: LEMMA 
       topjob(g, j) AND member(k, blk(g`rsrc, j1)) IMPLIES prio(k) <= prio(j)
  
    dispatch_blocker: LEMMA 
       topjob(g, j) AND member(k, blk(g`rsrc, j1)) AND prio(k) = prio(j)
  	IMPLIES dispatch(j) <= dispatch(k)
  
  
   
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%
    %   Transition system    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%
  
    %------------------
    %  initial state
    %------------------
  
    init_rsrc: rsrc_state =
         (# alloc   := lambda j: emptyset, 
  	  request := lambda j: emptyset #)
    
    init_sch: good_state = 
  	(# rsrc := init_rsrc, pc := lambda j: 0, time := 0 #)
  
  
    %------------------------
    %  transition relation
    %------------------------
  
    T(g1, g2): bool = (idle(g1) AND g2 = idle_step(g1))
  	OR (EXISTS j: eligible(g1, j) AND g2 = step(g1, j))
  
  
  
    %------------------------------------------------------
    % - transitions increment time
    % - jobs ready after a transition were ready before
    %   unless they've just been dispatched
    %------------------------------------------------------
  
    time_step: LEMMA T(g1, g2) IMPLIES g2`time = 1 + g1`time
  
    readiness_step: LEMMA
        T(g1, g2) AND ready(g2, j) AND dispatch(j) <= g1`time 
  	  IMPLIES ready(g1, j)
  
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%
    %  Main Invariants  %
    %%%%%%%%%%%%%%%%%%%%%
  
    P2(r): bool = FORALL j, k, s: member(s, r`alloc(j)) AND prio(j) <= prio(k)
  	AND prio(k) <= ceil(s) AND j /= k IMPLIES empty?(r`alloc(k))
  
    P3(r): bool = FORALL j, s: member(s, r`alloc(j)) IMPLIES prio(j) <= ceil(s)
  
    Q(g): bool = FORALL j, k: ready(g, j) AND prio(k) <= prio(j) AND 
  	dispatch(j) < dispatch(k) IMPLIES empty?(g`rsrc`alloc(k))
  
  
    %-------------------
    %  Invariance of Q
    %-------------------
  
    init_Q: LEMMA Q(init_sch)
  
    step_Q: LEMMA Q(g1) AND T(g1, g2) IMPLIES Q(g2)
  
  
  
    %-------------------------
    %  Induction step for P2
    %-------------------------
  
    alloc_P2: LEMMA P3(r) AND P2(r) IMPLIES P2(alloc_step(r, j, s))
  
    wakeup_P2: LEMMA P3(r) AND P2(r) AND not blocked(r, j) IMPLIES P2(wakeup(r,
  j))
  
    release_P2: LEMMA P2(r) IMPLIES P2(release_step(r, j, s))
  
  
    %---------------------------------
    %  Auxiliary results:
    %  - blocking is intransitive
    %  - P3 holds in good states
    %  - eligible job is not blocked
    %---------------------------------
  
    intransitive_blocking: LEMMA
  	P2(r) AND member(j1, blk(r, k)) AND prio(j2) <= prio(k) 
  	   IMPLIES NOT member(j2, blk(r, j1))
  
    invar_P2_aux: LEMMA P3(g`rsrc)
  
    invar_P2_aux2: LEMMA P3(wakeup(g`rsrc, j))
  
    step_P2_aux: LEMMA 
  	P2(g`rsrc) AND eligible(g, j) IMPLIES not blocked(g`rsrc, j)
  
  
  
    %--------------------
    %  Invariance of P2
    %--------------------
  
    init_P2: LEMMA P2(init_rsrc)
  
    step_P2: LEMMA P2(g1`rsrc) AND T(g1, g2) IMPLIES P2(g2`rsrc)
  
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Consequences of P2 and Q %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   
    %--------------------
    %  Mutual exclusion
    %---------------------
  
    mutual_exclusion: LEMMA
  	P2(r) AND P3(r) AND j /= k IMPLIES disjoint?(r`alloc(j), r`alloc(k))
  
  
    %-------------------------------------------------------------
    %  Job of lower priority than j that can run when j is ready
    %-------------------------------------------------------------
  
    blockers(r, j): set[job] = { k | member(k, blk(r, j)) AND prio(k) < prio(j)
  }
  
    unique_blocker: LEMMA
  	P2(r) AND member(j1, blockers(r, k)) AND member(j2, blockers(r, k)) IMP
 LIES j1 = j2
  
    blockers_in_cs: LEMMA
  	member(k, blockers(g`rsrc, j)) IMPLIES cs(prog(k), g`pc(k), prio(j))
  
    eligible_prio: LEMMA
  	Q(g) AND ready(g, j) AND eligible(g, k) IMPLIES
  	    precedes(k, j) OR member(k, blockers(g`rsrc, j))
  
    blockers_step: LEMMA 
  	Q(g1) AND ready(g1, j) AND T(g1, g2) IMPLIES
  	    subset?(blockers(g2`rsrc, j), blockers(g1`rsrc, j))
  
  
  
    %--------------------------------------------------------------------------
 --
    %  blockers(r, p): jobs of priority <p that can block jobs of priority >= p
    %--------------------------------------------------------------------------
 --
  
    blockers(r, p): set[job] =
       { k | prio(k) < p AND EXISTS s: member(s, r`alloc(k)) AND ceil(s) >= p }
  
    unique_blocker2: LEMMA
  	P2(r) AND member(j1, blockers(r, p)) AND member(j2, blockers(r, p)) IMP
 LIES j1 = j2
  
    blockers_in_cs2: LEMMA
  	member(k, blockers(g`rsrc, p)) IMPLIES cs(prog(k), g`pc(k), p)
  
    eligible_prio2: LEMMA 
  	(EXISTS j: prio(j) >= p AND ready(g, j)) AND eligible(g, k)
  	    IMPLIES prio(k) >= p OR member(k, blockers(g`rsrc, p))
  
    blockers_step2: LEMMA 
  	(EXISTS j: prio(j) >= p AND ready(g1, j)) AND T(g1, g2) 
  	    IMPLIES subset?(blockers(g2`rsrc, p), blockers(g1`rsrc, p))
  	
    END priority_ceiling
  
  $$$priority_ceiling.prf
  (|priority_ceiling| (|step_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|step_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|topjob_maxprio| "" (GRIND :EXCLUDE "ready") NIL NIL)
   (|topjob_dispatch| "" (GRIND :EXCLUDE "ready") NIL NIL)
   (|topjob_exists| "" (SKOSIMP)
    ((""
      (USE "precedence[job,prio,dispatch].topjob_exists"
           ("A" "{ j | ready(q!1, j) }"))
      (("1" (DELETE -2)
        (("1" (GRIND :DEFS NIL :REWRITES ("topjob") :POLARITY? T) NIL
          NIL))
        NIL)
       ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("ready")) NIL NIL)) NIL))
      NIL))
    NIL)
   (|eligible_exists| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "topjob_exists")
      (("" (DELETE -2)
        (("" (SKOLEM!)
          (("" (CASE "blocked(q!1`rsrc, j!1)")
            (("1" (ASSERT)
              (("1" (EXPAND* "blocked" "empty?")
                (("1" (SKOSIMP*)
                  (("1" (INST + "x!1")
                    (("1" (EXPAND "eligible")
                      (("1" (FLATTEN)
                        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (ASSERT)
              (("2" (INST?)
                (("2" (EXPAND "eligible") (("2" (PROPAX) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|alloc_P| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|wakeup_P| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|release_P| "" (SKOLEM!)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL)
   (|step_P| "" (EXPAND "P")
    (("" (SKOSIMP)
      (("" (SPLIT)
        (("1" (DELETE -2)
          (("1"
            (AUTO-REWRITE "alloc_P" "wakeup_P" "release_P" "needs"
                          ("step" "run_step"))
            (("1" (SKOSIMP)
              (("1" (INST - "j!2")
                (("1" (SMASH)
                  (("1" (REPLACE*)
                    (("1" (REPLACE -3 + RL)
                      (("1" (DELETE -1 -2 -3 1)
                        (("1" (APPLY-EXTENSIONALITY :HIDE? T)
                          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE -1)
          (("2" (GRIND :EXCLUDE ("finished" "run_step") :IF-MATCH NIL)
            (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|idle_P| "" (GRIND :EXCLUDE ("union" "needs")) NIL NIL)
   (|good_state_TCC1| ""
    (INST +
     "(# rsrc:= (# alloc:= lambda j: emptyset, request:= lambda j: emptyset #),
  pc:= lambda j: 0, time := 0 #)")
    (("1" (GRIND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
     ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|good_prop| "" (AUTO-REWRITE "P") (("" (REDUCE) NIL NIL)) NIL)
   (|alloc_not_ready| "" (GRIND :IF-MATCH NIL)
    (("1" (INST?)
      (("1" (USE "good_programs")
        (("1" (EXPAND "well_behaved")
          (("1" (REPLACE*)
            (("1" (REPLACE -2 - RL)
              (("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST?)
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (REPLACE*)
            (("2" (ASSERT)
              (("2" (REWRITE "emptyset_is_empty?" :DIR RL)
                (("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|alloc_before_dispatch| "" (GRIND)
    (("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL)
      (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|request_not_ready| "" (GRIND :IF-MATCH NIL)
    (("1" (INST?)
      (("1" (USE "good_programs")
        (("1" (EXPAND "well_behaved")
          (("1" (REPLACE*)
            (("1" (REPLACE -2 - RL)
              (("1" (DELETE -2 -3 -4) (("1" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST?)
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (REPLACE*)
            (("2" (ASSERT)
              (("2" (REWRITE "emptyset_is_empty?" :DIR RL)
                (("2" (DELETE -2 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|request_before_dispatch| "" (GRIND)
    (("" (REWRITE "emptyset_is_empty?[semaphore]" :DIR RL)
      (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|eligible_ready| "" (EXPAND "eligible")
    (("" (REDUCE)
      (("1" (FORWARD-CHAIN "alloc_not_ready")
        (("1" (DELETE -2 -3 -4 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)
       ("2" (EXPAND "topjob") (("2" (PROPAX) NIL NIL)) NIL))
      NIL))
    NIL)
   (|alloc_prop1| "" (SKOSIMP :PREDS? T)
    (("" (EXPAND "P")
      (("" (GROUND)
        (("" (INST?)
          (("" (USE "rsrc_needs4")
            (("" (REPLACE -2 - RL)
              (("" (DELETE -2 -3)
                (("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|ceiling_prop1| "" (SKOSIMP)
    (("" (REWRITE "good_ceiling")
      (("" (USE "alloc_prop1")
        (("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL))
      NIL))
    NIL)
   (|alloc_prop2| "" (SKOSIMP :PREDS? T)
    (("" (EXPAND "P")
      (("" (GROUND)
        (("" (INST?)
          (("" (USE "rsrc_needs4")
            (("" (REPLACE -2 - RL)
              (("" (DELETE -2 -3)
                (("" (GRIND :EXCLUDE ("resources")) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|ceiling_prop2| "" (SKOSIMP)
    (("" (REWRITE "good_ceiling")
      (("" (USE "alloc_prop2")
        (("" (GRIND :EXCLUDE "resources") NIL NIL)) NIL))
      NIL))
    NIL)
   (|idle_equiv| "" (EXPAND "idle")
    (("" (SKOLEM!)
      (("" (GROUND)
        (("1" (REWRITE "eligible_exists") NIL NIL)
         ("2" (SKOLEM!)
          (("2" (INST?)
            (("2" (USE "eligible_ready") (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|prio_blocker| "" (SKOSIMP)
    (("" (USE "topjob_maxprio")
      (("" (ASSERT)
        (("" (FORWARD-CHAIN "alloc_not_ready")
          (("" (DELETE -2 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|dispatch_blocker| "" (SKOSIMP)
    (("" (USE "topjob_dispatch")
      (("" (ASSERT)
        (("" (FORWARD-CHAIN "alloc_not_ready")
          (("" (DELETE -2 -4 1 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|init_sch_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|init_sch_TCC2| "" (GRIND)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)
   (T_TCC1 "" (SKOSIMP*)
    (("" (DELETE 1) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL))
    NIL)
   (|time_step| "" (GRIND :EXCLUDE ("eligible" "run_step")) NIL NIL)
   (|readiness_step| "" (SKOSIMP)
    (("" (EXPAND "T")
      (("" (REDUCE)
        (("1" (EXPAND* "idle_step" "ready" "finished") NIL NIL)
         ("2" (CASE-REPLACE "j!1 = j!2")
          (("1" (FORWARD-CHAIN "eligible_ready") NIL NIL)
           ("2" (ASSERT)
            (("2" (EXPAND* "step" "ready" "finished" "complete") NIL
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|init_Q| "" (GRIND) NIL NIL)
   (|step_Q| "" (EXPAND "Q")
    (("" (SKOSIMP*)
      (("" (USE "readiness_step" ("g1" "g1!1" "g2" "g2!1"))
        (("" (GROUND)
          (("1" (INST?)
            (("1" (ASSERT)
              (("1" (AUTO-REWRITE "idle_equiv" "T")
                (("1" (REDUCE)
                  (("1" (DELETE -4 -5)
                    (("1" (CASE-REPLACE "j!2 = k!1")
                      (("1" (ASSERT)
                        (("1" (DELETE +)
                          (("1" (EXPAND "eligible")
                            (("1" (REDUCE)
                              (("1" (DELETE -1 -2 -4 -5 -7 -8)
                                (("1" (GRIND) NIL NIL)) NIL)
                               ("2" (EXPAND* "topjob" "precedes")
                                (("2"
                                  (GROUND)
                                  (("2"
                                    (INST - "j!1")
                                    (("2" (GROUND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (GRIND :EXCLUDE ("eligible")) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (FORWARD-CHAIN "time_step")
            (("2" (REWRITE "alloc_not_ready")
              (("2" (EXPAND "ready") (("2" (PROPAX) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|alloc_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?")
    (("1" (DELETE -2)
      (("1" (EXPAND "empty?")
        (("1" (SKOLEM!)
          (("1" (INST - "k!1" "x!1")
            (("1" (INST - "k!1") (("1" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST - "j!2" "k!1" "s!2") (("2" (ASSERT) NIL NIL)) NIL)
     ("3" (DELETE -1 -2 3)
      (("3" (EXPAND "empty?")
        (("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL))
      NIL)
     ("4" (INST - "j!2" "k!1" "s!2") (("4" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|wakeup_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE "empty?")
    (("1" (INST - "j!2" "k!1" "s!1") (("1" (ASSERT) NIL NIL)) NIL)
     ("2" (DELETE -2 -4 -5 -7)
      (("2" (EXPAND "empty?")
        (("2" (SKOLEM!)
          (("2" (INST - "k!1" "x!1")
            (("2" (INST - "k!1") (("2" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("3" (DELETE -1 -2 3)
      (("3" (EXPAND "empty?")
        (("3" (INST - "j!2") (("3" (REDUCE) NIL NIL)) NIL)) NIL))
      NIL)
     ("4" (INST - "j!2" "k!1" "s!1") (("4" (ASSERT) NIL NIL)) NIL)
     ("5" (INST - "j!2" "k!1" "s!1") (("5" (ASSERT) NIL NIL)) NIL)
     ("6" (DELETE -1 -2 -4 -6 -7 1 2)
      (("6" (EXPAND "empty?") (("6" (REDUCE) NIL NIL)) NIL)) NIL)
     ("7" (INST - "j!2" "k!1" "s!1")
      (("7" (ASSERT)
        (("7" (DELETE -1 -4 -5 -6 -7 1 2)
          (("7" (EXPAND "empty?") (("7" (REDUCE) NIL NIL)) NIL)) NIL))
        NIL))
      NIL)
     ("8" (INST - "j!2" "k!1" "s!1") (("8" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|release_P2| "" (GRIND :IF-MATCH NIL :EXCLUDE ("empty?"))
    (("1" (INST - "j!2" "k!1" "s!2") (("1" (ASSERT) NIL NIL)) NIL)
     ("2" (INST - "j!2" "k!1" "s!2")
      (("2" (ASSERT)
        (("2" (DELETE -2 -3 -4 -5 1 2)
          (("2" (EXPAND "empty?")
            (("2" (SKOLEM!)
              (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("3" (INST - "j!2" "k!1" "s!2") (("3" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|intransitive_blocking| "" (GRIND :IF-MATCH NIL)
    (("" (CASE "prio(j1!1) <= prio(j2!1)")
      (("1" (INST - "j1!1" "j2!1" "s!1")
        (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
       ("2" (INST - "j2!1" "j1!1" "s!2")
        (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|invar_P2_aux| "" (EXPAND "P3")
    (("" (SKOSIMP*) (("" (FORWARD-CHAIN "ceiling_prop1") NIL NIL)) NIL))
    NIL)
   (|invar_P2_aux2| "" (SKOLEM-TYPEPRED)
    ((""
      (USE "invar_P2_aux"
           ("g" "g!1 WITH [rsrc := wakeup(g!1`rsrc, j!1)]"))
      (("" (DELETE 2)
        (("" (EXPAND "P")
          (("" (GROUND)
            (("" (DELETE -2)
              (("" (AUTO-REWRITE "wakeup_P") (("" (REDUCE) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|step_P2_aux| "" (EXPAND "eligible")
    (("" (REDUCE)
      (("" (DELETE -4)
        (("" (EXPAND* "blocked" "empty?")
          (("" (REDUCE)
            (("" (USE "intransitive_blocking" ("j1" "j!1"))
              (("" (ASSERT)
                (("" (DELETE -4)
                  (("" (FORWARD-CHAIN "prio_blocker") NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|init_P2| "" (GRIND) NIL NIL)
   (|step_P2| ""
    (AUTO-REWRITE "idle_step" "alloc_P2" "wakeup_P2" "release_P2"
                  "step_P2_aux" "invar_P2_aux" "invar_P2_aux2"
                  ("step" "run_step" "T"))
    (("" (REDUCE) NIL NIL)) NIL)
   (|mutual_exclusion| "" (GRIND :IF-MATCH NIL)
    (("" (INST? -2 :IF-MATCH ALL)
      (("" (ASSERT)
        (("" (INST-CP - "j!1" "k!1" "x!1")
          (("" (INST - "k!1" "j!1" "x!1") (("" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|unique_blocker| "" (GRIND :IF-MATCH NIL)
    (("" (CASE "prio(j1!1) <= prio(j2!1)")
      (("1" (INST - "j1!1" "j2!1" "s!1")
        (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
       ("2" (INST - "j2!1" "j1!1" "s!2")
        (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|blockers_in_cs| "" (SKOSIMP)
    (("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL))
    NIL)
   (|eligible_prio| "" (SKOSIMP)
    (("" (CASE "topjob(g!1, k!1)")
      (("1" (ASSERT)
        (("1" (EXPAND* "topjob" "precedes")
          (("1" (FLATTEN) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL)
       ("2" (ASSERT)
        (("2" (EXPAND "eligible")
          (("2" (SKOSIMP)
            (("2" (DELETE 1)
              (("2" (CASE "prio(j!1) = prio(k!1)")
                (("1" (ASSERT)
                  (("1" (EXPAND "Q")
                    (("1" (INST - "j!1" "k!1")
                      (("1" (ASSERT)
                        (("1" (EXPAND "precedes")
                          (("1" (DELETE -1 -3 -4 -5 2)
                            (("1" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (FORWARD-CHAIN "topjob_maxprio")
                  (("2" (DELETE -2 -3 -4 -5) (("2" (GRIND) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blockers_step| "" (SKOSIMP)
    (("" (EXPAND* "T" "subset?")
      (("" (REDUCE)
        (("1" (EXPAND "idle_step") (("1" (PROPAX) NIL NIL)) NIL)
         ("2" (DELETE -4)
          (("2" (CASE-REPLACE "j!2 = x!1")
            (("1" (CASE "prio(j!1) <= prio(x!1)")
              (("1" (ASSERT)
                (("1" (DELETE -2 -3 -4 -5 1)
                  (("1" (GRIND :EXCLUDE ("blk" "step")) NIL NIL)) NIL))
                NIL)
               ("2" (FORWARD-CHAIN "eligible_prio")
                (("2" (EXPAND "precedes") (("2" (GROUND) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (FORWARD-CHAIN "eligible_ready")
              (("2" (ASSERT)
                (("2" (DELETE -1 -2 -3 -4)
                  (("2" (EXPAND* "member" "blockers")
                    (("2" (GROUND)
                      (("2" (DELETE -2) (("2" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|unique_blocker2| "" (GRIND :IF-MATCH NIL)
    (("" (CASE "prio(j1!1) <= prio(j2!1)")
      (("1" (INST - "j1!1" "j2!1" "s!1")
        (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
       ("2" (INST - "j2!1" "j1!1" "s!2")
        (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|blockers_in_cs2| "" (SKOSIMP)
    (("" (GRIND :EXCLUDE ("needs") :REWRITES ("good_prop")) NIL NIL))
    NIL)
   (|eligible_prio2| "" (SKOSIMP*)
    (("" (GRIND :EXCLUDE ("blocked")) NIL NIL)) NIL)
   (|blockers_step2| "" (SKOSIMP)
    (("" (EXPAND* "T" "subset?" "idle_step")
      (("" (REDUCE)
        (("" (DELETE -4)
          (("" (CASE-REPLACE "j!2 = x!1")
            (("1" (USE "eligible_prio2")
              (("1" (GROUND)
                (("1" (DELETE -2 -3 -4 -5 1)
                  (("1" (GRIND :EXCLUDE ("step")) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (FORWARD-CHAIN "eligible_ready")
              (("2" (ASSERT)
                (("2" (DELETE -1 -2 -3 -4) (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$traces.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Traces for priority ceiling protocol  %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  traces [ (IMPORTING programs)
  	job: TYPE,
  	prio: [job -> priority],
  	dispatch: [job -> nat],
  	prog: [job -> prog] ] : THEORY
  
    BEGIN
  
    ASSUMING
  
    j: VAR job 
    s: VAR semaphore
  
    good_ceiling: ASSUMPTION
        member(s, resources(prog(j))) IMPLIES prio(j) <= ceil(s)
  
    good_programs: ASSUMPTION  well_behaved(prog(j))
  
    ENDASSUMING
  
    IMPORTING priority_ceiling[job, prio, dispatch, prog]
  
    j1, j2, k: VAR job
    p: VAR priority
    n, m, t, t1, t2: VAR nat
  
    g, g1, g2: VAR good_state
  
   
  
    %%%%%%%%%%%%%%%
    %   Traces    %
    %%%%%%%%%%%%%%%
  
    %-----------------------
    %  Existence of traces
    %-----------------------      
  
    next_state_exists: LEMMA EXISTS g2: T(g1, g2)
  
    tr(t): RECURSIVE good_state = 
       IF t=0 THEN init_sch ELSE epsilon! g: T(tr(t-1), g) ENDIF
     MEASURE t
  
  
    %----------
    %  traces
    %---------- 
  
    trace: NONEMPTY_TYPE = 
       { w: [nat -> good_state] | w(0) = init_sch AND FORALL t: T(w(t), w(t+1))
  }
  	CONTAINING tr
  
    tr_is_a_trace: JUDGEMENT tr HAS_TYPE trace
  
    u, v: VAR trace
  
    init_trace: LEMMA u(0) = init_sch
  
    step_trace: LEMMA T(u(t), u(t+1))
  
  
    %-------------------
    %  Main invariants
    %-------------------
  
    invariance_P2: PROPOSITION  FORALL t: P2(u(t)`rsrc)
  
    invariance_Q: PROPOSITION FORALL t: Q(u(t))
  
    time_invariant: PROPOSITION FORALL t: u(t)`time = t
  
    
  
    %-------------
    %  Clean up
    %-------------
  
    pc(u, j, t): pc(prog(j)) = u(t)`pc(j)
  
    finished(u, j, t): bool = finished(u(t), j)
  
    ready(u, j, t): bool = ready(u(t), j)
  
    active(u, j, t): bool = eligible(u(t), j) AND u(t+1) = step(u(t), j)
  
    blockers(u, j, t): set[job] = blockers(u(t)`rsrc, j)
  
    blockers(u, p, t): set[job] = blockers(u(t)`rsrc, p)
  
    busy(u, p, t): bool = EXISTS j: prio(j) >= p AND ready(u, j, t)
  
    busy(u, p, t1, t2): bool = FORALL t: t1 <= t AND t <= t2 IMPLIES busy(u, p,
  t)
  
  
  
    %------------------------------------
    %  Results from priority_ceiling
    %------------------------------------
  
    pc_init: LEMMA pc(u, j, 0) = 0
  
    pc_step: LEMMA 
  	pc(u, j, t+1) = IF active(u, j, t) THEN pc(u, j, t) + 1 ELSE pc(u, j, t
 ) ENDIF
  
    pc_increasing: LEMMA
  	t1 <= t2 IMPLIES pc(u, j, t1) <= pc(u, j, t2)
  
    pc_before_dispatch: LEMMA t <= dispatch(j) IMPLIES pc(u, j, t) = 0
  
  
    active_ready: LEMMA active(u, j, t) IMPLIES ready(u, j, t)
  
    active_unique: LEMMA active(u, j, t) AND active(u, k, t) IMPLIES j = k
  
  
    ready_after_dispatch: LEMMA ready(u, j, t) IMPLIES dispatch(j) <= t
  
    ready_equiv: LEMMA 
  	ready(u, j, t) IFF dispatch(j) <= t AND pc(u, j, t) < length(prog(j))
  
    ready_at_dispatch: LEMMA ready(u, j, dispatch(j))
  
    finished_equiv: LEMMA
  	finished(u, j, t) IFF pc(u, j, t) = length(prog(j))
  
    finished_stable: LEMMA
  	t1 <= t2 AND finished(u, j, t1) IMPLIES finished(u, j, t2)
  
    readiness: LEMMA (EXISTS j: ready(u, j, t)) IMPLIES (EXISTS j: active(u, j,
  t))
  
    readiness_step2: LEMMA
   	ready(u, j, t+1) AND dispatch(j) <= t IMPLIES ready(u, j, t)
   
    readiness_interval: LEMMA
  	ready(u, j, t1) AND dispatch(j) <= t AND t <= t1 IMPLIES ready(u, j, t)
  
  
    active_prio: LEMMA 
  	active(u, k, t) AND ready(u, j, t)
  	    IMPLIES precedes(k, j) OR member(k, blockers(u, j, t))
  
    active_prio2: LEMMA
  	busy(u, p, t) AND active(u, k, t) IMPLIES 
  	    prio(k) >= p OR member(k, blockers(u, p, t))
  
  
    single_blocker: LEMMA 
  	member(j1, blockers(u, k, t)) AND member(j2, blockers(u, k, t)) IMPLIES
  j1 = j2
  
    single_blocker2: LEMMA
  	member(j1, blockers(u, p, t)) AND member(j2, blockers(u, p, t)) IMPLIES
  j1 = j2
  
  
    blocker_in_cs: LEMMA
          member(j, blockers(u, k, t)) IMPLIES cs(prog(j), pc(u, j, t), prio(k)
 )   
  
    blocker_in_cs2: LEMMA
  	member(k, blockers(u, p, t)) IMPLIES cs(prog(k), pc(u, k, t), p)
  
  
    blocker_step: LEMMA
          ready(u, j, t) IMPLIES subset?(blockers(u, j, t+1), blockers(u, j, t)
 )
  
    blocker_step2: LEMMA
  	busy(u, p, t) IMPLIES subset?(blockers(u, p, t+1), blockers(u, p, t))
  
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%
    %   Scheduling analysis   %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    IMPORTING schedules[job]
  
    %-----------------------------
    %  schedule given by trace u
    %-----------------------------
  
    sch(u): schedule = sched(lambda j, t: active(u, j, t))
  
    active_prop: LEMMA active(sch(u), j, t) IFF active(u, j, t)
  
    process_time1: LEMMA process_time(sch(u), t, j) = pc(u, j, t)
  
    process_time2: LEMMA 
  	t1 <= t2 IMPLIES 
  	    process_time(sch(u), t1, t2, j) = pc(u, j, t2) - pc(u, j, t1)
  
    process_time_max: LEMMA
  	process_time(sch(u), t, j) <= length(prog(j))
  
    process_time_before_dispatch: LEMMA 
  	t <= dispatch(j) IMPLIES process_time(sch(u), t, j) = 0
  
    process_time_at_dispatch: LEMMA
  	process_time(sch(u), dispatch(j), j) = 0
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Blocking time for a job j   %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   
    %-------------------------------------------------------
    %  the blocker of j is determined at j's dispatch time
    %-------------------------------------------------------
  
    blocker(u, j): set[job] = blockers(u, j, dispatch(j))
  
    blockers_at_dispatch: LEMMA 
  	ready(u, j, t) IMPLIES subset?(blockers(u, j, t), blocker(u, j))
  
    active_priority: LEMMA
  	ready(u, j, t) AND active(u, k, t) IMPLIES
  	    precedes(k, j) OR member(k, blocker(u, j))
  
    blockers_in_critical_section: LEMMA
  	ready(u, j, t) AND member(k, blocker(u, j)) AND t1=dispatch(j)
  	    IMPLIES pc(u, k, t) = pc(u, k, t1)
  	         OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), prio(j
 ))
  
    blockers_dispatch: LEMMA
  	member(k, blocker(u, j)) IMPLIES dispatch(k) < dispatch(j)
  
  
    %------------------
    %  Blocking for j
    %------------------
  
    the_blocker(u, (j | not empty?(blocker(u, j)))): job = choose(blocker(u, j)
 )
  
    blocker_def: LEMMA 
  	empty?(blocker(u, j)) OR blocker(u, j) = singleton(the_blocker(u, j))
  
    blocker_prio: LEMMA
  	not empty?(blocker(u, j)) IMPLIES prio(the_blocker(u, j)) < prio(j)
  
    blocker_prop: LEMMA
  	not empty?(blocker(u, j)) IMPLIES j /= the_blocker(u, j)
  
    blocking(u, j): nat =
  	IF empty?(blocker(u, j)) THEN 0 ELSE max_cs(prog(the_blocker(u, j)), pr
 io(j)) ENDIF
  
    blocking_time: LEMMA
  	ready(u, j, t2) AND t1=dispatch(j)
  	    IMPLIES process_time(sch(u), t1, t2, blocker(u, j)) <= blocking(u, 
 j)
  
  
  
    %--------------------------------------------------------------------------
 -
    %  schedulable(u, j, t): j can fit in the interval [dispatch(j), t]
    %--------------------------------------------------------------------------
 -
  
    H(j): set[job] = { k | k /= j AND precedes(k, j) }
  
    schedulable(u, j, t): bool = 
  	process_time(sch(u), dispatch(j), t, H(j)) + blocking(u, j) + 
  	    length(prog(j)) <= t - dispatch(j)
  
    process_time_ready_job: LEMMA
  	ready(u, j, t2) AND t1 = dispatch(j) IMPLIES
  	    process_time(sch(u), t1, t2, j) = (t2 - t1) 
  		- process_time(sch(u), t1, t2, H(j))
  		- process_time(sch(u), t1, t2, blocker(u, j))
  
    schedulable_prop: LEMMA
  	schedulable(u, j, t) IMPLIES finished(u, j, t)
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %  Blocking for the set of jobs of priority >= p   %
    %  in a busy interval [t1, t2]                     %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    K(p): set[job] = { j | prio(j) >= p }
  
    %----------------------------------------------------------
    %  The blocker is determined at the start of the interval
    %----------------------------------------------------------
  
    blockers_busy: LEMMA
  	busy(u, p, t1, t2) AND t1 <= t AND t <= t2 IMPLIES 
  	    subset?(blockers(u, p, t), blockers(u, p, t1))
  
    active_priority2: LEMMA
  	busy(u, p, t1, t2) AND t1 <= t AND t <= t2 AND active(u, j, t)
  	    IMPLIES prio(j) >= p OR member(j, blockers(u, p, t1))
  
    blocker_in_critical_section2: LEMMA 
  	busy(u, p, t1, t2) AND member(k, blockers(u, p, t1))
  	    AND t1 <= t AND t <= t2 IMPLIES pc(u, k, t) = pc(u, k, t1)
  		OR critical_section(prog(k), pc(u, k, t1), pc(u, k, t), p)
  
    blocker_dispatch2: LEMMA
  	member(k, blockers(u, p, t1)) IMPLIES dispatch(k) < t1
  
  
    %---------------------
    %  Blocking for K(p)
    %---------------------
  
    the_blocker(u, p, (t | not empty?(blockers(u, p, t)))): job = choose(blocke
 rs(u, p, t))
  
    blocker_def2: LEMMA 
         empty?(blockers(u, p, t)) OR blockers(u, p, t) = singleton(the_blocker
 (u, p, t))
  
    blocker_prio2: LEMMA
  	not empty?(blockers(u, p, t)) IMPLIES prio(the_blocker(u, p, t)) < p
  
    blocking(u, p, t): nat = 
        IF empty?(blockers(u, p, t)) THEN 0 ELSE max_cs(prog(the_blocker(u, p, 
 t)), p) ENDIF
  
    blocking_time2: LEMMA busy(u, p, t1, t2) IMPLIES 
  	process_time(sch(u), t1, t2, blockers(u, p, t1)) <= blocking(u, p, t1)
  
  
    %-----------------------------------------------------
    %  Process time allocated to K(p) in a busy interval
    %-----------------------------------------------------
  
    process_time_busy_interval: LEMMA
  	busy(u, p, t1, t2) AND t1 <= t2 IMPLIES 
  	   process_time(sch(u), t1, t2, K(p)) = 
  		t2 - t1 - process_time(sch(u), t1, t2, blockers(u, p, t1))
  
    busy_time2: LEMMA busy(u, p, t1, t2) AND t1 <= t2 IMPLIES 
  	process_time(sch(u), t1, t2, K(p)) >= t2 - t1 - blocking(u, p, t1)
  
  
  
    %-----------------------------------------------------------------
    %  Relation between blocker of j and blocker of K(p) in [t1, t2]
    %-----------------------------------------------------------------
  
    blockers_prop: LEMMA
  	busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio
 (j) = p 
  	    IMPLIES subset?(blocker(u, j), blockers(u, p, t1))
  
    blocking_prop: LEMMA
  	busy(u, p, t1, t2) AND t1 <= dispatch(j) AND dispatch(j) <= t2 AND prio
 (j) = p 
  	    IMPLIES blocking(u, j) = 0 OR blocking(u, j) = blocking(u, p, t1)
  
    END traces
  
  $$$traces.prf
  (|traces|
   (|IMP_priority_ceiling_TCC1| "" (LEMMA "good_ceiling")
    (("" (PROPAX) NIL NIL)) NIL)
   (|IMP_priority_ceiling_TCC2| "" (LEMMA "good_programs")
    (("" (PROPAX) NIL NIL)) NIL)
   (|next_state_exists| "" (AUTO-REWRITE "T" "idle_P" "step_P" "eligible_ready"
 )
    (("" (SKOLEM!)
      (("" (CASE "idle(g1!1)")
        (("1" (INST + "idle_step(g1!1)") (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (ASSERT)
          (("2" (EXPAND "idle")
            (("2" (SKOLEM!)
              (("2" (ASSERT)
                (("2" (INST + "step(g1!1, j!1)")
                  (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|tr_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|tr_TCC2| "" (TERMINATION-TCC) NIL NIL
 )
   (|trace_TCC1| "" (AUTO-REWRITE "tr")
    (("" (GROUND)
      (("" (SKOLEM!)
        (("" (USE "epsilon_ax[good_state]")
          (("" (ASSERT) (("" (REWRITE "next_state_exists") NIL NIL)) NIL)) NIL)
 )
        NIL))
      NIL))
    NIL)
   (|tr_is_a_trace| "" (LEMMA "trace_TCC1") (("" (PROPAX) NIL NIL)) NIL)
   (|init_trace| "" (REDUCE) NIL NIL)
   (|step_trace| "" (REDUCE :POLARITY? T) NIL NIL)
   (|invariance_P2| "" (AUTO-REWRITE "init_sch" "init_P2")
    (("" (SKOLEM + ("u!1" _))
      (("" (INDUCT "t")
        (("1" (ASSERT)
          (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (SKOSIMP)
          (("2" (USE* "step_trace" "step_P2") (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|invariance_Q| "" (SKOLEM + ("u!1" _))
    (("" (AUTO-REWRITE "init_Q" "init_trace")
      (("" (INDUCT "t")
        (("1" (ASSERT)
          (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (SKOSIMP)
          (("2" (USE* "step_trace" "step_Q") (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|time_invariant| "" (AUTO-REWRITE "init_sch")
    (("" (INDUCT "t")
      (("1" (SKOLEM!)
        (("1" (REWRITE "init_trace") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
       ("2" (SKOSIMP*)
        (("2" (INST?)
          (("2" (USE "step_trace")
            (("2" (GRIND :EXCLUDE ("idle" "eligible" "run_step")) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|active_TCC1| "" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL))
    NIL)
   (|pc_init| "" (GRIND :EXCLUDE ("T")) NIL NIL)
   (|pc_step| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (AUTO-REWRITE "pc" "step" "active") (("1" (REDUCE) NIL NIL)) NIL)
       ("2" (EXPAND "active")
        (("2" (USE "step_trace")
          (("2" (EXPAND "T")
            (("2" (AUTO-REWRITE "pc" "idle_step" "step")
              (("2" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|pc_increasing| "" (SKOLEM + ("j!1" "t1!1" _ "u!1"))
    (("" (INDUCT-AND-REWRITE "t2" 1 "pc_init" "pc_step")
      (("1" (CASE-REPLACE "t1!1 = 0")
        (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)
       ("2" (CASE "active(u!1, j!1, j!2)")
        (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|pc_before_dispatch| "" (AUTO-REWRITE "pc" "P" "time_invariant")
    (("" (SKOSIMP) (("" (TYPEPRED "u!1(t!1)") (("" (REDUCE) NIL NIL)) NIL))
      NIL))
    NIL)
   (|active_ready| "" (EXPAND* "active" "ready")
    (("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_ready") NIL NIL)) NIL)) NIL)
   (|active_unique| "" (EXPAND "active")
    (("" (SKOSIMP)
      (("" (FORWARD-CHAIN "eligible_ready")
        (("" (ASSERT)
          (("" (AUTO-REWRITE "step")
            (("" (CASE "step(u!1(t!1), j!1)`pc(j!1) = u!1(t!1)`pc(j!1)")
              (("1" (ASSERT) NIL NIL)
               ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|ready_after_dispatch| "" (AUTO-REWRITE "time_invariant" "ready")
    (("" (SKOSIMP) (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)
   (|ready_equiv| "" (SKOLEM!)
    (("" (GRIND :REWRITES ("time_invariant")) NIL NIL)) NIL)
   (|ready_at_dispatch| "" (SKOLEM!)
    (("" (AUTO-REWRITE "ready_equiv" "pc_before_dispatch")
      (("" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|finished_equiv| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL)
   (|finished_stable| "" (AUTO-REWRITE "finished_equiv")
    (("" (SKOSIMP)
      (("" (ASSERT)
        (("" (USE "pc_increasing" ("t2" "t2!1")) (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|readiness| "" (SKOSIMP)
    (("" (EXPAND* "ready" "active")
      (("" (AUTO-REWRITE "idle")
        (("" (FORWARD-CHAIN "eligible_exists")
          (("" (USE "step_trace")
            (("" (EXPAND "T") (("" (GROUND) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|readiness_step2| "" (AUTO-REWRITE "step_trace" "time_invariant")
    (("" (EXPAND "ready")
      (("" (SKOSIMP)
        (("" (USE "readiness_step" ("g1" "u!1(t!1)")) (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|readiness_interval| "" (EXPAND* "ready" "ready" "finished" "complete")
    (("" (AUTO-REWRITE "time_invariant" "pc")
      (("" (SKOSIMP)
        (("" (ASSERT)
          (("" (DELETE -1 -2)
            (("" (USE "pc_increasing") (("" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|active_prio| "" (EXPAND* "active" "ready" "blockers")
    (("" (SKOSIMP)
      (("" (USE "invariance_Q") (("" (FORWARD-CHAIN "eligible_prio") NIL NIL))
        NIL))
      NIL))
    NIL)
   (|active_prio2| "" (EXPAND* "busy" "blockers" "active" "ready")
    (("" (SKOSIMP) (("" (FORWARD-CHAIN "eligible_prio2") NIL NIL)) NIL)) NIL)
   (|single_blocker| "" (EXPAND "blockers")
    (("" (SKOSIMP)
      (("" (AUTO-REWRITE "invariance_P2")
        (("" (USE "unique_blocker") (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|single_blocker2| "" (AUTO-REWRITE "invariance_P2" "blockers")
    (("" (SKOSIMP)
      (("" (ASSERT) (("" (USE "unique_blocker2") (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_in_cs| "" (EXPAND* "blockers" "pc")
    (("" (SKOSIMP) (("" (REWRITE "blockers_in_cs") NIL NIL)) NIL)) NIL)
   (|blocker_in_cs2| "" (AUTO-REWRITE "pc" "blockers" "time_invariant")
    (("" (SKOSIMP)
      (("" (ASSERT) (("" (FORWARD-CHAIN "blockers_in_cs2") NIL NIL)) NIL)) NIL)
 )
    NIL)
   (|blocker_step| "" (AUTO-REWRITE "step_trace" "invariance_Q")
    (("" (EXPAND* "ready" "blockers")
      (("" (SKOSIMP) (("" (REWRITE "blockers_step") NIL NIL)) NIL)) NIL))
    NIL)
   (|blocker_step2| "" (EXPAND* "busy" "blockers" "ready")
    (("" (AUTO-REWRITE "step_trace")
      (("" (SKOSIMP) (("" (REWRITE "blockers_step2") NIL NIL)) NIL)) NIL))
    NIL)
   (|sch_TCC1| "" (SKOSIMP*)
    (("" (USE "active_unique") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|active_prop| "" (AUTO-REWRITE "sch_TCC1")
    (("" (SKOLEM!)
      (("" (EXPAND "sch") (("" (REWRITE "schedule_from_act1") NIL NIL)) NIL))
      NIL))
    NIL)
   (|process_time1| ""
    (INDUCT-AND-REWRITE "t" 1 "pc_init" "pc_step"
     ("process_time_init" "process_time_step") "active_prop")
    NIL NIL)
   (|process_time2| "" (AUTO-REWRITE "process_time_equiv2" "process_time1")
    (("" (REDUCE) NIL NIL)) NIL)
   (|process_time_max| "" (AUTO-REWRITE "process_time1" "pc")
    (("" (REDUCE) NIL NIL)) NIL)
   (|process_time_before_dispatch| ""
    (INDUCT-AND-REWRITE "t" 1 "process_time1" "pc_init" ("pc_step"))
    (("" (FORWARD-CHAIN "active_ready")
      (("" (FORWARD-CHAIN "ready_after_dispatch") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|process_time_at_dispatch| "" (SKOLEM!)
    (("" (REWRITE "process_time_before_dispatch") NIL NIL)) NIL)
   (|blockers_at_dispatch| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: ready(u!1, j!1, n + dispatch(j!1)) IMPLIES subset?(block
 ers(u!1, j!1, n + dispatch(j!1)), blockers(u!1, j!1, dispatch(j!1)))")
      (("1" (FORWARD-CHAIN "ready_after_dispatch")
        (("1" (EXPAND "blocker")
          (("1" (ASSERT)
            (("1" (INST - "t!1 - dispatch(j!1)") (("1" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE -1 2)
        (("2" (AUTO-REWRITE-THEORY "sets[job]")
          (("2" (INDUCT "n")
            (("1" (REDUCE) NIL NIL)
             ("2" (SKOSIMP)
              (("2" (USE "readiness_step2")
                (("2" (ASSERT)
                  (("2" (FORWARD-CHAIN "blocker_step")
                    (("2" (ASSERT)
                      (("2" (APPLY (THEN (SKOSIMP) (INST?) (INST?) (ASSERT)))
                        NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|active_priority| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "active_prio")
      (("" (FORWARD-CHAIN "blockers_at_dispatch")
        (("" (APPLY (THEN (EXPAND "subset?") (INST?) (ASSERT))) NIL NIL)) NIL))
      NIL))
    NIL)
   (|blockers_in_critical_section| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: ready(u!1, j!1, t1!1 + n) IMPLIES pc(u!1, k!1, t1!1 + n)
  = pc(u!1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!
 1, k!1, t1!1 + n), prio(j!1))")
      (("1" (FORWARD-CHAIN "ready_after_dispatch")
        (("1" (ASSERT)
          (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL)
       ("2" (DELETE -1 2 3)
        (("2" (INDUCT "n")
          (("1" (GROUND) NIL NIL)
           ("2" (SKOSIMP)
            (("2" (CASE "ready(u!1, j!1, t1!1+j!2)")
              (("1" (ASSERT)
                (("1" (AUTO-REWRITE "pc_step")
                  (("1" (CASE "active(u!1, k!1, j!2 + t1!1)")
                    (("1" (ASSERT)
                      (("1" (FORWARD-CHAIN "active_prio")
                        (("1" (DELETE -2 -3 -4 -5 -7 1 2)
                          (("1" (GRIND :EXCLUDE ("blk")) NIL NIL)) NIL)
                         ("2" (FORWARD-CHAIN "blocker_in_cs")
                          (("2" (DELETE -2 -3 -4 -6 -7 -8)
                            (("2" (EXPAND "critical_section")
                              (("2" (REDUCE :IF-MATCH NIL)
                                (("2" (INST? :POLARITY? T)
                                  (("2" (ASSERT) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (DELETE -1 -3 2 3)
                (("2" (USE "readiness_step2") (("2" (GROUND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blockers_dispatch| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant")
    (("" (SKOSIMP)
      (("" (EXPAND "blocker")
        (("" (FORWARD-CHAIN "blocker_in_cs")
          (("" (EXPAND "pc")
            (("" (TYPEPRED "u!1(dispatch(j!1))")
              (("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|the_blocker_TCC1| "" (EXPAND "nonempty?") (("" (PROPAX) NIL NIL)) NIL)
   (|blocker_def| "" (SKOSIMP)
    (("" (AUTO-REWRITE "member" "singleton" "the_blocker" "nonempty?")
      (("" (APPLY-EXTENSIONALITY 2 :HIDE? T)
        (("" (SMASH)
          (("" (USE "single_blocker" ("t" "dispatch(j!1)"))
            (("" (REWRITE "blocker" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)
 )
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_prio| "" (SKOSIMP)
    (("" (AUTO-REWRITE "nonempty?" "the_blocker")
      (("" (ASSERT)
        (("" (TYPEPRED "choose(blocker(u!1, j!1))")
          (("" (AUTO-REWRITE "blocker" "blockers")
            (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_prop| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "blocker_prio") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|blocking_time| "" (EXPAND "blocking")
    (("" (SKOSIMP)
      (("" (USE "blocker_def")
        (("" (SMASH)
          (("1" (REWRITE "emptyset_is_empty?")
            (("1" (REPLACE*)
              (("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL)
           ("2" (REPLACE*)
            (("2" (REWRITE "process_time" :DIR RL)
              (("2" (FORWARD-CHAIN "ready_after_dispatch")
                (("2" (ASSERT)
                  (("2" (REWRITE "process_time2")
                    (("2"
                      (USE "blockers_in_critical_section"
                           ("k" "the_blocker(u!1, j!1)" "t" "t2!1" "t1" "t1!1")
 )
                      (("2" (GROUND)
                        (("1" (FORWARD-CHAIN "max_cs2") (("1" (ASSERT) NIL NIL)
 )
                          NIL)
                         ("2" (EXPAND* "member" "the_blocker") NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_ready_job| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "ready_after_dispatch")
      (("" (ASSERT)
        (("" (AUTO-REWRITE "active_prop" "idle_equiv")
          (("" (EXPAND "process_time" 1 1)
            (("" (REPLACE -3 - RL)
              (("" (USE "total_cpu")
                (("" (ASSERT)
                  (("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0")
                    (("1" (DELETE -1)
                      (("1" (ASSERT)
                        (("1"
                          (USE "process_time_partition4"
                               ("E" "fullset[job]" "E1" "singleton(j!1)" "E2"
                                "H(j!1)" "E3" "blocker(u!1, j!1)" "E4"
                                "{ k | not blocker(u!1, j!1)(k) AND not precede
 s(k, j!1) }"))
                          (("1" (GROUND)
                            (("1"
                              (CASE-REPLACE
                               "process_time(sch(u!1), t1!1, t2!1, {k: job | NO
 T blocker(u!1, j!1)(k) AND NOT precedes(k, j!1)}) = 0")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (DELETE -1 -2 2)
                                (("2" (REWRITE "zero_process_time")
                                  (("2" (SKOSIMP)
                                    (("2"
                                      (USE "readiness_interval"
                                           ("t" "t!1" "t1" "t2!1"))
                                      (("2" (ASSERT)
                                        (("2"
                                          (FORWARD-CHAIN "active_priority")
                                          (("2"
                                            (EXPAND "member")
                                            (("2" (PROPAX) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (DELETE -1 -2 -3 -4 2)
                              (("2" (GRIND :EXCLUDE ("blk"))
                                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                                  (("2" (SMASH) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (DELETE -1 2)
                      (("2" (REWRITE "zero_idle_time")
                        (("2" (SKOSIMP)
                          (("2" (USE "readiness" ("t" "t!1"))
                            (("2" (GROUND)
                              (("2"
                                (USE "readiness_interval"
                                     ("t" "t!1" "t1" "t2!1"))
                                (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|schedulable_prop| "" (SKOSIMP)
    (("" (EXPAND "schedulable")
      (("" (ASSERT)
        (("" (CASE "ready(u!1, j!1, t!1)")
          (("1" (ASSERT)
            (("1" (USE* "process_time_ready_job" "blocking_time")
              (("1" (ASSERT)
                (("1"
                  (AUTO-REWRITE "process_time_equiv2" "process_time_at_dispatch
 "
                                "ready_equiv" "process_time1")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (DELETE -)
            (("2" (AUTO-REWRITE "ready_equiv" "finished" "complete" "pc")
              (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blockers_busy| "" (SKOSIMP)
    ((""
      (CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES subset?(blockers(u!1, p!1, t1!1
 +n), blockers(u!1, p!1, t1!1))")
      (("1" (ASSERT) (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL))
        NIL)
       ("2" (DELETE -2 -3 2)
        (("2" (INDUCT "n")
          (("1" (GROUND) (("1" (GRIND :EXCLUDE ("blockers" "busy")) NIL NIL))
            NIL)
           ("2" (SKOSIMP)
            (("2" (ASSERT)
              (("2" (EXPAND "busy")
                (("2" (INST - "t1!1 + j!1")
                  (("2" (ASSERT)
                    (("2" (FORWARD-CHAIN "blocker_step2")
                      (("2" (DELETE -3 -4)
                        (("2" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|active_priority2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "blockers_busy")
      (("" (EXPAND "busy")
        (("" (INST?)
          (("" (ASSERT)
            (("" (FORWARD-CHAIN "active_prio2")
              (("" (DELETE -3 -4 -5 -6 1)
                (("" (GRIND :EXCLUDE ("blockers")) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_in_critical_section2| "" (SKOSIMP)
    (("" (ASSERT)
      ((""
        (CASE "FORALL n: t1!1 + n <= t2!1 IMPLIES pc(u!1, k!1, t1!1 + n) = pc(u
 !1, k!1, t1!1) OR critical_section(prog(k!1), pc(u!1, k!1, t1!1), pc(u!1, k!1,
  t1!1+n), p!1)")
        (("1" (INST - "t!1 - t1!1") (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2 3)
          (("2" (INDUCT "n")
            (("1" (GROUND) NIL NIL)
             ("2" (SKOSIMP)
              (("2" (ASSERT)
                (("2" (AUTO-REWRITE "pc_step")
                  (("2" (CASE "active(u!1, k!1, j!1 + t1!1)")
                    (("1" (ASSERT)
                      (("1" (DELETE 1)
                        (("1" (EXPAND "busy")
                          (("1" (INST - "t1!1 + j!1")
                            (("1" (ASSERT)
                              (("1" (FORWARD-CHAIN "active_prio2")
                                (("1" (DELETE -2 -3 -4 -5 -7 -8 1)
                                  (("1" (GRIND) NIL NIL)) NIL)
                                 ("2" (FORWARD-CHAIN "blocker_in_cs2")
                                  (("2" (DELETE -2 -3 -5 -6 -7 -8 -9)
                                    (("2" (EXPAND "critical_section")
                                      (("2" (GROUND)
                                        (("1"
                                          (SKOSIMP)
                                          (("1" (ASSERT) NIL NIL))
                                          NIL)
                                         ("2"
                                          (SKOSIMP)
                                          (("2"
                                            (INST?)
                                            (("2" (ASSERT) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_dispatch2| "" (AUTO-REWRITE "initially_not_cs2" "time_invariant")
    (("" (SKOSIMP)
      (("" (EXPAND "blockers")
        (("" (FORWARD-CHAIN "blockers_in_cs2")
          (("" (TYPEPRED "u!1(t1!1)")
            (("" (EXPAND "P") (("" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|the_blocker_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|blocker_def2| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (AUTO-REWRITE "singleton" "member" "nonempty?" "the_blocker")
        (("" (APPLY-EXTENSIONALITY :HIDE? T)
          (("" (SMASH)
            ((""
              (USE "single_blocker2"
                   ("j1" "x!1" "j2" "the_blocker(u!1, p!1, t!1)"))
              (("" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocker_prio2| "" (SKOSIMP)
    (("" (AUTO-REWRITE "nonempty?" "the_blocker")
      (("" (ASSERT)
        (("" (TYPEPRED "choose(blockers(u!1, p!1, t!1))")
          (("" (AUTO-REWRITE "blockers")
            (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|blocking_time2| "" (SKOLEM!)
    (("" (EXPAND "blocking")
      (("" (SMASH)
        (("1" (REWRITE "emptyset_is_empty?")
          (("1" (REPLACE*)
            (("1" (REWRITE "process_time_emptyset") (("1" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL)
         ("2" (CASE "t1!1 <= t2!1")
          (("1" (USE "blocker_def2")
            (("1" (REDUCE)
              (("1" (REWRITE "process_time" :DIR RL)
                (("1" (REWRITE "process_time2")
                  (("1" (USE "blocker_in_critical_section2")
                    (("1" (GROUND)
                      (("1" (FORWARD-CHAIN "max_cs2") NIL NIL)
                       ("2" (EXPAND* "the_blocker" "member") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (AUTO-REWRITE "process_time" "sum") (("2" (ASSERT) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|process_time_busy_interval| "" (SKOSIMP)
    (("" (USE "total_cpu")
      (("" (AUTO-REWRITE "active_prop" "idle_equiv")
        (("" (ASSERT)
          (("" (CASE-REPLACE "idle_time(sch(u!1), t1!1, t2!1) = 0")
            (("1" (DELETE -1)
              (("1" (ASSERT)
                (("1"
                  (USE "process_time_partition3"
                       ("E" "fullset[job]" "E1" "K(p!1)" "E2"
                        "blockers(u!1, p!1, t1!1)" "E3"
                        "{ k | prio(k) < p!1 AND not member(k, blockers(u!1, p!
 1, t1!1)) }"))
                  (("1" (GROUND)
                    (("1"
                      (CASE-REPLACE
                       "process_time(sch(u!1), t1!1, t2!1, {k: job | prio(k) < 
 p!1 AND NOT member(k, blockers(u!1, p!1, t1!1))}) = 0")
                      (("1" (ASSERT) NIL NIL)
                       ("2" (DELETE -1 -2 2)
                        (("2" (REWRITE "zero_process_time")
                          (("2" (SKOSIMP)
                            (("2" (USE "active_priority2" ("j" "j!1"))
                              (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (DELETE -1 -2 -3 2)
                      (("2" (GRIND)
                        (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                          (("2" (SMASH) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (REWRITE "zero_idle_time")
                (("2" (SKOSIMP)
                  (("2" (REWRITE "readiness")
                    (("2" (AUTO-REWRITE "busy") (("2" (REDUCE) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|busy_time2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "process_time_busy_interval")
      (("" (FORWARD-CHAIN "blocking_time2") (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|blockers_prop| "" (SKOSIMP)
    (("" (CASE "subset?(blocker(u!1, j!1), blockers(u!1, p!1, dispatch(j!1)))")
      (("1" (FORWARD-CHAIN "blockers_busy")
        (("1" (DELETE -3 -4 -5 -6)
          (("1" (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL)
            (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE -1 -2 -3 2) (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|blocking_prop| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "blockers_prop")
      (("" (EXPAND "blocking")
        (("" (SMASH)
          (("1" (DELETE -2 -3 -4 -5 2)
            (("1"
              (APPLY (THEN (GRIND :EXCLUDE ("blocker" "blockers") :IF-MATCH NIL
 )
                      (INST?) (INST?) (ASSERT)))
              NIL NIL))
            NIL)
           ("2" (USE* "blocker_def" "blocker_def2")
            (("2" (GROUND)
              (("1" (DELETE -1 -4 -5 -6 -7 2 3)
                (("1" (GRIND :IF-MATCH NIL :EXCLUDE ("blockers" "blocker"))
                  (("1" (INST? :POLARITY? T)
                    (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL)
               ("2" (REPLACE*)
                (("2" (DELETE -1 -2 -4 -5 -6 -7 1 2)
                  (("2" (AUTO-REWRITE-THEORY "sets[job]")
                    (("2" (REDUCE :IF-MATCH NIL)
                      (("2" (INST - "the_blocker(u!1, j!1)")
                        (("2" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$fsets_sum.pvs
  %------------------------------------------------------------------------
  %  Finite sum over real-valued functions
  %  (reworked from Ricky Butler's version in finite set lib)
  %------------------------------------------------------------------------
  
  fsets_sum[T: TYPE]: THEORY
  
    BEGIN
  
  %%  IMPORTING finite_sets@finite_sets_sum[T,real,0,+]
  
    IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions
  
    S, A, B: VAR finite_set[T]
    E: VAR non_empty_finite_set[T]
    t, x, x1, x2: VAR T
    c, N: VAR real
    f, g: VAR function[T -> real]
  
  
  
  %% Things below and up to sum_distributive have been
  %% copied from finite_set@finite_sets_sum.
  %%
  %% Shouldn't need to do that but there was a problem with
  %% judgements otherwise. Bug in PVS: I can't reverse the 
  %% change? (7/19/99)
  %%
  %% Fixed by Sam (9/1/99) but still things do not work so well
  %% (auto-rewrite in proof of sum_indexed_partitions.sum_partition)
  %%
  
    %------------------------------------
    %  Definition and basic properties
    %------------------------------------
  
    sum(S, f) : RECURSIVE real  = 
        IF (empty?(S)) THEN 0 ELSE f(choose(S)) + sum(rest(S),f) ENDIF 
     MEASURE card(S)
  
  
    sum_emptyset  : THEOREM sum(emptyset, f) = 0
  
    sum_singleton : THEOREM sum(singleton(x), f) = f(x)
  
    sum_x         : THEOREM FORALL (x: (S)): sum(S, f) = f(x) + sum(remove(x, S
 ), f)
  
    sum_x1_x2     : THEOREM FORALL (x1, x2: (S)): 
  				f(x1) + sum(remove(x1, S), f) = f(x2) + sum(rem
 ove(x2, S), f)
  
    sum_add       : THEOREM sum(add(x, S),f) = 
  				IF S(x) THEN sum(S, f) ELSE sum(S, f) + f(x) EN
 DIF
  
    sum_remove    : THEOREM sum(remove(x, S),f) = 
  				IF S(x) THEN sum(S, f) - f(x) ELSE sum(S, f) EN
 DIF
  
    sum_rest      : THEOREM NOT empty?(S) IMPLIES 
  				f(choose(S)) + sum(rest(S),f) = sum(S,f)
   
    sum_disj_union: THEOREM disjoint?(A, B) IMPLIES 
  				sum(union(A, B), f) = sum(A, f) + sum(B, f) 
  
    sum_diff_subset: THEOREM subset?(A, B) IMPLIES 
  				sum(difference(B, A), f) = sum(B, f) - sum(A, f
 )
  
    sum_union      : THEOREM sum(union(A, B), f) + sum(intersection(A, B),f ) =
  sum(A, f) + sum(B, f) 
  
    sum_diff_intersection: THEOREM sum(A, f) = sum(difference(A, B), f) + sum(i
 ntersection(A, B), f) 
  
    sum_f_g         : THEOREM (FORALL (x: (S)): f(x) = g(x)) IMPLIES sum(S, f) 
 = sum(S, g)
  
    sum_particular  : THEOREM sum(S, f WITH [x := c]) = 
  				IF S(x) THEN  sum(S, f) + c - f(x) ELSE sum(S, 
 f) ENDIF 
  
    sum_distributive: THEOREM sum(A, f) + sum(A, g) = sum(A, LAMBDA x: f(x) + g
 (x)) 
  
  
  
    %---------------------------
    %  Sum for a few functions
    %---------------------------
  
    sum_const    : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) 
  
    sum_mult     : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) 
  
    sum_1_is_card: THEOREM sum(S,(LAMBDA t: 1)) = card(S)
  
    sum_update   : THEOREM sum(S, f WITH [(t) := c]) =
  			     IF S(t) THEN sum(S, f) - f(t) + c ELSE sum(S, f) E
 NDIF
  
  
    %------------------------------------------------------
    %  Ordering properties for two sums over the same set
    %------------------------------------------------------
  
    sum_le       : THEOREM (FORALL (t: (S)): f(t) <= g(t))
                               IMPLIES sum(S, f) <= sum(S, g)
  
    sum_ge       : THEOREM (FORALL (t: (S)): f(t) >= g(t))
                               IMPLIES sum(S, f) >= sum(S, g)
  
    sum_lt       : THEOREM (FORALL (t: (E)): f(t) < g(t))
                               IMPLIES sum(E, f) < sum(E, g)
  
    sum_gt       : THEOREM (FORALL (t: (E)): f(t) > g(t))
                               IMPLIES sum(E, f) > sum(E, g)
  
  
    %------------------------------------------------
    %  Bounds on sum derived from bounds of f on S
    %------------------------------------------------
  
    sum_bound    : THEOREM (FORALL (t: (S)): f(t) <= N) 
                               IMPLIES sum(S,f) <= N*card(S)
  
    sum_bound2   : THEOREM (FORALL (t: (S)): f(t) >= N) 
                               IMPLIES sum(S,f) >= N*card(S)
  
    sum_bound3   : THEOREM (FORALL (t: (E)): f(t) < N) 
                               IMPLIES sum(E,f) < N*card(E)
  
    sum_bound4   : THEOREM (FORALL (t: (E)): f(t) > N) 
                               IMPLIES sum(E,f) > N*card(E)
  
  
    %---------------------
    %  Sign of sum(S, f)
    %---------------------
  
    sum_nonneg   : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0
  
    sum_nonpos   : LEMMA (FORALL (t: (S)): f(t) <= 0) IMPLIES sum(S,f) <= 0
  
    sum_pos      : LEMMA (FORALL (t: (S)): f(t) >= 0) 
  			   AND (EXISTS (t: (S)): f(t) > 0) IMPLIES sum(S, f) > 
 0
  
    sum_pos2     : LEMMA (FORALL (t: (E)): f(t) > 0) IMPLIES sum(E,f) > 0
  
    sum_neg      : LEMMA (FORALL (t: (S)): f(t) <= 0) 
  			   AND (EXISTS (t: (S)): f(t) < 0) IMPLIES sum(S, f) < 
 0
  
    sum_neg2     : LEMMA (FORALL (t: (E)): f(t) < 0) IMPLIES sum(E,f) < 0
  
    sum_zero     : LEMMA (FORALL (t: (S)): f(t) = 0) IMPLIES sum(S, f) = 0
  
  
  
    %-----------------------
    %  Closure properties
    %-----------------------
  
    U: VAR set[real]  
  
    sum_closure1: LEMMA 
       (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (E)): U(f(t))) 
  	  IMPLIES U(sum(E, f))
  
    sum_closure2: LEMMA 
       U(0) AND (FORALL (a, b: (U)): U(a+b)) AND (FORALL (t: (S)): U(f(t))) 
  	  IMPLIES U(sum(S, f))
  
  
    %---------------
    %   Judgements
    %---------------
  
    nnf: VAR [T -> nonneg_real]
    npf: VAR [T -> nonpos_real]
    pf:  VAR [T -> posreal]
    nf:  VAR [T -> negreal]
  
    sum_nnreal_is_nnreal:   JUDGEMENT sum(S, nnf) HAS_TYPE nonneg_real
    sum_npreal_is_npreal:   JUDGEMENT sum(S, npf) HAS_TYPE nonpos_real
    sum_posreal_is_posreal: JUDGEMENT sum(E, pf)  HAS_TYPE posreal
    sum_negreal_is_negreal: JUDGEMENT sum(E, nf)  HAS_TYPE negreal
  
  
    u:   VAR [T -> rat]
    nnu: VAR [T -> nonneg_rat]
    npu: VAR [T -> nonpos_rat]
    pu:  VAR [T -> posrat]
    nu:  VAR [T -> negrat]
  
    sum_rat_is_rat:       JUDGEMENT sum(S, u)   HAS_TYPE rat
    sum_nnrat_is_nnrat:   JUDGEMENT sum(S, nnu) HAS_TYPE nonneg_rat
    sum_nprat_is_nprat:   JUDGEMENT sum(S, npu) HAS_TYPE nonpos_rat
    sum_posrat_is_posrat: JUDGEMENT sum(E, pu)  HAS_TYPE posrat
    sum_negrat_is_negrat: JUDGEMENT sum(E, nu)  HAS_TYPE negrat
  
  
    v:   VAR [T -> int]
    npv: VAR [T -> nonpos_int]
    nv:  VAR [T -> negint]
  
    sum_int_is_int:       JUDGEMENT sum(S, v)   HAS_TYPE int
    sum_npint_is_npint:   JUDGEMENT sum(S, npv) HAS_TYPE nonpos_int
    sum_negint_is_negint: JUDGEMENT sum(E, nv)  HAS_TYPE negint
  
    w:   VAR [T -> nat]
    pw:  VAR [T -> posnat]
  
    sum_nat_is_nat:       JUDGEMENT sum(S, w)  HAS_TYPE nat
    sum_posnat_is_posnat: JUDGEMENT sum(E, pw) HAS_TYPE posnat
  
  
  
    %-------------------------------------------------------
    %  Properties of f derived from the value of Sum(S, f) 
    %-------------------------------------------------------
  
    sum_max_bound  : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) 
 <= N)
  			      IMPLIES (FORALL (t: (S)): f(t) = N)
  
    sum_min_bound  : THEOREM sum(S,f) = N * card(S) AND (FORALL (t: (S)): f(t) 
 >= N)
  			      IMPLIES (FORALL (t: (S)): f(t) = N)
  
    sum_0_non_neg  : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) 
                               IMPLIES (FORALL (t: (S)): f(t) = 0)
    
    sum_0_non_pos  : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) <= 0) 
                               IMPLIES (FORALL (t: (S)): f(t) = 0)
  
    equal_sum_le   : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) <
 = g(t))
  			     IMPLIES (FORALL (t: (S)): f(t) = g(t))
  
    equal_sum_ge   : THEOREM sum(S, f) = sum(S, g) AND (FORALL (t: (S)): f(t) >
 = g(t))
  			     IMPLIES (FORALL (t: (S)): f(t) = g(t))
  
    h, h1, h2: VAR function[T -> nonneg_real]
  
    sum_0_non_neg2 : COROLLARY sum(S, h) = 0 IMPLIES (FORALL (t : (S)) : h(t) =
  0)
  
  
    k, k1, k2: VAR function[T -> nonpos_real]
  
    sum_0_non_pos2 : COROLLARY sum(S, k) = 0 IMPLIES (FORALL (t : (S)) : k(t) =
  0)
  
  
  
    %--------------------------------------------------
    %  Some relations between Sum(A, f) AND Sum(B, f)
    %   when A is a subset of B
    %--------------------------------------------------
  
    sum_subset: THEOREM subset?(A, B) IMPLIES sum(A, h) <= sum(B, h)
  
    sum_subset2: THEOREM subset?(A, B) IMPLIES sum(A, k) >= sum(B, k)
  
  
    sum_order_sub: THEOREM subset?(A, B) AND (FORALL (t:T): h1(t) <= h2(t))
          IMPLIES sum(A, h1) <= sum(B, h2)
  
    sum_order_sub2: THEOREM subset?(A, B) AND (FORALL (t:T): k1(t) >= k2(t))
          IMPLIES sum(A, k1) >= sum(B, k2)
  
  
    sum_subset3: THEOREM
       subset?(A, B) AND (FORALL (t: (B)): A(t) OR f(t) = 0)
  	IMPLIES sum(A, f) = sum(B, f)
  
    END fsets_sum
  
  
  $$$fsets_sum.prf
  (|fsets_sum| (|sum_TCC1| "" (GRIND) NIL NIL)
   (|sum_TCC2| "" (AUTO-REWRITE "nonempty?" "card_rest")
    (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_TCC3| "" (TERMINATION-TCC)) (|sum_emptyset| "" (GRIND) NIL NIL)
   (|sum_singleton_TCC1| "" (SUBTYPE-TCC))
   (|sum_singleton| ""
    (AUTO-REWRITE "singleton" "sum_emptyset" "nonempty?")
    (("" (SKOLEM!)
      (("" (EXPAND "sum")
        (("" (CASE "empty?(singleton(x!1))")
          (("1" (DELETE +) (("1" (GRIND) NIL NIL)) NIL)
           ("2" (ASSERT)
            (("2" (TYPEPRED "choose(singleton(x!1))")
              (("2" (CASE-REPLACE "rest(singleton(x!1)) = emptyset")
                (("1" (REDUCE) NIL NIL)
                 ("2" (DELETE 3)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (GRIND :EXCLUDE ("empty?" "choose")) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_x_TCC1| "" (SUBTYPE-TCC))
   (|sum_x| "" (SKOLEM + (_ "f!1" _))
    ((""
      (AUTO-REWRITE "sum" "nonempty?" "emptyset" "card_rest"
                    "card_remove")
      (("" (INDUCT "S" :NAME "finite_set_induction_gen[T]")
        (("" (SKOSIMP)
          (("" (SKOLEM-TYPEPRED)
            (("" (CASE "empty?(S!1)")
              (("1" (DELETE -3 1) (("1" (GRIND) NIL NIL)) NIL)
               ("2" (ASSERT)
                (("2" (CASE "rest(S!1)(x!1)")
                  (("1" (INST-CP - "rest(S!1)")
                    (("1" (INST - "remove(x!1, S!1)")
                      (("1" (ASSERT)
                        (("1" (INST - "choose(S!1)")
                          (("1" (INST - "x!1")
                            (("1"
                              (CASE-REPLACE
                               "remove(x!1, rest(S!1)) = remove(choose(S!1), re
 move(x!1, S!1))")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (DELETE -3 -4 2 3)
                                (("2"
                                  (AUTO-REWRITE "remove" "rest" "member")
                                  (("2"
                                    (APPLY-EXTENSIONALITY :HIDE? T)
                                    (("2" (SMASH) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (DELETE -3 2 3)
                            (("2" (AUTO-REWRITE "remove" "rest" "member")
                              (("2" (REDUCE) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (DELETE -2)
                    (("2" (AUTO-REWRITE "rest" "member" "remove")
                      (("2" (REDUCE) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_x1_x2_TCC1| "" (SUBTYPE-TCC))
   (|sum_x1_x2| "" (SKOLEM!)
    (("" (REWRITE "sum_x" :DIR RL)
      (("" (REWRITE "sum_x" :DIR RL) NIL NIL)) NIL))
    NIL)
   (|sum_add_TCC1| "" (SUBTYPE-TCC))
   (|sum_add| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (CASE-REPLACE "add(x!1, S!1) = S!1")
        (("1" (DELETE 2)
          (("1" (AUTO-REWRITE "add" "member")
            (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (AUTO-REWRITE "add")
        (("2" (USE "sum_x" ("S" "add(x!1, S!1)"))
          (("2" (CASE-REPLACE "remove(x!1, add(x!1, S!1)) = S!1")
            (("2" (DELETE -1 3)
              (("2" (AUTO-REWRITE "remove" "add" "member")
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (SMASH) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_remove_TCC1| "" (SUBTYPE-TCC))
   (|sum_remove| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (USE "sum_x") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (CASE-REPLACE "remove(x!1, S!1) = S!1")
        (("2" (DELETE 3)
          (("2" (AUTO-REWRITE-DEFS)
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_rest| "" (AUTO-REWRITE "sum") (("" (REDUCE) NIL NIL)) NIL)
   (|sum_disj_union_TCC1| "" (SUBTYPE-TCC))
   (|sum_disj_union| ""
    (AUTO-REWRITE "sum_add" "sum_emptyset" "union" "member" "disjoint?"
                  "intersection" "add" "empty?" "emptyset")
    (("" (SKOLEM + ("A!1" _ "f!1"))
      (("" (INDUCT "B" :NAME "finite_set_ind_modified[T]")
        (("1" (GROUND)
          (("1" (CASE-REPLACE "union(A!1, emptyset[T]) = A!1")
            (("1" (DELETE -1 2)
              (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (SKOSIMP)
          (("2" (GROUND)
            (("1" (INST - "e!1")
              (("1"
                (CASE-REPLACE
                 "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))")
                (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (DELETE -1 3 4)
                  (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("2" (SMASH) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_diff_subset_TCC1| "" (SUBTYPE-TCC))
   (|sum_diff_subset| "" (SKOSIMP)
    (("" (USE "sum_disj_union" ("A" "A!1" "B" "difference(B!1, A!1)"))
      (("" (GROUND)
        (("1" (CASE-REPLACE "union(A!1, difference(B!1, A!1)) = B!1")
          (("1" (ASSERT) NIL NIL)
           ("2" (DELETE -1 2)
            (("2" (AUTO-REWRITE-DEFS)
              (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                (("2" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_union_TCC1| "" (SUBTYPE-TCC))
   (|sum_union_TCC2| "" (SUBTYPE-TCC))
   (|sum_union| "" (SKOLEM!)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "union(A!1, B!1)"))
      (("" (GROUND)
        (("1"
          (USE "sum_diff_subset"
               ("A" "intersection(A!1, B!1)" "B" "B!1"))
          (("1" (GROUND)
            (("1"
              (CASE-REPLACE
               "difference(union(A!1, B!1), A!1) = difference(B!1, intersection
 (A!1, B!1))")
              (("1" (ASSERT) NIL NIL)
               ("2" (DELETE -1 -2 2)
                (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                  (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_diff_intersection_TCC1| "" (SUBTYPE-TCC))
   (|sum_diff_intersection| "" (SKOLEM!)
    (("" (REWRITE "sum_disj_union" :DIR RL)
      (("1"
        (CASE-REPLACE
         "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1")
        (("1" (DELETE 2)
          (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_f_g| "" (SKOLEM + (_ "f!1" "g!1"))
    (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
      (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
        (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (SKOSIMP)
          (("2" (GROUND)
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("choose")) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_particular| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (USE "sum_remove" ("f" "f!1"))
        (("1" (USE "sum_remove" ("f" "f!1 WITH [x!1 := c!1]"))
          (("1" (ASSERT)
            (("1" (USE "sum_f_g" ("g" "f!1"))
              (("1" (GROUND)
                (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (REWRITE "sum_f_g") NIL NIL))
      NIL))
    NIL)
   (|sum_distributive| "" (SKOLEM + (_ "f!1" "g!1"))
    (("" (AUTO-REWRITE "sum" "sum_emptyset" "nonempty?")
      (("" (INDUCT "A" :NAME "finite_set_induction_rest[T]")
        (("1" (ASSERT) NIL NIL)
         ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_const| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset" "card_emptyset" "card_rest"))
    NIL NIL)
   (|sum_mult| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset"))
    NIL NIL)
   (|sum_1_is_card| "" (SKOLEM!)
    (("" (REWRITE "sum_const") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_update| "" (SKOLEM!)
    (("" (SMASH)
      (("1" (AUTO-REWRITE "member")
        (("1" (USE "sum_remove")
          (("1" (USE "sum_remove" ("f" "f!1 WITH [(t!1) := c!1]"))
            (("1" (ASSERT)
              (("1"
                (CASE "sum(remove(t!1, S!1), f!1) = sum(remove(t!1, S!1), f!1 W
 ITH [(t!1) := c!1])")
                (("1" (ASSERT) NIL NIL)
                 ("2" (REWRITE "sum_f_g")
                  (("2" (DELETE -1 -2 2 3) (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (REWRITE "sum_f_g") NIL NIL))
      NIL))
    NIL)
   (|sum_le| ""
    (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
     NIL :REWRITES ("sum" "sum_emptyset" "nonempty?") :IF-MATCH NIL)
    (("" (INST - "f!1" "g!1")
      (("" (GROUND)
        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2)
          (("2" (AUTO-REWRITE "rest" "remove" "member")
            (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_ge| "" (SKOSIMP)
    (("" (USE "sum_le" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
      NIL))
    NIL)
   (|sum_lt| ""
    (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
     NIL :REWRITES ("sum_singleton" "sum_add") :THEORIES ("sets[T]")
     :IF-MATCH NIL)
    (("1" (INST?) NIL NIL)
     ("2" (INST - "f!1" "g!1")
      (("2" (GROUND)
        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2 3) (("2" (REDUCE) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_gt| "" (SKOSIMP)
    (("" (USE "sum_lt" ("f" "g!1" "g" "f!1")) (("" (REDUCE) NIL NIL))
      NIL))
    NIL)
   (|sum_bound| "" (SKOLEM + ("N!1" _ "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
       NIL :REWRITES
       ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
      (("" (TYPEPRED "t!1")
        (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_bound2| "" (SKOLEM + ("N!1" _ "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "S" :NAME "finite_set_induction_rest[T]" :DEFS
       NIL :REWRITES
       ("sum" "card_emptyset" "card_rest" "sum_emptyset" "nonempty?"))
      (("" (TYPEPRED "t!1")
        (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_bound3| ""
    (AUTO-REWRITE "sum_singleton" "card_singleton" "sum_add" "card_add")
    (("" (AUTO-REWRITE-THEORY "sets[T]")
      ((""
        (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
         :DEFS NIL)
        NIL NIL))
      NIL))
    NIL)
   (|sum_bound4| ""
    (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]" :DEFS
     NIL :REWRITES
     ("sum_singleton" "card_singleton" "sum_add" "card_add") :THEORIES
     "sets[T]")
    NIL NIL)
   (|sum_nonneg| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound2") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_nonpos| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_pos| "" (SKOSIMP*)
    (("" (AUTO-REWRITE "remove" "member")
      (("" (USE "sum_nonneg" ("S" "remove(t!1, S!1)"))
        (("" (GROUND)
          (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_pos2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound4") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_neg| "" (SKOSIMP*)
    (("" (AUTO-REWRITE "remove" "member")
      (("" (USE "sum_nonpos" ("S" "remove(t!1, S!1)"))
        (("" (GROUND)
          (("1" (USE "sum_remove") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_neg2| "" (SKOSIMP)
    (("" (FORWARD-CHAIN "sum_bound3") (("" (ASSERT) NIL NIL)) NIL)) NIL)
   (|sum_zero| "" (SKOSIMP)
    (("" (USE* "sum_nonneg" "sum_nonpos")
      (("" (APPLY (REPEAT (THEN (SPLIT) (SKOLEM!) (INST?) (ASSERT)))) NIL
        NIL))
      NIL))
    NIL)
   (|sum_closure1| "" (SKOLEM + (_ "U!1" "f!1"))
    ((""
      (INDUCT-AND-SIMPLIFY "E" :NAME "nonempty_finite_set_induct[T]"
       :REWRITES ("sum_add" "sum_singleton") :EXCLUDE ("sum") :THEORIES
       ("sets[T]"))
      (("" (INST? -2) NIL NIL)) NIL))
    NIL)
   (|sum_closure2| "" (SKOLEM + (_ "U!1" "f!1"))
    ((""
      (AUTO-REWRITE "sum" "sum_emptyset" "rest" "remove" "member"
                    "nonempty?")
      (("" (INDUCT "S" :NAME "finite_set_induction_rest[T]")
        (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_nnreal_is_nnreal| "" (SKOLEM!)
    (("" (REWRITE "sum_nonneg")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_npreal_is_npreal| "" (SKOLEM!)
    (("" (REWRITE "sum_nonpos")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_posreal_is_posreal| "" (SKOLEM!)
    (("" (REWRITE "sum_pos2")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_negreal_is_negreal| "" (SKOLEM!)
    (("" (REWRITE "sum_neg2")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|sum_rat_is_rat| "" (SKOLEM!) (("" (REWRITE "sum_closure2") NIL NIL))
    NIL)
   (|sum_nnrat_is_nnrat| "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)
   (|sum_nprat_is_nprat| "" (SKOLEM!)
    (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
   (|sum_posrat_is_posrat| "" (SUBTYPE-TCC) NIL NIL)
   (|sum_negrat_is_negrat| "" (SKOLEM!)
    (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
   (|sum_int_is_int| "" (AUTO-REWRITE-THEORY "integers")
    ((""
      (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest[T]" :DEFS NIL
       :REWRITES ("sum_emptyset" "sum"))
      NIL NIL))
    NIL)
   (|sum_npint_is_npint| "" (SKOLEM!)
    (("" (REWRITE "sum_npreal_is_npreal") NIL NIL)) NIL)
   (|sum_negint_is_negint| "" (SKOLEM!)
    (("" (REWRITE "sum_negreal_is_negreal") NIL NIL)) NIL)
   (|sum_nat_is_nat| "" (SKOLEM!)
    (("" (REWRITE "sum_nnreal_is_nnreal") NIL NIL)) NIL)
   (|sum_posnat_is_posnat| "" (AUTO-REWRITE-DEFS :EXPLICIT? T)
    (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL)
   (|sum_max_bound| "" (SKOSIMP)
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "card_remove" "member")
        (("" (USE "sum_bound" ("S" "remove(t!1, S!1)" "N" "N!1"))
          (("" (GROUND)
            (("1" (USE "sum_remove")
              (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_min_bound| "" (SKOSIMP)
    (("" (SKOLEM!)
      (("" (AUTO-REWRITE "card_remove" "member")
        (("" (USE "sum_bound2" ("S" "remove(t!1, S!1)" "N" "N!1"))
          (("" (GROUND)
            (("1" (USE "sum_remove")
              (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL)
             ("2" (DELETE -1 2)
              (("2" (AUTO-REWRITE "remove") (("2" (REDUCE) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_0_non_neg| "" (SKOSIMP)
    (("" (USE "sum_min_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
   (|sum_0_non_pos| "" (SKOSIMP)
    (("" (USE "sum_max_bound") (("" (GROUND) NIL NIL)) NIL)) NIL)
   (|equal_sum_le| "" (SKOSIMP*)
    (("" (ASSERT)
      (("" (USE "sum_le" ("S" "remove(t!1, S!1)" "f" "f!1" "g" "g!1"))
        (("" (GROUND)
          (("1" (AUTO-REWRITE "member")
            (("1" (USE "sum_remove" ("f" "f!1"))
              (("1" (USE "sum_remove" ("f" "g!1"))
                (("1" (ASSERT)
                  (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (DELETE -1 2)
            (("2" (AUTO-REWRITE "remove" "member")
              (("2" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|equal_sum_ge| "" (SKOSIMP)
    (("" (USE "equal_sum_le" ("f" "g!1" "g" "f!1"))
      (("" (REDUCE) NIL NIL)) NIL))
    NIL)
   (|sum_0_non_neg2| "" (SKOSIMP)
    (("" (USE "sum_0_non_neg")
      (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|sum_0_non_pos2| "" (SKOSIMP)
    (("" (USE "sum_0_non_pos")
      (("" (GROUND) (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|sum_subset| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_nonneg" ("S" "difference(B!1, A!1)"))
          (("" (GROUND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_subset2| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_nonpos" ("S" "difference(B!1, A!1)"))
          (("" (GROUND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|sum_order_sub| "" (SKOSIMP)
    (("" (USE "sum_subset" ("h" "h1!1"))
      (("" (ASSERT)
        (("" (USE "sum_le" ("S" "B!1" "f" "h1!1" "g" "h2!1"))
          (("" (GROUND)
            (("" (DELETE -1 -2 2) (("" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_order_sub2| "" (SKOSIMP)
    (("" (USE "sum_subset2" ("k" "k1!1"))
      (("" (ASSERT)
        (("" (USE "sum_ge" ("S" "B!1" "f" "k1!1" "g" "k2!1"))
          (("" (GROUND) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sum_subset3| "" (SKOSIMP)
    (("" (USE "sum_diff_subset" ("f" "f!1" "A" "A!1" "B" "B!1"))
      (("" (ASSERT)
        (("" (USE "sum_zero" ("S" "difference(B!1, A!1)"))
          (("" (GROUND)
            (("" (DELETE -1 -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$tasks_and_jobs.pvs
  tasks_and_jobs [ n: posnat ] : THEORY
  
    BEGIN
  
    task: NONEMPTY_TYPE = below(n)
    job: NONEMPTY_TYPE = [task, nat]
  
    set_of_tasks: JUDGEMENT set[task] SUBTYPE_OF finite_set[task]
  
    END tasks_and_jobs
  
  $$$tasks_and_jobs.prf
  (|tasks_and_jobs| (|task_TCC1| "" (INST + "0") (("" (ASSERT) NIL NIL)) NIL)
   (|set_of_tasks| "" (GRIND :IF-MATCH NIL)
    (("" (INST + "n" "lambda (i: (x!1)): i")
      (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  
  
  $$$max_bounded.pvs
  max_bounded[T: TYPE FROM nat] : THEORY
  
    BEGIN
  
    x, y: VAR nat
  
    E: VAR set[T]
  
    %-------------------------
    %  Bound and bounded set
    %-------------------------
  
    bound(E, x): bool = FORALL (y: (E)): y <= x
  
    sup(E, x): bool =
       bound(E, x) AND FORALL y: bound(E, y) IMPLIES x <= y
  
    sup_unique: LEMMA sup(E, x) AND sup(E, y) IMPLIES x = y
  
    bounded?(E): bool = EXISTS x: bound(E, x)
  
    bounded_set: TYPE = { E | bounded?(E) }
  
    F, F1, F2: VAR bounded_set
  
    sup_exists: LEMMA EXISTS x: sup(F, x)
  
    sup_empty: LEMMA empty?(F) IMPLIES sup(F, 0)
  
    sup_nonempty: LEMMA not empty?(F) IMPLIES EXISTS (x: (F)): sup(F, x)  
  
  
    %------------------------------------
    %  Maximum element of a bounded set
    %------------------------------------
  
    A, B: VAR { F | not empty?(F) }
  
    bounded_union1: JUDGEMENT union(F1, F2) HAS_TYPE bounded_set
  
    bounded_union2: JUDGEMENT union(A, B) HAS_TYPE { F | not empty?(F) }
  
    bounded_inter1: JUDGEMENT intersection(F, E) HAS_TYPE bounded_set
  
    bounded_inter2: JUDGEMENT intersection(E, F) HAS_TYPE bounded_set
  
  
    max(A): { (x:(A)) | sup(A, x) }
  
    max_prop1: LEMMA  FORALL (y: (A)): y <= max(A)
  
    max_prop2: LEMMA  max(A) <= x IFF FORALL (y: (A)): y <= x
  
    max_subset: LEMMA subset?(A, B) IMPLIES max(A) <= max(B)
  
    max_union: LEMMA max(union(A, B)) = max(max(A), max(B))
  
    max_intersection1: LEMMA 
  	not empty?(intersection(A, E)) IMPLIES max(intersection(A, E)) <= max(A
 )
  
    max_intersection2: LEMMA 
  	not empty?(intersection(E, B)) IMPLIES max(intersection(E, B)) <= max(B
 )
  
    END max_bounded
  
  $$$max_bounded.prf
  (|max_bounded|
   (|sup_unique| "" (EXPAND "sup") (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)
   (|sup_exists| "" (LEMMA "wf_nat")
    (("" (GRIND :IF-MATCH NIL :EXCLUDE ("bound"))
      (("" (DELETE -1)
        (("" (INST - "{ n: nat | bound(F!1, n) }")
          (("" (GROUND)
            (("" (SKOSIMP* :PREDS? T)
              (("" (INST? +)
                (("" (ASSERT)
                  (("" (SKOSIMP)
                    (("" (ASSERT)
                      (("" (INST - "y!2") (("" (ASSERT) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sup_empty| "" (GRIND) NIL NIL)
   (|sup_nonempty| "" (SKOSIMP)
    (("" (USE "sup_exists")
      (("" (SKOLEM!)
        (("" (INST?)
          (("" (EXPAND* "empty?" "member" "sup" "bound")
            (("" (SKOLEM!)
              (("" (FLATTEN)
                (("" (ASSERT)
                  (("" (INST -2 "x!1 - 1")
                    (("1" (ASSERT)
                      (("1" (SKOLEM!)
                        (("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL))
                        NIL))
                      NIL)
                     ("2" (INST - "x!2") (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|bounded_union1| "" (GRIND :IF-MATCH NIL)
    (("" (INST + "max(x!1, x!2)")
      (("" (REDUCE :IF-MATCH NIL)
        (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (INST? -6) (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|bounded_union2| "" (GRIND :EXCLUDE ("bounded?")) NIL NIL)
   (|bounded_inter1| "" (GRIND :IF-MATCH NIL)
    (("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL)
   (|bounded_inter2| "" (GRIND :IF-MATCH NIL)
    (("" (INST + "x!1") (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL)) NIL)
   (|max_TCC1| "" (INST + "lambda A: epsilon! (x: (A)): sup(A, x)")
    (("1" (SKOLEM-TYPEPRED)
      (("1" (USE "epsilon_ax[(A!1)]")
        (("1" (GROUND) (("1" (REWRITE "sup_nonempty") NIL NIL)) NIL)
         ("2" (DELETE -1 3) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL)
     ("2" (SKOLEM-TYPEPRED) (("2" (DELETE -) (("2" (GRIND) NIL NIL)) NIL)) NIL)
 )
    NIL)
   (|max_prop1| "" (SKOLEM!)
    (("" (TYPEPRED "max(A!1)") (("" (GRIND) NIL NIL)) NIL)) NIL)
   (|max_prop2| "" (SKOLEM!)
    (("" (TYPEPRED "max(A!1)")
      (("" (EXPAND* "sup" "bound")
        (("" (GROUND)
          (("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (ASSERT) NIL NIL)) NIL))
            NIL)
           ("2" (INST? -5) (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_subset| "" (SKOSIMP)
    (("" (REWRITE "max_prop2")
      (("" (GRIND :IF-MATCH NIL)
        (("" (INST?)
          (("" (ASSERT) (("" (USE "max_prop1" ("A" "B!1" "y" "y!1")) NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_union| "" (SKOLEM!)
    (("" (CASE "max(max(A!1), max(B!1)) <= max(union(A!1, B!1))")
      (("1" (ASSERT)
        (("1"
          (USE "max_prop2"
               ("A" "union(A!1, B!1)" "x" "max(max(A!1), max(B!1))"))
          (("1" (GROUND)
            (("1" (DELETE -1 2 3)
              (("1" (GRIND :EXCLUDE "max")
                (("1" (USE "max_prop1" ("A" "A!1" "y" "y!1"))
                  (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (USE "max_prop1" ("A" "B!1" "y" "y!1"))
                  (("2" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE 2)
        (("2" (EXPAND "max")
          (("2" (LIFT-IF)
            (("2" (GROUND)
              (("1" (REWRITE "max_subset")
                (("1" (DELETE -1 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)
               ("2" (REWRITE "max_subset")
                (("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_intersection1| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)
 )
        NIL))
      NIL))
    NIL)
   (|max_intersection2| "" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "max_subset") (("" (DELETE 2 3) (("" (GRIND) NIL NIL)) NIL)
 )
        NIL))
      NIL))
    NIL))
  
  
  $$$command_adt.pvs
  %%% ADT file generated from command
  
  command_adt: THEORY
   BEGIN
  
    IMPORTING basic_types
  
    command: TYPE
  
    P?, V?, step?: [command -> boolean]
  
    P: [semaphore -> (P?)]
  
    request: [(P?) -> semaphore]
  
    V: [semaphore -> (V?)]
  
    sem: [(V?) -> semaphore]
  
    Step: (step?)
  
    ord(x: command): upto(2) =
        CASES x OF P(P1_var): 0, V(V1_var): 1, Step: 2 ENDCASES
  
      command_P_extensionality: AXIOM
      FORALL (P?_var: (P?), (P?_var2: (P?))):
        request(P?_var) = request(P?_var2) IMPLIES P?_var = P?_var2;
  
    command_P_eta: AXIOM FORALL (P?_var: (P?)): P(request(P?_var)) = P?_var;
  
    command_V_extensionality: AXIOM
      FORALL (V?_var: (V?), (V?_var2: (V?))):
        sem(V?_var) = sem(V?_var2) IMPLIES V?_var = V?_var2;
  
    command_V_eta: AXIOM FORALL (V?_var: (V?)): V(sem(V?_var)) = V?_var;
  
    command_Step_extensionality: AXIOM
      FORALL (step?_var: (step?), (step?_var2: (step?))): step?_var = step?_var
 2;
  
    command_request_P: AXIOM
      FORALL (P1_var: semaphore): request(P(P1_var)) = P1_var;
  
    command_sem_V: AXIOM FORALL (V1_var: semaphore): sem(V(V1_var)) = V1_var;
  
    command_inclusive: AXIOM
      FORALL (command_var: command):
        P?(command_var) OR V?(command_var) OR step?(command_var);
  
    command_induction: AXIOM
      FORALL (p: [command -> boolean]):
        (FORALL (P1_var: semaphore): p(P(P1_var))) AND
         (FORALL (V1_var: semaphore): p(V(V1_var))) AND p(Step)
         IMPLIES (FORALL (command_var: command): p(command_var));
  
    subterm(x, y: command):  boolean = x = y;
  
      <<(x, y: command):  boolean = FALSE;
  
      command_well_founded: AXIOM well_founded?[command](<<);
  
    reduce_nat(P?_fun, V?_fun: [semaphore -> nat], (step?_fun: nat)):
    [command -> nat] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var),
               V(V1_var): V?_fun(V1_var),
               Step: step?_fun
            ENDCASES;
  
      REDUCE_nat(P?_fun, V?_fun: [[semaphore, command] -> nat],
                 (step?_fun: [command -> nat])):
       [command -> nat] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var, command_adtvar),
               V(V1_var): V?_fun(V1_var, command_adtvar),
               Step: step?_fun(command_adtvar)
            ENDCASES;
  
      reduce_ordinal(P?_fun, V?_fun: [semaphore -> ordinal],
                     (step?_fun: ordinal)):
       [command -> ordinal] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var),
               V(V1_var): V?_fun(V1_var),
               Step: step?_fun
            ENDCASES;
  
      REDUCE_ordinal(P?_fun, V?_fun: [[semaphore, command] -> ordinal],
                     (step?_fun: [command -> ordinal])):
       [command -> ordinal] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var, command_adtvar),
               V(V1_var): V?_fun(V1_var, command_adtvar),
               Step: step?_fun(command_adtvar)
            ENDCASES;
   END command_adt
  
  command_adt_reduce[range: TYPE]: THEORY
   BEGIN
  
    IMPORTING basic_types
  
    IMPORTING command_adt
  
    reduce(P?_fun, V?_fun: [semaphore -> range], (step?_fun: range)):
    [command -> range] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var),
               V(V1_var): V?_fun(V1_var),
               Step: step?_fun
            ENDCASES;
  
      REDUCE(P?_fun, V?_fun: [[semaphore, command] -> range],
             (step?_fun: [command -> range])):
       [command -> range] =
        LAMBDA (command_adtvar: command):
          CASES command_adtvar
            OF P(P1_var): P?_fun(P1_var, command_adtvar),
               V(V1_var): V?_fun(V1_var, command_adtvar),
               Step: step?_fun(command_adtvar)
            ENDCASES;
   END command_adt_reduce
  $$$basic_types.pvs
  basic_types : THEORY
  
    BEGIN
  
    %--------------------
    %  Priority of jobs
    %--------------------
  
    maxprio: posnat
  
    priority: NONEMPTY_TYPE = below(maxprio)
  
  
    %--------------------------
    %  Semaphores and ceiling
    %--------------------------
  
    semaphore: NONEMPTY_TYPE
  
    ceil: [semaphore -> priority]
  
    rsrc_set: TYPE = set[semaphore]
  
    END basic_types
  
  $$$basic_types.prf
  (|basic_types| (|priority_TCC1| "" (INST + "0") (("" (ASSERT) NIL))))
  
  $$$command.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  commands available to jobs    %
  %   P(S): request to lock S      %
  %   V(S): request to unlock S    %
  %   Step: any other command      %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  command : DATATYPE 
  
    BEGIN
      IMPORTING basic_types
  
      P(request: semaphore): P?
  
      V(sem: semaphore): V?
  
      Step: step?
  
    END command
  
  $$$programs.pvs
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Programs: finite sequences of commands  %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  programs : THEORY
  
    BEGIN
  
    IMPORTING command, max_bounded
  
    prog: TYPE = [# length: posnat, clist: [below(length) -> command] #]
  
    p: VAR prog
    s: VAR semaphore
    n: VAR priority
  
  
    %--------------------------------------------
    %  pc(p): type of index for program counter
    %--------------------------------------------
  
    pc(p): NONEMPTY_TYPE = upto(length(p))
  
  
    %--------------------------------------------------
    %  complete(p, i): index i points to the end of p
    %  cmd(p, i): command for step i of p
    %--------------------------------------------------
  
    complete(p, (i: pc(p))): bool = i = length(p)
  
    cmd(p, (i: below(length(p)))): command = clist(p)(i)
  
  
    %---------------------------------------------------
    %  Resources needed by p to perform step i =
    %   all the resources acquired in steps [0..i-1]
    %   and not released
    %---------------------------------------------------
  
    needs(p, (i: pc(p))): RECURSIVE rsrc_set =
       IF i=0 THEN emptyset
       ELSE 
         CASES cmd(p, i-1) OF
            P(s): add(s, needs(p, i-1)),
            V(s): remove(s, needs(p, i-1)),
            Step: needs(p, i-1)
         ENDCASES
       ENDIF
      MEASURE i
  
  
    %-------------------------------------------------
    %  Resources used by p:
    %  resources(p, i) = resources used in [0..i-1]
    %  resources(p) = all resources used by p
    %-------------------------------------------------
  
    resources(p, (i: pc(p))): RECURSIVE rsrc_set =
       IF i=0 THEN emptyset
       ELSE 
         CASES cmd(p, i-1) OF
            P(s): add(s, resources(p, i-1)),
            V(s): resources(p, i-1),
            Step: resources(p, i-1)
         ENDCASES
       ENDIF
      MEASURE i
  
    resources(p): rsrc_set = resources(p, length(p))
  
  
    %-----------------------------------------
    %  Relations between needs and resources
    %-----------------------------------------
  
    rsrc_needs1: LEMMA
       FORALL (i: pc(p)): subset?(needs(p, i), resources(p, i))
  
    rsrc_needs2: LEMMA
       FORALL (i, j: pc(p)):
  	i <= j IMPLIES subset?(resources(p, i), resources(p, j))
  
    rsrc_needs3: LEMMA
       FORALL (i: pc(p)): subset?(resources(p, i), resources(p))
  
    rsrc_needs4: LEMMA
       FORALL (i: pc(p)): subset?(needs(p, i), resources(p))
  
    rsrc_equiv1: LEMMA 
       FORALL (i: pc(p)): resources(p, i) = 
  	{ s | EXISTS (j: pc(p) | j <= i): member(s, needs(p, j)) }
  
    rsrc_equiv2: LEMMA 
       resources(p) = { s | EXISTS (j: pc(p)): member(s, needs(p, j)) }
  
    rsrc_equiv3: LEMMA
       member(s, resources(p)) IFF EXISTS (j: below(length(p))): cmd(p, j) = P(
 s)
  
  
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%
    %   Critical Sections    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%
  
    %-------------------------------------------------------------------
    %  well_behaved(p): p releases all its resources on termination
    %  cs(p, i): step i is within a critical section of p
    %  cs(p, i, n): step i is within a critical section of level n
    %      (i.e. between  P(s) and V(s) where s has ceiling >= n)
    %-------------------------------------------------------------------
  
    well_behaved(p): bool = empty?(needs(p, length(p)))
  
    good_prog: TYPE = (well_behaved)
  
    cs(p, (i: pc(p))): bool = not empty?(needs(p, i))
  
    cs(p, (i: pc(p)), n): bool = 
       EXISTS s: member(s, needs(p, i)) AND ceil(s) >= n
  
  
  
    cs_level1: LEMMA 
       FORALL (i: pc(p)): cs(p, i, n) IMPLIES cs(p, i)
  
    cs_level2: LEMMA
       FORALL (i: pc(p)): cs(p, i) IFF EXISTS n: cs(p, i, n)
  
    well_behaved1: LEMMA
       well_behaved(p) IFF not cs(p, length(p))
  
  
    initially_not_cs1: LEMMA  NOT cs(p, 0)
  
    initially_not_cs2: LEMMA  NOT cs(p, 0, n)
  
    cs_exists1: LEMMA 
       (EXISTS (i: pc(p)): cs(p, i)) IFF not empty?(resources(p))
  
    cs_exists2: LEMMA
       (EXISTS (i: pc(p)): cs(p, i, n)) IFF 
  	EXISTS s: member(s, resources(p)) AND ceil(s) >= n
  
  
  
    %-----------------------------------------------------------------------
    %  critical_section(p, i, j): p[i]...p[j-1] is a critical section
    %  critical_section(p, i, j, n): same thing but at level n
    %-----------------------------------------------------------------------
  
    critical_section(p, (i, j: pc(p))): bool =
        i < j AND
  	FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k)
  
    critical_section(p, (i, j: pc(p)), n): bool =
        i < j AND
  	FORALL (k: pc(p)): i <= k AND k < j IMPLIES cs(p, k, n)
  
  
    critical_section1: LEMMA
        FORALL (i, j: pc(p)): critical_section(p, i, j, n)
  	IMPLIES critical_section(p, i, j) 
  
  
    subsection1: LEMMA
        FORALL (i, j, k, l: pc(p)): critical_section(p, i, j)
  	AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l)
  
    subsection2: LEMMA
        FORALL (i, j, k, l: pc(p)): critical_section(p, i, j, n)
  	AND i <= k AND k < l AND l <= j IMPLIES critical_section(p, k, l, n)
  
  
    max_critical_section_length: LEMMA
  	FORALL (i, j: pc(p)):
  	   critical_section(p, i, j) IMPLIES j - i < length(p)
  
  
    %-------------------------------------------
    %  length of the longest critical sections
    %-------------------------------------------
  
    len_cs(p): bounded_set[pc(p)] =
       { a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j) AND a = j-i
  }
  
    max_cs(p): pc(p) = IF empty?(len_cs(p)) THEN 0 ELSE max(len_cs(p)) ENDIF
  
  
    len_cs(p, n): bounded_set[pc(p)] =
       { a: pc(p) | EXISTS (i, j: pc(p)): critical_section(p, i, j, n) AND a = 
 j-i }
  
    max_cs(p, n): pc(p) = IF empty?(len_cs(p, n)) THEN 0 ELSE max(len_cs(p, n))
  ENDIF
  
  
    len_section_level: LEMMA  subset?(len_cs(p, n), len_cs(p))
  
    max_section_level: LEMMA  max_cs(p, n) <= max_cs(p)
  
  
    max_cs1: LEMMA
       FORALL (i, j: pc(p)):
  	critical_section(p, i, j) IMPLIES j - i <= max_cs(p)
  
    max_cs2: LEMMA
       FORALL (i, j: pc(p)):
  	critical_section(p, i, j, n) IMPLIES j - i <= max_cs(p, n)
  
  
    no_critical_section: LEMMA 
       well_behaved(p) IMPLIES (max_cs(p) = 0 IFF empty?(resources(p)))
  
    max_cs3: LEMMA max_cs(p) <= length(p) - 1
  
  
    no_critical_section_lev: LEMMA
       well_behaved(p) IMPLIES 
          (max_cs(p, n) = 0 IFF (FORALL s: member(s, resources(p)) IMPLIES ceil
 (s) < n))
  
    max_cs4: LEMMA  max_cs(p, n) <= length(p) - 1
  
    END programs
  
  $$$programs.prf
  (|programs| (|needs_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|needs_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|needs_TCC3| "" (TERMINATION-TCC) NIL NIL)
   (|needs_TCC4| "" (SUBTYPE-TCC) NIL NIL)
   (|needs_TCC5| "" (TERMINATION-TCC) NIL NIL)
   (|needs_TCC6| "" (SUBTYPE-TCC) NIL NIL)
   (|needs_TCC7| "" (TERMINATION-TCC) NIL NIL)
   (|resources_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|rsrc_needs1| "" (SKOLEM + ("p!1" _))
    (("" (INDUCT-AND-SIMPLIFY "i") NIL NIL)) NIL)
   (|rsrc_needs2| "" (SKOLEM + ("p!1" "i!1" _))
    (("" (INDUCT-AND-SIMPLIFY "j") NIL NIL)) NIL)
   (|rsrc_needs3| "" (SKOLEM!)
    (("" (EXPAND "resources" 1 2) (("" (REWRITE "rsrc_needs2") NIL NIL))
      NIL))
    NIL)
   (|rsrc_needs4| "" (SKOLEM!)
    (("" (USE* "rsrc_needs1" "rsrc_needs3")
      (("" (AUTO-REWRITE "subset?" "member") (("" (REDUCE) NIL NIL))
        NIL))
      NIL))
    NIL)
   (|rsrc_equiv1| "" (SKOLEM + ("p!1" _))
    (("" (INDUCT-AND-SIMPLIFY "i" :IF-MATCH NIL)
      (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)
       ("2" (REPLACE*)
        (("2" (DELETE -2)
          (("2" (APPLY-EXTENSIONALITY :HIDE? T)
            (("2" (REDUCE :IF-MATCH NIL)
              (("1" (INST + "1 + jt!1") (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (INST?) NIL NIL)
               ("3" (CASE-REPLACE "j!1 = 1 + jt!1")
                (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)
                 ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("3" (DELETE -1)
        (("3" (APPLY-EXTENSIONALITY 2 :HIDE? T)
          (("3" (REDUCE :IF-MATCH NIL)
            (("1" (INST?) NIL NIL)
             ("2" (CASE-REPLACE "j!1 = jt!1 + 1")
              (("1" (SMASH) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL))
                NIL)
               ("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|rsrc_equiv2| "" (SKOLEM!)
    (("" (EXPAND "resources")
      (("" (REWRITE "rsrc_equiv1")
        (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|rsrc_equiv3| "" (EXPAND "resources")
    (("" (SKOLEM!)
      ((""
        (CASE "FORALL (i: pc(p!1)): member(s!1, resources(p!1, i)) IFF EXISTS (
 j: pc(p!1)): j < i AND cmd(p!1, j) = P(s!1)")
        (("1" (INST?)
          (("1" (REPLACE*)
            (("1" (DELETE -)
              (("1" (APPLY (THEN (PROP) (SKOSIMP) (INST?) (ASSERT))) NIL
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE 2)
          (("2"
            (APPLY (THEN (INDUCT-AND-SIMPLIFY$ "i" :IF-MATCH NIL)
                    (REPEAT* (INST?)) (ASSERT)))
            (("1" (DELETE 2) (("1" (APPLY-EXTENSIONALITY 2) NIL NIL))
              NIL)
             ("2" (CASE-REPLACE "j!1 = jt!1")
              (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL)
         ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|cs_level1| "" (GRIND) NIL NIL)
   (|cs_level2| "" (GRIND :EXCLUDE "resources" :IF-MATCH NIL)
    (("1" (INST?) NIL NIL)
     ("2" (INST + "ceil(x!1)")
      (("2" (INST + "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|well_behaved1| "" (GRIND :EXCLUDE ("empty?" "resources")) NIL NIL)
   (|initially_not_cs1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|initially_not_cs1| "" (GRIND) NIL NIL)
   (|initially_not_cs2| "" (GRIND) NIL NIL)
   (|cs_exists1| "" (SKOLEM!)
    (("" (REWRITE "rsrc_equiv2")
      (("" (GRIND :EXCLUDE ("needs")) NIL NIL)) NIL))
    NIL)
   (|cs_exists2| "" (SKOLEM!)
    (("" (REWRITE "rsrc_equiv2")
      (("" (GRIND :EXCLUDE ("needs") :IF-MATCH NIL)
        (("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)
         ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|critical_section1| ""
    (AUTO-REWRITE "critical_section_lev" "critical_section" "cs_level2")
    (("" (REDUCE :IF-MATCH NIL)
      (("" (INST - "k!1") (("" (INST? +) (("" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|subsection1| ""
    (APPLY (THEN (EXPAND "critical_section")
            (REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT)))
    NIL NIL)
   (|subsection2| ""
    (APPLY (THEN (EXPAND "critical_section")
            (REPEAT* (THEN (SKOSIMP) (ASSERT))) (INST?) (ASSERT)))
    NIL NIL)
   (|max_critical_section_length| "" (EXPAND "critical_section")
    (("" (SKOSIMP)
      (("" (ASSERT)
        (("" (INST - "i!1")
          (("" (ASSERT)
            (("" (USE "initially_not_cs1") (("" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|len_cs_TCC1| "" (GRIND :EXCLUDE "critical_section" :IF-MATCH NIL)
    (("" (INST + "length(p!1)")
      (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|len_cs_TCC2| "" (EXPAND* "bounded?" "bound")
    (("" (SKOLEM!)
      (("" (INST + "length(p!1)")
        (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|len_section_level| ""
    (GRIND :EXCLUDE ("critical_section" "critical_section_lev") :IF-MATCH
     NIL)
    (("" (FORWARD-CHAIN "critical_section1")
      (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL)
   (|max_section_level| "" (SKOLEM!)
    (("" (USE "len_section_level")
      (("" (EXPAND "max_cs")
        (("" (SMASH)
          (("1" (DELETE 2)
            (("1"
              (APPLY (THEN (GRIND :EXCLUDE ("len_cs") :IF-MATCH NIL)
                      (INST?) (INST?) (ASSERT)))
              NIL NIL))
            NIL)
           ("2" (REWRITE "max_subset") NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_cs1| "" (SKOSIMP)
    (("" (EXPAND "max_cs")
      (("" (SMASH)
        (("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL)
          (("1" (INST - "j!1 - i!1")
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL)
         ("2" (REWRITE "max_prop1")
          (("2" (DELETE 2 3)
            (("2" (FORWARD-CHAIN "max_critical_section_length")
              (("2" (ASSERT)
                (("2" (EXPAND "len_cs")
                  (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_cs2| "" (SKOSIMP)
    (("" (EXPAND "max_cs")
      (("" (SMASH)
        (("1" (GRIND :EXCLUDE ("critical_section") :IF-MATCH NIL)
          (("1" (INST - "j!1 - i!1")
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL)
         ("2" (REWRITE "max_prop1")
          (("2" (DELETE 2 3)
            (("2" (FORWARD-CHAIN "critical_section1")
              (("2" (FORWARD-CHAIN "max_critical_section_length")
                (("2" (ASSERT)
                  (("2" (EXPAND "len_cs")
                    (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|no_critical_section| "" (SKOSIMP)
    (("" (EXPAND "max_cs")
      (("" (REWRITE "well_behaved1")
        (("" (USE "cs_exists1")
          (("" (CASE "empty?(len_cs(p!1))")
            (("1" (SMASH)
              (("1" (DELETE -3 1)
                (("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
                  (("1" (INST - "1")
                    (("1" (INST + "i!1" "i!1+1") (("1" (REDUCE) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SMASH)
              (("1" (CASE "1 <= max(len_cs(p!1))")
                (("1" (ASSERT) NIL NIL)
                 ("2" (SKOLEM!)
                  (("2" (AUTO-REWRITE "len_cs" "critical_section")
                    (("2" (REWRITE "max_prop1")
                      (("2" (INST + "i!1" "i!1 + 1")
                        (("2" (REDUCE) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (DELETE -1 4)
                (("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
                  (("2" (INST + "i!1")
                    (("2" (INST? -) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_cs3| "" (SKOSIMP)
    (("" (EXPAND "max_cs")
      (("" (SMASH)
        (("" (REWRITE "max_prop2")
          (("" (SKOLEM-TYPEPRED)
            (("" (EXPAND "len_cs" -)
              (("" (SKOSIMP)
                (("" (FORWARD-CHAIN "max_critical_section_length")
                  (("" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|no_critical_section_lev| "" (SKOSIMP)
    (("" (REWRITE "well_behaved1")
      (("" (USE "cs_level1")
        (("" (ASSERT)
          (("" (DELETE 2)
            (("" (EXPAND "max_cs")
              (("" (CASE "empty?(len_cs(p!1, n!1))")
                (("1" (SMASH)
                  (("1" (USE "cs_exists2")
                    (("1" (GROUND)
                      (("1" (DELETE -2 -4 2)
                        (("1" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
                          (("1" (INST - "1")
                            (("1" (INST + "i!1" "i!1+1")
                              (("1" (REDUCE) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (DELETE -1 -2 2 3) (("2" (REDUCE) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (SMASH)
                  (("1" (USE "cs_exists2")
                    (("1" (GROUND)
                      (("1" (DELETE -2 3)
                        (("1" (CASE "1 <= max(len_cs(p!1, n!1))")
                          (("1" (ASSERT) NIL NIL)
                           ("2"
                            (AUTO-REWRITE "len_cs" "critical_section")
                            (("2" (REWRITE "max_prop1")
                              (("2" (SKOLEM!)
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (INST + "i!1" "i!1+1")
                                    (("2" (REDUCE) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (DELETE -1 2 3 4) (("2" (REDUCE) NIL NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (USE "cs_exists2")
                    (("2" (GROUND)
                      (("1" (DELETE -1 1 2 3) (("1" (REDUCE) NIL NIL))
                        NIL)
                       ("2" (DELETE -1 1 5)
                        (("2" (GRIND :EXCLUDE ("cs") :IF-MATCH NIL)
                          (("2" (INST + "i!1")
                            (("2" (INST - "i!1") (("2" (ASSERT) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|max_cs4| "" (SKOSIMP)
    (("" (EXPAND "max_cs")
      (("" (SMASH)
        (("" (REWRITE "max_prop2")
          (("" (SKOLEM-TYPEPRED)
            (("" (EXPAND "len_cs" -)
              (("" (SKOSIMP)
                (("" (FORWARD-CHAIN "critical_section1")
                  (("" (FORWARD-CHAIN "max_critical_section_length")
                    (("" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  --------------DEF11F3F21E0131D32F94669--

How-To-Repeat: 

Fix: 
The slow proofs problem was due to loading the patch file interpreted.
Once it was compiled, everything worked as usual.  This only affected
users at SRI, as only the compiled patches are available otherwise.

Added a new test in determine-operator-type after the locality and
fully-instantiated tests to look for exact matches.  This is needed since
the exact match is disabled for function types in resolve.lisp.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools