		Search-engine friendly clone of the ACL2 documentation.

Observability-fix

Observability-split-supergate-aux

Signature
(observability-split-supergate-aux lits config full-size aignet) → (mv hyps rest)
Arguments: lits — Guard (lit-listp lits).; config — Guard (observability-config-p config).; full-size — Guard (natp full-size).
Returns: hyps — Type (lit-listp hyps).; rest — Type (lit-listp rest).

Definitions and Theorems

Function: observability-split-supergate-aux

(defun observability-split-supergate-aux
       (lits config full-size aignet)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (and (lit-listp lits)
                             (observability-config-p config)
                             (natp full-size))))
 (declare (xargs :guard (aignet-lit-listp lits aignet)))
 (let ((__function__ 'observability-split-supergate-aux))
   (declare (ignorable __function__))
   (b*
     (((when (atom lits)) (mv nil nil))
      (lit (lit-fix (car lits)))
      (size (count-gates-mark (lit-id lit) aignet))
      (ok (observability-size-check size full-size config))
      ((mv hyps rest)
       (observability-split-supergate-aux (cdr lits)
                                          config full-size aignet)))
     (if ok (mv (cons lit hyps) rest)
       (mv hyps (cons lit rest))))))

Theorem: lit-listp-of-observability-split-supergate-aux.hyps

(defthm lit-listp-of-observability-split-supergate-aux.hyps
  (b* (((mv ?hyps common-lisp::?rest)
        (observability-split-supergate-aux
             lits config full-size aignet)))
    (lit-listp hyps))
  :rule-classes :rewrite)

Theorem: lit-listp-of-observability-split-supergate-aux.rest

(defthm lit-listp-of-observability-split-supergate-aux.rest
  (b* (((mv ?hyps common-lisp::?rest)
        (observability-split-supergate-aux
             lits config full-size aignet)))
    (lit-listp rest))
  :rule-classes :rewrite)

Theorem: aignet-lit-listp-of-observability-split-supergate-aux

(defthm aignet-lit-listp-of-observability-split-supergate-aux
  (b* (((mv ?hyps common-lisp::?rest)
        (observability-split-supergate-aux
             lits config full-size aignet)))
    (implies (aignet-lit-listp lits aignet)
             (and (aignet-lit-listp hyps aignet)
                  (aignet-lit-listp rest aignet)))))

Theorem: eval-of-observability-split-supergate-aux

(defthm eval-of-observability-split-supergate-aux
 (b* (((mv ?hyps common-lisp::?rest)
       (observability-split-supergate-aux
            lits config full-size aignet)))
   (equal
        (b-and (aignet-eval-conjunction hyps invals regvals aignet)
               (aignet-eval-conjunction rest invals regvals aignet))
        (aignet-eval-conjunction lits invals regvals aignet))))

Theorem: observability-split-supergate-aux-of-lit-list-fix-lits

(defthm observability-split-supergate-aux-of-lit-list-fix-lits
 (equal
  (observability-split-supergate-aux (lit-list-fix lits)
                                     config full-size aignet)
  (observability-split-supergate-aux lits config full-size aignet)))

Theorem: observability-split-supergate-aux-lit-list-equiv-congruence-on-lits

(defthm
 observability-split-supergate-aux-lit-list-equiv-congruence-on-lits
 (implies
  (satlink::lit-list-equiv lits lits-equiv)
  (equal
    (observability-split-supergate-aux lits config full-size aignet)
    (observability-split-supergate-aux
         lits-equiv config full-size aignet)))
 :rule-classes :congruence)

Theorem: observability-split-supergate-aux-of-observability-config-fix-config

(defthm
 observability-split-supergate-aux-of-observability-config-fix-config
 (equal
  (observability-split-supergate-aux
       lits (observability-config-fix config)
       full-size aignet)
  (observability-split-supergate-aux lits config full-size aignet)))

Theorem: observability-split-supergate-aux-observability-config-equiv-congruence-on-config

(defthm
 observability-split-supergate-aux-observability-config-equiv-congruence-on-config
 (implies
  (observability-config-equiv config config-equiv)
  (equal
    (observability-split-supergate-aux lits config full-size aignet)
    (observability-split-supergate-aux
         lits config-equiv full-size aignet)))
 :rule-classes :congruence)

Theorem: observability-split-supergate-aux-of-nfix-full-size

(defthm observability-split-supergate-aux-of-nfix-full-size
 (equal
  (observability-split-supergate-aux lits config (nfix full-size)
                                     aignet)
  (observability-split-supergate-aux lits config full-size aignet)))

Theorem: observability-split-supergate-aux-nat-equiv-congruence-on-full-size

(defthm
 observability-split-supergate-aux-nat-equiv-congruence-on-full-size
 (implies
  (nat-equiv full-size full-size-equiv)
  (equal
    (observability-split-supergate-aux lits config full-size aignet)
    (observability-split-supergate-aux
         lits config full-size-equiv aignet)))
 :rule-classes :congruence)

Theorem: observability-split-supergate-aux-of-node-list-fix-aignet

(defthm observability-split-supergate-aux-of-node-list-fix-aignet
 (equal
  (observability-split-supergate-aux
       lits
       config full-size (node-list-fix aignet))
  (observability-split-supergate-aux lits config full-size aignet)))

Theorem: observability-split-supergate-aux-node-list-equiv-congruence-on-aignet

(defthm
 observability-split-supergate-aux-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
    (observability-split-supergate-aux lits config full-size aignet)
    (observability-split-supergate-aux
         lits config full-size aignet-equiv)))
 :rule-classes :congruence)