		Search-engine friendly clone of the ACL2 documentation.
Svtv-to-fsm
Svtv-to-fsm-final-thm

Signature
(svtv-to-fsm-final-thm x) → *
Definitions and Theorems

Function: svtv-to-fsm-final-thm
(defun svtv-to-fsm-final-thm (x)
 (declare (xargs :guard t))
 (let ((__function__ 'svtv-to-fsm-final-thm))
  (declare (ignorable __function__))
  (b*
   (((svtv-to-fsm-thm x))
    ((with-fast x.bindings x.outmap x.triple-val-alist))
    ((mv var-bindings1 cycle-eqns1)
     (svtv-to-fsm-final-thm-var-bindings
          x.input-vars x.bindings nil 'envs
          x))
    ((mv var-bindings2 cycle-eqns2)
     (svtv-to-fsm-final-thm-var-bindings x.remaining-override-vars
                                         x.bindings :val 'envs
                                         x))
    ((mv var-bindings3 cycle-eqns3)
     (svtv-to-fsm-final-thm-var-bindings
          x.all-eliminated-override-vars
          x.bindings nil 'outs
          x))
    ((mv var-bindings4 cycle-eqns4)
     (svtv-to-fsm-final-thm-var-bindings
          x.output-vars x.outmap nil 'outs
          x))
    (var-bindings (append var-bindings1 var-bindings2
                          var-bindings3 var-bindings4))
    (cycle-eqns-all (append cycle-eqns1
                            cycle-eqns2 cycle-eqns3 cycle-eqns4))
    (cycle-eqns
     (case x.cycle-num-rewrite-strategy
      (:single-var (cons (cons 'natp
                               (cons x.base-cycle-var 'nil))
                         'nil))
      (t
        (b*
         ((first-cycle-eqn
               (cdr (assoc-eq x.primary-output-var cycle-eqns-all)))
          (rest-cycle-eqns
               (remove-equal first-cycle-eqn
                             (strip-cdrs cycle-eqns-all))))
         (if first-cycle-eqn (cons first-cycle-eqn rest-cycle-eqns)
           (cons (cons 'natp
                       (cons x.base-cycle-var 'nil))
                 rest-cycle-eqns))))))
    (- (and (member-eq nil cycle-eqns)
            (raise "Error: generated hyp of NIL"))))
   (acl2::template-subst
    *svtv-to-fsm-final-thm-template*
    :atom-alist
    (cons
     (cons '<fsmname> x.fsmname)
     (cons
      (cons '<hyp> x.hyp)
      (cons
       (cons '<concl> x.concl)
       (cons
        (cons '<run-length> x.run-length)
        (cons
         (cons '<svtv-spec-thmname>
               x.svtv-spec-thmname)
         (cons
          (cons '<specname> x.svtv-spec)
          (cons
             (cons '<override-test-envs>
                   (cons 'quote
                         (cons x.override-test-envs 'nil)))
             (cons (cons '<basecycle> x.base-cycle-var)
                   (cons (cons '<thmname> x.thmname)
                         (cons (cons '<rule-classes> x.rule-classes)
                               'nil))))))))))
    :splice-alist
    (cons (cons '<bindings> var-bindings)
          (cons (cons '<cycle-num-equations> cycle-eqns)
                'nil))
    :str-alist
    (cons (cons '"<SVTVNAME>"
                (symbol-name x.svtv))
          (cons (cons '"<SPECNAME>"
                      (symbol-name x.svtv-spec))
                (cons (cons '"<THMNAME>"
                            (symbol-name x.thmname))
                      (cons (cons '"<FSMNAME>"
                                  (symbol-name x.fsmname))
                            'nil))))
    :pkg-sym x.pkg-sym))))