$$$pvs-strategies
(defstep simp ()
  (then (flatten)(assert)(simplify)(flatten))
  " Flatten, assert, simplify"
  " ")

(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 expand-rho (&optional (inv nil))
  (then (EXPAND "rho_issue")(EXPAND "rho_execute")
        (EXPAND "rho_writeb")(EXPAND "rho_retire")(EXPAND "rho_extint")
        (EXPAND inv)
        (SKOSIMP*) (REPLACE*) (simp))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep expand-issue (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil))
  (then (EXPAND "rho_issue") (EXPAND "dispatch")(EXPAND "succ")
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (SKOSIMP*) (REPLACE*) (simp) (hide -2 -3 -4 -5 -6 -7 -8))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep exp-inv-issue (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_issue") (EXPAND "dispatch")
        (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "freeHeadROBempty")
        (EXPAND "occBuffBusyRAT")(EXPAND "occRS")(EXPAND "RATpointsNewestBuff")(EXPAND "busyRAT")
         (EXPAND "occTailROBfull")(EXPAND "activeRes")(EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual")
         (EXPAND "busyROBoccRSorActiveRes")(EXPAND "writeBoperandsNearest")
         (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")
         (EXPAND "busyOperandsNearest")(EXPAND "opsMatchROB")
        (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal")
        (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB")
         (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (EXPAND "totalIssued") (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex")
        (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer")(EXPAND "succ")
        (SKOSIMP*) (REPLACE*) (simp) (hide -2 -3 -4 -5 -6 -7 -8)
        (if (eq split 't)(then (split +)(skosimp*)(simp))(skip)))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep exp-inv-exec (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t)(hideiex f))
  (then (EXPAND "rho_execute") (EXPAND "enabled")
        (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")
         (EXPAND "occBuffBusyRAT")(EXPAND "occTailROBfull")(EXPAND "freeHeadROBempty")
        (EXPAND "RATpointsNewestBuff")(EXPAND "busyRAT")(EXPAND "occRS")(EXPAND "activeRes")(EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual")         
         (EXPAND "busyROBoccRSorActiveRes")
         (EXPAND "busyROBoccRSorActiveRes")(EXPAND "writeBoperandsNearest")
         (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB")
        (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal")
        (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB")
         (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
          (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex")
         (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer")
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2  -4 -5 -6 -7 -8)
         (if (eq hideiex 't)(hide -1)(skip))
         (if (eq split 't)(then (split +)(skosimp*)(simp))(skip))) 
   "Expands out rho, skosimps, replaces and hides" 
   " "
)


(defstep expand-exec (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil))
  (then (EXPAND "rho_execute") (EXPAND "enabled")
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2  -4 -5 -6 -7 -8 ))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep expand-writeb (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_writeb") 
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6 -7 -8 )
        (if (eq split 't)(then (split +)(skosimp*)(simp))(skip)))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep exp-inv-writeb (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_writeb") 
        (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull")
        (EXPAND "freeHeadROBempty")
        (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT")(EXPAND "RATpointsNewestBuff")
        (EXPAND "occRS")(EXPAND "activeRes")  (EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual")
         (EXPAND "busyROBoccRSorActiveRes")  (EXPAND "busyOperandsNearest")
         (EXPAND "writeBoperandsNearest")
         (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB")
        (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal")
        (EXPAND "headROBEcorrectVal")(expand "numOcc")(expand "chosenFUunique")
        (expand "busyOpBusyROB")
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
         (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex")
        (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer")
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6 -7 -8 )
         (if (eq split 't)(then (split +)(skosimp*)(simp))(skip)))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)


(defstep expand-retire (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_retire")(expand "succ") 
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (SKOSIMP*) (then (split -2) (simp) (REPLACE*) (simp) 
        (hide -1 -2 -3 -4 -5 -6 -7 )
        (if (eq split 't)(then (split 2)(skosimp*)(simp))(skip))))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep exp-inv-retire (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_retire")
        (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull")
        (EXPAND "freeHeadROBempty")
        (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT")(EXPAND "RATpointsNewestBuff")(EXPAND "occRS") 
        (EXPAND "activeRes")(EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual")
        (EXPAND "busyROBoccRSorActiveRes")(EXPAND "busyOperandsNearest")
         (EXPAND "writeBoperandsNearest")
         (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB")
        (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal")
        (EXPAND "headROBEcorrectVal")(expand "numOcc") (expand "busyOpBusyROB")
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
         (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex")
        (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer")(expand "succ") 
        (SKOSIMP*) (then (split -2) (simp) (REPLACE*) (simp) 
        (hide -1 -2 -3 -4 -5 -6 -7 )
        (if (eq split 't)(then (split 2)(skosimp*)(simp))(skip))))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep expand-extint (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil))
  (then (EXPAND "rho_extint") 
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep exp-inv-extint (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(inv5 nil)(split t))
  (then (EXPAND "rho_extint") 
        (EXPAND "wrapWraps") (EXPAND "headTailEq")(EXPAND "occEqual")(EXPAND "occTailROBfull")
        (EXPAND "freeHeadROBempty")
        (EXPAND "occBuffBusyRAT")(EXPAND "busyRAT")(EXPAND "RATpointsNewestBuff")
        (EXPAND "occRS")(EXPAND "activeRes") (EXPAND "occRSops")(EXPAND "RS_ROB_opsEqual")
        (EXPAND "busyROBoccRSorActiveRes")
         (EXPAND " busyOperandsNearest")(EXPAND "writeBoperandsNearest")
         (EXPAND "retiredOperandsMatchRF")(EXPAND "activeResOpsNotBusy")(EXPAND "opsMatchROB")
        (EXPAND "robeMatchesProg")(expand "activeResCorrectVal")(EXPAND "completedROBEcorrectVal")
        (EXPAND "headROBEcorrectVal")(expand "numOcc")(expand "busyOpBusyROB")
        (EXPAND inv1) (EXPAND inv2) (EXPAND inv3) (EXPAND inv4) (EXPAND inv5) 
         (EXPAND "issuedBefore")(expand "numOccBuffers")(expand "bufferIndex")   
  (EXPAND "weakPreceed")(expand "preceed")(expand "occ_buffer")
        (SKOSIMP*) (REPLACE*) (simp) (hide -1 -2 -4 -5 -6)
         (if (eq split 't)(then (split +)(skosimp*)(simp))(skip)))
   "Expands out rho, skosimps, replaces and hides" 
   " "
)

(defstep expand-out  (&optional (inv nil))
  (then (EXPAND "PredInv")(EXPAND "rho")(EXPAND inv)
  (SKOSIMP*) (REPLACE*) (simp) (HIDE -4 -5 -6 -7)
   )
  "Expands out the definitions, and rho, replaces and hides "
  " " 
)

(defstep expand-out-prop (&optional (inv nil)(dir +))
   (then (EXPAND "rho")(expand "TomInvariants")(skosimp*)
         (expand inv dir)(skosimp*)(replace*)(simp)(hide -4 -5 -6 -7))
   "Expands out the defintions, and rho, replaces and hides. 
    The optional invariant is only expanded in succeedents, or as specified by dir"
   " "
)  
 
(defstep do-rewrites (&optional (toexpand nil))
   (apply (then (AUTO-REWRITE-THEORY "TomPropRewrite")
                (expand toexpand)(SIMP)
                (SIMPLIFY-WITH-REWRITES :DEFS T :EXCLUDE "FUn")
                (auto-rewrite-ante)(assert)))
   "Rewrites using theory TomPropRewrite, expands an optional statement,
    simplifies, then SIMPLIFY-WITH-REWRITES"
   " Rewrites using theory TomPropRewrite, expands an optional statement,
    simplifies, then SIMPLIFY-WITH-REWRITES"
)


(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 stew (&optional lazy-match (if-match t) (defs !) rewrites theories
               exclude (updates? t) &rest lemmas)
   (then
     (if lemmas
       (let ((lemmata (if (listp lemmas) lemmas (list lemmas)))
             (x `(then ,@(loop for lemma in lemmata append `((skosimp*)(use ,lemma))))))
          x)
       (skip))
     (if lazy-match
       (then (grind$ :if-match nil :defs defs :rewrites rewrites
                     :theories theories :exclude exclude :updates? updates?)
             (reduce$ :if-match if-match :updates? updates?))
       (grind$ :if-match if-match :defs defs :rewrites rewrites
                     :theories theories :exclude exclude :updates? updates?)))
"Does a combination of (lemma) and (grind)."
  "~%Grinding away with the supplied lemmas,")

(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 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)))
                                              (tc-eq (args1 (args1 (formula sform))) *false*)))
                                   (and (conjunction? (formula sform))
                                        (or (tc-eq (args1 (formula sform)) *false*)
                                            (tc-eq (args1 (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 IMPLIES X and consequents FALSE AND Y "
   "Hide all antecedents of the form FALSE IMPLIES 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 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 auto-rewrite-ante-new (&optional (exclude nil))
  (let ( ;(fmla (formula sform))
        ( fnums (gather-fnums (s-forms (current-goal *ps*))
			      * exclude
                              #'(lambda (sform)
                                 (and (negation? (formula sform))
                                    (or  (and (forall-expr? (args1 (formula sform)))
                                              (implication? (expression (args1 (formula sform)))))
                                         (and (implication? (args1 (formula sform)))
                                               (not (equality? (args2 (args1 (formula sform) ))))))))))

        (fnum (when fnums (car fnums))))
        (if fnum
              (rewrite-all$ fnums)
              (skip-msg "Nothing to auto-rewrite")))
 " " 
 " "
)



(defstep auto-rewrite-ante (&optional (exclude nil))
  (let ( ;(fmla (formula sform))
        ( fnums (gather-fnums (s-forms (current-goal *ps*))
			      * exclude
                              #'(lambda (sform)
                                 (and (negation? (formula sform))
                                    (or  (and (forall-expr? (args1 (formula sform)))
                                              (implication? (expression (args1 (formula sform)))))
                                         (implication? (args1 (formula sform))))))))

        (fnum (when fnums (car fnums))))
        (if fnum
              (rewrite-all$ fnums)
              (skip-msg "Nothing to auto-rewrite")))
 " " 
 " "
)



(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 my-hide-all-but (keepnums &optional (hidefrom *))
   (let ((fnums (gather-fnums (s-forms (current-goal *ps*))
                              hidefrom keepnums)))
     (hide :fnums fnums))
  "Hides all sequent formulas"
  "Hiding" )



(defstep prove-rewrites (&optional (prop nil))
  (apply (then (EXPAND prop)(skosimp*)(iff)(then (split)(skosimp*)(repeat* (then (split 1)(skosimp*))))))
  "Expands out the definitions, and rho, replaces and hides "
  " " 
)

$$$TomRefinesSeq.pvs
TomRefinesSeq[N, R, U, Z: posnat]: THEORY
 BEGIN
  
  IMPORTING seq[N, R], TomInvs[N, R, U, Z]
  
  reg, reg_p: VAR [REG_ID -> VALUE]
  
  RF, RF_p: VAR [REG_ID -> R_TYPE]
  
  rs, rs_p, rsprev: VAR [FU_ID, SLOT_ID -> S_TYPE]
  
  res, res_p: VAR [FU_ID -> result_TYPE]
  
  top, top_p: VAR upto_nz[1 + N]
  
  O_C(RF): [REG_ID -> VALUE] = (LAMBDA (r: REG_ID): pv(RF(r)))
  
  O_A(reg): [REG_ID -> VALUE] = reg
  
  reg_I(RF): [REG_ID -> VALUE] = (LAMBDA (r: REG_ID): 0)
  
  reg_del(top, top_p, reg): [REG_ID -> VALUE] =
    (LAMBDA (r: REG_ID):
       IF top <= N AND top /= top_p AND r = t(prog(top))
         THEN
         do_op(op(prog(top)), reg(src(prog(top))(1)), reg(src(prog(top))(2)))
       ELSE reg(r)
       ENDIF)
  
  alpha(top, res, RF, rs, reg): boolean = O_C(RF) = O_A(reg)
  
  R1: LEMMA
        Tomasulo.Theta(top, res, RF, rs)
            IMPLIES
          (seq.THETA(top, reg_I(RF)) AND alpha(top, res, RF, rs, reg_I(RF)))
  
  R2: LEMMA
        (Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
             AND alpha(top, res, RF, rs, reg))
            IMPLIES
          (seq.rho(top, reg, top_p, reg_del(top, top_p, reg))
               AND alpha(top_p, res_p, RF_p, rs_p, reg_del(top, top_p, reg)))
  
  R3: LEMMA alpha(top, res, RF, rs, reg) IMPLIES O_C(RF) = O_A(reg)
  
  R3a: LEMMA
        (term(rs)
             AND alpha(top, res, RF, rs, reg) AND TomInvariants(res, RF, rs))
            IMPLIES (FORALL (r: REG_ID): v(RF(r)) = reg(r))
  
  END TomRefinesSeq








$$$TomRefinesSeq.prf
(|TomRefinesSeq| (|reg_del_TCC1| "" (SUBTYPE-TCC) NIL)
 (|reg_del_TCC2| "" (SUBTYPE-TCC) NIL)
 (|reg_del_TCC3| "" (SUBTYPE-TCC) NIL)
 (R1 "" (EXPAND "Theta")
  (("" (EXPAND "THETA")
    (("" (EXPAND "alpha")
      (("" (SKOSIMP*)
        (("" (EXPAND "reg_I")
          (("" (EXPAND "O_C")
            (("" (SPLIT)
              (("1" (PROPAX) NIL)
               ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                (("2" (GRIND-BEST) NIL)))
               ("3" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                (("3" (GRIND-BEST) NIL)))))))))))))))))
 (R2 "" (EXPAND "rho")
  (("" (EXPAND "alpha")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (HIDE -4 -5 -6 -7)
          (("" (SIMP)
            (("" (EXPAND "O_A")
              (("" (EXPAND "O_C")
                (("" (SIMP)
                  (("" (EXPAND "reg_del")
                    (("" (SPLIT +)
                      (("1" (SIMP)
                        (("1" (EXPAND "dispatch")
                          (("1" (NEW-SPLIT-IF)
                            (("1" (INST 1 "false")
                              (("1"
                                (SIMP)
                                (("1"
                                  (APPLY-EXTENSIONALITY 1 :HIDE? T)
                                  (("1"
                                    (LIFT-IF)
                                    (("1" (SPLIT-ALL) NIL)))))))))
                             ("2" (INST? +)
                              (("2"
                                (APPLY-EXTENSIONALITY 2 :HIDE? T)
                                NIL)))))))))
                       ("2" (EXPAND "dispatch")
                        (("2" (REPLACE -4 :DIR RL)
                          (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                            (("1" (SPLIT-ALL) NIL) ("2" (SKOSIMP*) NIL)
                             ("3" (SKOSIMP*) NIL) ("4" (SKOSIMP*) NIL)
                             ("5" (SKOSIMP*) NIL)
                             ("6" (SKOSIMP*)
                              (("6"
                                (APPLY-EXTENSIONALITY 2 :HIDE? T)
                                NIL)))
                             ("7" (APPLY-EXTENSIONALITY 2 :HIDE? T)
                              (("7"
                                (SIMP)
                                NIL)))))))))))))))))))))))))))))))
 (R3 "" (EXPAND "alpha")
  (("" (EXPAND "O_C") (("" (EXPAND "O_A") (("" (SKOSIMP*) NIL)))))))
 (|R3a| "" (EXPAND "alpha")
  (("" (EXPAND "O_C")
    (("" (EXPAND "O_A")
      (("" (EXPAND "TomInvariants")
        (("" (SKOSIMP*)
          (("" (EXPAND "RFpredCorrectProp")
            (("" (INST?)
              (("" (EXPAND " termNotBusyRFprop")
                (("" (SIMP)
                  (("" (INST?)
                    (("" (SIMP)
                      (("" (REPLACE -2 :DIR RL)
                        (("" (SIMP) NIL))))))))))))))))))))))))))

$$$Tomasulo.pvs
Tomasulo[N, R, U, Z: posnat]: THEORY
 BEGIN
  
  IMPORTING more_nat_types, Tdef[N, R, U, Z]
  
  RF, RF_p: VAR [REG_ID -> R_TYPE]
  
  rs, rs_p: VAR [FU_ID, SLOT_ID -> S_TYPE]
  
  res, res_p: VAR [FU_ID -> result_TYPE]
  
  top, top_p: VAR upto_nz[1 + N]
  
  FU: VAR FU_ID
  
  S: VAR SLOT_ID
  
  r: VAR REG_ID
  
  op0: OP_TYPE
  
  Theta(top, res, RF, rs): bool =
    top = 1
        AND
      (FORALL FU:
         res(FU)
             = (# a := FALSE,
                  rt :=
                    (# b := FALSE,
                       p := (# f := 0, s := 0 #),
                       v := 0,
                       pv := 0 #),
                  t := 0 #))
          AND
        (FORALL r:
           RF(r)
               = (# b := FALSE, p := (# f := 0, s := 0 #), v := 0, pv := 0 #))
            AND
          (FORALL (FU: FU_ID[N, R, U, Z], S: SLOT_ID[N, R, U, Z]):
             rs(FU, S)
                 = (# oc := FALSE,
                      rt :=
                        (# b := FALSE,
                           p := (# f := 0, s := 0 #),
                           v := 0,
                           pv := 0 #),
                      op := op0,
                      t := 0,
                      ss :=
                        (LAMBDA (i: TWO):
                           (# b := FALSE,
                              p := (# f := 0, s := 0 #),
                              v := 0,
                              pv := 0 #))
                      #))
  
  rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p): bool =
    EXISTS (master: upto[U], Sn: upto[Z],
            iex: [FU_ID -> upto[Z]], delay: [FU_ID -> bool]):
      (Sn > 0 IMPLIES dispatch(top, rs, Sn))
          AND
        (FORALL (FU: FU_ID):
           iex(FU) > 0 IMPLIES enabled(rs, FU, iex(FU)) AND NOT a(res(FU)))
            AND (master > 0 IMPLIES bus_active(res, master))
              AND top_p = IF Sn > 0 THEN 1 + top ELSE top ENDIF
                AND res_p
                  =
                (LAMBDA (FU: FU_ID):
                   IF iex(FU) > 0 AND NOT delay(FU)
                     THEN (# a := TRUE,
                             rt :=
                               (# b := FALSE,
                                  p := p(rt(rs(FU, iex(FU)))),
                                  v :=
                                    do_op(op(rs(FU, iex(FU))),
                                          v(ss(rs(FU,
                                                  iex(FU)))(1)),
                                          v(ss(rs(FU,
                                                  iex(FU)))(2))),
                                  pv := pv(rt(rs(FU, iex(FU)))) #),
                             t := t(rs(FU, iex(FU))) #)
                   ELSE
                     (# a := a(res(FU)) AND NOT (master > 0 AND FU = master),
                        rt := rt(res(FU)),
                        t := t(res(FU)) #)
                   ENDIF)
                  AND RF_p
                    =
                  (LAMBDA (r: REG_ID):
                     IF Sn > 0 AND r = t(prog(top))
                       THEN (# b := TRUE,
                               p := (# f := FUn(top), s := Sn #),
                               v := 0,
                               pv :=
                                 do_op(op(prog(top)),
                                       pv(RF(src(prog(top))(1))),
                                       pv(RF(src(prog(top))(2))))
                               #)
                     ELSIF master > 0
                             AND b(RF(t(res(master))))
                               AND p(RF(t(res(master)))) = p(rt(res(master)))
                                 AND r = t(res(master))
                       THEN (# b := b(rt(res(master))),
                               p := p(rt(res(master))),
                               v := v(rt(res(master))),
                               pv := pv(RF(r)) #)
                     ELSE RF(r)
                     ENDIF)
                    AND rs_p
                      =
                    (LAMBDA (FU: FU_ID, S: SLOT_ID):
                       IF Sn > 0 AND FU = FUn(top) AND S = Sn
                         THEN (# oc := TRUE,
                                 rt :=
                                   (# b := TRUE,
                                      p :=
                                        (# f := FUn(top),
                                           s := Sn #),
                                      v := 0,
                                      pv :=
                                        do_op(op(prog(top)),
                                              pv
                                                (RF
                                                   (src(prog(top))(1))),
                                              pv
                                                (RF
                                                   (src(prog(top))(2))))
                                      #),
                                 op := op(prog(top)),
                                 t := t(prog(top)),
                                 ss :=
                                   (LAMBDA (j: TWO):
                                      IF master > 0
                                              AND
                                            b(RF(src(prog(top))(j)))
                                                AND
                                              p(RF(src(prog(top))(j)))
                                                  = p(rt(res(master)))
                                        THEN (# b := FALSE,
                                                p :=
                                                  p(rt(res(master))),
                                                v :=
                                                  v(rt(res(master))),
                                                pv :=
                                                  pv
                                                    (RF
                                                       (src(prog(top))(j)))
                                                #)
                                      ELSE RF(src(prog(top))(j))
                                      ENDIF)
                                 #)
                       ELSIF NOT delay(FU) AND iex(FU) > 0 AND S = iex(FU)
                         THEN (# oc := oc(rs(FU, S)),
                                 rt :=
                                   (# b := FALSE,
                                      p := p(rt(rs(FU, S))),
                                      v :=
                                        do_op(op(rs(FU, S)),
                                              v(ss(rs(FU,
                                                      S))(1)),
                                              v(ss(rs(FU,
                                                      S))(2))),
                                      pv := pv(rt(rs(FU, S))) #),
                                 op := op(rs(FU, S)),
                                 t := t(rs(FU, S)),
                                 ss := ss(rs(FU, S)) #)
                       ELSIF master > 0 AND oc(rs(FU, S))
                         THEN
                         (# oc :=
                              oc(rs(FU, S))
                                  AND NOT
                                  (FU = f(p(rt(res(master))))
                                       AND S
                                         = s(p(rt(res(master))))),
                            rt := rt(rs(FU, S)),
                            op := op(rs(FU, S)),
                            t := t(rs(FU, S)),
                            ss :=
                              (LAMBDA (j: TWO):
                                 IF b(ss(rs(FU, S))(j))
                                         AND p(ss(rs(FU, S))(j))
                                           = p(rt(res(master)))
                                   THEN (# b := FALSE,
                                           p := p(ss(rs(FU, S))(j)),
                                           v := v(rt(res(master))),
                                           pv := pv(ss(rs(FU, S))(j))
                                           #)
                                 ELSE ss(rs(FU, S))(j)
                                 ENDIF)
                            #)
                       ELSE rs(FU, S)
                       ENDIF)
  
  END Tomasulo



$$$Tomasulo.prf
(|Tomasulo| (|rho_TCC1| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC2| "" (SUBTYPE-TCC) NIL) (|rho_TCC3| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC4| "" (SUBTYPE-TCC) NIL) (|rho_TCC5| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC6| "" (SUBTYPE-TCC) NIL) (|rho_TCC7| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC8| "" (SUBTYPE-TCC) NIL) (|rho_TCC9| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC10| "" (SUBTYPE-TCC) NIL) (|rho_TCC11| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC12| "" (SUBTYPE-TCC) NIL) (|rho_TCC13| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC14| "" (SUBTYPE-TCC) NIL) (|rho_TCC15| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC16| "" (SUBTYPE-TCC) NIL) (|rho_TCC17| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC18| "" (SUBTYPE-TCC) NIL) (|rho_TCC19| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC20| "" (SUBTYPE-TCC) NIL) (|rho_TCC21| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC22| "" (SUBTYPE-TCC) NIL) (|rho_TCC23| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC24| "" (SUBTYPE-TCC) NIL) (|rho_TCC25| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC26| "" (SUBTYPE-TCC) NIL))

$$$Tdef.pvs
Tdef[N, R, U, Z: posnat]: THEORY
 BEGIN
  
  IMPORTING def[N, R]
  
  FU_ID: TYPE = upto_nz[U]
  
  SLOT_ID: TYPE = upto_nz[Z]
  
  HW_NAME: TYPE = [# f: upto[U], s: upto[Z] #]
  
  I_NAME: TYPE = INST_INDEXz
  
  PRODUCER: TYPE = [# f: upto[U], s: upto[Z] #]
  
  BUSY: TYPE = bool
  
  OCCUPIED: TYPE = bool
  
  ACTIVE: TYPE = bool
  
  R_TYPE: TYPE = [# b: BUSY, p: PRODUCER, v: VALUE, pv: VALUE #]
  
  SRC_TYPE: TYPE = [TWO -> R_TYPE]
  
  S_TYPE:
      TYPE =
        [# oc: OCCUPIED, rt: R_TYPE, op: OP_TYPE, t: TARGET, ss: SRC_TYPE #]
  
  result_TYPE: TYPE = [# a: ACTIVE, rt: R_TYPE, t: TARGET #]
  
  fu_table: FUNCTION[OP_TYPE -> FU_ID]
  
  rs: VAR [FU_ID, SLOT_ID -> S_TYPE]
  
  res: VAR [FU_ID -> result_TYPE]
  
  top: VAR upto_nz[1 + N]
  
  master: VAR upto[U]
  
  bus_active(res, master): bool = master > 0 AND a(res(master))
  
  FUn(top): FU_ID = fu_table(op(prog(IF top < N THEN top ELSE N ENDIF)))
  
  Sn: VAR upto[Z]
  
  dispatch(top, rs, Sn): bool =
    (Sn > 0 AND top <= N AND NOT oc(rs(FUn(top), Sn)))
  
  FU: VAR FU_ID
  
  S: VAR upto[Z]
  
  enabled(rs, FU, S): bool =
    S > 0
        AND b(rt(rs(FU, S)))
          AND NOT b(ss(rs(FU, S))(1))
            AND NOT b(ss(rs(FU, S))(2)) AND oc(rs(FU, S))
  
  END Tdef



$$$Tdef.prf
(|Tdef| (|bus_active_TCC1| "" (SUBTYPE-TCC) NIL)
 (|FUn_TCC1| "" (SUBTYPE-TCC) NIL) (|FUn_TCC2| "" (SUBTYPE-TCC) NIL)
 (|dispatch_TCC1| "" (SUBTYPE-TCC) NIL) (|enabled_TCC1| "" (SUBTYPE-TCC) NIL)
 (|enabled_TCC2| "" (SUBTYPE-TCC) NIL) (|enabled_TCC3| "" (SUBTYPE-TCC) NIL))

$$$TomDefs.pvs
TomDefs[N, R, U, Z: posnat]: THEORY
 BEGIN
  
  IMPORTING def[N, R], Tdef[N, R, U, Z]
  
  RF, RF_p: VAR [REG_ID -> R_TYPE]
  
  rs, rs_p, rsprev: VAR [FU_ID, SLOT_ID -> S_TYPE]
  
  res, res_p: VAR [FU_ID -> result_TYPE]
  
  top, top_p: VAR upto_nz[1 + N]
  
  FU: VAR FU_ID
  
  S: VAR SLOT_ID
  
  r: VAR REG_ID
  
  rc: VAR R_TYPE
  
  rse: VAR S_TYPE
  
  j: TWO
  
  prodProp(res, rs): bool =
    (FORALL (FU: FU_ID, S: SLOT_ID):
       (oc(rs(FU, S))
            IMPLIES f(p(rt(rs(FU, S)))) = FU AND s(p(rt(rs(FU, S)))) = S)
           AND (a(res(FU)) IMPLIES f(p(rt(res(FU)))) = FU))
  
  resRSsameTargetProp(res, rs): boolean =
    (FORALL FU:
       a(res(FU))
           IMPLIES
         (s(p(rt(res(FU)))) > 0
              AND f(p(rt(res(FU)))) > 0
                AND oc(rs(f(p(rt(res(FU)))), s(p(rt(res(FU))))))
                  AND t(res(FU))
                    = t(rs(f(p(rt(res(FU)))), s(p(rt(res(FU))))))))
  
  RF_RSsameTargetProp(RF, rs): boolean =
    (FORALL (r: REG_ID):
       b(RF(r))
           IMPLIES
         (f(p(RF(r))) > 0
              AND s(p(RF(r))) > 0
                AND oc(rs(f(p(RF(r))), s(p(RF(r)))))
                  AND t(rs(f(p(RF(r))), s(p(RF(r))))) = r))
  
  ActiveResNotBusyProp(res): boolean =
    (FORALL (FU: FU_ID): (a(res(FU)) IMPLIES NOT b(rt(res(FU)))))
  
  term(rs): bool = FORALL (FU: FU_ID, S: SLOT_ID): NOT oc(rs(FU, S))
  
  termNotBusyRFprop(rs, RF): bool =
    term(rs) IMPLIES NOT (EXISTS (r: REG_ID): b(RF(r)))
  
  RegRSequalPredProp(rs, RF): boolean =
    (FORALL r:
       b(RF(r))
           IMPLIES
         (f(p(RF(r))) > 0
              AND s(p(RF(r))) > 0
                AND oc(rs(f(p(RF(r))), s(p(RF(r)))))
                  AND pv(RF(r)) = pv(rt(rs(f(p(RF(r))), s(p(RF(r))))))))
  
  ResRSequalPredProp(rs, res): boolean =
    (FORALL FU:
       a(res(FU))
           IMPLIES
         (f(p(rt(res(FU)))) > 0
              AND s(p(rt(res(FU)))) > 0
                AND oc(rs(f(p(rt(res(FU)))), s(p(rt(res(FU))))))
                  AND pv(rt(res(FU)))
                    = pv(rt(rs(f(p(rt(res(FU)))), s(p(rt(res(FU)))))))))
  
  SSpredEqualRSprop(rs): boolean =
    (FORALL FU, S, (j: TWO):
       (oc(rs(FU, S)) AND b(ss(rs(FU, S))(j)))
           IMPLIES
         (f(p(ss(rs(FU, S))(j))) > 0
              AND s(p(ss(rs(FU, S))(j))) > 0
                AND oc(rs(f(p(ss(rs(FU, S))(j))), s(p(ss(rs(FU, S))(j)))))
                  AND pv(ss(rs(FU, S))(j))
                    =
                  pv(rt(rs(f(p(ss(rs(FU, S))(j))), s(p(ss(rs(FU, S))(j))))))))
  
  RSpredEqualsDoOpProp(rs): boolean =
    (FORALL FU, S:
       oc(rs(FU, S))
           IMPLIES pv(rt(rs(FU, S)))
             =
           do_op(op(rs(FU, S)), pv(ss(rs(FU, S))(1)), pv(ss(rs(FU, S))(2))))
  
  ResPredCorrectProp(res): boolean =
    (FORALL FU: a(res(FU)) IMPLIES pv(rt(res(FU))) = v(rt(res(FU))))
  
  RFpredCorrectProp(RF): boolean =
    (FORALL r: NOT b(RF(r)) IMPLIES pv(RF(r)) = v(RF(r)))
  
  SSpredCorrectProp(rs): boolean =
    (FORALL FU, S, (j: TWO):
       oc(rs(FU, S)) AND NOT b(ss(rs(FU, S))(j))
           IMPLIES v(ss(rs(FU, S))(j)) = pv(ss(rs(FU, S))(j)))
  
  active((rc: R_TYPE), res, rs, RF): boolean =
    (EXISTS (r: REG_ID): rc = RF(r) AND b(RF(r)))
        OR (EXISTS (FU: FU_ID): (a(res(FU)) AND rc = rt(res(FU))))
          OR
        (EXISTS (FU: FU_ID[N, R, U, Z], S: SLOT_ID[N, R, U, Z]):
           oc(rs(FU, S))
               AND
             (rc = rt(rs(FU, S))
                  OR
                (EXISTS (j: TWO):
                   rc = ss(rs(FU, S))(j) AND b(ss(rs(FU, S))(j)))))
  
  predMatchProp(res, rs, RF): boolean =
    (FORALL (rc1: R_TYPE, rc2: R_TYPE):
       (active(rc1, res, rs, RF)
            AND active(rc2, res, rs, RF) AND p(rc1) = p(rc2))
           IMPLIES pv(rc1) = pv(rc2))
  
  END TomDefs

$$$TomDefs.prf
(|TomDefs| (|resRSsameTargetProp_TCC1| "" (SUBTYPE-TCC) NIL)
 (|resRSsameTargetProp_TCC2| "" (SUBTYPE-TCC) NIL)
 (|RF_RSsameTargetProp_TCC1| "" (SUBTYPE-TCC) NIL)
 (|RF_RSsameTargetProp_TCC2| "" (SUBTYPE-TCC) NIL)
 (|SSpredEqualRSprop_TCC1| "" (SUBTYPE-TCC) NIL)
 (|SSpredEqualRSprop_TCC2| "" (SUBTYPE-TCC) NIL)
 (|RSpredEqualsDoOpProp_TCC1| "" (SUBTYPE-TCC) NIL)
 (|RSpredEqualsDoOpProp_TCC2| "" (SUBTYPE-TCC) NIL))

$$$TomInvs.pvs
TomInvs[N, R, U, Z: posnat]: THEORY
 BEGIN
  
  IMPORTING TomDefs[N, R, U, Z:posnat], Tomasulo[N, R, U, Z]
  
  RF, RF_p: VAR [REG_ID -> R_TYPE]
  
  rs, rs_p, rsprev: VAR [FU_ID, SLOT_ID -> S_TYPE]
  
  res, res_p: VAR [FU_ID -> result_TYPE]
  
  top, top_p: VAR upto_nz[1 + N]
  
  FU: VAR FU_ID
  
  S: VAR SLOT_ID
  
  r: VAR REG_ID
  
  rc: VAR R_TYPE
  
  rse: VAR S_TYPE
  
  j: TWO
  
  prodLemma: LEMMA
        (Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
             AND prodProp(res, rs))
            IMPLIES prodProp(res_p, rs_p)
  
  ActiveResNotBusy: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND ActiveResNotBusyProp(res)
            IMPLIES ActiveResNotBusyProp(res_p)
  
  resRSsameTarget: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND resRSsameTargetProp(res, rs) AND prodProp(res, rs)
            IMPLIES resRSsameTargetProp(res_p, rs_p)
  
  RF_RSsameTarget: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND RF_RSsameTargetProp(RF, rs)
              AND prodProp(res, rs)
                AND ActiveResNotBusyProp(res) AND resRSsameTargetProp(res, rs)
            IMPLIES RF_RSsameTargetProp(RF_p, rs_p)
  
  RSpredEqualsDoOp: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND RSpredEqualsDoOpProp(rs)
            IMPLIES RSpredEqualsDoOpProp(rs_p)
  
  RegRSequalPred: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND RegRSequalPredProp(rs, RF)
              AND ActiveResNotBusyProp(res)
                AND resRSsameTargetProp(res, rs)
                  AND RF_RSsameTargetProp(RF, rs)
            IMPLIES RegRSequalPredProp(rs_p, RF_p)
  
  SSpredEqualRS: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND SSpredEqualRSprop(rs) AND RegRSequalPredProp(rs, RF)
            IMPLIES SSpredEqualRSprop(rs_p)
  
  ResRSequalPred: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND ResRSequalPredProp(rs, res) AND prodProp(res, rs)
            IMPLIES ResRSequalPredProp(rs_p, res_p)
  
  predMatch: LEMMA
        RegRSequalPredProp(rs, RF)
            AND SSpredEqualRSprop(rs)
              AND ResRSequalPredProp(rs, res) AND prodProp(res, rs)
            IMPLIES predMatchProp(res, rs, RF)
  
  ResPredCorrect: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND ResPredCorrectProp(res)
              AND RSpredEqualsDoOpProp(rs) AND SSpredCorrectProp(rs)
            IMPLIES ResPredCorrectProp(res_p)
  
  SSpredCorrect: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND SSpredCorrectProp(rs)
              AND ResPredCorrectProp(res)
                AND RFpredCorrectProp(RF) AND predMatchProp(res, rs, RF)
            IMPLIES SSpredCorrectProp(rs_p)
  
  RFpredCorrect: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND RFpredCorrectProp(RF)
              AND ResPredCorrectProp(res) AND predMatchProp(res, rs, RF)
            IMPLIES RFpredCorrectProp(RF_p)
  
  termNotBusyRF: LEMMA
        RF_RSsameTargetProp(RF, rs) IMPLIES termNotBusyRFprop(rs, RF)
  
  TomInvariants(res, RF, rs): bool =
    prodProp(res, rs)
        AND resRSsameTargetProp(res, rs)
          AND RF_RSsameTargetProp(RF, rs)
            AND ActiveResNotBusyProp(res)
              AND termNotBusyRFprop(rs, RF)
                AND RegRSequalPredProp(rs, RF)
                  AND ResRSequalPredProp(rs, res)
                    AND SSpredEqualRSprop(rs)
                      AND RSpredEqualsDoOpProp(rs)
                        AND ResPredCorrectProp(res)
                          AND RFpredCorrectProp(RF)
                            AND SSpredCorrectProp(rs)
                              AND predMatchProp(res, rs, RF)
  
  AllInv: LEMMA
        Tomasulo.rho(top, res, RF, rs, top_p, res_p, RF_p, rs_p)
            AND TomInvariants(res, RF, rs)
            IMPLIES TomInvariants(res_p, RF_p, rs_p)
  
  END TomInvs

$$$TomInvs.prf
(|TomInvs|
 (|prodLemma| "" (EXPAND "rho")
  (("" (EXPAND "prodProp")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            (("" (EXPAND "enabled")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "dispatch")
                  (("" (INST?)
                    (("" (SPLIT-ALL)
                      (("1" (INST?) (("1" (SIMP) NIL)))
                       ("2" (INST?) (("2" (SIMP) NIL)))
                       ("3" (INST?) (("3" (SIMP) (("3" (SIMP) NIL)))))
                       ("4" (INST-CP -8 "FU!1" "S!1")
                        (("4" (INST -8 "FU!1" "iex!1(FU!1)")
                          (("4" (SIMP) (("4" (SIMP) NIL)))))))
                       ("5" (INST-CP -6 "FU!1" "S!1")
                        (("5" (INST -6 "FU!1" "iex!1(FU!1)")
                          (("5" (SIMP) (("5" (SIMP) NIL)))))))
                       ("6" (INST?)
                        (("6" (SIMP)
                          (("6" (SIMP) (("6" (SIMP) NIL)))))))
                       ("7" (INST?)
                        (("7" (SIMP)
                          (("7" (GROUND) NIL)))))))))))))))))))))))))))
 (|ActiveResNotBusy| "" (EXPAND "rho")
  (("" (EXPAND "ActiveResNotBusyProp")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (HIDE -4 -5 -6 -7) (("" (GRIND-BEST) NIL)))))))))))
 (|resRSsameTarget| "" (EXPAND "rho")
  (("" (EXPAND "resRSsameTargetProp")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            (("" (EXPAND "dispatch")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "enabled")
                  (("" (INST?)
                    (("" (INST?)
                      (("" (EXPAND "prodProp")
                        (("" (SPLIT-ALL)
                          (("1" (INST?)
                            (("1" (SIMP) (("1" (SIMP) NIL)))))
                           ("2" (INST?)
                            (("2" (SIMP) (("2" (SIMP) NIL)))))
                           ("3" (INST?)
                            (("3" (SIMP) (("3" (SIMP) NIL)))))
                           ("4" (INST?)
                            (("4" (SIMP) (("4" (SIMP) NIL)))))
                           ("5" (INST-CP -10 "FU!1" "1")
                            (("5" (INST -10 "master!1" "1")
                              (("5"
                                (SIMP)
                                NIL)))))))))))))))))))))))))))))))
 (|RF_RSsameTarget| "" (EXPAND "rho")
  (("" (EXPAND "RF_RSsameTargetProp")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            (("" (EXPAND "dispatch")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "enabled")
                  (("" (INST?)
                    (("" (INST -4 "r!1")
                      (("" (EXPAND "prodProp")
                        (("" (SPLIT-ALL)
                          (("1" (EXPAND "ActiveResNotBusyProp")
                            (("1" (INST?)
                              (("1" (INST?) (("1" (SIMP) NIL)))))))
                           ("2" (HIDE -5 -6 -8 -9 2 3 4)
                            (("2" (HIDE -7 -8)
                              (("2"
                                (EXPAND "resRSsameTargetProp")
                                (("2"
                                  (INST?)
                                  (("2"
                                    (SIMP)
                                    (("2"
                                      (APPLY-EXTENSIONALITY 1 :HIDE? T)
                                      NIL)))))))))))))))))))))))))))))))))))))
 (|RSpredEqualsDoOp| "" (EXPAND "rho")
  (("" (EXPAND "RSpredEqualsDoOpProp")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            ((""
              (EXPAND "enabled
")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "dispatch")
                  (("" (INST?)
                    (("" (INSTBEST)
                      (("" (SPLIT-ALL -) NIL)))))))))))))))))))))))
 (|RegRSequalPred| "" (SKOSIMP*)
  (("" (EXPAND "rho")
    (("" (EXPAND "RegRSequalPredProp")
      (("" (SKOSIMP*)
        (("" (EXPAND "dispatch")
          (("" (EXPAND "bus_active")
            (("" (EXPAND "enabled")
              (("" (REPLACE*)
                (("" (SIMP)
                  (("" (HIDE -4 -5 -6 -7)
                    (("" (INSTBEST -4)
                      (("" (SPLIT-ALL)
                        (("1" (EXPAND "ActiveResNotBusyProp")
                          (("1" (SPLIT-ALL) (("1" (GRIND-BEST) NIL)))))
                         ("2" (EXPAND "resRSsameTargetProp")
                          (("2" (EXPAND "RF_RSsameTargetProp")
                            (("2" (INSTBEST)
                              (("2"
                                (SIMP)
                                (("2"
                                  (INST?)
                                  (("2"
                                    (INSTBEST)
                                    (("2"
                                      (SIMP)
                                      (("2"
                                        (REPLACE*)
                                        (("2"
                                          (SIMP)
                                          (("2"
                                            (APPLY-EXTENSIONALITY
                                             1
                                             :HIDE?
                                             T)
                                            NIL)))))))))))))))))))))))))))))))))))))))))))
 (|SSpredEqualRS| "" (SKOSIMP*)
  (("" (EXPAND "SSpredEqualRSprop")
    (("" (EXPAND "rho")
      (("" (SKOSIMP*)
        (("" (EXPAND "dispatch")
          (("" (EXPAND "enabled")
            (("" (EXPAND "bus_active")
              (("" (REPLACE*)
                (("" (SIMP)
                  (("" (HIDE -4 -5 -6 -7)
                    (("" (EXPAND "RegRSequalPredProp")
                      (("" (SPLIT-ALL)
                        (("1" (INSTBEST)
                          (("1" (INSTBEST -11) (("1" (SIMP) NIL)))))
                         ("2" (INST? -12)
                          (("2" (SIMP) (("2" (SIMP) NIL)))))
                         ("3" (INST? -10)
                          (("3" (SIMP) (("3" (SIMP) NIL)))))
                         ("4" (INST? -11)
                          (("4" (SIMP) (("4" (SIMP) NIL)))))
                         ("5" (INST? -11)
                          (("5" (SIMP)
                            (("5" (SIMP)
                              (("5"
                                (SIMP)
                                (("5"
                                  (APPLY-EXTENSIONALITY 2 :HIDE? T)
                                  NIL)))))))))
                         ("6" (INST? -9) (("6" (SIMP) NIL)))
                         ("7" (INST?)
                          (("7" (INST?) (("7" (SPLIT-ALL -) NIL)))))
                         ("8" (SPLIT-ALL -)
                          (("1" (INST?)
                            (("1" (SIMP)
                              (("1"
                                (INST?)
                                (("1" (SIMP) (("1" (SIMP) NIL)))))))))
                           ("2" (INST?)
                            (("2" (INST?)
                              (("2" (SIMP) (("2" (SIMP) NIL)))))))
                           ("3" (INST?)
                            (("3" (INST?)
                              (("3" (SIMP) (("3" (SIMP) NIL)))))))))
                         ("9" (INSTBEST)
                          (("9" (INST?)
                            (("9" (SPLIT-ALL -)
                              (("1" (ASSERT :FLUSH? T) NIL)
                               ("2"
                                (APPLY-EXTENSIONALITY 1 :HIDE? T)
                                NIL)))))))
                         ("10" (INSTBEST)
                          (("10" (INST?)
                            (("10" (SPLIT-ALL -)
                              NIL)))))))))))))))))))))))))))))
 (|ResRSequalPred| "" (EXPAND "ResRSequalPredProp")
  (("" (EXPAND "rho")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (EXPAND "dispatch")
          (("" (EXPAND "bus_active")
            (("" (EXPAND "enabled")
              (("" (HIDE -4 -5 -6 -7)
                (("" (SIMP)
                  (("" (INSTBEST)
                    (("" (INSTBEST)
                      (("" (EXPAND "prodProp")
                        (("" (SPLIT-ALL)
                          (("1" (GRIND-BEST) NIL)
                           ("2" (GRIND-BEST) NIL)
                           ("3" (GRIND-BEST) NIL)
                           ("4" (GRIND-BEST) NIL)
                           ("5" (INST-CP -10 "FU!1" "1")
                            (("5" (INST -10 "master!1" "1")
                              (("5"
                                (SIMP)
                                NIL)))))))))))))))))))))))))))))))
 (|predMatch| "" (EXPAND " predMatchProp")
  (("" (EXPAND "active")
    (("" (SKOSIMP*)
      (("" (EXPAND "RegRSequalPredProp")
        (("" (EXPAND "ResRSequalPredProp")
          (("" (EXPAND "SSpredEqualRSprop")
            (("" (EXPAND "prodProp")
              (("" (APPLY (THEN (SPLIT) (SKOSIMP*) (SIMP)))
                (("1" (INST-CP -3 "r!1")
                  (("1" (SIMP)
                    (("1" (APPLY (THEN (SPLIT) (SKOSIMP*) (SIMP)))
                      (("1" (INST -5 "r!2") (("1" (SIMP) NIL)))
                       ("2" (INST?)
                        (("2" (INST? -11) (("2" (SIMP) NIL)))))
                       ("3" (GRIND-BEST) NIL)))))))
                 ("2" (INST-CP -5 "FU!1")
                  (("2" (SIMP)
                    (("2" (APPLY (THEN (SPLIT) (SKOSIMP*) (SIMP)))
                      (("1" (GRIND-BEST) NIL)
                       ("2" (INST -7 "FU!2") (("2" (SIMP) NIL)))
                       ("3" (GRIND-BEST) NIL)))))))
                 ("3" (SPLIT)
                  (("1" (INST-CP -6 "FU!1" "S!1")
                    (("1" (SIMP)
                      (("1" (SIMP)
                        (("1"
                          (APPLY (THEN (SPLIT -10) (SKOSIMP*) (SIMP)))
                          (("1" (GRIND-BEST) NIL)
                           ("2" (GRIND-BEST) NIL)
                           ("3" (SPLIT -)
                            (("1" (INST -8 "FU!2" "S!2")
                              (("1" (SIMP) (("1" (SIMP) NIL)))))
                             ("2" (SKOSIMP*)
                              (("2" (GRIND-BEST) NIL)))))))))))))
                   ("2" (SKOSIMP*)
                    (("2" (INST-CP -5 "FU!1" "S!1" "j!1")
                      (("2" (SIMP)
                        (("2" (APPLY (THEN (SPLIT) (SKOSIMP*) (SIMP)))
                          (("1" (GRIND-BEST) NIL)
                           ("2" (GRIND-BEST) NIL)
                           ("3" (SPLIT)
                            (("1" (INST -13 "FU!2" "S!2")
                              (("1" (SIMP) (("1" (SIMP) NIL)))))
                             ("2" (SKOSIMP*)
                              (("2"
                                (INST -8 "FU!2" "S!2" "j!2")
                                (("2"
                                  (SIMP)
                                  NIL)))))))))))))))))))))))))))))))))
 (|ResPredCorrect| "" (EXPAND "ResPredCorrectProp")
  (("" (EXPAND "rho")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            (("" (INST?)
              (("" (EXPAND "dispatch")
                (("" (EXPAND "enabled")
                  (("" (INST?)
                    (("" (EXPAND "RSpredEqualsDoOpProp")
                      (("" (EXPAND "SSpredCorrectProp")
                        (("" (SPLIT-ALL)
                          (("" (INST?)
                            (("" (INST-CP -8 "FU!1" "iex!1(FU!1)" "1")
                              ((""
                                (INST -8 "FU!1" "iex!1(FU!1)" "2")
                                ((""
                                  (SIMP)
                                  NIL)))))))))))))))))))))))))))))))))
 (|SSpredCorrect| "" (EXPAND "SSpredCorrectProp")
  (("" (EXPAND "rho")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -4 -5 -6 -7)
            (("" (EXPAND "enabled")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "dispatch")
                  (("" (INST?)
                    (("" (INSTBEST)
                      (("" (EXPAND "ResPredCorrectProp")
                        (("" (EXPAND "predMatchProp")
                          (("" (EXPAND "RFpredCorrectProp")
                            (("" (SPLIT-ALL)
                              (("1"
                                (INST?)
                                (("1"
                                  (INST?)
                                  (("1"
                                    (INST?)
                                    (("1" (GRIND) NIL)))))))
                               ("2"
                                (INST?)
                                (("2" (INST?) (("2" (SIMP) NIL)))))
                               ("3"
                                (INST?)
                                (("3"
                                  (HIDE -10)
                                  (("3"
                                    (INST?)
                                    (("3"
                                      (HIDE -5 -6 -8 1 2 3)
                                      (("3"
                                        (GRIND)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|RFpredCorrect| "" (EXPAND "RFpredCorrectProp")
  (("" (EXPAND "rho")
    (("" (SKOSIMP*)
      (("" (REPLACE*)
        (("" (SIMP)
          (("" (HIDE -2 -5 -6 -7 -4)
            (("" (EXPAND "dispatch")
              (("" (EXPAND "bus_active")
                (("" (EXPAND "ResPredCorrectProp")
                  (("" (EXPAND "predMatchProp")
                    (("" (INSTBEST)
                      (("" (SPLIT-ALL)
                        (("" (INST?)
                          (("" (INST?)
                            (("" (GRIND)
                              NIL)))))))))))))))))))))))))))))
 (|termNotBusyRF| "" (GRIND-BEST) NIL)
 (|AllInv| "" (EXPAND "TomInvariants")
  (("" (SKOSIMP*)
    (("" (LEMMA "prodLemma")
      (("" (LEMMA "resRSsameTarget")
        (("" (LEMMA "RF_RSsameTarget")
          (("" (INST?)
            (("" (INST?)
              (("" (INST?)
                (("" (SIMP)
                  (("" (LEMMA "ActiveResNotBusy")
                    (("" (LEMMA "ActiveResNotBusyRS")
                      (("" (LEMMA "termNotBusyRF")
                        (("" (LEMMA "RegRSequalPred")
                          (("" (INST?)
                            (("" (INST?)
                              ((""
                                (INST?)
                                ((""
                                  (INST?)
                                  ((""
                                    (SIMP)
                                    ((""
                                      (LEMMA "termNotBusyRF")
                                      ((""
                                        (INST? :WHERE +)
                                        ((""
                                          (SIMP)
                                          ((""
                                            (LEMMA " ResRSequalPred")
                                            ((""
                                              (LEMMA "SSpredEqualRS")
                                              ((""
                                                (LEMMA
                                                 " RSpredEqualsDoOp")
                                                ((""
                                                  (LEMMA
                                                   "ResPredCorrect")
                                                  ((""
                                                    (INST?)
                                                    ((""
                                                      (INST?)
                                                      ((""
                                                        (INST?)
                                                        ((""
                                                          (INST?)
                                                          ((""
                                                            (SIMP)
                                                            ((""
                                                              (LEMMA
                                                               "RFpredCorrect")
                                                              ((""
                                                                (LEMMA
                                                                 "SSpredCorrect")
                                                                ((""
                                                                  (INST?)
                                                                  ((""
                                                                    (INST?)
                                                                    ((""
                                                                      (SIMP)
                                                                      ((""
                                                                        (LEMMA
                                                                         "predMatch")
                                                                        ((""
                                                                          (INST?
                                                                           :WHERE
                                                                           +)
                                                                          ((""
                                                                            (SIMP)
                                                                            NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

$$$def.pvs
def[N: posnat, R: posnat]: THEORY
 BEGIN
  
  IMPORTING more_nat_types
  
  REG_ID: TYPE = upto[R]
  
  TARGET: TYPE = REG_ID
  
  VALUE: TYPE = real
  
  OP_TYPE: TYPE+
  
  TWO: TYPE = upto_nz[2]
  
  SRC: TYPE = [TWO -> REG_ID]
  
  INST: TYPE = [# op: OP_TYPE, t: TARGET, src: SRC #]
  
  INST_INDEX: TYPE = upto_nz[N]
  
  INST_INDEXz: TYPE = upto[N]
  
  prog: [INST_INDEX -> INST]
  
  do_op: FUNCTION[OP_TYPE, VALUE, VALUE -> VALUE]
  
  lw((i: INST_INDEXz), (r: REG_ID)):
      RECURSIVE
        INST_INDEXz = (IF i = 0 THEN 0
                       ELSIF t(prog(i)) = r THEN i
                       ELSE lw(i - 1, r)
                       ENDIF)
       MEASURE (LAMBDA (i: INST_INDEXz, r: REG_ID): i)
  
  reg0((r: REG_ID)): VALUE = 0
  
  END def

$$$def.prf
(|def| (|lw_TCC1| "" (SUBTYPE-TCC) NIL) (|lw_TCC2| "" (SUBTYPE-TCC) NIL)
 (|lw_TCC3| "" (TERMINATION-TCC) NIL))

$$$more_nat_types.pvs
more_nat_types [m: posnat]: THEORY

  BEGIN

  upto_nz : TYPE = {i: upto[m] | NOT i = 0} CONTAINING m

  END more_nat_types

$$$more_nat_types.prf
(|more_nat_types| (|upto_nz_TCC1| "" (SUBTYPE-TCC) NIL)
 (|upto_nz_TCC2| "" (SUBTYPE-TCC) NIL))

$$$seq.pvs
seq[N: posnat, R: posnat]: THEORY
 BEGIN
  
  IMPORTING more_nat_types, def[N, R]
  
  top, top_p: VAR upto_nz[N + 1]
  
  reg, reg_p: VAR [REG_ID[N, R] -> VALUE]
  
  delay: VAR bool
  
  THETA(top, reg): bool = (top = 1 AND reg = reg0)
  
  rho(top, reg, top_p, reg_p): bool =
    EXISTS delay:
      (NOT delay
           AND top <= N
             AND top_p = top + 1
               AND reg_p
                 = reg
                 WITH [(t(prog(top))) :=
                         do_op(op(prog(top)),
                               reg(src(prog(top))(1)),
                               reg(src(prog(top))(2)))])
          OR (top_p = top AND reg_p = reg)
  
  END seq



$$$seq.prf
(|seq| (|top_TCC1| "" (SAME-NAME-TCC) NIL) (|rho_TCC1| "" (SUBTYPE-TCC) NIL)
 (|rho_TCC2| "" (SUBTYPE-TCC) NIL) (|rho_TCC3| "" (SUBTYPE-TCC) NIL))