		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Transunit-ensemble-split-fn-when-loop

Signature
(transunit-ensemble-split-fn-when-loop tunits triggers steps) → (mv er? tunits$)
Arguments: tunits — Guard (transunit-ensemblep tunits).; triggers — Guard (ident-setp triggers).
Returns: er? — Type (maybe-msgp er?).; tunits$ — Type (transunit-ensemblep tunits$).

Definitions and Theorems

Function: transunit-ensemble-split-fn-when-loop

(defun transunit-ensemble-split-fn-when-loop (tunits triggers steps)
  (declare (type (unsigned-byte 60) steps))
  (declare (xargs :guard (and (transunit-ensemblep tunits)
                              (ident-setp triggers))))
  (b* (((reterr) (irr-transunit-ensemble))
       ((when (= 0
                 (mbe :logic (nfix steps)
                      :exec (acl2::the-fixnat steps))))
        (retmsg$ "Out of steps."))
       ((erp found tunits$)
        (transunit-ensemble-try-split-fn-when tunits triggers))
       ((unless found) (retok tunits$)))
    (transunit-ensemble-split-fn-when-loop
         tunits$ triggers (- steps 1))))

Theorem: maybe-msgp-of-transunit-ensemble-split-fn-when-loop.er?

(defthm maybe-msgp-of-transunit-ensemble-split-fn-when-loop.er?
  (b*
   (((mv ?er? ?tunits$)
     (transunit-ensemble-split-fn-when-loop tunits triggers steps)))
   (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: transunit-ensemblep-of-transunit-ensemble-split-fn-when-loop.tunits$

(defthm
 transunit-ensemblep-of-transunit-ensemble-split-fn-when-loop.tunits$
 (b*
  (((mv ?er? ?tunits$)
    (transunit-ensemble-split-fn-when-loop tunits triggers steps)))
  (transunit-ensemblep tunits$))
 :rule-classes :rewrite)