(svtv-to-fsm-final-thm x) → *
Function:
(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))))