$$$pvs-strategies (defstep simp () (then (flatten)(assert)(simplify)(flatten)) " Flatten, assert, simplify" " ") (defstep spsi (&optional (fnum +)) (then (split fnum)(simp)) "split then simp" "split then simp" ) (defstep LazyGrind () (then (grind$ :if-match nil)(grind$)) " Grind with the instantiation postponed to the end" " ") (defstep MyGrind () (grind$ :if-match nil) " Grind with no instantiation" " ") (defstep grind-best () (grind$ :if-match best) " Grind with best instantiation" " Grind with best instantiation") (defstep replace-all (fnums into) (let ((fnum (car fnums)) (rems (cdr fnums))) (if fnum (then (replace fnum into)(replace-all$ rems into)) (skip-msg " "))) " " " " ) (defstep rep-plus(&optional (fnum +)) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) * +)) (first (when fnums (car fnums)))) (if first (then (replace-all fnums fnum)(simp)) (skip-msg "Nothing to replace"))) " replace into consequents" " replace into consequents" ) (defstep expand-rho (&optional (inv nil)) (then (EXPAND "rho") (EXPAND inv) (SKOSIMP*) (REPLACE*) (simp)) "Expands out rho, skosimps, replaces and hides" " " ) (defstep exp-inv () (then (expand "reachable") (expand "memhistCorrect")(expand "cacheEqualMemhist ") (expand "cEntryExists")(expand "idPCunique")(expand "homeNotReq") (expand "channelsNonNeg")(expand "inQmatchHist")(expand "outQpcInc") (expand "localTimeInc")(expand "localTimeEarlier")(expand "timeChannelProc") (expand "channelTimeInc")(expand "channelsMatchProg")(expand "waiting") (expand "histComplete")(expand "histMatchPC")(expand "histMatchTime") (expand "firstExists")(expand "readValuesCorrect")(expand "histLt") (expand "indexCorrect")(expand "histFull")(expand "histJ0write") (expand "requestMessage")(expand "grantMessage")) "expand all properties" "expand all properties" ) (defstep split-rho () (then (expand "canRead")(expand "canWrite")(expand "canReadReq")(expand "empty")(expand "home")(repeat* (then (lift-if "rho")(split "rho")))(simp)) "Splits `rho' on `action' type" "Splits `rho' on `action' type" ) (defstep split-rho-all () (then (split-rho)(replace*)(simp)(split-all)) "Splits `rho' on `action' type, replace and split-all" "Splits `rho' on `action' type, replace and split-all" ) (defstep exp-rho (&optional (split f)(hide? t)(exp t)) (then (skosimp*)(label "orig" (-1 -2 1))(hide -1 -2 1)(reveal -1 -2 1) (expand "rho")(exp-inv)(skosimp*)(expand "addCentry")(expand "insert")(expand "timestamp")(simp) (label "rho" -1) (label "memhistCorrect" -2) (label "memhistCorrect" -3) (label "memhistCorrectInit" -4) (label "channelsMatchProg" -5) (label "cacheEqualMemhist" -6) (label "channelsNonNeg" -7) (label "cEntryExists" -8) (label "channelTimeInc" -9) (label "localTimeEarlier" -10) (label "timeChannelProc" -11) (label "idPCunique" -12) (label "homeNotReq" -13) (label "waiting" -14) (label "histLt" -15) (label "histComplete" -16) (label "histCompleteNumRead" -17) (label "histMatchPC" -18) (label "histMatchPCe" -19) (label "histMatchTime" -20) (label "histMatchTimeE" -21) (label "histJ0write" -22) (label "readValuesCorrect" -23) (label "firstExists" -24) (label "toProve" +) (expand "home") (simp) (if (eq exp 't)(then (expand "occEntry")(expand "empty")(expand "removeCentry"))(skip)) (if (eq hide? 't) (hide -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24)(skip)) (if (eq split 't)(split-rho)(skip)) ) " exp-rho" "exp-rho" ) (defstep lift-split(&optional (num +)) (then (lift-if +)(split num)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep instbest (&optional (fnum *)) (then (inst? fnum :if-match best)) "Applies inst? :if-match best to the optional line number (num, +, -)" " " ) (defstep lazy-grind (&optional (if-match t) (defs !) rewrites theories exclude (updates? t)) (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) "Equiv. to (grind) with the instantiations postponed until after simplification." "By skolemization, if-lifting, simplification and instantiation") (defstep split-if (&optional (fnum *)) (then (lift-if) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (or (branch? (formula sform)) (and (negation? (formula sform)) (branch? (args1 (formula sform)))))))) (fnum (when fnums (car fnums)))) (if fnum (split fnum) (skip-msg "No IF-THEN-ELSE in the sequent.")))) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep split-if-new (&optional (fnum *)) (try (lift-if fnum) (let ((newfnum (car *new-fmla-nums*))) (if newfnum (then (split newfnum)(split-if-new$ fnum)) (skip-msg "No IF-THEN-ELSE in the sequent."))) (skip-msg "Nothing to lift-if.")) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep new-split-if (&optional (fnum +)) (then (split-if fnum)(simp)(replace*)(simp)) "Lift, split, replace and simplify " " " ) (defstep split-if-simp (&optional (fnum +)) (then (lift-if fnum)(then (split fnum)(simp))) "Lift, split and simplify " " " ) (defstep clean-up () (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * nil #'(lambda (sform) (or (and (negation? (formula sform)) (and (implication? (args1 (formula sform))) (or (tc-eq (args1 (args1 (formula sform))) *false*) (tc-eq (args2 (args1 (formula sform))) *true*)))) (and (negation? (formula sform)) (and (disjunction? (args1 (formula sform))) (or (tc-eq (args1 (args1 (formula sform))) *true*) (tc-eq (args2 (args1 (formula sform))) *true*)))) (and (conjunction? (formula sform)) (or (tc-eq (args1 (formula sform)) *false*) (tc-eq (args2 (formula sform)) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (hide fnums)(skip-msg "No formulae to clean-up"))) "Hide all antecedents of the form FALSE IMPLIS X, X IMPLIES TRUE, TRUE OR X and consequents FALSE AND Y " "Hide all antecedents of the form FALSE IMPLIES X, X IMPLIES TRUE, TRUE OR X and consequents FALSE AND Y" ) (defstep reduce-if (&optional (toreplace nil)(exclude nil)) (let ( ;(fmla (formula sform)) (fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (and (negation? (formula sform)) (and (branch? (args1 (formula sform))) (or (tc-eq (then-part (args1 (formula sform))) *false*) (tc-eq (else-part (args1 (formula sform))) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (then (split fnum)(flatten)(replace toreplace)) (skip-msg "Nothing to reduce if"))) "Split an antecedent if-formula if either the then-part or the else-part is false" "Reducing void if-formulae" ) (defstep split-all (&optional (fnum nil)(sko t)) (repeat* (then (split-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (split-if$ fnum)(simp$)(replace*)(simp$)))) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split" "Splitting consequents and antecedents with FALSE then- or else-parts " ) (defstep reduce-all (&optional (fnum nil)(sko t)) (repeat* (then (reduce-if$ +)(simp$)(if (eq sko 't)(skosimp*)(skip))(replace*)(simp$))) "Split all antecedent if-formulae where either the then-part or the else-part is false. Skolemizes and replaces" "Splitting all if-then antecedents with false" ) (defstep split-all-sko (&optional (fnum nil)(sko t)) (repeat* (then (split-if$ +)(simp$)(if (eq sko 't) (skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (split-if$ fnum)(simp$)(replace*)(simp$)))) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split. Also skolemize" "Splitting consequents and antecedents with FALSE then- or else-parts. Also skolemize " ) (defstep simp-split (&optional (fnum +)) (then (lift-if)(then (split fnum)(simp))) "lift-if, split, simp" "lift-if, split, simp" ) (defstep rewrite-all (fnums) (let ((fnum (car fnums)) (rems (cdr fnums))) (if fnum (then (auto-rewrite fnum)(rewrite-all$ rems)) (skip-msg "Auto-rewrote all formulae"))) " " " " ) (defstep hide-all-but (&optional (hidefrom *) keepnums) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) hidefrom keepnums))) (hide :fnums fnums)) "Hides all sequent formulas from FNUMS except those listed in KEEP-FNUMS. Useful when all but a few formulas need to be hidden." "Hiding ~a but keeping ~a") (defstep exp-nonempty(&optional (fnum +)) (then (expand "nonempty?")(expand "empty?")(expand "member")) " Expands nonempty?" " Expands nonempty?" ) (defstep exp-prec(&optional (fnum *)) (then (expand "weakPreceed" fnum)(expand "preceed" fnum)) " Expands (weak) preceed" " Expands (weak) preceed" ) (defstep lemLtStrict () (then (lemma "ltIsStrict")(label "ltIsStrict" -1)(flatten)(label "linear" -1 :push? t)(label "trans" -2 :push? t)) "introduces ltIsStrict lemma" "introduces ltIsStrict lemma" ) (defstep introNext () (then (skip)(CASE "exists (next : posnat): next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)) = next") (label "next" -1)(SKOSIMP*)(replace*)(LEMMA "nextSize") (label "nextSize" -1)(INST? -)(replace*)) "introduces next!1" "introduces next!1" ) $$$refine2.pvs refine2[U : posnat]: THEORY % This theory proves the refinement. % Using the history table, and the invariants about reachable ring algorithm states % we construct a serial execution, stored in the serRun array. % Each entry of serRun contains a copy of the processors and memory of the serial % system and is related to the previous entry by the serial.rho relation. % We property "Match" defines a relationship between a serial run, stored in serRun % and a reachable ring state. % This relationship is proved inductively: we first show that Match holds between % the initial states of the two systems, and then that if Match(R, serRun) holds % where R are the ring data structures and reachable(R), for every R' a % successor state of R, there exists serRun' s.t. rho_ring(R, R') and match(R',serRun'). % Amongst other things, Match ensures that the memory of the lazy and serial systems % agree at the end of the run, and that every read in the two systems returns the % same value. BEGIN IMPORTING propInvs[U], serial[U] procs, procs1, procs2, procs3, procs_p: VAR [PROC_ID -> PROC_INFO] memhist, memhist1, memhist2, memhist_p: VAR MEM_HIST_TYPE mem, mem1, mem2, mem_p: VAR MEM_TYPE hist, hist1, hist2, hist3, hist_p: VAR HISTORY_TYPE channels, channels_p : VAR CHANNELS time, t, time_p: VAR TIME proc: VAR PROC_INFO id, id2, p_id: VAR PROC_ID action: VAR ACTION_TYPE addr: VAR ADDRESS pc: VAR PC_RANGE cPoint, ol: VAR posnat serOrderedList_TYPE: TYPE = [# sprocs: [PROC_ID -> SERIAL_PROC_TYPE], smem: MEM_TYPE #] serRun, serRun_p: VAR [nat -> serOrderedList_TYPE] % The properties relating the data structures of the ring algorithm % and the serial run Match(channels, hist, mem, memhist, procs, serRun): bool = % The first state in serRun fulfills the intial conditions for serial serial.theta(smem(serRun(0)), sprocs(serRun(0))) AND % Every state in serRun is related to its successor by serial.rho (FORALL (sr: nat): sr < size(hist) IMPLIES serial.rho (smem(serRun(sr)), sprocs(serRun(sr)), smem(serRun(sr + 1)), sprocs(serRun(sr + 1)), id(lst(hist)(sr + 1)))) AND % the final serRun memory is the ring memory smem(serRun(size(hist))) = mem AND % the values read, stored in readValues, agree in the two systems (FORALL id, pc: op(instlist(id, pc)) = READ IMPLIES readValues(sprocs(serRun(size(hist)))(id))(pc) = readValues(procs(id))(pc)) AND % If P_i is waiting for a write return message then its program counter is % one less than in the serial system. Otherwise, the program counters in the % two systems are identical. (FORALL id: IF waiting(procs(id)) and exists id2, cPoint : id2 < id and (let cEntry = CE(channels(id2))(cPoint) in occEntry(channels(id2), cPoint) and id(cEntry) = id and pc(cEntry) = pc(procs(id(cEntry))) and message(cEntry) = writeRet) THEN pc(sprocs(serRun(size(hist)))(id)) = pc(procs(id)) +1 ELSE pc(sprocs(serRun(size(hist)))(id)) = pc(procs(id)) ENDIF) AND % For every entry sr of serRun, its memory equals that stored in memhist at the % time of the sr'th element of hist. (FORALL (sr: posnat): sr <= size(hist) IMPLIES smem(serRun(sr)) = mem(memhist(t(lst(hist)(sr))))) % The program counters in the serial run increase, for all processors. % The program counter of P_i only increases if there is a preceding element nsr in which % hist[nsr].id = i. That is, there is some element in which P_i took a transition, thus % increasing the program counter. pcSeqRun: LEMMA (FORALL id, (sr: nat): Match(channels, hist, mem, memhist, procs, serRun) AND sr <= size(hist) IMPLIES (FORALL (srs: nat): srs < sr IMPLIES pc(sprocs(serRun(srs))(id)) <= pc(sprocs(serRun(sr))(id)) AND (pc(sprocs(serRun(srs))(id)) < pc(sprocs(serRun(sr))(id)) IFF (EXISTS (newsr: posnat): srs < newsr AND newsr <= sr AND id(lst(hist)(newsr)) = id)))) % The next 2 lemmas prove that Match is inductive over reachable ring states: % Base case: There is a serial execution matching the initial ring state. thetaSeq: LEMMA theta(channels, hist, mem, memhist, procs) IMPLIES (EXISTS serRun: Match(channels, hist, mem, memhist, procs, serRun)) % Inductive step : If R is a reachable ring state, and rho(R, R') then there is % a serial run such that Match(R, serRun) reachSeq: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) AND (EXISTS serRun: Match(channels, hist, mem, memhist, procs, serRun)) IMPLIES (EXISTS serRun_p: Match(channels_p, hist_p, mem_p, memhist_p, procs_p, serRun_p)) END refine2 $$$refine2.prf (|refine2| (|pcSeqRun| "" (SKOSIMP*) (("" (LABEL "Match" -1) (("" (LABEL "toProve" 1) (("" (CASE "Forall (offset: nat): forall (sr : nat): sr <= size(hist!1) and offset <= sr IMPLIES pc(sprocs(serRun!1(sr - offset))(id!1)) <= pc(sprocs(serRun!1(sr))(id!1))") (("1" (LABEL "PCinc" -1) (("1" (INST - "sr!1 - srs!1") (("1" (INST - "sr!1") (("1" (SIMP) (("1" (CASE "FORALL (offset: nat): offset <= sr!1 IMPLIES (pc(sprocs(serRun!1(sr!1 - offset))(id!1)) < pc(sprocs(serRun!1(sr!1))(id!1)) IFF (EXISTS (newsr: posnat): sr!1 - offset < newsr AND newsr <= sr!1 AND id(lst(hist!1)(newsr)) = id!1))") (("1" (INST -1 "sr!1 - srs!1") (("1" (SIMP) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "offset") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "PCinc") (("2" (HIDE -1) (("2" (SPSI) (("1" (SPSI -) (("1" (SKOSIMP*) (("1" (INST? +) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "pc(sprocs(serRun!1(-1 - j!1 + sr!1))(id!1)) < pc(sprocs(serRun!1(sr!1 - j!1))(id!1))") (SIMP))) (("2" (HIDE "PCinc" -2 1) (("2" (EXPAND "Match") (("2" (FLATTEN) (("2" (INST - "-1 - j!1 + sr!1") (("2" (EXPAND "rho") (("2" (INST 1 "sr!1 - j!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "1") (("2" (INST - "sr!1 - j!1") (("2" (SIMP) (("2" (INST + "newsr!1") (("2" (SIMP) (("2" (APPLY (THEN (CASE "newsr!1 = sr!1 - j!1") (REPLACE*) (SIMP))) (("2" (APPLY (THEN (CASE "pc(sprocs(serRun!1(sr!1 - j!1 -1))(id!1)) < pc(sprocs(serRun!1(sr!1 -j!1))(id!1))") (SIMP))) (("1" (REVEAL "PCinc") (("1" (HIDE -1 -2) (("1" (INST - "j!1") (("1" (INST - "sr!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "Match") (("2" (EXPAND "rho") (("2" (FLATTEN) (("2" (INST "Match" "-1 - j!1 + sr!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL) ("2" (HIDE "toProve") (("2" (INDUCT "offset") (("1" (SKOSIMP*) (("1" (SIMP) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "sr!2") (("2" (SIMP) (("2" (APPLY (THEN (CASE " pc(sprocs(serRun!1(-1 - j!1 + sr!2))(id!1)) <= pc(sprocs(serRun!1(sr!2 - j!1))(id!1))") (SIMP))) (("2" (HIDE -1 2) (("2" (EXPAND "Match") (("2" (EXPAND "rho") (("2" (SIMP) (("2" (INST - "-1 - j!1 + sr!2") (("2" (SIMP) (("2" (SPLIT-ALL -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|thetaSeq| "" (SKOSIMP*) (("" (INST 1 "(lambda (sr:nat) : (# smem := initmem, sprocs := initsprocs #))") (("" (LAZYGRIND) NIL NIL)) NIL)) NIL) (|reachSeq| "" (SKOSIMP*) (("" (LABEL "Match" -3) (("" (LABEL "toProve" 1) (("" (LABEL "reach" -2) (("" (LEMMA "reachable") (("" (INST?) (("" (SIMP) (("" (LABEL "newReach" -1) (("" (EXPAND "reachable" -1) (("" (FLATTEN) (("" (LABEL "new_histMatchPC" -14) (("" (LABEL "new_histLt" -12) (("" (HIDE "newReach") (("" (LEMMA "pcSeqRun") (("" (INST?) (("" (SIMP) (("" (LABEL "pcSeq" -1) (("" (LABEL "rho" -4) (("" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (LABEL "nextSmall" -1) (("1" (HIDE-ALL-BUT -) (("1" (REVEAL "rho" "reach" "Match") (("1" (EXPAND "Match") (("1" (EXP-RHO) (("1" (REVEAL "new_histLt") (("1" (REVEAL "new_histMatchPC") (("1" (EXPAND "histLt") (("1" (EXPAND "histMatchPC") (("1" (SPLIT-RHO) (("1" (LABEL "canRead" (-2 -3)) (("1" (REPLACE*) (("1" (SIMP) (("1" (HIDE "rho" "new_histLt" "new_histMatchPC") (("1" (REVEAL "next" "nextSmall") (("1" (INST + "(lambda (n : nat): if n < next!1 then serRun!1(n) else (# smem := smem(serRun!1(n - 1)), sprocs:= (lambda (id : PROC_ID) : (let oldpc = pc(sprocs(serRun!1(next!1 - 1))(p_id!1)), val = smem(serRun!1(next!1 - 1))(a(instlist(p_id!1, pc(sprocs(serRun!1(next!1 - 1))(p_id!1))))) in (if id = p_id!1 then sprocs(serRun!1(next!1 - 1))(id) with [pc := oldpc + 1, readValues := (lambda pc : if pc = oldpc then val else readValues(sprocs(serRun!1(n - 1))(id))(pc) endif) ] else sprocs(serRun!1(n-1))(id) endif )))#) endif)") (("1" (REPLACE*) (("1" (SIMP) (("1" (EXPAND "theta") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST - "sr!1") (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (SPSI) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? "Match") (("2" (INST?) (("2" (REPLACE*) (("2" (CLEAN-UP) (("2" (HIDE 2) (("2" (SIMP) (("2" (CASE "sr!1 = 0") (("1" (REPLACE*) (("1" (EXPAND "initsprocs") (("1" (REVEAL "histMatchPCe") (("1" (INST? :WHERE 1) (("1" (INST -1 "1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histMatchPC") (("1" (EXPAND "histMatchPC") (("1" (REVEAL "rho") (("1" (REPLACE*) (("1" (SIMP) (("1" (INST - "index!1 + 1") (("1" (HIDE "rho") (("1" (SIMP) (("1" (INST -1 "1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "pcSeq") (("2" (INST -1 "p_id!1" "size(hist!1)") (("2" (SIMP) (("2" (INST - "sr!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "new_histMatchPC") (("2" (INST - "1 + sr!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) (("2" (INST - "newsr!1 + 1") (("2" (SIMP) (("2" (REVEAL "histMatchPC") (("2" (INST - "newsr!1") (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "next!1 < 1 + sr!1") (SIMP))) (("2" (REVEAL "Match") (("2" (INST - "sr!1 - 1") (("2" (NEW-SPLIT-IF) (("1" (HIDE "Match" 1) (("1" (REVEAL "new_histMatchPC") (("1" (INST - "next!1") (("1" (REPLACE*) (("1" (SIMP) (("1" (INST - "sr!1 + 1") (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchPC") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -8) (("2" (INST - "id!1" "pc!1") (("2" (NEW-SPLIT-IF) (("2" (INST?) (("2" (SIMP) (("2" (REVEAL "readValuesCorrect") (("2" (INST - "p_id!1" "pc!1") (("2" (SIMP) (("2" (REVEAL "pcSeq") (("2" (INST - "p_id!1" "size(hist!1)") (("2" (SIMP) (("2" (INST - "next!1 - 1") (("2" (CASE "next!1 <= size(hist!1)") (("1" (SIMP) (("1" (CASE "pc(sprocs(serRun!1(next!1 - 1))(p_id!1))= pc(sprocs(serRun!1(size(hist!1)))(p_id!1))") (("1" (SIMP) (("1" (REPLACE*) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "cacheEqualMemhist") (("1" (INST - "p_id!1") (("1" (SIMP) (("1" (INST? -) (("1" (SIMP) (("1" (REPLACE*) (("1" (CASE "next!1 = 1") (("1" (REPLACE*) (("1" (EXPAND "initsprocs") (("1" (REPLACE*) (("1" (SIMP) (("1" (REVEAL "memhistCorrectInit") (("1" (CASE "t(procs!1(p_id!1)) = 0") (("1" (SIMP) NIL NIL) ("2" (REVEAL "histMatchTimeE") (("2" (INST - "t(procs!1(p_id!1))") (("2" (REVEAL "localTimeEarlier") (("2" (INST - "p_id!1") (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "new_histLt") (("2" (INST - "next!1" "index!1 + 1") (("2" (REPLACE*) (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "next!1 - 1") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (REVEAL "new_histLt") (("1" (INST - "next!1 - 1" "next!1") (("1" (REPLACE*) (("1" (EXPAND "timestamp") (("1" (SIMP) (("1" (EXPAND "lt") (("1" (REVEAL "histMatchTimeE") (("1" (INST - " t(procs!1(p_id!1))") (("1" (REVEAL "localTimeEarlier") (("1" (INST - "p_id!1") (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histLt") (("1" (REPLACE*) (("1" (INST - "next!1" "index!1 + 1") (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (CASE "next!1 < 1 + index!1") (("1" (SIMP) NIL NIL) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (REVEAL "new_histLt") (("2" (INST - "index!1" "next!1 - 1") (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "new_histMatchPC") (("2" (INST - "next!1") (("2" (REPLACE*) (("2" (SIMP) (("2" (SIMP) (("2" (INST - "newsr!1 + 1") (("2" (SIMP) (("2" (REVEAL "histMatchPC") (("2" (INST - "newsr!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "next!1 = size(hist!1) + 1") (SIMP) (REPLACE*))) (("2" (NEW-SPLIT-IF) (("2" (CLEAN-UP) (("2" (REVEAL "cacheEqualMemhist") (("2" (INST - "p_id!1") (("2" (SIMP) (("2" (INST?) (("2" (SIMP) (("2" (REPLACE*) (("2" (REVEAL "memhistCorrect") (("2" (CASE "t(procs!1(p_id!1)) = t(procs!1(0))") (("1" (REPLACE*) NIL NIL) ("2" (REVEAL "localTimeEarlier") (("2" (INST - "p_id!1") (("2" (SIMP) (("2" (INST - "t(procs!1(0)) - 1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histLt") (("1" (INST - "index!1") (("1" (INST - "index!1" "next!1") (("1" (REPLACE*) (("1" (EXPAND "timestamp") (("1" (SIMP) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST -10 "id!1") (("3" (NEW-SPLIT-IF) (("1" (REVEAL "pcSeq") (("1" (INST -1 "id!1" "size(hist!1)") (("1" (SIMP) (("1" (INST -1 "next!1 - 1") (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "histMatchTime") (("1" (INST - "newsr!1") (("1" (SIMP) (("1" (HIDE "Match") (("1" (REPLACE*) (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (REVEAL "new_histLt") (("2" (EXPAND "histLt") (("2" (INST - "next!1" "newsr!1 + 1") (("2" (REVEAL "rho") (("2" (REPLACE*) (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (HIDE "rho") (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (REDUCE-ALL) (("1" (INST? +) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REDUCE-ALL) (("2" (INST? +) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST-CP -12 "sr!1") (("4" (NEW-SPLIT-IF) (("4" (CASE "sr!1 >= 2") (("1" (INST -13 "sr!1 - 1") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "t(lst(hist!1)(next!1 - 1)) = t(procs!1(p_id!1))") (SIMP))) (("1" (LEMMA "nextExists") (("1" (INST?) (("1" (NEW-SPLIT-IF -) (("1" (INST - "next!1 - 1") (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (HIDE "Match") (("1" (HIDE -1) (("1" (REVEAL "histMatchTimeE") (("1" (INST -1 "t(procs!1(p_id!1))") (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "histLt") (("1" (INST -1 "index!1" "next!1 - 1") (("1" (EXPAND "lt") (("1" (SIMP) (("1" (APPLY (THEN (CASE "next!1 <= index!1") (SIMP))) (("1" (REVEAL "new_histLt") (("1" (INST - "next!1" "index!1 + 1") (("1" (REPLACE*) (("1" (EXPAND "timestamp") (("1" (SIMP) (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (REPLACE -5 :DIR RL :HIDE? T) (("2" (SIMP) (("2" (HIDE "Match") (("2" (INST + "size(hist!1)") (("2" (EXPAND "lt") (("2" (EXPAND "timestamp") (("2" (REVEAL "histMatchTimeE") (("2" (INST - "t(procs!1(p_id!1))") (("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "histLt") (("2" (INST - "index!1" "size(hist!1)") (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL) ("2" (APPLY (THEN (CASE "sr!1 = 1") (SIMP) (REPLACE*))) (("2" (REVEAL "memhistCorrectInit") (("2" (APPLY (THEN (CASE "t(procs!1(p_id!1)) = 0") (SIMP))) (("2" (HIDE "Match") (("2" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("2" (REVEAL "histMatchTimeE") (("2" (INST - "t(procs!1(p_id!1))") (("2" (REVEAL "localTimeEarlier") (("2" (INST?) (("2" (SIMP) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "new_histLt") (("2" (EXPAND "histLt") (("2" (INST - "1" "index!1 + 1") (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (REVEAL "rho") (("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (SIMP) NIL NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "serRun!1") (("2" (REPLACE*) (("2" (HIDE "rho" "new_histMatchPC" "new_histLt") (("2" (SIMP) (("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST? -) (("1" (INST? -) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (INST - "id!1") (("2" (REVEAL "rho") (("2" (SIMP) (("2" (REPLACE*) (("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "waiting") (("1" (INST - "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI -5) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST + "serRun!1") (("3" (REPLACE*) (("3" (HIDE "rho" "new_histMatchPC" "new_histLt") (("3" (SIMP) (("3" (INST?) (("3" (SPSI) (("1" (SKOSIMP*) (("1" (INST?) (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "Match") (("2" (INST -1 "id!1") (("2" (NEW-SPLIT-IF -) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI "toProve") (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST + "serRun!1") (("4" (REPLACE*) (("4" (SIMP) (("4" (HIDE "rho" "new_histMatchPC" "new_histLt") (("4" (INST? -) (("4" (SPSI) (("1" (SKOSIMP*) (("1" (INST? -) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST - "id!1") (("2" (SPSI -5) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (SPSI) (("1" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (INST + "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (CASE "id(CE(channels!1(inChannel(id!1)))(head(channels!1(inChannel(id!1))))) = id!1") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (REVEAL "channelsMatchProg") (("1" (INST?) (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "inChannel") (("1" (REPLACE*) (("1" (SIMP) (("1" (REDUCE-ALL) (("1" (REVEAL "channelsMatchProg") (("1" (INST - "id2!1" "cPoint!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (CASE "pc(CE(channels!1(id!1 - 1))(head(channels!1(id!1 - 1)))) = pc(procs!1(id!1))") (("1" (SIMP) (("1" (INST + "id2!1" "cPoint!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (EXPAND "inChannel") (("2" (REPLACE -1 :DIR RL :HIDE? T) (("2" (REVEAL 1) (("2" (INST + "p_id!1" "tail(channels!1(p_id!1))") (("2" (NEW-SPLIT-IF) (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP + "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (CLEAN-UP) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (SIMP) (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (SIMP) (("2" (EXPAND "inChannel") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) (("2" (INST + "id!1 - 1" "head(channels!1(id!1 - 1))") (("2" (SIMP) (("2" (REVEAL "rho") (("2" (EXPAND "inChannel") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (SKOSIMP*) (("2" (INST-CP + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (CLEAN-UP) (("1" (REVEAL 2) (("1" (EXPAND "inChannel") (("1" (INST + "id2!1 - 1" "head(channels!1(id2!1 - 1))") (("1" (SIMP) (("1" (REVEAL "channelsNonNeg" "rho") (("1" (INST - "id2!1 - 1") (("1" (EXPAND "inChannel") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (INST + "serRun!1 with [(size(hist_p!1)) := (# smem := mem_p!1, sprocs := sprocs(serRun!1(size(hist!1))) WITH [(id(CE(channels!1(U))(head(channels!1(U))))) := sprocs(serRun!1(size(hist!1)))(id(CE(channels!1(U))(head(channels!1(U))))) with [pc := pc(sprocs(serRun!1(size(hist!1)))(id(CE(channels!1(U))(head(channels!1(U)))))) + 1]] #)]") (("5" (EXPAND "inChannel") (("5" (SIMP) (("5" (REVEAL "channelsNonNeg") (("5" (INST - "U") (("5" (SPSI) (("1" (HIDE "new_histMatchPC" "new_histLt") (("1" (SKOSIMP*) (("1" (SIMP) (("1" (SPSI) (("1" (INST "Match" "sr!1") (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (HIDE 1) (("1" (REVEAL "rho") (("1" (REVEAL "channelsMatchProg") (("1" (INST?) (("1" (SIMP) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) (("1" (APPLY (THEN (CASE "pc(sprocs(serRun!1(sr!1)) (id(CE(channels!1(U))(head(channels!1(U)))))) = pc(CE(channels!1(U))(head(channels!1(U))))") (SIMP))) (("1" (INST? "Match") (("1" (INST? "Match") (("1" (SIMP) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (REVEAL "idPCunique") (("1" (INST - "U" "id2!1" "head(channels!1(U))" "cPoint!1") (("1" (SIMP) (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "channelsMatchProg") (("2" (INST?) (("2" (SIMP) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SIMP) (("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (REVEAL "idPCunique") (("2" (INST - "U" "id2!1" "head(channels!1(U))" "cPoint!1") (("2" (SIMP) (("2" (EXPAND "weakPreceed") (("2" (EXPAND "occEntry") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (SIMP) (("2" (REVEAL "channelsMatchProg") (("2" (INST?) (("2" (SIMP) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (SIMP) (("2" (INST? "Match") (("2" (INST? "Match") (("2" (SIMP) (("2" (INST? "Match") (("2" (NEW-SPLIT-IF) (("1" (HIDE "rho") (("1" (SPSI) (("1" (REDUCE-IF) (("1" (REPLACE*) (("1" (HIDE 1) (("1" (SKOSIMP*) (("1" (REVEAL "idPCunique") (("1" (INST - "U" "id2!1" "head(channels!1(U))" "cPoint!1") (("1" (SIMP) (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (NEW-SPLIT-IF) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "Match") (("2" (INST -3 "sr!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? "Match") (("2" (INST? "Match") (("2" (REPLACE*) (("2" (SIMP) (("2" (HIDE "rho" "new_histLt" "new_histMatchPC") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST? "Match") (("3" (INST? "Match") (("3" (INST "Match" "id!1") (("3" (REPLACE*) (("3" (HIDE "rho" "new_histLt" "new_histMatchPC") (("3" (SIMP) (("3" (HIDE -3 -5) (("3" (REVEAL "waiting") (("3" (INST?) (("3" (REVEAL "channelsMatchProg") (("3" (INST?) (("3" (SIMP) (("3" (REVEAL "homeNotReq") (("3" (INST?) (("3" (NEW-SPLIT-IF) (("3" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (REVEAL "idPCunique") (("1" (INST - "U" "id2!2" "head(channels!1(U))" "cPoint!2") (("1" (SIMP) (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (INST + "0" "tail(channels!1(0))") (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST - "0") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id2!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (REPLACE*) (("4" (HIDE "rho" "new_histLt" "new_histMatchPC") (("4" (INST? "Match") (("4" (INST? "Match") (("4" (INST? "Match") (("4" (INST "Match" "sr!1") (("4" (NEW-SPLIT-IF) (("4" (NEW-SPLIT-IF) (("4" (REVEAL "histMatchTime") (("4" (INST?) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (INST + "serRun!1") (("6" (REVEAL "channelsNonNeg") (("6" (INST - "U") (("6" (EXPAND "inChannel") (("6" (REPLACE*) (("6" (HIDE "rho" "new_histMatchPC" "new_histLt") (("6" (SIMP) (("6" (SKOSIMP*) (("6" (INST? "Match") (("6" (INST? "Match") (("6" (INST? "Match") (("6" (SPSI) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "homeNotReq") (("1" (INST?) (("1" (SIMP) (("1" (REDUCE-IF) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id2!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (LIFT-IF) (("7" (SPSI -) (("1" (INST + "serRun!1 with [(size(hist_p!1)) := (# smem := mem_p!1, sprocs := sprocs(serRun!1(size(hist!1))) WITH [(0) := sprocs(serRun!1(size(hist!1)))(0) with [pc := pc(sprocs(serRun!1(size(hist!1)))(0)) + 1]] #)]") (("1" (REPLACE*) (("1" (HIDE "rho" "new_histMatchPC" "new_histLt") (("1" (SIMP) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST - "sr!1") (("1" (INST?) (("1" (INST - "0") (("1" (SPLIT-ALL) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "size(hist!1)") (("2" (INST?) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST - "size(hist!1)") (("3" (INST?) (("3" (INST - "id!1") (("3" (NEW-SPLIT-IF) (("3" (SPSI) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (SPLIT-ALL -) NIL NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "id2!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST - "size(hist!1)") (("4" (INST?) (("4" (INST?) (("4" (INST - "sr!1") (("4" (SIMP) (("4" (CLEAN-UP) (("4" (NEW-SPLIT-IF) (("4" (NEW-SPLIT-IF) (("4" (REVEAL "histMatchTime") (("4" (INST?) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "next" "nextSmall") (("2" (INST + "(lambda (n : nat): if n < next!1 then serRun!1(n) else (# smem := smem(serRun!1(n - 1)), sprocs:= (lambda (id : PROC_ID) : (let oldpc = pc(sprocs(serRun!1(next!1 - 1))(p_id!1)), val = smem(serRun!1(next!1 - 1))(a(instlist(p_id!1, pc(sprocs(serRun!1(next!1 - 1))(p_id!1))))) in (if id = p_id!1 then sprocs(serRun!1(next!1 - 1))(id) with [pc := oldpc + 1, readValues := (lambda pc : if pc = oldpc then val else readValues(sprocs(serRun!1(n - 1))(id))(pc) endif) ] else sprocs(serRun!1(n-1))(id) endif )))#) endif)") (("1" (REPLACE*) (("1" (SIMP) (("1" (REPLACE*) (("1" (HIDE "rho" "new_histMatchPC" "new_histLt") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST?) (("1" (NEW-SPLIT-IF) (("1" (INST? -) (("1" (INST? -) (("1" (SPSI) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (SPSI) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (REVEAL "rho") (("2" (SIMP) (("2" (CASE "serRun!1(sr!1)`sprocs(0)`pc = pc(procs!1(0))") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) (("1" (ASSERT :FLUSH? T) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (CASE "sr!1 = size(hist!1)") (("1" (SIMP) NIL NIL) ("2" (HIDE 4 -5) (("2" (REVEAL "pcSeq") (("2" (INST - "0" "size(hist!1)") (("2" (SIMP) (("2" (INST - "sr!1") (("2" (SIMP) (("2" (APPLY (THEN (CASE "pc(sprocs(serRun!1(sr!1))(0)) < pc(sprocs(serRun!1(size(hist!1)))(0))") (SIMP))) (("2" (SKOSIMP*) (("2" (REVEAL "new_histMatchPC") (("2" (SIMP) (("2" (INST - "next!1") (("2" (SIMP) (("2" (INST - "1 + newsr!1") (("2" (SIMP) (("2" (REVEAL "histMatchPC") (("2" (INST?) (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "Match") (("2" (INST -3 "sr!1 - 1") (("2" (APPLY (THEN (CASE "next!1 <= sr!1") (SIMP))) (("2" (NEW-SPLIT-IF) (("1" (HIDE 1 "Match") (("1" (REVEAL "new_histLt") (("1" (INST - "next!1" "sr!1 + 1") (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) (("1" (REDUCE-IF) (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SPSI) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (HIDE "Match") (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("2" (HIDE "Match") (("2" (NEW-SPLIT-IF) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY 2 :HIDE? T) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "size(hist!1)") (("2" (INST?) (("2" (SIMP) (("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF) (("2" (CASE "pc(sprocs(serRun!1(next!1 - 1))(0)) /= pc(procs!1(0))") (("1" (HIDE 1) (("1" (SIMP) (("1" (INST? -) (("1" (SIMP) (("1" (REVEAL "pcSeq") (("1" (INST - "size(hist!1)") (("1" (INST - "0" "size(hist!1)") (("1" (SIMP) (("1" (INST - "next!1 - 1") (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histMatchPC") (("1" (INST - "next!1") (("1" (SIMP) (("1" (INST - "newsr!1 + 1") (("1" (SIMP) (("1" (REVEAL "histMatchPC") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (CASE "next!1 = 1") (("1" (REPLACE*) (("1" (EXPAND "theta") (("1" (SIMP) (("1" (REPLACE*) (("1" (EXPAND "initsprocs") (("1" (REVEAL "memhistCorrectInit") (("1" (REVEAL "memhistCorrect") (("1" (HIDE -2) (("1" (CASE "t(procs!1(0)) = 0") (("1" (SIMP) NIL NIL) ("2" (REVEAL "histMatchTimeE") (("2" (INST - "t(procs!1(0))") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "new_histLt") (("2" (INST -1 "1" "index!1 + 1") (("2" (SIMP) (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST - "next!1 - 1") (("1" (SIMP) (("1" (REVEAL "memhistCorrect") (("1" (CASE "t(lst(hist!1)(next!1 - 1)) = t(procs!1(0))") (("1" (SIMP) NIL NIL) ("2" (HIDE "memhistCorrect") (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SIMP) (("2" (HIDE -2) (("2" (REVEAL "histMatchTimeE") (("2" (INST - "t(procs!1(0))") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "histLt") (("2" (INST-CP - "index!1" "next!1 -1") (("2" (INST - "next!1 - 1" "index!1") (("2" (EXPAND "lt") (("2" (SIMP) (("2" (APPLY (THEN (CASE "next!1 - 1 < index!1") (SIMP))) (("2" (REVEAL "new_histLt") (("2" (INST - "next!1" "index!1 + 1") (("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST - "size(hist!1)") (("3" (INST?) (("3" (INST - "id!1") (("3" (SIMP) (("3" (CLEAN-UP) (("3" (NEW-SPLIT-IF) (("1" (REVEAL "pcSeq") (("1" (INST - "0" "size(hist!1)") (("1" (SIMP) (("1" (INST - "next!1 - 1") (("1" (SIMP) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histMatchPC") (("1" (INST - "next!1") (("1" (SIMP) (("1" (INST - "newsr!1 + 1") (("1" (SIMP) (("1" (REVEAL "histMatchPC") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id2!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST - "sr!1 - 1") (("4" (INST?) (("4" (INST?) (("4" (INST-CP - "sr!1") (("4" (NEW-SPLIT-IF) (("4" (CASE "sr!1 = 1") (("1" (REPLACE*) (("1" (EXPAND "theta") (("1" (EXPAND "initsprocs") (("1" (SIMP) (("1" (REPLACE*) (("1" (REVEAL "memhistCorrectInit") (("1" (APPLY (THEN (CASE "t(procs!1(0)) = 0") (SIMP))) (("1" (HIDE "Match") (("1" (REVEAL "histMatchTimeE") (("1" (INST - "t(procs!1(0))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "new_histLt") (("1" (INST - "1" "index!1 + 1") (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "sr!1 - 1") (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) (("1" (HIDE -2) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "t(procs!1(0))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (HIDE "Match") (("1" (REVEAL "histLt") (("1" (INST-CP - "index!1" "next!1 - 1") (("1" (INST - "next!1 - 1" "index!1") (("1" (EXPAND "lt") (("1" (SIMP) (("1" (REVEAL "new_histLt") (("1" (INST - "next!1" "index!1 + 1") (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (SIMP) NIL NIL)) NIL) ("3" (SKOSIMP*) (("3" (SIMP) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (REPLACE*) (("8" (SIMP) (("8" (INST + "serRun!1") (("8" (SIMP) (("8" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("9" (REPLACE*) (("9" (SIMP) (("9" (INST + "serRun!1") (("9" (SIMP) (("9" (SPSI) (("1" (SKOSIMP*) (("1" (INST? "Match") (("1" (INST? "Match") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? "Match") (("2" (INST? "Match") (("2" (INST "Match" "id!1") (("2" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF) (("1" (REDUCE-IF) (("1" (INST + "id2!1" "cPoint!1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (INST + "id2!1" "cPoint!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (REDUCE-IF) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (INST + "id2!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-IF) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id2!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$serial.pvs serial[U : posnat]: THEORY % Definition of the serial system. % There is an array procs of processors. % At each step process p_id performs the next access in the instlist (either a % read or a write.) % The global memory, mem, is updated if the access is a write. % The auxiliary variable readValues records the values returned by reads. BEGIN IMPORTING shared[U] SERIAL_PROC_TYPE : TYPE = [# pc : PC_RANGE, readValues : [PC_RANGE -> VALUE] #] mem, mem_p : VAR MEM_TYPE proc_id, p_id, id : VAR PROC_ID procs, procs_p : VAR [PROC_ID -> SERIAL_PROC_TYPE] a, addr : VAR ADDRESS pc : VAR PC_RANGE initsprocs : [PROC_ID -> SERIAL_PROC_TYPE] = (lambda proc_id : (# pc := 1, readValues := (lambda pc : 0) #)) theta(mem, procs): bool = procs = initsprocs and mem = initmem rho(mem, procs, mem_p, procs_p, p_id): bool = (let proc = procs(p_id), pc = pc(procs(p_id)), a = a(instlist(p_id, pc(procs(p_id)))), v = v(instlist(p_id, pc(procs(p_id)))) in if op(instlist(p_id, pc)) = READ then mem_p = mem and procs_p = procs with [(p_id) := (# pc := pc + 1, readValues := readValues(proc) with [(pc) := mem(a)] #)] else mem_p = mem with [(a) := v] and procs_p = procs with [(p_id) := (# pc := pc + 1, readValues := readValues(proc) #)] endif ) END serial $$$more_nat_types.pvs more_nat_types[m: posnat]: THEORY BEGIN upto_nz : TYPE = {i: upto[m] | NOT i = 0} CONTAINING m greater_one_nat : TYPE = {i : posnat | NOT i = 1} containing 2 END more_nat_types $$$more_nat_types.prf (|more_nat_types| (|upto_nz_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|greater_one_nat_TCC1| "" (SUBTYPE-TCC) NIL NIL)) $$$shared.pvs shared[U : posnat]: THEORY % Structures common to the ring and serial algorithms BEGIN IMPORTING more_nat_types % The range of instruction indices PC_RANGE: TYPE = posnat OP_TYPE: TYPE = {READ, WRITE} ADDRESS : TYPE = nat VALUE : TYPE = real TIME : TYPE = nat % Processor identities are in the range 0..U PROC_ID : TYPE = upto[U] % A memory is an function from ADDRESS to VALUE MEM_TYPE: TYPE = [ADDRESS -> VALUE] % Instructions have operations, addresses, and values. INST: TYPE = [# op: OP_TYPE, a: ADDRESS, v: VALUE #] % This data structure stores the instruction lists ("programs") % for all processors instlist: [PROC_ID, PC_RANGE -> INST] % The initial memory state. It is undefined, but must be the % same in both systems. initmem : [ADDRESS -> VALUE] END shared $$$ring.pvs ring[U : posnat]: THEORY BEGIN % In this file we define the ring algorithm. % Data structures: % memhist of type MEM_HIST_TYPE. % mem(memhist(t)) gives the memory at time t, id and pc identify the instruction % that upated memhist(t-1) to memhist(t). % hist of HISTORY_TYPE % size(hist) gives the number of occupied entries in hist, lst is the list of entries. % Each entry is of type HIST_RECORD_TYPE, containing an operation op, pc, time, % reads(r), address and processor id field. % procs of type [PROC_ID -> PROC_INFO] % There are U + 1 processors numbered 0..U, with processor 0 being the supervisor, or "home". % Information about each processor is recorded in a record of type PROC_INFO recording % the current program counter (pc), the cache, the local time t, % numRead, the number of reads since the last writeReturn was received, % and the array readValues of values read, for each instruction. % The cache is of type CACHE_TYPE. The domain is "ADDRESS" and each entry % has a value v and a flag oc, which is true iff the value is valid i.e. is "in" the cache. % Entries which are not valid (not occupied) are "not in the cache." % The supervisor does not have a cache, and accesses the memory directly % (We note that this was not made clear enough in the article, and will clarify it.) % channels, of type CHANNELS is an array of U+1 channels. % For each processor i channels[i] is the outChannel of i on which it sends it messages, % while receiving messages on channels[i-1 mod (U+1)] % Each individual channel of type CHANNEL_TYPE is modeled as a queue. The % top (oldest) entry in the queue is pointed to by a head pointer, and a tail % pointer points to the next free slot. % Each entry on a channel is of type CHANNEL_ENTRY_TYPE, noting the type of % message (read request, write request, write return or read return) % the value, the local time of the processor which sent the message (when it was % first sent) the processor id of the originating processor, and the program % counter to which this message corresponds. % In the case of read returns and write returns the time, processor id and pc fields % refer to the processor which sent the original read request or write request % to which this message is a response. % Actions % Actions read, readReq, writeReq, cacheUpdate and cacheInvalidate are performed by processors % i /= 0 % Actions homeAnswerWrite, homeAnswerOther and homeReadWrite are peformed by the supervisor. % The idle action can be performed by any processor. % read Processor i /= 0 performs a read from its cache, updating the history % table, and recording the value in the readValues array % readReq (read request) % The next instruction is a read to an address which is not % valid in the cache. The processor i /= 0 sends a read request message for % this address and enters a waiting state. % writeReq (write request) % The processor i /= 0 requests to do a write, and sends a writeRequest % messaage. It enters a waiting state. % cacheUpdate The processor i /= 0 pops the oldest entry off its inChannel and pushes % it onto its outChannel. % If the message is a writeReturn it updates its cache accordingly and % considers the write instruction compleated. % If the message is a readReturn corresponding to a readRequest sent % by this processor, the cache is also updated. % If the message is a readReturn or writeReturn and its id is that of the % processor, the processor releases itself from the waiting state. % cacheInvalidate The processor invalidates a cache entry by setting oc to false. % homeAnswerWrite The home pops the oldest entry off its in channel and this entry is % a writeRequest. % It updates its cache (which is the shared memory) with the specified % value, and sends a writeReturn message on its outChannel. % The write is recorded in the history and memhist tables. % homeAnswerOther The home pops the oldest entry off its in channel and this entry is % not a writeRequest. % If the entry is a readRequest then it reads the appropriate address % from its cache and sends a readReturn message. % Otherwise, nothing is done and the message is effectively removed from % the system. % homeReadWrite The home performs the next instruction in its instruction list, % updating the history and memhist structures appropriately. % If the instruction is a write a writeReturn message is sent so that % all other processors can update their caches. % idle Idle. IMPORTING shared[U] MEM_HIST_TYPE: TYPE = [TIME -> [# mem : MEM_TYPE, id : PROC_ID, pc : PC_RANGE #]] TIMESTAMP : TYPE = [# t : TIME, r : nat, id : PROC_ID #] CACHE_TYPE : TYPE = [ADDRESS -> [# v : VALUE, oc : boolean #]] HIST_RECORD_TYPE : TYPE = [# op : OP_TYPE, pc : PC_RANGE, t : TIME, r : nat, v : VALUE, a : ADDRESS, id : PROC_ID #] HISTORY_TYPE : TYPE = [# size : nat, lst : [posnat -> HIST_RECORD_TYPE] #] messageType : TYPE = {readReq, writeReq, writeRet, readRet} CHANNEL_ENTRY_TYPE : TYPE = [# message : messageType, a : ADDRESS, v : VALUE, t : TIME, id : PROC_ID, pc : PC_RANGE#] CHANNEL_TYPE : TYPE = [# head, tail : posnat, CE : [posnat -> CHANNEL_ENTRY_TYPE] #] CHANNELS : TYPE = [PROC_ID -> CHANNEL_TYPE] PROC_INFO : TYPE = [# pc : PC_RANGE, cache : CACHE_TYPE, t : TIME, numRead : nat, waiting : boolean, readValues : [PC_RANGE -> VALUE] #] ACTION_TYPE : TYPE = {read, readReq, writeReq, cacheUpdate, idle, cacheInvalidate, homeAnswerOther, homeAnswerWrite, homeReadWrite} procs, procs_p : VAR [PROC_ID -> PROC_INFO] memhist, memhist_p : VAR MEM_HIST_TYPE mem, mem_p : VAR MEM_TYPE hist, hist_p : VAR HISTORY_TYPE proc, proc2 : VAR PROC_INFO proc_id, p_id, id : VAR PROC_ID cPoint : VAR posnat update : VAR bool action : VAR ACTION_TYPE channels, channels_p : VAR CHANNELS channel : VAR CHANNEL_TYPE cEntry : VAR CHANNEL_ENTRY_TYPE a, addr : VAR ADDRESS home : PROC_ID = 0 newrec, hrec : VAR HIST_RECORD_TYPE; index, index2, rank : VAR posnat h, h1, h2, h3, next, new : VAR TIMESTAMP % Returns the index of the in-channel of processor id inChannel(id) : PROC_ID = if id > 0 then id - 1 else U endif outChannel(id) : PROC_ID = id % Extract the timestamp from a history table entry. timestamp(hrec): TIMESTAMP = (# t := t(hrec), r := r(hrec), id := id(hrec) #) % Defines an ordering over timestamps. lt(h1, h2: TIMESTAMP) : bool = t(h1) < t(h2) or (t(h1) = t(h2) and (r(h1) < r(h2) or (r(h1) = r(h2) and id(h1) < id(h2)))) % Finds the position where a new entry should be entered into the history table. next(hist, h1): posnat = if (exists index : index <= size(hist) and lt(h1, timestamp(lst(hist)(index))) and (forall index2: index2 <= size(hist) and lt(h1, timestamp(lst(hist)(index2))) implies index <= index2)) then (choose (lambda index : index <= size(hist) and lt(h1, timestamp(lst(hist)(index))) and (forall index2: index2 <= size(hist) and lt(h1, timestamp(lst(hist)(index2))) implies index <= index2))) else size(hist) + 1 endif % Places entry hrec in its correct position in the history table, shifting % any succeeding entries up by one insert(hist, hrec): HISTORY_TYPE = (let rank = next(hist, timestamp(hrec)) in (# size := size(hist) + 1, lst := (lambda index: if index < rank then lst(hist)(index) elsif index = rank then hrec else lst(hist)(index-1) endif) #)) % pushes a message onto a channel, returning the updated channel addCentry(channel, cEntry): CHANNEL_TYPE = (# head := head(channel), tail := tail(channel) + 1, CE := CE(channel) with [(tail(channel)) := cEntry] #) % pops a message off a channel, returning the updated channel removeCentry(channel) : CHANNEL_TYPE = channel WITH [head := head(channel) + 1] % Returns true iff entry cPoint of a channel is occupied occEntry(channel, cPoint) : bool = cPoint < tail(channel) and cPoint >= head(channel) % Returns true iff channel is empty empty(channel) : bool = head(channel) = tail(channel) % pre-conditions for a processor i/=0 to perform a read canRead(proc, proc_id) : bool = proc_id /= home and op(instlist(proc_id, pc(proc))) = READ and not waiting(proc) and oc(cache(proc)(a(instlist(proc_id, pc(proc))))) % pre-conditions for a processor i/=0 to perform a write canWrite(proc, proc_id): bool = proc_id /= home and op(instlist(proc_id, pc(proc))) = WRITE and not waiting(proc) canReadReq(proc, proc_id) : bool = proc_id /= home and op(instlist(proc_id, pc(proc))) = READ and not waiting(proc) and not oc(cache(proc)(a(instlist(proc_id, pc(proc))))) % The initial state. theta(channels, hist, mem, memhist, procs): bool = size(hist) = 0 and mem(memhist(0)) = initmem and mem = initmem and (forall proc_id : head(channels(proc_id)) = 1 and tail(channels(proc_id)) = 1 and (let proc = procs(proc_id) in not waiting(proc) and pc(proc) = 1 and numRead(proc) = 0 and t(proc) = 0 and readValues(proc) =(lambda (pc : PC_RANGE) : 0) and (forall addr : oc(cache(proc)(addr)) implies v(cache(proc)(addr)) = mem(addr)))) % The transition relation. % Processor p_id is the processor that will "do something" and the chosen % action is "action". Note that the action must fulfill some system requirements. % I.e. it is not possible to perform every action from every state. rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action): bool = (let proc = procs(p_id), pc = pc(procs(p_id)), a = a(instlist(p_id, pc(procs(p_id)))), v = v(instlist(p_id, pc(procs(p_id)))) in CASES (action) of read : canRead(procs(p_id), p_id) and procs_p = procs with [(p_id) := procs(p_id) with [pc := pc + 1, numRead := numRead(proc) + 1, readValues := readValues(proc) with [(pc) := v(cache(proc)(a))]]] and (let newrec = (# t:= t(proc), r:= numRead(proc) + 1, id := p_id, op := READ, pc := pc, v := v(cache(proc)(a)), a := a #) in hist_p = insert(hist, newrec)) and channels_p = channels and memhist_p = memhist and mem_p = mem, readReq : canReadReq(procs(p_id), p_id) and channels_p = channels WITH [(p_id) := addCentry(channels(p_id), (# message := readReq, a := a, v := v, t := 0, id := p_id, pc := pc#))] and procs_p = procs with [(p_id) := proc with [waiting := true]] and memhist_p = memhist and hist_p = hist and mem_p = mem, writeReq : canWrite(procs(p_id), p_id) and channels_p = channels WITH [(p_id) := addCentry(channels(p_id), (# message := writeReq, a := a, v := v, t := 0, id := p_id, pc := pc#))] and procs_p = procs with [(p_id) := proc with [pc := pc, waiting := true]] and memhist_p = memhist and hist_p = hist and mem_p = mem, cacheUpdate : not empty(channels(inChannel(p_id))) and p_id /= home and (let cEntry = CE(channels(inChannel(p_id)))(head(channels(inChannel(p_id)))) in (let upDate = message(cEntry) = writeRet or message(cEntry) = readRet and id(cEntry) = p_id in channels_p = channels WITH [(inChannel(p_id)) := removeCentry(channels(inChannel(p_id))), (p_id) := addCentry(channels(p_id), cEntry)] and procs_p = procs WITH [(p_id) := proc WITH [ t := if message(cEntry) = writeRet then t(proc) + 1 else t(proc) endif, numRead := if message(cEntry) = writeRet then 0 else numRead(proc) endif, pc := if message(cEntry) = writeRet and id(cEntry) = p_id then pc + 1 else pc endif, waiting := waiting(proc) and not id(cEntry) = p_id, cache := (lambda a: if a = a(cEntry) and upDate then (# oc := true, v := v(cEntry) #) else cache(proc)(a) endif )]])) and hist_p = hist and memhist_p = memhist and mem_p = mem, homeAnswerWrite : not empty(channels(inChannel(home))) and (let cEntry = CE(channels(inChannel(home)))(head(channels(inChannel(home)))) in message(cEntry) = writeReq and channels_p = channels WITH [(inChannel(home)) := removeCentry(channels(inChannel(home))), (home) := addCentry(channels(home), cEntry WITH [message := writeRet, t := t(procs(home)) + 1])] and procs_p = procs with [(home) := procs(home) WITH [ t := t(procs(home)) + 1, numRead := 0 ]] and (let newrec = (# t := t(procs(home)) + 1, r := 0, id := id(cEntry), op := WRITE, pc := pc(cEntry), v := v(cEntry), a := a(cEntry) #) in hist_p = (# size := size(hist) + 1, lst := lst(hist) with [(size(hist) + 1) := newrec] #)) and memhist_p = memhist WITH [(t(procs(home)) + 1) := (# pc := pc(cEntry), id := id(cEntry), mem := mem with [(a(cEntry)) := v(cEntry)] #)] and mem_p = mem WITH [(a(cEntry)) := v(cEntry)]), homeAnswerOther : not empty(channels(inChannel(home))) and (let cEntry = CE(channels(inChannel(home)))(head(channels(inChannel(home)))) in message(cEntry) /= writeReq and channels_p = channels WITH [(inChannel(home)) := removeCentry(channels(inChannel(home))), (home) := if message(cEntry) = readReq then addCentry(channels(home), cEntry WITH [message := readRet, v := mem(a(cEntry)), t := t(procs(home))] ) else channels(home) endif ]) and procs_p = procs and hist_p = hist and memhist_p = memhist and mem_p = mem, homeReadWrite : p_id = home and (let op = op(instlist(home, pc)) in channels_p = channels with [(home) := if op = WRITE then addCentry(channels(home), (# t := t(proc) + 1, message := writeRet, a := a, v := v, id := home, pc := pc#)) else channels(home) endif] and procs_p = procs with [(home) := proc WITH [pc := pc + 1, numRead := if op = WRITE then 0 else numRead(proc) + 1 endif, readValues := if op = READ then readValues(proc) with [(pc) := mem(a)] else readValues(proc) endif, t := if op = WRITE then t(proc) + 1 else t(proc) endif]] and let newrec = (# t := if op = WRITE then t(procs(home)) + 1 else t(procs(home)) endif, r := if op = WRITE then 0 else numRead(proc) + 1 endif, id := home, op := op, pc := pc, v := v, a := a #) in hist_p = if op = WRITE then (# size := size(hist) + 1, lst := lst(hist) with [(size(hist) + 1) := newrec] #) else insert(hist, newrec) endif and mem_p = if op = WRITE then mem with [(a) := v] else mem endif and memhist_p = if op = WRITE then memhist WITH [(t(procs(home)) + 1) := (# pc := pc, id := home, mem := mem with [(a) := v]#)] else memhist endif), idle : procs_p = procs and channels_p = channels and hist_p = hist and memhist_p = memhist and mem_p = mem, cacheInvalidate : p_id /= 0 and procs_p = procs WITH [(p_id) := proc WITH [cache := cache(proc) WITH [(a) := (# oc := false, v := v(cache(proc)(a)) #)]]] and channels_p = channels and hist_p = hist and memhist_p = memhist and mem_p = mem endcases ) END ring $$$ring.prf (|ring| (|home_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|inChannel_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|inChannel_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|next_TCC1| "" (EXPAND "nonempty?") (("" (EXPAND "empty?") (("" (SKOSIMP*) (("" (INST? -4) (("" (EXPAND "member") (("" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|insert_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|rho_TCC4| "" (SUBTYPE-TCC) NIL NIL)) $$$propDefs.pvs propDefs[U : posnat]: THEORY BEGIN IMPORTING ring[U] procs, procs_p : VAR [PROC_ID -> PROC_INFO] memhist, memhist_p : VAR MEM_HIST_TYPE mem, mem_p : VAR MEM_TYPE hist, hist_p : VAR HISTORY_TYPE time, time_p, t : VAR TIME proc, proc2 : VAR PROC_INFO proc_id, p_id, id, id2, id3 : VAR PROC_ID cPoint, cPoint2, cPoint3 : VAR posnat update : VAR bool action : VAR ACTION_TYPE channels, channels_p : VAR CHANNELS channel : VAR CHANNEL_TYPE cEntry : VAR CHANNEL_ENTRY_TYPE a, addr : VAR ADDRESS h, h1, new : VAR TIMESTAMP pc : VAR PC_RANGE hEntry : VAR HIST_RECORD_TYPE r, r2 : VAR nat index, index2 : VAR posnat % Constructs a timestamp. timestamp(t,r,id): TIMESTAMP = (# t:= t, r:= r, id := id #) % returns true iff there is an entry in the history table with timestamp h1 oc(hist, h1) : bool = (exists index : index <= size(hist) and timestamp(lst(hist)(index)) = h1) grantMessage(cEntry) : bool = message(cEntry) = readRet or message(cEntry) = writeRet requestMessage(cEntry) : bool = message(cEntry) = readReq or message(cEntry) = writeReq % True if the message cPoint of channel id preceeds cPoint2 of id2, meaning that % it will take shorter time to reach the home. preceed(channels, id, id2, cPoint, cPoint2) : bool = occEntry(channels(id), cPoint) and occEntry(channels(id2), cPoint2) and (id > id2 or id = id2 and cPoint < cPoint2) % a message preceeds, or is equal to, another message. weakPreceed(channels, id, id2, cPoint, cPoint2) : bool = occEntry(channels(id), cPoint) and (id = id2 and cPoint = cPoint2 or occEntry(channels(id2), cPoint2) and (id > id2 or id = id2 and cPoint < cPoint2)) memhistCorrect(hist, mem, memhist, procs) : bool = (let time = t(procs(home)) in mem(memhist(time)) = mem and (forall t: t < time implies mem(memhist(t+1)) = mem(memhist(t)) with [(a(instlist(id(memhist(t+1)), pc(memhist(t+1))))) := v(instlist(id(memhist(t+1)), pc(memhist(t+1))))] and exists index : index <= size(hist) and timestamp(lst(hist)(index)) = timestamp(t+1, 0, id(memhist(t+1))) and pc(lst(hist)(index)) = pc(memhist(t+1)))) and mem(memhist(0)) = initmem channelsMatchProg(channels, hist, memhist, procs) : bool = forall id, cPoint : (let channel = channels(id), cEntry = CE(channels(id))(cPoint) in occEntry(channel, cPoint) implies a(cEntry) = a(instlist(id(cEntry), pc(cEntry))) and if message(cEntry) = writeReq then v(cEntry) = v(instlist(id(cEntry), pc(cEntry))) and op(instlist(id(cEntry), pc(cEntry))) = WRITE and id >= id(cEntry) % and elsif message(cEntry) = writeRet then v(cEntry) = v(instlist(id(cEntry), pc(cEntry))) and op(instlist(id(cEntry), pc(cEntry))) = WRITE and v(cEntry) = mem(memhist(t(cEntry)))(a(cEntry)) and id(cEntry) = id(memhist(t(cEntry))) and pc(cEntry) = pc(memhist(t(cEntry))) and t(cEntry) <= t(procs(home)) and (exists index : index <= size(hist) and t(lst(hist)(index)) = t(cEntry) and id(lst(hist)(index)) = id(cEntry) and a(lst(hist)(index)) = a(cEntry) and r(lst(hist)(index)) = 0 and pc(lst(hist)(index)) = pc(cEntry)) and (id < id(cEntry) implies pc(cEntry) = pc(procs(id(cEntry)))) elsif message(cEntry) = readReq then op(instlist(id(cEntry), pc(cEntry)))= READ and id >= id(cEntry) % and else % message = readRet op(instlist(id(cEntry), pc(cEntry)))= READ and v(cEntry) = mem(memhist(t(cEntry)))(a(cEntry)) and t(cEntry) <= t(procs(home)) and (id < id(cEntry) implies pc(cEntry) = pc(procs(id(cEntry)))) endif ) cacheEqualMemhist(memhist, procs) : bool = (forall id: id /= home implies (let proc = procs(id) in (forall a : oc(cache(proc)(a)) implies v(cache(proc)(a)) = mem(memhist(t(proc)))(a)) )) channelsNonNeg(channels) : bool = (forall id: head(channels(id)) <= tail(channels(id))) cEntryExists(channels, procs): bool = forall t, id: t >= 1 and t <= t(procs(home)) implies (t > t(procs(id)) implies (exists id2, cPoint : id2 < id and occEntry(channels(id2), cPoint) and t(CE(channels(id2))(cPoint)) = t and message(CE(channels(id2))(cPoint)) = writeRet)) and (forall cPoint: occEntry(channels(id), cPoint) and grantMessage(CE(channels(id))(cPoint)) and t(CE(channels(id))(cPoint)) < t and t <= t(procs(id)) implies (exists cPoint2: weakPreceed(channels, id, id, cPoint, cPoint2) and t(CE(channels(id))(cPoint2)) = t and message(CE(channels(id))(cPoint2))= writeRet)) channelTimeInc(channels) : bool = (forall id, id2, cPoint, cPoint2: (let cEntry = CE(channels(id))(cPoint), cEntry2 = CE(channels(id2))(cPoint2) in preceed(channels, id, id2, cPoint, cPoint2) and grantMessage(cEntry) and grantMessage(cEntry2) implies t(cEntry2) >= t(cEntry) and (t(cEntry2) = t(cEntry) iff (message(cEntry2) = readRet and forall id3, cPoint3: (let cEntry3 = CE(channels(id3))(cPoint3) in preceed(channels, id, id3, cPoint, cPoint3) and preceed(channels, id3, id2, cPoint3, cPoint2) and grantMessage(cEntry3) implies t(cEntry3) = t(cEntry) and message(cEntry3) = readRet))))) localTimeInc(channels, procs):bool = (forall id, id2: id < id2 implies (let proc = procs(id), proc2 = procs(id2) in t(proc) >= t(proc2) and (t(proc) = t(proc2) iff (forall id3, cPoint: id3 >= id and id3 < id2 and occEntry(channels(id3), cPoint) implies not message(CE(channels(id3))(cPoint)) = writeRet)))) localTimeEarlier(channels, procs):bool = (forall id: id /= home implies (let proc = procs(id) in t(procs(home)) >= t(proc) and (t(procs(home)) = t(proc) iff (forall id2, cPoint: id2 < id and occEntry(channels(id2), cPoint) implies not message(CE(channels(id2))(cPoint)) = writeRet)))) timeChannelProc(channels, procs):bool = (forall id: (forall id2, cPoint : let cEntry = CE(channels(id2))(cPoint) in occEntry(channels(id2), cPoint) and grantMessage(cEntry) implies if id2 < id then t(cEntry) > t(procs(id)) or message(cEntry) = readRet and t(cEntry) = t(procs(id)) else t(cEntry) <= t(procs(id)) endif)) homeNotReq(channels): bool = (forall id, cPoint: let cEntry = CE(channels(id))(cPoint) in occEntry(channels(id), cPoint) and requestMessage(cEntry) implies cEntry`id /= home and id /= home) idPCunique(channels):bool= (forall id, id2, cPoint, cPoint2: let cEntry = CE(channels(id))(cPoint), cEntry2 = CE(channels(id2))(cPoint2) in cEntry`pc = cEntry2`pc and cEntry`id = cEntry2`id and weakPreceed(channels, id, id2, cPoint, cPoint2) implies id = id2 and cPoint = cPoint2 or preceed(channels, id, id2, cPoint, cPoint2) and grantMessage(cEntry) and id>=cEntry`id) % Problem - need to show cannot be two messages with same id, pc waiting(channels, procs) : bool = (forall id, cPoint : (let channel = channels(id), cEntry = CE(channels(id))(cPoint) in occEntry(channel, cPoint) and (requestMessage(cEntry) or grantMessage(cEntry) and cEntry`id > id) implies pc(cEntry) = pc(procs(cEntry`id)) and waiting(procs(cEntry`id)))) waitingProc(channels, procs): bool = forall id: waiting(procs(id)) implies id /= home and exists id2, cPoint : (let cEntry = CE(channels(id2))(cPoint) in occEntry(channels(id2), cPoint) and id(cEntry) = id and pc(cEntry) = pc(procs(id(cEntry))) and if message(cEntry) = readReq or message(cEntry) = readRet then op(instlist(id(cEntry), pc(cEntry))) = READ else op(instlist(id(cEntry), pc(cEntry))) = WRITE and v(cEntry) = v(instlist(id(cEntry), pc(cEntry))) endif and if id2 < id then grantMessage(cEntry) else requestMessage(cEntry) endif ) histLt(hist) : bool = forall index, index2 : index < index2 and index2 <= size(hist) implies timestamp(lst(hist)(index)) /= timestamp(lst(hist)(index2)) and lt(timestamp(lst(hist)(index)), timestamp(lst(hist)(index2))) histComplete(hist, procs): bool = (forall index: index <= size(hist) implies (let h = timestamp(lst(hist)(index)) in if r(h) = 0 then forall index2: index2 <= size(hist) and r(lst(hist)(index2)) = 0 and t(lst(hist)(index2)) = t(h) implies index2 = index else (forall r2 : r2 < r(h) and r2 > 0 implies oc(hist, h with [r := r2])) endif)) and (forall id : (forall r2 : r2 < numRead(procs(id)) implies oc(hist, timestamp(t(procs(id)), r2 + 1, id))) and (t(procs(id)) > 0 and numRead(procs(id)) > 0 implies (exists id2 : oc(hist, timestamp(t(procs(id)), 0, id2))))) histMatchPC(channels, hist, procs) : bool = (forall index: index <= size(hist) implies (let hrec = lst(hist)(index) in pc(hrec) <= pc(procs(id(hrec))) and (pc(hrec) = pc(procs(id(hrec))) implies op(instlist(hrec`id, pc(hrec))) = WRITE and (exists id, cPoint : occEntry(channels(id), cPoint) and id < hrec`id and (let cEntry = CE(channels(id))(cPoint) in t(cEntry) = t(hrec) and pc(cEntry) = pc(hrec) and id(cEntry) = id(hrec) and message(cEntry) = writeRet))) and (forall index2 : (let hrec2 = lst(hist)(index2) in index2 <= size(hist) and hrec2`id = hrec`id implies (pc(hrec2) < pc(hrec)iff index2 < index))) and (forall pc: pc < pc(hrec) implies (exists index2 : (let hrec2 = lst(hist)(index2) in index2 < index and hrec2`id = hrec`id and hrec2`pc = pc ))))) and (forall id, pc: pc < pc(procs(id)) implies (exists index : index <= size(hist) and pc(lst(hist)(index)) = pc and (lst(hist)(index))`id = id)) histMatchTime(channels, hist, procs) : bool = (forall index: index <= size(hist) implies (let hrec = lst(hist)(index) in t(hrec) <= t(procs(home)) and if t(hrec) > t(procs(hrec`id)) then r(hrec) = 0 and (exists id, cPoint : occEntry(channels(id), cPoint) and id < hrec`id and (let cEntry = CE(channels(id))(cPoint) in t(cEntry) = t(hrec) and pc(cEntry) = pc(hrec) and id(cEntry) = id(hrec) and message(cEntry) = writeRet)) else t(hrec) = t(procs(hrec`id)) implies r(hrec) <= numRead(procs(hrec`id)) endif)) and (forall t: t <= t(procs(home)) and t >= 1 implies (exists index : index <= size(hist) and t(lst(hist)(index)) = t and r(lst(hist)(index)) = 0)) histJ0write(hist): bool = (forall index: index <= size(hist) implies (op(instlist(lst(hist)(index)`id, pc(lst(hist)(index)))) = WRITE iff r(lst(hist)(index)) = 0)) readValuesCorrect(hist, memhist, procs): bool = (forall id: (let proc = procs(id) in (forall pc: if pc < pc(proc) and op(instlist(id, pc)) = READ then (exists index : index <= size(hist) and pc(lst(hist)(index)) = pc and (lst(hist)(index))`id = id and readValues(proc)(pc) = mem(memhist(t(lst(hist)(index))))(a(instlist(id, pc)))) else readValues(proc)(pc) = 0 endif ))) firstExists(hist) : bool = size(hist) > 0 implies (t(lst(hist)(1)) = 0 and r(lst(hist)(1)) = 1 or t(lst(hist)(1)) = 1 and r(lst(hist)(1)) = 0) % A conjuction of all the above properties reachable(channels, hist, mem, memhist, procs): bool = memhistCorrect(hist, mem, memhist, procs) and channelsMatchProg(channels, hist, memhist, procs) and cacheEqualMemhist(memhist, procs) and channelsNonNeg(channels) and cEntryExists(channels, procs) and channelTimeInc(channels) and localTimeEarlier(channels, procs) and timeChannelProc(channels, procs) and idPCunique(channels)and homeNotReq(channels) and waiting(channels, procs) and histLt(hist) and histComplete(hist, procs) and histMatchPC(channels, hist, procs) and histMatchTime(channels, hist, procs) and histJ0write(hist) and readValuesCorrect(hist, memhist, procs) and firstExists(hist) END propDefs $$$propInvs.pvs propInvs[U: posnat]: THEORY BEGIN IMPORTING propDefs[U] procs, procs_p: VAR [PROC_ID -> PROC_INFO] memhist, memhist_p: VAR MEM_HIST_TYPE mem, mem_p: VAR MEM_TYPE hist, hist_p: VAR HISTORY_TYPE time, time_p, t: VAR TIME p_id: VAR PROC_ID update: VAR bool action: VAR ACTION_TYPE channels, channels_p: VAR CHANNELS h, h1, h2, h3: VAR TIMESTAMP index, index2: VAR posnat % lt defines a strict ordering. ltIsStrict : lemma (forall h1, h2: % linear (lt(h1, h2) or lt(h2, h1) or h1 = h2) and % anti-symmetric not (lt(h1, h2) and lt(h2, h1)) and % irreflexive not lt(h1, h1)) and (forall h1, h2, h3: % transitive lt(h1, h2) and lt(h2, h3) implies lt(h1, h3)) % The function next(hist, h) returns a value in the range 1..1 + size(hist) nextSize: LEMMA FORALL hist, h: next(hist, h) = 1 + size(hist) OR next(hist, h) <= size(hist) AND lt(h, timestamp(lst(hist)(next(hist, h)))) AND (FORALL index2: index2 <= size(hist) AND lt(h, timestamp(lst(hist)(index2))) IMPLIES next(hist, h) <= index2) nextExists: LEMMA FORALL h: IF (EXISTS (index: posnat): index <= size(hist) AND lt(h, timestamp(lst(hist)(index)))) THEN next(hist, h) <= size(hist) AND (FORALL (index2: posnat): index2 <= size(hist) AND lt(h, timestamp(lst(hist)(index2))) IMPLIES next(hist, h) <= index2) ELSE next(hist, h) = 1 + size(hist) ENDIF thetaReachable: LEMMA theta(channels, hist, mem, memhist, procs) IMPLIES reachable(channels, hist, mem, memhist, procs) memhistCorrect: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES memhistCorrect(hist_p, mem_p, memhist_p, procs_p) localTimeEarlier: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES localTimeEarlier(channels_p, procs_p) channelsMatchProg: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES channelsMatchProg(channels_p, hist_p, memhist_p, procs_p) cacheEqualMemhist: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES cacheEqualMemhist(memhist_p, procs_p) channelsNonNeg: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES channelsNonNeg(channels_p) cEntryExists: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES cEntryExists(channels_p, procs_p) channelTimeInc: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES channelTimeInc(channels_p) timeChannelProc: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES timeChannelProc(channels_p, procs_p) idPCunique: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES idPCunique(channels_p) homeNotReq: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES homeNotReq(channels_p) waiting: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES waiting(channels_p, procs_p) histLt: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES histLt(hist_p) histComplete: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES histComplete(hist_p, procs_p) histMatchPC: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES histMatchPC(channels_p, hist_p, procs_p) histMatchTime: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES histMatchTime(channels_p, hist_p, procs_p) histJ0write: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES histJ0write(hist_p) readValuesCorrect: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES readValuesCorrect(hist_p, memhist_p, procs_p) firstExists: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES firstExists(hist_p) reachable: LEMMA rho(channels, hist, mem, memhist, procs, channels_p, hist_p, mem_p, memhist_p, procs_p, p_id, action) AND reachable(channels, hist, mem, memhist, procs) IMPLIES reachable(channels_p, hist_p, mem_p, memhist_p, procs_p) END propInvs $$$propInvs.prf (|propInvs| (|ltIsStrict| "" (GRIND) (("" (APPLY-EXTENSIONALITY 7 :HIDE? T) NIL NIL)) NIL) (|nextSize| "" (SKOSIMP*) (("" (CASE "not (exists (next : posnat) : next(hist!1, h!1) = next)") (("1" (INST + "next(hist!1, h!1)") NIL NIL) ("2" (SKOSIMP*) (("2" (REPLACE*) (("2" (EXPAND "next") (("2" (NEW-SPLIT-IF -) (("2" (EXPAND "choose") (("2" (USE "epsilon_ax[posnat]") (("2" (SPSI -) (("2" (SKOSIMP*) (("2" (INST - "index2!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nextExists| "" (SKOSIMP*) (("" (NEW-SPLIT-IF) (("1" (EXPAND "next") (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (CASE "exists (myset : setof[posnat]): myset = {(index : posnat)| index <= size(hist!1) AND lt(h!1, timestamp(lst(hist!1)(index))) }") (("1" (SKOSIMP*) (("1" (CASE "exists (small : posnat) : member(small, myset!1) and forall (ind : posnat) : member (ind, myset!1) implies small <= ind") (("1" (SKOSIMP*) (("1" (INST + "small!1") (("1" (SIMP) (("1" (EXPAND "member") (("1" (REPLACE*) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "not member(index!1, myset!1)") (("1" (EXPAND "member") (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (CASE "forall (upper : posnat): (forall (ind : posnat): member(ind, myset!1) and ind <= upper implies EXISTS (small: posnat): member(small, myset!1) AND (FORALL (ind: posnat): member(ind, myset!1) IMPLIES small <= ind))") (("1" (INST - "index!1") (("1" (INST - "index!1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (INDUCT "upper") (("1" (SIMP) NIL NIL) ("2" (SIMP) NIL NIL) ("3" (SKOSIMP*) (("3" (SIMP) (("3" (CASE "j!1 = 0") (("1" (INST + 1) (("1" (SIMP) NIL NIL)) NIL) ("2" (SIMP) (("2" (INST + "ind!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST -1 "ind!2") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "({index: posnat | index <= size(hist!1) AND lt(h!1, timestamp(lst(hist!1)(index)))})") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "next") (("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST? +) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|thetaReachable| "" (EXPAND "theta") (("" (EXPAND "reachable") (("" (SKOSIMP*) (("" (SPLIT +) (("1" (LAZYGRIND) NIL NIL) ("2" (LAZYGRIND) NIL NIL) ("3" (LAZYGRIND) NIL NIL) ("4" (LAZYGRIND) NIL NIL) ("5" (EXPAND "cEntryExists") (("5" (SKOSIMP*) (("5" (SPSI) (("1" (INST? -) (("1" (SIMP) (("1" (REVEAL -1) (("1" (INST -1 "home") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (EXPAND "occEntry") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (LAZYGRIND) NIL NIL) ("7" (EXPAND "localTimeEarlier") (("7" (SKOSIMP*) (("7" (INST? -) (("7" (REVEAL -1) (("7" (INST -1 "id!1") (("7" (SIMP) (("7" (SKOSIMP*) (("7" (REVEAL -1) (("7" (INST -1 "id2!1") (("7" (EXPAND "occEntry") (("7" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (LAZYGRIND) NIL NIL) ("9" (LAZYGRIND) NIL NIL) ("10" (LAZYGRIND) NIL NIL) ("11" (LAZYGRIND) NIL NIL) ("12" (LAZYGRIND) NIL NIL) ("13" (LAZYGRIND) NIL NIL) ("14" (LAZYGRIND) NIL NIL) ("15" (LAZYGRIND) NIL NIL) ("16" (LAZYGRIND) NIL NIL) ("17" (LAZYGRIND) NIL NIL) ("18" (LAZYGRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|memhistCorrect| "" (EXP-RHO) (("" (REVEAL "memhistCorrect") (("" (REVEAL "memhistCorrectInit") (("" (SPSI) (("1" (SPLIT-RHO-ALL) NIL NIL) ("2" (SKOSIMP*) (("2" (INST "memhistCorrect" "t!1") (("2" (SIMP) (("2" (SPSI) (("1" (SPLIT-RHO-ALL) (("1" (REVEAL "channelsMatchProg") (("1" (INST?) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE " t!1 < t(procs!1(0)) ") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SPLIT-RHO-ALL) (("1" (REVEAL 1) (("1" (INST + "1 + size(hist!1)") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL) ("2" (REVEAL 1) (("2" (INST + "1 + size(hist!1)") (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|localTimeEarlier| "" (EXP-RHO) (("" (REVEAL "localTimeEarlier") (("" (INST -1 "id!1") (("" (CASE "not t(procs_p!1(home)) >= t(procs_p!1(id!1)) ") (("1" (SIMP) (("1" (SPLIT-RHO-ALL) (("1" (INST?) (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "inChannel") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (THEN (SPSI) (SKOSIMP*) (NEW-SPLIT-IF "toProve")))) (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL) ("2" (INST?) (("2" (NEW-SPLIT-IF -) (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST?) (("3" (INST - "cPoint!1") (("3" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST?) (("4" (INST - "cPoint!1") (("4" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("5" (INST?) (("5" (SIMP) NIL NIL)) NIL) ("6" (INST?) (("6" (NEW-SPLIT-IF -) (("6" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("7" (SKOSIMP*) (("7" (INST - "id2!1" "cPoint!1") (("7" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("8" (SKOSIMP*) (("8" (INST - "id2!1" "cPoint!1") (("8" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("9" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (REVEAL "channelTimeInc") (("1" (INST -1 "inChannel(id!1)" "id2!1" "head(channels!1(inChannel(id!1)))" "cPoint!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (REVEAL "channelsNonNeg") (("1" (INST -1 "inChannel(id!1)") (("1" (APPLY (THEN (CASE " t(CE(channels!1(id2!1))(cPoint!1)) = t (CE(channels!1(inChannel(id!1))) (head(channels!1(inChannel(id!1)))))") (SIMP))) (("1" (NEW-SPLIT-IF -) (("1" (EXPAND "inChannel") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REVEAL "timeChannelProc") (("2" (INST-CP -1 "id!1") (("2" (INST -2 "inChannel(id!1)" "head(channels!1(inChannel(id!1)))") (("2" (INST -1 "0") (("2" (INST -1 "id2!1" "cPoint!1") (("2" (SIMP) (("2" (NEW-SPLIT-IF -) (("1" (EXPAND "inChannel") (("1" (CLEAN-UP) (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("2" (EXPAND "inChannel") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("10" (INST - "id2!1" "cPoint!1") (("10" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "localTimeEarlier") (("1" (INST - "inChannel(id2!1)" "head(channels!1(inChannel(id2!1)))") (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "inChannel") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("11" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST - "id2!1" "cPoint!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "cEntryExists") (("1" (INST -1 "2 + t(procs!1(id!1))" "id!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "toProve") (("1" (INST -1 "id2!2" "cPoint!2") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "cEntryExists") (("1" (INST -1 "1 + t(procs!1(id!1))" "id!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "toProve") (("1" (INST -1 "id2!3" "cPoint!3") (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "id2!1" "cPoint!1") (("2" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("12" (SKOSIMP*) (("12" (INST-CP -1 "id2!1" "cPoint!1") (("12" (NEW-SPLIT-IF -) (("12" (NEW-SPLIT-IF -) (("12" (INST - "p_id!1" "tail(channels!1(p_id!1))") (("12" (REVEAL "channelsNonNeg") (("12" (INST -1 "p_id!1") (("12" (SIMP) (("12" (EXPAND "inChannel") (("12" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("13" (INST -1 "0" "tail(channels!1(0))") (("13" (NEW-SPLIT-IF -) (("13" (REVEAL "channelsNonNeg") (("13" (INST?) (("13" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("14" (REVEAL "channelsNonNeg") (("14" (INST -1 "id2!1") (("14" (NEW-SPLIT-IF -) (("1" (NEW-SPLIT-IF -) (("1" (INST - "id2!1" "cPoint!1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (INST - "id2!1" "cPoint!1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("15" (INST - "id2!1" "cPoint!1") (("15" (NEW-SPLIT-IF -) NIL NIL)) NIL) ("16" (INST - "id2!1" "cPoint!1") (("16" (NEW-SPLIT-IF -) NIL NIL)) NIL) ("17" (INST - "id2!1" "cPoint!1") (("17" (NEW-SPLIT-IF -) (("17" (NEW-SPLIT-IF -) (("17" (EXPAND "inChannel") (("17" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("18" (INST - "id2!1" "cPoint!1") (("18" (NEW-SPLIT-IF -) NIL NIL)) NIL) ("19" (INST - "0" "tail(channels!1(0))") (("19" (SIMP) (("19" (REVEAL "channelsNonNeg") (("19" (INST?) (("19" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("20" (SKOSIMP*) (("20" (INST?) (("20" (INST - "cPoint!1") (("20" (SIMP) (("20" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|channelsMatchProg| "" (EXP-RHO) (("" (REVEAL "channelsMatchProg") (("" (INST -1 "id!1" "cPoint!1") (("" (INTRONEXT) (("1" (CASE " cPoint!1 < tail(channels!1(id!1)) AND cPoint!1 >= head(channels!1(id!1))") (("1" (SIMP) (("1" (CASE "not a(CE(channels_p!1(id!1))(cPoint!1)) = a (instlist(id(CE(channels_p!1(id!1))(cPoint!1)), pc(CE(channels_p!1(id!1))(cPoint!1))))") (("1" (RERUN ("1" (JUST-INSTALL-PROOF ("1" (HIDE "toProve") (SPLIT-RHO-ALL))))) NIL NIL) ("2" (SIMP) (("2" (SPLIT-RHO) (("1" (RERUN ("1" (JUST-INSTALL-PROOF ("1" (REPLACE*) (SIMP) (SPSI) (SPSI) (("1" (SKOSIMP*) (SIMP) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SPSI) (SIMP) (NEW-SPLIT-IF) (REPLACE -1 :DIR RL) (HIDE "next" "nextSize") (REVEAL "waiting") (INST?) (SIMP))))))) NIL NIL) ("2" (RERUN ("2" (JUST-INSTALL-PROOF ("2" (HIDE "next" "nextSize") (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (LIFT-IF) (SPSI) (("1" (SIMP) (SPSI) (SKOSIMP*) (INST + "index!1") (SIMP)) ("2" (SIMP) (SPSI)))) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (NEW-SPLIT-IF))))))))))))) NIL NIL) ("3" (RERUN ("3" (JUST-INSTALL-PROOF ("3" (HIDE "next" "nextSize") (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (NEW-SPLIT-IF)))) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (NEW-SPLIT-IF))))))))))))) NIL NIL) ("4" (RERUN ("4" (JUST-INSTALL-PROOF ("4" (HIDE "next" "nextSize") (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (SPSI) (("1" (SIMP) (HIDE "rho") (SPSI) (("1" (SKOSIMP*) (INST?) (SIMP)) ("2" (NEW-SPLIT-IF) (NEW-SPLIT-IF) (NEW-SPLIT-IF) (REPLACE -2 :DIR RL) (REVEAL "channelsMatchProg") (INST?) (SIMP) (EXPAND "inChannel") (NEW-SPLIT-IF -) (REPLACE -13 :DIR RL) (REPLACE -8 :DIR RL) (REPLACE -26 :DIR RL) (REPLACE -2 :DIR RL) (APPLY (THEN (CASE "id(CE(channels!1(id!1))(head(channels!1(id!1)))) = id!1 + 1") (SIMP) (REPLACE -1))) (REPLACE -14 :DIR RL) (SIMP) (APPLY (THEN (CASE "p_id!1 = id!1 + 1") (SIMP))) (REPLACE -1) (SIMP) (REVEAL "idPCunique") (INST - "id!1" "id!1" "head(channels!1(id!1))" "cPoint!1") (SIMP) (EXPAND "weakPreceed") (EXPAND "occEntry") (PROPAX)))) ("2" (SIMP) (SPSI) (EXPAND "inChannel") (HIDE "rho") (NEW-SPLIT-IF) (NEW-SPLIT-IF) (NEW-SPLIT-IF) (REPLACE -12 :DIR RL) (REPLACE -3 :DIR RL) (REVEAL "idPCunique") (INST - "p_id!1 - 1" "id!1" "head(channels!1(p_id!1 - 1))" "cPoint!1") (SIMP) (EXPAND "weakPreceed") (EXPAND "occEntry") (REVEAL "channelsNonNeg") (INST?) (REVEAL "channelsMatchProg") (INST?) (SIMP) (REVEAL "rho") (SIMP)))))) ("2" (SPSI) (("1" (REPLACE*) (SIMP) (SPLIT-ALL)) ("2" (REPLACE*) (SIMP) (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (NEW-SPLIT-IF) (("1" (SPSI) (SPSI) (EXPAND "inChannel") (NEW-SPLIT-IF) (APPLY (THEN (CASE "p_id!1 = id!1 + 1") (SIMP))) (REPLACE -1) (REVEAL "channelsNonNeg") (INST?) (REVEAL "idPCunique") (INST - "id!1" "id!1" "head(channels!1(id!1))" "cPoint!1") (SIMP) (EXPAND "weakPreceed") (EXPAND "occEntry") (REVEAL "channelsMatchProg") (INST?) (SIMP)) ("2" (EXPAND "inChannel") (REVEAL "channelsNonNeg") (INST - "p_id!1 - 1") (HIDE "rho") (SPSI) (("1" (NEW-SPLIT-IF) (SPSI) (SPSI) (REPLACE -4 :DIR RL) (REVEAL "idPCunique") (INST - "p_id!1 - 1" "id!1" "head(channels!1(p_id!1 - 1))" "cPoint!1") (SIMP) (EXPAND "weakPreceed") (EXPAND "occEntry") (REVEAL "channelsMatchProg") (INST?) (REVEAL "rho") (SIMP)) ("2" (NEW-SPLIT-IF) (SPSI) (NEW-SPLIT-IF) (REPLACE -3 :DIR RL) (REVEAL "idPCunique") (INST - "p_id!1 - 1" "id!1" "head(channels!1(p_id!1 - 1))" "cPoint!1") (EXPAND "weakPreceed") (EXPAND "occEntry") (REVEAL "channelsMatchProg" "rho") (INST?) (SIMP))))))))))))))))) NIL NIL) ("5" (RERUN ("5" (JUST-INSTALL-PROOF ("5" (EXPAND "inChannel") (SPSI) (("1" (REPLACE*) (HIDE "rho") (SPLIT-ALL)) ("2" (SPSI) (("1" (REPLACE*) (HIDE "rho") (NEW-SPLIT-IF) (("1" (SPSI) (SKOSIMP*) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SPSI) (("1" (SKOSIMP*) (SIMP) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SIMP) (SKOSIMP*) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)))))) ("2" (SPSI) (("1" (REPLACE*) (HIDE "rho") (SPLIT-ALL)) ("2" (HIDE "next" "nextSize") (REPLACE*) (SIMP) (HIDE "rho") (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF)) ("2" (NEW-SPLIT-IF) (NEW-SPLIT-IF))))))))))))) NIL NIL) ("6" (RERUN ("6" (JUST-INSTALL-PROOF ("6" (HIDE "next" "nextSize") (REPLACE*) (CASE "id!1 = 0") (("1" (EXPAND "inChannel") (SIMP) (SPLIT-ALL)) ("2" (CASE "inChannel(0) = id!1") (("1" (EXPAND "inChannel") (SIMP) (SPLIT-ALL)) ("2" (EXPAND "inChannel") (SPLIT-ALL))))))))) NIL NIL) ("7" (RERUN ("7" (JUST-INSTALL-PROOF ("7" (LIFT-IF -) (SPSI -) (("1" (REPLACE*) (HIDE "rho") (SIMP) (LIFT-IF) (REVEAL "homeNotReq") (INST - "id!1" "cPoint!1") (SPSI) (("1" (SPSI) (SPSI) (("1" (SIMP) (SKOSIMP*) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SIMP) (NEW-SPLIT-IF)))) ("2" (HIDE "next" "nextSize") (SPSI) (SPSI) (("1" (SIMP) (SKOSIMP*) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SPLIT-ALL)))))) ("2" (REPLACE*) (HIDE "rho") (SPSI) (("1" (SPLIT-ALL)) ("2" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)) ("2" (SKOSIMP*) (SPSI) (INST-CP + "index!1 + 1") (INST + "index!1") (SPLIT-ALL)))) ("2" (SPSI) (("1" (SPLIT-ALL)) ("2" (NEW-SPLIT-IF) (("1" (SPLIT-ALL)) ("2" (SPLIT-ALL))))))))))))))) NIL NIL) ("8" (REPLACE*) NIL NIL) ("9" (REPLACE*) (("9" (SPSI) (("9" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SPSI) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "toProve") (("2" (REVEAL "channelsMatchProg") (("2" (INST -1 "inChannel(id!1)" "head(channels!1(inChannel(id!1)))") (("2" (HIDE -4) (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (LIFT-IF "orig") (THEN (SPSI "orig") (REVEAL "toProve")))) (("1" (RERUN ("1" (JUST-INSTALL-PROOF ("1" (REPLACE*) (SIMP))))) NIL NIL) ("2" (RERUN ("2" (JUST-INSTALL-PROOF ("2" (REPLACE*) (SIMP))))) NIL NIL) ("3" (RERUN ("3" (JUST-INSTALL-PROOF ("3" (REPLACE*) (SIMP) (EXPAND "inChannel") (SPSI) (("1" (NEW-SPLIT-IF)) ("2" (SPSI) (("1" (SIMP) (SKOSIMP*) (SPSI) (INST? +) (SIMP)) ("2" (SPLIT-ALL))))))))) NIL NIL) ("4" (RERUN ("4" (JUST-INSTALL-PROOF ("4" (SPSI -))))) NIL NIL) ("5" (RERUN ("5" (JUST-INSTALL-PROOF ("5" (NEW-SPLIT-IF) (HIDE "rho") (SPSI) (("1" (INST + "1 + size(hist!1)") (SPLIT-ALL)) ("2" (EXPAND "inChannel") (REVEAL "rho") (EXPAND "inChannel") (SIMP) (LABEL "msg" -2) (HIDE "rho" "next" "nextSize") (REVEAL "waiting") (INST?) (SIMP))))))) NIL NIL) ("6" (RERUN ("6" (JUST-INSTALL-PROOF ("6" (SPSI -))))) NIL NIL) ("7" (RERUN ("7" (JUST-INSTALL-PROOF ("7" (SPSI -) (REPLACE*) (SIMP) (REVEAL "waiting") (INST?) (SIMP))))) NIL NIL) ("8" (RERUN ("8" (JUST-INSTALL-PROOF ("8" (SPSI -))))) NIL NIL) ("9" (NEW-SPLIT-IF -) (("9" (INST + "1 + size(hist!1)") (("9" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (RERUN ("2" (JUST-INSTALL-PROOF ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))"))))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cacheEqualMemhist| "" (EXP-RHO) (("" (REVEAL "cacheEqualMemhist") (("" (INST -1 "id!1") (("" (SIMP) (("" (INST -1 "a!1") (("" (SPLIT-RHO) (("1" (REPLACE*) (("1" (SIMP) (("1" (SPLIT-ALL) NIL))))) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPLIT-ALL) NIL))))) ("3" (REPLACE*) (("3" (SIMP) (("3" (SPLIT-ALL) NIL))))) ("4" (REPLACE*) (("4" (SIMP) (("4" (NEW-SPLIT-IF) (("4" (REVEAL "localTimeEarlier") (("4" (INST?) (("4" (CASE "t(procs!1(home)) = t(procs!1(id!1))") (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (EXPAND "inChannel") (("1" (EXPAND "home") (("1" (SPSI) (("1" (INST?) (("1" (SIMP) NIL))) ("2" (NEW-SPLIT-IF) (("2" (REPLACE -1 :DIR RL) (("2" (REVEAL "channelsMatchProg") (("2" (INST?) (("2" (SIMP) (("2" (REPLACE -5 :DIR RL) (("2" (REVEAL "timeChannelProc") (("2" (INST -1 "id!1") (("2" (INST?) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))) ("2" (SIMP) (("2" (EXPAND "home") (("2" (EXPAND "inChannel") (("2" (SIMP) (("2" (REVEAL "memhistCorrect") (("2" (INST - "t(procs!1(id!1))") (("2" (REVEAL "timeChannelProc") (("2" (INST -1 "id!1") (("2" (INST -1 "id!1 - 1" "channels!1(id!1 - 1)`head") (("2" (REVEAL "channelsNonNeg") (("2" (INST -1 "id!1 -1") (("2" (REVEAL "channelsMatchProg") (("2" (INST -1 "id!1 - 1" " channels!1(id!1 - 1)`head") (("2" (SPSI) (("1" (CASE " t(CE(channels!1(id!1 - 1))(channels!1(id!1 - 1)`head)) = t(procs!1(id!1)) + 1") (("1" (NEW-SPLIT-IF) NIL) ("2" (HIDE "rho") (("2" (REVEAL "cEntryExists") (("2" (INST -1 "t(procs!1(id!1)) + 1" "id!1") (("2" (SKOSIMP*) (("2" (REVEAL "channelTimeInc") (("2" (EXPAND "preceed") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST - "id!1 - 1" "id2!2" "head(channels!1(id!1 - 1))" "cPoint!2") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SIMP) NIL))))))))))))))))))))))))) ("2" (NEW-SPLIT-IF) (("2" (REVEAL "cEntryExists") (("2" (INST -1 "t(procs!1(id!1)) + 1" "id!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "channelTimeInc") (("2" (EXPAND "preceed") (("2" (INST -1 "id!1 - 1" "id2!1" "channels!1(id!1 - 1)`head" "cPoint!1") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SPSI -) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("5" (REPLACE*) (("5" (NEW-SPLIT-IF) (("5" (NEW-SPLIT-IF) (("5" (REVEAL "localTimeEarlier") (("5" (INST -1 "id!1") (("5" (SIMP) NIL))))))))))) ("6" (REPLACE*) (("6" (NEW-SPLIT-IF) (("6" (NEW-SPLIT-IF) (("6" (REVEAL "localTimeEarlier") (("6" (INST -1 "id!1") (("6" (SIMP) (("6" (SPSI) NIL))))))))))))) ("7" (REPLACE*) (("7" (SIMP) (("7" (SPLIT-ALL) NIL))))))))))))))))) (|channelsNonNeg| "" (EXP-RHO) (("" (REVEAL "channelsNonNeg") (("" (INST -1 "id!1") (("" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL) (|cEntryExists| "" (EXP-RHO) (("" (REVEAL "cEntryExists") (("" (INST -1 "t!1" "id!1") (("" (SIMP) (("" (SPSI) (("1" (CASE "t!1 <= t(procs!1(0)) AND t!1 > t(procs!1(id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id2!1" "cPoint!1") (("1" (SIMP) (("1" (SPLIT-RHO-ALL) (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "cEntryExists") (("1" (INST -1 " 1 + t(procs!1(id!1))" "id!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "channelTimeInc") (("1" (INST -1 "id2!1" "id2!2" "cPoint!1" "cPoint!2") (("1" (EXPAND "preceed") (("1" (SIMP) (("1" (EXPAND "occEntry") (("1" (EXPAND "inChannel") (("1" (SIMP) NIL))))))))))))))))))))) ("2" (REVEAL "toProve") (("2" (INST 1 "p_id!1" "tail(channels!1(p_id!1))") (("2" (SIMP) (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (REVEAL "rho") (("2" (REPLACE*) (("2" (NEW-SPLIT-IF) (("2" (HIDE "rho") (("2" (EXPAND "inChannel") (("2" (SIMP) NIL))))))))))))))))))))))))) ("2" (EXPAND "inChannel") (("2" (SIMP) NIL))))))))))))) ("2" (HIDE "cEntryExists") (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (NEW-SPLIT-IF "orig"))) (("1" (INST + "0" "tail(channels!1(0))") (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST? :WHERE "toProve") (("1" (SIMP) NIL))))))))) ("2" (INST "toProve" "0" "tail(channels!1(0))") (("2" (SIMP) (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (SIMP) NIL))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "weakPreceed") (("2" (EXPAND "occEntry") (("2" (CASE " t!1 <= t(procs!1(0)) and (cPoint!1 < tail(channels!1(id!1)) AND cPoint!1 >= head(channels!1(id!1))) AND (message(CE(channels!1(id!1))(cPoint!1)) = readRet OR message(CE(channels!1(id!1))(cPoint!1)) = writeRet) AND t(CE(channels!1(id!1))(cPoint!1)) < t!1 AND t!1 <= t(procs!1(id!1))") (("1" (SIMP) (("1" (INST - "cPoint!1") (("1" (SIMP) (("1" (SPSI "cEntryExists") (("1" (SKOSIMP*) (("1" (INST + "cPoint2!1") (("1" (SPLIT-RHO-ALL) NIL))))))))))))) ("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (NEW-SPLIT-IF "orig"))) (("1" (SPLIT-ALL -) NIL) ("2" (SPLIT-ALL -) NIL) ("3" (EXPAND "inChannel") (("3" (HIDE "rho") (("3" (SPSI -) (("1" (NEW-SPLIT-IF -) (("1" (CLEAN-UP) (("1" (HIDE 1) (("1" (REVEAL "timeChannelProc") (("1" (INST - "id!1") (("1" (INST?) (("1" (SIMP) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (REVEAL "rho") (("1" (SIMP) (("1" (HIDE "rho") (("1" (SPSI -) NIL))))))))))))))))))))))))) ("2" (SPSI) (("2" (REDUCE-ALL) (("2" (INST + "tail(channels!1(id!1))") (("2" (SIMP) (("2" (REVEAL "channelTimeInc") (("2" (EXPAND "preceed") (("2" (INST - "id!1 - 1" "id2!1" "head(channels!1(id!1 - 1))" "cPoint!2") (("2" (EXPAND "occEntry") (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (REVEAL "rho") (("2" (SIMP) (("2" (HIDE "rho") (("2" (SPSI -) (("2" (REPLACE*) (("2" (REVEAL "timeChannelProc") (("2" (INST -1 "id!1") (("2" (INST - "id!1 - 1" "(head(channels!1(id!1 - 1)))") (("2" (SIMP) NIL))))))))))))))))))))))))))))))))))))))) ("2" (SPSI -) (("2" (CLEAN-UP) (("2" (INST? +) (("2" (SIMP) NIL))))))))))))) ("4" (EXPAND "inChannel") (("4" (HIDE "rho") (("4" (SPSI -) (("1" (INST + "tail(channels!1(0))") (("1" (SIMP) (("1" (NEW-SPLIT-IF -) NIL))))) ("2" (REVEAL "localTimeEarlier") (("2" (INST -1 "id!1") (("2" (NEW-SPLIT-IF) NIL))))))))))) ("5" (HIDE "rho") (("5" (EXPAND "inChannel") (("5" (SPSI -) (("1" (SPSI -) (("1" (NEW-SPLIT-IF -) NIL) ("2" (SIMP) NIL))) ("2" (SPLIT-ALL -) NIL))))))) ("6" (HIDE "rho") (("6" (SPSI -) (("1" (NEW-SPLIT-IF -) (("1" (INST + "tail(channels!1(id!1))") (("1" (SIMP) NIL))))) ("2" (SPSI) (("2" (CLEAN-UP) (("2" (REVEAL "localTimeEarlier") (("2" (INST - "id!1") (("2" (SIMP) NIL))))))))))))) ("7" (SPLIT-ALL -) NIL) ("8" (SPLIT-ALL -) NIL))))))))))))))))))))) (|channelTimeInc| "" (EXP-RHO) (("" (REVEAL "channelTimeInc") (("" (INST -1 "id!1" "id2!1" "cPoint!1" "cPoint2!1") (("" (EXPAND "preceed") (("" (EXPAND "occEntry") (("" (APPLY (THEN (SPLIT-RHO) (EXPAND "home"))) (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (SIMP) NIL))))) ("2" (REPLACE*) (("2" (HIDE "rho") (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SIMP) (("1" (SPLIT-ALL) NIL))))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))))))) ("3" (REPLACE*) (("3" (HIDE "rho") (("3" (SIMP) (("3" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))))))) ("4" (REVEAL "channelTimeInc") (("4" (EXPAND "preceed") (("4" (INST-CP -1 "id!1" "p_id!1 - 1" "cPoint!1" "head(channels!1(p_id!1 - 1))") (("4" (INST -1 "p_id!1 - 1" "id2!1" "head(channels!1(p_id!1 - 1))" "cPoint2!1") (("4" (EXPAND "occEntry") (("4" (REPLACE*) (("4" (SIMP) (("4" (EXPAND "inChannel") (("4" (LABEL "noneq" 4) (("4" (HIDE "rho") (("4" (REVEAL "channelsNonNeg") (("4" (INST -1 "p_id!1 - 1") (("4" (NEW-SPLIT-IF "orig") (("1" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (CLEAN-UP) (("2" (SPLIT-ALL -) NIL))))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (NEW-SPLIT-IF -) (("2" (APPLY (THEN (CASE "not cPoint3!1 = head(channels!1(id2!1))") (SIMP))) (("2" (REPLACE*) (("2" (REVEAL -1) (("2" (INST -1 "id!1" "tail(channels!1(id!1))") (("2" (SIMP) (("2" (SPSI -) NIL))))))))))))))))))))) ("2" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) (("2" (APPLY (THEN (CASE "cPoint3!1 = head(channels!1(id3!1))") (SIMP))) (("2" (REPLACE*) (("2" (REVEAL -1) (("2" (INST -1 "id!1" "tail(channels!1(id!1) )") (("2" (CLEAN-UP) (("2" (SPLIT-ALL -) NIL))))))))))))))))))))))))) ("2" (SPSI) (("1" (CLEAN-UP) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (NEW-SPLIT-IF) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))) ("2" (NEW-SPLIT-IF) (("2" (SPSI) (("1" (SPSI) (("1" (CLEAN-UP) (("1" (REPLACE*) (("1" (SIMP) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))) ("2" (REPLACE*) (("2" (CLEAN-UP) (("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))) ("2" (REPLACE*) (("2" (SPSI) (("1" (REPLACE*) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) (("2" (APPLY (THEN (CASE " cPoint3!1 = head(channels!1(id3!1))") (SIMP) (REPLACE*))) (("2" (REVEAL -1) (("2" (INST -1 "p_id!1" "tail(channels!1(p_id!1))") (("2" (NEW-SPLIT-IF -) (("2" (REVEAL "channelsNonNeg") (("2" (INST? :WHERE 1) (("2" (SIMP) NIL))))))))))))))))))))))) ("2" (REPLACE*) (("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) (("2" (APPLY (THEN (CASE "cPoint3!1 = head(channels!1(id3!1))") (SIMP) (REPLACE*))) (("2" (REVEAL -1) (("2" (INST -1 "p_id!1" "tail(channels!1(p_id!1))") (("2" (SPLIT-ALL -) (("2" (REVEAL "channelsNonNeg") (("2" (INST? :WHERE 1) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("5" (LABEL "nonneg" 5) (("5" (REPLACE*) (("5" (HIDE "rho") (("5" (SIMP) (("5" (EXPAND "inChannel") (("5" (REVEAL "timeChannelProc") (("5" (INST -1 "0") (("5" (INST-CP -1 "id!1" "cPoint!1") (("5" (INST -1 "id2!1" "cPoint2!1") (("5" (SIMP) (("5" (REVEAL "channelsNonNeg") (("5" (INST? :WHERE +) (("5" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL))) ("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (REPLACE*) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (REPLACE*) (("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))))) ("2" (APPLY (THEN (SPLIT-ALL) (REPLACE*) (THEN (SPSI) (SIMP) (SKOSIMP*) (INST - "id3!1" "cPoint3!1") (SPLIT-ALL -)))) NIL))))))))))))))))))))))))))) ("6" (REPLACE*) (("6" (SIMP) (("6" (EXPAND "inChannel") (("6" (HIDE "rho") (("6" (REVEAL "channelsNonNeg") (("6" (INST -1 "U") (("6" (REVEAL "timeChannelProc") (("6" (INST -1 "0") (("6" (INST-CP -1 "id!1" "cPoint!1") (("6" (INST -1 "id2!1" "cPoint2!1") (("6" (APPLY (THEN (LIFT-IF) (THEN (SPLIT +) (THEN (SPLIT "orig") (FLATTEN) (SIMP))))) (("1" (APPLY (THEN (LIFT-IF) (THEN (SPLIT +) (THEN (SPLIT "orig") (FLATTEN) (SIMP))))) (("1" (CLEAN-UP) (("1" (REPLACE*) (("1" (SIMP) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (SPLIT-IF-SIMP) (("1" (REVEAL "timeChannelProc") (("1" (CLEAN-UP) (("1" (INST -1 "0" "cPoint3!1") (("1" (SIMP) (("1" (HIDE -2) (("1" (REVEAL "channelTimeInc") (("1" (CLEAN-UP) (("1" (INST -1 "0" "0" "cPoint!1" "cPoint3!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (REPLACE*) (("1" (REPLACE*) (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))))))))))))))) ("2" (REVEAL "cEntryExists") (("2" (INST -1 "t(procs!1(id2!1))" "1") (("2" (REVEAL "localTimeEarlier") (("2" (INST -1 "1") (("2" (SIMP) (("2" (CASE " t(procs!1(0)) > t(procs!1(1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "0" "cPoint!3") (("1" (SIMP) (("1" (REVEAL "channelTimeInc") (("1" (INST - "0" "0" "cPoint!3" "cPoint!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (SPSI) NIL))))))))))))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (REVEAL "timeChannelProc") (("2" (INST -3 "1") (("2" (INST -3 "0" "cPoint!1") (("2" (SIMP) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))) ("2" (REPLACE*) (("2" (SIMP) (("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (NEW-SPLIT-IF) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SIMP) (("2" (REPLACE*) (("2" (SIMP) NIL))))))))))))))) ("3" (REPLACE*) (("3" (SIMP) (("3" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (NEW-SPLIT-IF) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (NEW-SPLIT-IF -) NIL))))))))))))) ("2" (APPLY (THEN (LIFT-IF) (THEN (SPLIT +) (THEN (SPLIT "orig") (FLATTEN) (SIMP) (REPLACE*) (REPLACE*) (SIMP))))) (("1" (REDUCE-IF) (("1" (CLEAN-UP) (("1" (SIMP) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "channelTimeInc") (("1" (INST - "id!1" "id3!1" "cPoint!1" "cPoint3!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (CLEAN-UP) (("1" (SPSI -) (("1" (REVEAL "timeChannelProc") (("1" (INST - "0" "cPoint3!1") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (SPSI -) NIL))))))))))))))))))))) ("2" (REVEAL "channelTimeInc") (("2" (INST - "id!1" "id3!1" "cPoint!1" "cPoint3!1") (("2" (REVEAL "timeChannelProc") (("2" (INST - "id3!1" "cPoint3!1") (("2" (CLEAN-UP) (("2" (EXPAND "preceed") (("2" (EXPAND "occEntry") (("2" (SPLIT-ALL) NIL))))))))))))))))))) ("2" (REVEAL "cEntryExists") (("2" (INST - "t(procs!1(0))" "U") (("2" (REVEAL "localTimeEarlier") (("2" (INST - "U") (("2" (SIMP) (("2" (CASE "t(procs!1(0)) = t(procs!1(U)) ") (("1" (INST "cEntryExists" "cPoint!1") (("1" (SIMP) (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (CLEAN-UP) (("1" (SPSI "cEntryExists") (("1" (SKOSIMP*) (("1" (INST "toProve" "U" "cPoint2!2") (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST - "id2!3" "cPoint!3") (("2" (SIMP) (("2" (NEW-SPLIT-IF -) NIL))))))))))))))))))))))))))))) ("2" (NEW-SPLIT-IF -) (("2" (CLEAN-UP) (("2" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "channelTimeInc") (("1" (INST - "id!1" "id3!1" "cPoint!1" "cPoint3!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (REVEAL "timeChannelProc") (("1" (INST - "id3!1" "cPoint3!1") (("1" (CLEAN-UP) (("1" (SPLIT-ALL) NIL))))))))))))))))) ("2" (REVEAL "cEntryExists") (("2" (INST "cEntryExists" "t(procs!1(id2!1))" "id!1") (("2" (REVEAL "localTimeEarlier") (("2" (INST - "id!1") (("2" (SIMP) (("2" (INST - "cPoint!1") (("2" (SIMP) (("2" (APPLY (THEN (CASE "t(procs!1(0)) = t(procs!1(id!1))") (SIMP))) (("1" (CLEAN-UP) (("1" (SPSI "cEntryExists") (("1" (SKOSIMP*) (("1" (INST "toProve" "id!1" "cPoint2!2") (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (NEW-SPLIT-IF -) NIL))))))))))))) ("2" (SKOSIMP*) (("2" (CLEAN-UP) (("2" (INST - "id2!3" "cPoint!3") (("2" (SPLIT-ALL -) NIL))))))))))))))))))))))))))))) ("3" (SPSI) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (CLEAN-UP) (("1" (SPLIT-ALL) NIL))))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (CLEAN-UP) (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("4" (SPSI) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))) ("3" (APPLY (THEN (SPLIT +) (THEN (SPLIT "orig") (SIMP) (REPLACE*) (SIMP)))) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))) ("3" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))))))))))))))))))))))))) ("7" (REPLACE*) (("7" (SIMP) (("7" (HIDE "rho") (("7" (CASE "op(instlist(0, pc(procs!1(0)))) = WRITE") (("1" (SIMP) (("1" (APPLY (THEN (NEW-SPLIT-IF) (THEN (SPSI "orig") (SIMP)))) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "timeChannelProc") (("1" (INST - "id!1") (("1" (INST - "id!1" "cPoint!1") (("1" (SIMP) (("1" (SPSI -) NIL))))))))) ("2" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SPLIT-ALL) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (NEW-SPLIT-IF) (("1" (REVEAL "timeChannelProc") (("1" (INST - "id2!1" "id!1" "cPoint!1") (("1" (SIMP) (("1" (SPSI -) NIL))))))) ("2" (APPLY (THEN (SPSI) (SIMP) (SKOSIMP*) (INST - "id3!1" "cPoint3!1") (SPLIT-ALL -))) NIL))) ("3" (APPLY (THEN (SPSI) (SIMP) (SKOSIMP*) (INST - "id3!1" "cPoint3!1") (SPLIT-ALL -))) (("1" (INST - "id3!1" "cPoint3!1") (("1" (SIMP) (("1" (REPLACE*) (("1" (SIMP) NIL))))))) ("2" (INST - "id3!1" "cPoint3!1") (("2" (SPLIT-ALL -) NIL))))))))) ("2" (SIMP) (("2" (APPLY (THEN (SPLIT-ALL) (THEN (SPSI) (SIMP) (SKOSIMP*) (INST - "id3!1" "cPoint3!1") (SPLIT-ALL -)))) NIL))))))))))) ("8" (REPLACE*) (("8" (SIMP) NIL))) ("9" (REPLACE*) (("9" (SIMP) NIL))))))))))))))) (|timeChannelProc| "" (EXP-RHO) (("" (REVEAL "timeChannelProc") (("" (INST - "id!1" "id2!1" "cPoint!1") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL) NIL) ("3" (SPLIT-ALL) NIL) ("4" (EXPAND "inChannel") (("4" (REVEAL "channelsNonNeg") (("4" (INST - "p_id!1 - 1") (("4" (NEW-SPLIT-IF "orig") (("1" (NEW-SPLIT-IF "orig") (("1" (REVEAL "timeChannelProc") (("1" (INST - "id2!1 - 1" "head(channels!1(id2!1 - 1))") (("1" (SPSI) (("1" (SPSI -) NIL) ("2" (SPLIT-ALL) (("1" (CLEAN-UP) (("1" (REVEAL "cEntryExists") (("1" (INST - " 1 + t(procs!1(id!1))" "id!1") (("1" (INST "timeChannelProc" "0" "id!1 - 1" "head(channels!1(id!1 - 1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "channelTimeInc") (("1" (INST -1 "id!1 -1" "id2!2" "head(channels!1(id!1 - 1))" "cPoint!2") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (REPLACE*) (("1" (SIMP) (("1" (SIMP) NIL))))))))))))))))))))))))) ("2" (REVEAL "cEntryExists") (("2" (INST - "t(CE(channels!1(id!1 - 1))(head(channels!1(id!1 - 1))))" "id!1") (("2" (INST "timeChannelProc" "id!1 - 1" "id!1 - 1" "head(channels!1(id!1 - 1))") (("2" (REVEAL "localTimeEarlier") (("2" (INST - "id!1 -1") (("2" (SIMP) (("2" (SPSI "cEntryExists") (("2" (SKOSIMP*) (("2" (REVEAL "channelTimeInc") (("2" (EXPAND "preceed") (("2" (INST -1 "id!1 - 1" "id2!2" "head(channels!1(id!1 - 1))" "cPoint!2") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))))) ("2" (SPSI) (("2" (NEW-SPLIT-IF) NIL))))) ("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("1" (REVEAL "timeChannelProc") (("1" (INST - "id!1 - 1" "(head(channels!1(id!1 - 1)))") (("1" (SIMP) (("1" (REVEAL "localTimeEarlier") (("1" (INST -1 "id!1") (("1" (SPSI) (("1" (REVEAL "channelTimeInc") (("1" (INST -1 "id!1 - 1" "id2!1" "head(channels!1(id!1 - 1))" "cPoint!1") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (CASE "t(CE(channels!1(id!1 - 1))(head(channels!1(id!1 - 1)))) = 1 + t(procs!1(id!1))") (("1" (SPSI) (("1" (REPLACE*) (("1" (SIMP) (("1" (SIMP) NIL))))) ("2" (NEW-SPLIT-IF) (("2" (SIMP) NIL))))) ("2" (HIDE 2) (("2" (HIDE -1) (("2" (REVEAL "cEntryExists") (("2" (INST - "1 + t(procs!1(id!1))" "id!1") (("2" (CASE "t(procs!1(0)) = t(procs!1(id!1))") (("1" (SIMP) (("1" (CLEAN-UP) (("1" (INST? :WHERE "toProve") (("1" (SIMP) NIL))))))) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (REVEAL "channelTimeInc") (("2" (HIDE -1) (("2" (INST - "id!1 - 1" "id2!2" "head(channels!1(id!1 - 1))" "cPoint!2") (("2" (EXPAND "preceed") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SIMP) NIL))))))))))))))))))))))))))))))))))))) ("2" (CASE "t(procs!1(0)) = t(procs!1(id!1))") (("1" (SIMP) (("1" (INST - "id2!1" "cPoint!1") (("1" (SPSI) (("1" (REPLACE*) (("1" (SIMP) NIL))) ("2" (SPSI) NIL))))))) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (SPLIT-ALL) NIL))))))))))))))))))) ("2" (SPLIT-ALL) NIL))))))))))))) ("5" (EXPAND "inChannel") (("5" (REVEAL "channelsNonNeg") (("5" (INST - "U") (("5" (HIDE "rho") (("5" (NEW-SPLIT-IF) (("1" (REVEAL "localTimeEarlier") (("1" (INST - "id!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL) ("2" (NEW-SPLIT-IF) NIL))))))) ("2" (REVEAL "localTimeEarlier") (("2" (INST -1 "id!1") (("2" (SPLIT-ALL) NIL))))))))))))))) ("6" (EXPAND "inChannel") (("6" (REVEAL "localTimeEarlier") (("6" (INST -1 "id!1") (("6" (HIDE "rho") (("6" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SPLIT-ALL) NIL) ("2" (SPLIT-ALL) NIL))) ("2" (SPLIT-ALL) NIL))))))))))) ("7" (HIDE "rho") (("7" (SPLIT-ALL) (("7" (REVEAL "localTimeEarlier") (("7" (INST - "id!1") (("7" (SIMP) NIL))))))))) ("8" (HIDE "rho") (("8" (SPLIT-ALL) (("8" (REVEAL "localTimeEarlier") (("8" (INST - "id!1") (("8" (SIMP) NIL))))))))))))))))) (|idPCunique| "" (EXP-RHO) (("" (REVEAL "idPCunique") (("" (INST? :WHERE +) (("" (EXPAND "weakPreceed") (("" (EXPAND "preceed") (("" (EXPAND "occEntry") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (REVEAL "waiting") (("1" (INST -1 "id!1" "cPoint!1") (("1" (SIMP) (("1" (APPLY (THEN (CASE "id(CE(channels!1(id!1))(cPoint!1)) = id!1"))) (("1" (REVEAL "channelsMatchProg") (("1" (INST -1 "id!1" "cPoint!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (CASE "id(CE(channels!1(id!1))(cPoint!1)) = id2!1") (("1" (REVEAL "waiting") (("1" (INST -1 "id!1" "cPoint!1") (("1" (SIMP) (("1" (REVEAL "channelsMatchProg") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (CASE "id(CE(channels!1(id2!1))(cPoint2!1)) = id!1") (("1" (CLEAN-UP) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (REVEAL "channelsMatchProg") (("1" (INST?) (("1" (SIMP) (("1" (REDUCE-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT - "orig") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (CASE "id(CE(channels!1(id!1))(cPoint!1)) = id!1") (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (CASE " id(CE(channels!1(id!1))(cPoint!1)) = id2!1") (("1" (REVEAL "waiting") (("1" (SIMP) (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (CASE "id(CE(channels!1(id2!1))(cPoint2!1)) = id!1") (("1" (CLEAN-UP) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT - "orig") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "inChannel") (("3" (REVEAL "channelsNonNeg") (("3" (INST?) (("3" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (REVEAL "idPCunique") (("1" (EXPAND "preceed") (("1" (EXPAND "weakPreceed") (("1" (INST -1 "id!1" "id!1 - 1" "cPoint!1" "head(channels!1(id!1 - 1))") (("1" (EXPAND "occEntry") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (REVEAL "idPCunique") (("2" (INST -1 "id!1" "p_id!1 - 1" "cPoint!1" "head(channels!1(p_id!1 - 1))") (("2" (CLEAN-UP) (("2" (EXPAND "weakPreceed") (("2" (EXPAND "preceed") (("2" (EXPAND "occEntry") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "idPCunique") (("2" (INST - "p_id!1 - 1" "id2!1" "head(channels!1(p_id!1 - 1))" "cPoint2!1") (("2" (EXPAND "preceed") (("2" (EXPAND "weakPreceed") (("2" (EXPAND "occEntry") (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (EXPAND "inChannel") (("4" (NEW-SPLIT-IF) (("1" (LIFT-IF) (("1" (REVEAL "channelsNonNeg") (("1" (INST -1 "U") (("1" (REVEAL "idPCunique") (("1" (INST - "U" "id!1" " head(channels!1(U))" "cPoint!1") (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (SPSI) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (SPSI) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (SPSI) NIL NIL) ("2" (SPSI) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (EXPAND "inChannel") (("5" (CASE "message(CE(channels!1(U))(head(channels!1(U)))) = readReq") (("1" (SIMP) (("1" (LIFT-IF) (("1" (APPLY (THEN (CASE "id!1 = 0") (THEN (CASE "id2!1 = 0") (SIMP)))) (("1" (REVEAL "idPCunique") (("1" (NEW-SPLIT-IF -) (("1" (INST - "U" "0" "head(channels!1(U))" "cPoint!1") (("1" (SIMP) (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (REVEAL "channelsNonNeg") (("1" (INST -1 "U") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (REVEAL "idPCunique") (("1" (INST - "U" "id!1" "head(channels!1(U))" "cPoint!1") (("1" (REVEAL "channelsNonNeg") (("1" (INST -1 "U") (("1" (EXPAND "weakPreceed") (("1" (EXPAND "occEntry") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("3" (LIFT-IF) (("3" (REVEAL "channelsNonNeg") (("3" (INST -1 "U") (("3" (SIMP) (("3" (NEW-SPLIT-IF) (("1" (SPSI) NIL NIL) ("2" (SPSI) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (APPLY (THEN (CASE "id2!1 = U") (THEN (CASE "id!1 = U") (SIMP)))) (("1" (SIMP) NIL NIL) ("2" (CLEAN-UP) (("2" (SPLIT-ALL) NIL NIL)) NIL) ("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("6" (CASE "op(instlist(0, pc(procs!1(0)))) = WRITE") (("1" (SIMP) (("1" (LIFT-IF) (("1" (CASE "id!1 = 0") (("1" (SIMP) (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "homeNotReq") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "homeNotReq") (("1" (INST?) (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|homeNotReq| "" (EXP-RHO) (("" (REVEAL "homeNotReq") (("" (INST-CP -1 "id!1" "cPoint!1") (("" (CASE "p_id!1 > 0") (("1" (INST - "p_id!1-1" "head(channels!1(p_id!1-1))") (("1" (REVEAL "channelsNonNeg") (("1" (INST -1 "p_id!1 -1") (("1" (EXPAND "inChannel") (("1" (SPLIT-RHO-ALL) (("1" (NEW-SPLIT-IF -) NIL NIL) ("2" (SPLIT-ALL -) NIL NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL) ("2" (EXPAND "inChannel") (("2" (SPLIT-RHO-ALL) (("1" (SPLIT-ALL -) NIL NIL) ("2" (SPLIT-ALL -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|waiting| "" (EXP-RHO) (("" (SKOSIMP*) (("" (REVEAL "waiting") (("" (INST - "id!1" "cPoint!1") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (SPLIT-ALL) NIL NIL) ("2" (SPLIT-ALL) NIL NIL) ("3" (SPLIT-ALL) NIL NIL) ("4" (EXPAND "inChannel") (("4" (REVEAL "channelsNonNeg") (("4" (INST - "p_id!1 - 1") (("4" (REVEAL "waiting") (("4" (INST -1 "p_id!1 - 1" "head(channels!1(p_id!1 - 1))") (("4" (NEW-SPLIT-IF) (("1" (REVEAL "idPCunique") (("1" (INST -1 "id!1" "id!1 - 1" "cPoint!1" "head(channels!1(id!1 -1))") (("1" (EXPAND "weakPreceed") (("1" (REVEAL "channelsMatchProg") (("1" (INST -1 "id!1 - 1" "head(channels!1(id!1 - 1))") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REPLACE -1 :DIR RL) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (REDUCE-IF) (("1" (CLEAN-UP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (REPLACE -1 :DIR RL) (("2" (REPLACE -1 :DIR RL :HIDE? T) (("2" (NEW-SPLIT-IF) (("2" (HIDE "channelsMatchProg") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (NEW-SPLIT-IF) (("1" (SPSI -) (("1" (CASE "id!1 = p_id!1 - 1") (("1" (REVEAL "idPCunique") (("1" (INST -1 "id!1" "id!1" " head(channels!1(id!1))" "cPoint!1") (("1" (EXPAND "weakPreceed") (("1" (EXPAND "preceed") (("1" (EXPAND "occEntry") (("1" (SIMP) (("1" (REVEAL "waiting") (("1" (INST -1 "id!1" "cPoint!1") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (REPLACE -1 :DIR RL :HIDE? T) (("2" (REVEAL "idPCunique") (("2" (INST-CP -1 "p_id!1 - 1" "id!1" "head(channels!1(p_id!1 - 1))" "cPoint!1") (("2" (INST -1 "id!1" "p_id!1 - 1" "cPoint!1" "head(channels!1(p_id!1 - 1))") (("2" (EXPAND "weakPreceed") (("2" (EXPAND "preceed") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SPSI -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (REPLACE -1 :DIR RL) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REVEAL "idPCunique") (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (NEW-SPLIT-IF) (("2" (REPLACE -1 :DIR RL :HIDE? T) (("2" (NEW-SPLIT-IF) (("2" (SPSI -) (("2" (REVEAL "idPCunique") (("2" (INST-CP -1 "p_id!1 - 1" "id!1" "head(channels!1(p_id!1 - 1))" "cPoint!1") (("2" (INST -1 "id!1" "p_id!1 - 1" "cPoint!1" "head(channels!1(p_id!1 - 1))") (("2" (EXPAND "weakPreceed") (("2" (EXPAND "preceed") (("2" (EXPAND "occEntry") (("2" (SIMP) (("2" (SPSI -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (EXPAND "inChannel") (("5" (REVEAL "waiting") (("5" (REVEAL "channelsNonNeg") (("5" (INST -1 "U") (("5" (INST - "U" "head(channels!1(U))") (("5" (REVEAL "homeNotReq") (("5" (INST -1 "U" "head(channels!1(U))") (("5" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF) (("1" (REVEAL "homeNotReq") (("1" (INST - "id!1" "cPoint!1") (("1" (SIMP) (("1" (REPLACE -2 :DIR RL :HIDE? T) (("1" (SPSI) (("1" (SIMP) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REPLACE*) (("1" (SIMP) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (EXPAND "inChannel") (("6" (CASE "message(CE(channels!1(U))(head(channels!1(U)))) = readReq") (("1" (SIMP) (("1" (REVEAL "waiting") (("1" (INST -1 "U" "head(channels!1(U))") (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("7" (REVEAL "homeNotReq") (("7" (INST -1 "id!1" "cPoint!1") (("7" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("8" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histLt| "" (EXP-RHO) (("" (REVEAL "histLt") (("" (INST?) (("" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (HIDE "nextSize") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (RERUN ("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (SPSI) (("1" (HIDE "rho") (REVEAL "histMatchTime") (INST?) (SPSI) (REVEAL "nextSize") (SPSI -) (("1" (HIDE -2) (CLEAN-UP) (LEMMA "nextExists") (INST?) (SIMP) (REDUCE-ALL) (INST + "index!1") (SIMP) (LEMLTSTRICT) (INST? :WHERE 1) (SIMP) (EXPAND "timestamp") (SIMP) (REPLACE*) (SIMP) (SIMP)) ("2" (LEMMA "nextExists") (INST?) (NEW-SPLIT-IF -) (INST - "index!1") (SIMP) (LEMLTSTRICT) (INST? :WHERE +) (EXPAND "timestamp") (SIMP) (REPLACE*) (SIMP) (CLEAN-UP) (SIMP)))) ("2" (HIDE "rho") (REVEAL "histLt") (INST - "index!1" "index2!1 - 1") (SIMP)))) ("2" (HIDE "histLt") (SPSI) (("1" (HIDE "rho") (REVEAL "histMatchTime") (INST - "index2!1 - 1") (SIMP) (SPSI) (LEMLTSTRICT) (INST? :WHERE 1) (SIMP) (SPSI -) (CLEAN-UP) (HIDE "histMatchTime") (REVEAL "nextSize") (SIMP) (EXPAND "timestamp") (REPLACE*) (INST "trans" "(# t := lst(hist!1)(index2!1 - 1)`t, r := lst(hist!1)(index2!1 - 1)`r, id := lst(hist!1)(index2!1 - 1)`id #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "(# t := t(lst(hist!1)(next!1)), r := r(lst(hist!1)(next!1)), id := id(lst(hist!1)(next!1)) #)") (SIMP) (SPSI "trans") (REVEAL "histLt") (INST - "index!1" "index2!1 - 1") (REVEAL "linear") (INST? :WHERE "trans") (SIMP)) ("2" (REVEAL "histLt") (INST - "index!1 - 1" "index2!1 - 1") (SIMP))))))) NIL NIL) ("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("2" (CLEAN-UP) (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SIMP) (("2" (SPSI) (("2" (EXPAND "lt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho") (("3" (REVEAL "histMatchTime") (("3" (INST - "index!1") (("3" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (EXPAND "lt") (("1" (SPSI) NIL NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (EXPAND "lt") (("1" (SIMP) (("1" (REVEAL "localTimeEarlier") (("1" (INST - " lst(hist!1)(index!1)`id") (("1" (CASE "lst(hist!1)(index!1)`id = 0") (("1" (SIMP) (("1" (REDUCE-ALL) NIL NIL)) NIL) ("2" (SIMP) (("2" (SIMP) (("2" (NEW-SPLIT-IF -) (("2" (LEMMA "nextExists") (("2" (INST?) (("2" (NEW-SPLIT-IF -) (("1" (INST - "index!1") (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "index!1") (("2" (EXPAND "lt") (("2" (EXPAND "timestamp") (("2" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REVEAL "histLt") (("1" (INST - "index!1" "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REVEAL "histMatchTime") (("1" (INST - "index2!1 - 1") (("1" (SIMP) (("1" (SPSI) (("1" (LEMLTSTRICT) (("1" (INST? :WHERE 1) (("1" (SIMP) (("1" (SPSI -) (("1" (CLEAN-UP) (("1" (HIDE "histMatchTime") (("1" (REVEAL "nextSize") (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (REPLACE*) (("1" (INST "trans" "(# t := lst(hist!1)(index2!1 - 1)`t, r := lst(hist!1)(index2!1 - 1)`r, id := lst(hist!1)(index2!1 - 1)`id #)" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "(# t := t(lst(hist!1)(next!1)), r := r(lst(hist!1)(next!1)), id := id(lst(hist!1)(next!1)) #)") (("1" (SIMP) (("1" (SPSI "trans") (("1" (REVEAL "histLt") (("1" (INST - "index!1" "index2!1 - 1") (("1" (REVEAL "linear") (("1" (INST? :WHERE "trans") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "lt") (("2" (REVEAL "histMatchTime") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histLt") (("2" (INST - "index!1 - 1" "index2!1 - 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (RERUN ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))"))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|histComplete| "" (EXP-RHO) (("" (SPSI) (("1" (REVEAL "histComplete") (("1" (SKOSIMP*) (("1" (INST?) (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (INTRONEXT) (("1" (HIDE "rho") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (LIFT-IF "toProve") (("1" (SPSI -) (("1" (APPLY (THEN (CASE "index!1 <= size(hist!1)") (SIMP))) (("1" (INST-CP "histComplete" "index2!1") (("1" (NEW-SPLIT-IF -) (("1" (REDUCE-ALL) (("1" (INST "histComplete" "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) (("2" (REVEAL "histComplete") (("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (INST-CP - "index2!1") (("2" (NEW-SPLIT-IF -) (("2" (REDUCE-ALL) (("2" (INST - "index2!1 - 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "oc") (("2" (LIFT-IF 1) (("2" (SPSI) (("1" (SPSI "histComplete") (("1" (INST - "r2!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!2") (("1" (INST + "index!2 + 1") (("1" (EXPAND "timestamp") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REVEAL "histCompleteNumRead") (("1" (INST? -) (("1" (EXPAND "oc") (("1" (SIMP) (("1" (INST-CP -1 "r2!1 - 1") (("1" (EXPAND "timestamp") (("1" (SKOSIMP*) (("1" (INST-CP + "index!2") (("1" (INST + "index!2 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histComplete") (("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (EXPAND "oc") (("2" (INST - "r2!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index!2") (("2" (INST + "index!2 + 1") (("2" (EXPAND "timestamp") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL) ("2" (HIDE "rho") (("2" (EXPAND "oc") (("2" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (EXPAND "timestamp") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho") (("3" (CASE "op(instlist(0, pc(procs!1(0)))) = WRITE") (("1" (SIMP) (("1" (EXPAND "oc") (("1" (EXPAND "timestamp") (("1" (CASE "index!1 <= size(hist!1)") (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (SPLIT-ALL -) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (CLEAN-UP) (("2" (NEW-SPLIT-IF -) (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INTRONEXT) (("1" (REVEAL "rho") (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (EXPAND "oc") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (EXPAND "timestamp") (("1" (NEW-SPLIT-IF -) (("1" (INST-CP - "index2!1") (("1" (SPLIT-ALL -) (("1" (INST "histComplete" "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) (("2" (REVEAL "histComplete") (("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (INST-CP - "index2!1") (("2" (NEW-SPLIT-IF -) (("2" (REDUCE-ALL) (("2" (INST - "index2!1 - 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "timestamp") (("2" (HIDE "nextSize") (("2" (NEW-SPLIT-IF) (("1" (INST? -) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!2") (("1" (INST + "index!2 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histComplete") (("2" (NEW-SPLIT-IF) (("1" (REVEAL "histCompleteNumRead") (("1" (HIDE "histComplete") (("1" (INST? -) (("1" (SIMP) (("1" (INST - "r2!1 - 1") (("1" (EXPAND "oc") (("1" (SKOSIMP*) (("1" (INST-CP + "index!2") (("1" (INST + "index!2 + 1") (("1" (EXPAND "timestamp") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (INST? -) (("2" (EXPAND "oc") (("2" (EXPAND "timestamp") (("2" (SKOSIMP*) (("2" (INST-CP + "index!2") (("2" (INST + "index!2 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "histCompleteNumRead") (("2" (INST - "id!1") (("2" (EXPAND "oc") (("2" (EXPAND "timestamp") (("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "r2!1") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (INTRONEXT) (("1" (HIDE "rho") (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (HIDE "nextSize") (("1" (NEW-SPLIT-IF) (("1" (INST-CP + "next!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL) ("3" (SPLIT-ALL) NIL NIL) ("4" (HIDE "rho") (("4" (SPLIT-ALL) NIL NIL)) NIL) ("5" (HIDE "rho") (("5" (NEW-SPLIT-IF) (("5" (SKOSIMP*) (("5" (INST-CP + "index!1") (("5" (INST + "index!1 + 1") (("5" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (HIDE "rho") (("6" (NEW-SPLIT-IF) (("1" (REDUCE-ALL) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (INTRONEXT) (("1" (APPLY (THEN (CASE " next!1 <= size(hist!1) + 1") (SIMP))) (("1" (HIDE "nextSize") (("1" (NEW-SPLIT-IF -) (("1" (REVEAL "rho") (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (INST-CP + "next!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST-CP + "index!1 + 1") (("2" (INST + "index!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL) ("7" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "(t(procs!1(id!1)) > 0 AND numRead(procs!1(id!1)) > 0)") (SIMP))) (("1" (SKOSIMP*) (("1" (INST + "id2!1") (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (HIDE "nextSize" "rho") (("1" (NEW-SPLIT-IF -) (("1" (CLEAN-UP) (("1" (REVEAL "histMatchTimeE") (("1" (REVEAL "localTimeEarlier") (("1" (INST - "id!1") (("1" (SIMP) (("1" (INST "histMatchTimeE" "t(procs!1(id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id(lst(hist!1)(index!1))") (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL) ("2" (NEW-SPLIT-IF -) NIL NIL) ("3" (NEW-SPLIT-IF -) NIL NIL) ("4" (HIDE "rho") (("4" (SPLIT-ALL -) NIL NIL)) NIL) ("5" (NEW-SPLIT-IF -) NIL NIL) ("6" (HIDE "rho") (("6" (NEW-SPLIT-IF -) (("6" (REDUCE-ALL) (("6" (INTRONEXT) (("1" (REVEAL "rho") (("1" (REPLACE*) (("1" (REPLACE*) (("1" (HIDE "rho") (("1" (CLEAN-UP) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "t(procs!1(id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "(lst(hist!1)(index!1))`id") (("1" (INST-CP + "index!1 + 1") (("1" (INST + "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("7" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|histMatchPC| "" (EXP-RHO) (("" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP) (LABEL "nextSize" -1))) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "histMatchPC") (("1" (INST - "index!1") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST - "index!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST - "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (SPLIT-ALL) (("1" (INST - "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST - "pc!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (SPSI "nextSize") (("1" (CLEAN-UP) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchPC") (("1" (INST - "index2!1") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST-CP "histMatchPC" "index2!1") (("2" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchPC") (("1" (INST - "index2!1") (("1" (SIMP) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (INST "histMatchPC" "index2!1 - 1") (("2" (SIMP) (("2" (HIDE "histMatchPC") (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index2!1 - 1") (("2" (SIMP) (("2" (REPLACE*) (("2" (NEW-SPLIT-IF -) (("1" (REVEAL "waiting") (("1" (SKOSIMP*) (("1" (INST? -) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("2" (APPLY (THEN (CASE "index2!1 = next!1 + 1") (SIMP))) (("1" (REPLACE*) (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "next") (("2" (CASE "lt((# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(index2!1 - 1)))") (("1" (EXPAND "lt") (("1" (EXPAND "timestamp") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (HIDE "histMatchTime") (("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index2!1 - 1") (("2" (SIMP) (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index2!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE "histMatchPC") (("2" (REVEAL "histMatchPCe") (("2" (INST?) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index!2 + 1") (("2" (INST + "index!2") (("2" (SPLIT-ALL) (("2" (HIDE "next") (("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index!2") (("2" (SIMP) (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index!2") (("2" (SIMP) (("2" (CASE "index!2 = next!1") (("1" (REPLACE*) (("1" (CLEAN-UP) (("1" (EXPAND "lt") (("1" (EXPAND "timestamp") (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index!2))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (EXPAND "lt") (("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histMatchPC") (("2" (INST -1 "index!1 - 1") (("2" (HIDE -2) (("2" (APPLY (THEN (CASE "next!1 < index!1") (SIMP))) (("2" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST -1 "next!1") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "index!1 = next!1 + 1") (REPLACE*) (SIMP))) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index!1 - 1") (("2" (SIMP) (("2" (HIDE "next" "histMatchPC") (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(lst(hist!1)(index!1 - 1)`id)), r := 1 + numRead(procs!1(lst(hist!1)(index!1 - 1)`id)), id := lst(hist!1)(index!1 - 1)`id #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (EXPAND "lt") (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index!1 - 1") (("2" (SIMP) (("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "index2!1 - 1") (("2" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST - "index2!1 - 1") (("1" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-RHO-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho" "next" "nextSize") (("3" (NEW-SPLIT-IF) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (HIDE "rho" "next" "nextSize") (("4" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) (("2" (EXPAND "inChannel") (("2" (APPLY (THEN (CASE "p_id!1 = id!1 + 1") (REPLACE*) (SIMP))) (("2" (REVEAL 1) (("2" (INST + "id!1 + 1" "tail(channels!1(id!1 + 1))") (("2" (EXPAND "inChannel") (("2" (REVEAL "channelsNonNeg") (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (EXPAND "inChannel") (("5" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (REVEAL "homeNotReq") (("1" (INST? -) (("1" (REVEAL "channelsNonNeg") (("1" (INST?) (("1" (SIMP) (("1" (SPSI) (("1" (REVEAL "waiting") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REVEAL "channelsMatchProg") (("2" (INST?) (("2" (SIMP) (("2" (SIMP) (("2" (INST + "0" "tail(channels!1(0))") (("2" (NEW-SPLIT-IF) (("2" (REVEAL "channelsNonNeg") (("2" (INST - "0") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (NEW-SPLIT-IF) (("3" (REVEAL "histMatchPC") (("3" (INST - "index2!1") (("3" (SIMP) (("3" (CLEAN-UP) (("3" (SIMP) (("3" (REPLACE*) (("3" (REVEAL "waiting") (("3" (INST?) (("3" (SIMP) (("3" (SIMP) (("3" (SKOSIMP*) (("3" (SIMP) (("3" (REVEAL "idPCunique") (("3" (EXPAND "weakPreceed") (("3" (INST - "U" "id!1" "head(channels!1(U))" "cPoint!1") (("3" (SIMP) (("3" (EXPAND "occEntry") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (REVEAL "histMatchPCe") (("4" (INST - "(CE(channels!1(U))(head(channels!1(U))))`id" "pc!1") (("4" (SIMP) (("4" (REVEAL "waiting") (("4" (INST?) (("4" (SIMP) (("4" (SIMP) (("4" (SKOSIMP*) (("4" (INST + "index!2") (("4" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST - "index2!1") (("3" (NEW-SPLIT-IF) (("3" (CLEAN-UP) (("3" (REVEAL "waiting") (("3" (INST?) (("3" (SIMP) (("3" (REVEAL "channelsNonNeg") (("3" (INST?) (("3" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST? -) (("4" (INST - "pc!1") (("4" (SIMP) (("4" (SKOSIMP*) (("4" (INST + "index2!1") (("4" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (HIDE "rho" "next" "nextSize") (("6" (SIMP) (("6" (SKOSIMP*) (("6" (SIMP) (("6" (INST + "id!1" "cPoint!1") (("6" (SPLIT-ALL) (("6" (EXPAND "inChannel") (("6" (REVEAL 1) (("6" (REPLACE -1 :DIR RL) (("6" (EXPAND "inChannel") (("6" (INST + "0" "tail(channels!1(0))") (("6" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (CASE "op(instlist(0, pc(procs!1(0)))) = WRITE") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (CLEAN-UP) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (REVEAL "histMatchPC") (("1" (INST - "index2!1") (("1" (CLEAN-UP) (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "histMatchPCe") (("2" (INST - "0" "pc!1") (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "index!2") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST - "index2!1") (("3" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST? -) (("4" (INST? -) (("4" (SIMP) (("4" (SKOSIMP*) (("4" (INST + "index2!1") (("4" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (NEW-SPLIT-IF) (("1" (HIDE "rho") (("1" (REVEAL "histMatchTime") (("1" (INST - "index!1") (("1" (SIMP) (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST - "index2!1 - 1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (SIMP) (("1" (INST + "id!1" "cPoint!1") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "index2!1") (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (REVEAL "histMatchPC") (("2" (INST - "index2!1 -1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST? -) (("3" (INST? -) (("3" (SIMP) (("3" (SKOSIMP*) (("3" (INST-CP + "index2!1") (("3" (INST + "index2!1 + 1") (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF) (("1" (HIDE "rho") (("1" (REVEAL "histMatchPC") (("1" (INST - "index2!1") (("1" (REVEAL "localTimeEarlier") (("1" (SIMP) (("1" (INST - "id(lst(hist!1)(index2!1))") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (HIDE "rho") (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index2!1 - 1") (("2" (SIMP) (("2" (REPLACE*) (("2" (NEW-SPLIT-IF -) (("2" (APPLY (THEN (CASE "index2!1 = next!1 + 1") (SIMP))) (("1" (REPLACE*) (("1" (SIMP) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "next") (("2" (CASE "lt((# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #), timestamp(lst(hist!1)(index2!1 - 1)))") (("1" (EXPAND "lt") (("1" (EXPAND "timestamp") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (HIDE "histMatchTime") (("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index2!1 - 1") (("2" (SIMP) (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index2!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho" "histMatchPC") (("2" (SKOSIMP*) (("2" (REVEAL "histMatchPCe") (("2" (INST?) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index!2 + 1") (("2" (INST + "index!2") (("2" (SPLIT-ALL) (("2" (HIDE "next") (("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index!2") (("2" (SIMP) (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index!2") (("2" (SIMP) (("2" (CASE "index!2 = next!1") (("1" (REPLACE*) (("1" (CLEAN-UP) (("1" (EXPAND "lt") (("1" (EXPAND "timestamp") (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index!2))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (REVEAL "histMatchPC") (("2" (INST -1 "index!1 - 1") (("2" (HIDE -2) (("2" (APPLY (THEN (CASE "next!1 < index!1") (SIMP))) (("2" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST -1 "next!1") (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP - "index2!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "index!1 = next!1 + 1") (REPLACE*) (SIMP))) (("1" (EXPAND "timestamp") (("1" (EXPAND "lt") (("1" (NEW-SPLIT-IF -) NIL NIL)) NIL)) NIL) ("2" (REVEAL "histLt") (("2" (INST -1 "next!1" "index!1 - 1") (("2" (SIMP) (("2" (HIDE "next" "histMatchPC") (("2" (LEMLTSTRICT) (("2" (INST "trans" "(# t := t(procs!1(lst(hist!1)(index!1 - 1)`id)), r := 1 + numRead(procs!1(lst(hist!1)(index!1 - 1)`id)), id := lst(hist!1)(index!1 - 1)`id #)" "timestamp(lst(hist!1)(next!1))" "timestamp(lst(hist!1)(index!1 - 1))") (("2" (EXPAND "timestamp") (("2" (SIMP) (("2" (EXPAND "lt") (("2" (REVEAL "histMatchTime") (("2" (INST -1 "index!1 - 1") (("2" (SIMP) (("2" (REDUCE-IF) (("2" (SIMP) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "index2!1 - 1") (("2" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST? -) (("2" (INST? -) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST-CP + "index2!1") (("2" (INST + "index2!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (NEW-SPLIT-IF) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST-CP - "index2!1") (("2" (HIDE "next" "nextSize") (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (INST - "index2!1 - 1") (("2" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST? -) (("3" (INST - "pc!1") (("3" (SIMP) (("3" (SKOSIMP*) (("3" (INST-CP + "index2!1") (("3" (INST + "index2!1 + 1") (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "histMatchPCe") (("2" (INST - "id!1" "pc!1") (("2" (CASE "pc!1 < pc(procs!1(id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (SPLIT-ALL) NIL NIL) ("2" (HIDE "rho") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (CLEAN-UP) (("2" (LABEL "split" -1) (("2" (INST-CP + "size(hist!1) + 1") (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP) (LIFT-IF "split") (THEN (SPLIT "split") (SIMP)))) (("1" (INST + "next!1") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL) ("2" (REDUCE-ALL) (("2" (NEW-SPLIT-IF -) (("2" (CLEAN-UP) (("2" (HIDE "next" "nextSize") (("2" (REVEAL "channelsMatchProg" "channelsNonNeg") (("2" (INST?) (("2" (INST?) (("2" (SIMP) (("2" (HIDE "rho") (("2" (SKOSIMP*) (("2" (INST + "index!1") (("2" (SIMP) (("2" (REVEAL "waiting") (("2" (INST?) (("2" (SIMP) (("2" (EXPAND "inChannel") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (NEW-SPLIT-IF) (("3" (INST + "next!1") (("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL) (|histMatchTime| "" (EXP-RHO) (("" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (SPSI) (("1" (REVEAL "histMatchTime") (("1" (SKOSIMP*) (("1" (INST - "index!1") (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (LIFT-IF +) (("1" (SPSI) (("1" (SIMP) (("1" (SPSI) (("1" (NEW-SPLIT-IF -) NIL NIL) ("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL) ("2" (SPSI) (("1" (REVEAL "localTimeEarlier") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REVEAL "histMatchTime") (("2" (INST - "index!1 - 1") (("2" (SIMP) (("2" (SIMP) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (HIDE "next" "nextSize") (("2" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (SKOSIMP*) (("2" (SIMP) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho" "next" "nextSize") (("3" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("2" (SIMP) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (HIDE "rho" "next" "nextSize") (("4" (EXPAND "inChannel") (("4" (SPSI) (("1" (NEW-SPLIT-IF -) (("1" (SPSI "histMatchTime") (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (REVEAL 1) (("1" (INST + "p_id!1" "tail(channels!1(p_id!1))") (("1" (NEW-SPLIT-IF) (("1" (REVEAL "cEntryExists") (("1" (INST - "t(procs!1(p_id!1)) + 1" "p_id!1") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (REVEAL "channelTimeInc") (("1" (INST - "id!1" "id2!1" "cPoint!1" "cPoint!2") (("1" (EXPAND "preceed") (("1" (SIMP) (("1" (EXPAND "occEntry") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "id!1 = p_id!1 - 1 and cPoint!1 = head(channels!1(p_id!1 - 1))") (("1" (INST + "p_id!1" "tail(channels!1(p_id!1))") (("1" (NEW-SPLIT-IF) (("1" (REVEAL "channelsNonNeg") (("1" (INST - "p_id!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("5" (HIDE "rho" "next" "nextSize") (("5" (EXPAND "inChannel") (("5" (SPSI "toProve") (("1" (NEW-SPLIT-IF) NIL NIL) ("2" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (INST + "0" "tail(channels!1(0))") (("1" (SIMP) (("1" (REDUCE-ALL) (("1" (REVEAL "channelsNonNeg") (("1" (INST - "0") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF -) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("6" (EXPAND "inChannel") (("6" (SPSI) (("6" (HIDE "rho" "next" "nextSize") (("6" (SIMP) (("6" (SKOSIMP*) (("6" (INST + "id!1" "cPoint!1") (("6" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (HIDE "rho") (("7" (NEW-SPLIT-IF) (("1" (HIDE "next" "nextSize") (("1" (SPSI) (("1" (SPSI) (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SPSI) (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (INST + "id!1" "cPoint!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL) ("2" (SPSI) (("2" (REVEAL "histMatchTime") (("2" (INST - "index!1 - 1") (("2" (HIDE -2) (("2" (SIMP) (("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) (("2" (SKOSIMP*) (("2" (INST + "id!1" "cPoint!1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REVEAL "histMatchTimeE") (("2" (INST - "t!1") (("2" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (SKOSIMP*) (("1" (INST-CP + "index!1") (("1" (INST + "index!1 + 1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho" "next" "nextSize") (("2" (CASE "t!1 <= t(procs!1(0))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INST + "size(hist!1) + 1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho" "next" "nextSize") (("3" (NEW-SPLIT-IF) (("1" (CASE " t!1 <= t(procs!1(0)) ") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (INST + " 1 + size(hist!1)") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST-CP + "index!1") (("2" (INST + "index!1 + 1") (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL) (|histJ0write| "" (EXP-RHO) (("" (REVEAL "histJ0write") (("" (INST-CP - "index!1") (("" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= size(hist!1) + 1") (SIMP))) (("1" (HIDE "nextSize") (("1" (SPLIT-ALL) (("1" (INST? "histJ0write") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL) ("2" (SPSI) NIL NIL) ("3" (SPSI) NIL NIL) ("4" (SPSI) NIL NIL) ("5" (NEW-SPLIT-IF) (("5" (REVEAL "channelsMatchProg") (("5" (INST?) (("5" (REVEAL "channelsNonNeg") (("5" (INST?) (("5" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (SPSI) NIL NIL) ("7" (NEW-SPLIT-IF) (("1" (SPSI) NIL NIL) ("2" (SPLIT-ALL) (("1" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) NIL NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(0)), r := 1 + numRead(procs!1(0)), id := 0 #))") NIL NIL)) NIL) ("2" (INST? "histJ0write") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL) ("8" (SPSI) NIL NIL) ("9" (SPSI) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|readValuesCorrect| "" (EXP-RHO) (("" (REVEAL "readValuesCorrect") (("" (INST - "id!1" "pc!1") (("" (INTRONEXT) (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (CASE " pc!1 < pc(procs!1(id!1))") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1 + 1") (("1" (INST + "index!1") (("1" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next!1") (("2" (SIMP) (("2" (SPSI) (("2" (REVEAL "cacheEqualMemhist") (("2" (INST?) (("2" (SIMP) (("2" (INST?) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (REDUCE-ALL) NIL NIL)) NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST-CP + "index!1 + 1") (("1" (INST + "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) NIL NIL) ("3" (NEW-SPLIT-IF) NIL NIL) ("4" (EXPAND "inChannel") (("4" (NEW-SPLIT-IF) (("4" (SPSI) (("4" (REVEAL "channelsMatchProg") (("4" (INST?) (("4" (REVEAL "channelsNonNeg") (("4" (INST?) (("4" (SIMP) (("4" (HIDE "rho") (("4" (SPSI) (("1" (LIFT-IF -) (("1" (SPSI -) NIL NIL)) NIL) ("2" (REDUCE-IF) (("2" (SIMP) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (NEW-SPLIT-IF) (("1" (SPSI) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST - "index!1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) NIL NIL)) NIL) ("2" (SPSI) (("1" (SKOSIMP*) (("1" (INST + "index!1") (("1" (REVEAL "histMatchTime") (("1" (INST - "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE-ALL) NIL NIL)) NIL)) NIL) ("6" (CASE " op(instlist(0, pc(procs!1(0)))) = WRITE") (("1" (SIMP) (("1" (HIDE "rho" "next" "nextSize") (("1" (NEW-SPLIT-IF -) (("1" (SKOSIMP*) (("1" (SPSI) (("1" (INST + "index!1") (("1" (NEW-SPLIT-IF) (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTime") (("1" (INST?) (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "index!1") (("2" (REVEAL "histMatchTime") (("2" (INST?) (("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (NEW-SPLIT-IF) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) (("2" (CASE " pc!1 < pc(procs!1(id!1)) AND op(instlist(id!1, pc!1)) = READ") (("1" (SIMP) (("1" (SKOSIMP*) (("1" (SPSI) (("1" (INST-CP + "index!1 + 1") (("1" (INST + "index!1") (("1" (SPLIT-ALL) NIL NIL)) NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (NEW-SPLIT-IF) (("2" (SPSI) (("1" (INST + "next!1") (("1" (SPLIT-ALL) NIL NIL)) NIL) ("2" (SPLIT-ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (SPLIT-ALL) NIL NIL)) NIL) ("2" (INST + " next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|firstExists| "" (EXP-RHO) (("" (REVEAL "firstExists") (("" (INTRONEXT) (("1" (APPLY (THEN (CASE "next!1 <= 1 + size(hist!1)") (SIMP))) (("1" (APPLY (THEN (SPLIT-RHO) (REPLACE*) (SIMP))) (("1" (HIDE "rho") (("1" (NEW-SPLIT-IF) (("1" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("1" (SPSI -) (("1" (CLEAN-UP) (("1" (REVEAL "histMatchTimeE") (("1" (INST? :WHERE +) (("1" (REVEAL "localTimeEarlier") (("1" (INST -1 "p_id!1") (("1" (SIMP) (("1" (CASE "t(procs!1(p_id!1)) = 0") (("1" (SIMP) (("1" (REVEAL "histCompleteNumRead") (("1" (INST?) (("1" (FLATTEN) (("1" (INST - "0") (("1" (EXPAND "oc") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "lt") (("2" (EXPAND "timestamp") (("2" (SPSI "firstExists") (("1" (REVEAL "histMatchTime") (("1" (INST - "next!1") (("1" (SIMP) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REVEAL "histCompleteNumRead") (("2" (INST?) (("2" (SIMP) (("2" (INST - "0") (("2" (EXPAND "oc") (("2" (SKOSIMP*) (("2" (CLEAN-UP) (("2" (EXPAND "timestamp") (("2" (REVEAL "histLt") (("2" (INST -1 "1" "index!1") (("2" (EXPAND "lt") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE "rho") (("2" (HIDE "next" "nextSize") (("2" (NEW-SPLIT-IF) (("2" (CLEAN-UP) (("2" (REVEAL "histMatchTimeE") (("2" (INST - "1") (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE "rho") (("3" (NEW-SPLIT-IF) (("1" (HIDE "next" "nextSize") (("1" (NEW-SPLIT-IF) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "1") (("1" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NEW-SPLIT-IF) (("2" (APPLY (THEN (CASE "next!1 = 1") (SIMP))) (("2" (SPSI -) (("1" (REVEAL "histMatchTimeE") (("1" (INST - "1") (("1" (SIMP) (("1" (REVEAL "histCompleteNumRead") (("1" (INST?) (("1" (SIMP) (("1" (INST - "0") (("1" (EXPAND "oc") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "timestamp") (("2" (EXPAND "lt") (("2" (SIMP) (("2" (REVEAL "histMatchTime") (("2" (INST -1 "1") (("2" (SIMP) (("2" (SPSI "firstExists") (("2" (REPLACE*) (("2" (REPLACE*) (("2" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "next(hist!1, (# t := t(procs!1(p_id!1)), r := 1 + numRead(procs!1(p_id!1)), id := p_id!1 #))") NIL NIL)) NIL)) NIL)) NIL) (|reachable| "" (SKOSIMP*) (("" (EXPAND "reachable" +) (("" (LEMMA "memhistCorrect") (("" (LEMMA "channelsMatchProg") (("" (LEMMA " cacheEqualMemhist") (("" (LEMMA "channelsNonNeg") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "cEntryExists") (("" (LEMMA "channelTimeInc") (("" (LEMMA "localTimeEarlier") (("" (LEMMA "timeChannelProc") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "homeNotReq") (("" (LEMMA "waiting") (("" (LEMMA "histLt") (("" (LEMMA "histComplete") (("" (LEMMA "histMatchPC") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "histMatchTime") (("" (LEMMA "histJ0write") (("" (LEMMA "readValuesCorrect") (("" (LEMMA "firstExists") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (SIMP) (("" (LEMMA "idPCunique") (("" (INST?) (("" (SIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))