		Search-engine friendly clone of the ACL2 documentation.

Semantics

Nxsts-comb-equiv

Combinational equivalence of aignets, considering only next-states

outs-comb-equiv says that two aignets' next-states are combinationally equivalent, that is, the next-states of corresponding registers evaluate to the same value under the same input/register assignment.

Definitions and Theorems

Theorem: nxsts-comb-equiv-necc

(defthm nxsts-comb-equiv-necc
  (implies (nxsts-comb-equiv aignet aignet2)
           (equal (equal (nxst-eval n invals regvals aignet)
                         (nxst-eval n invals regvals aignet2))
                  t)))

Theorem: nxsts-comb-equiv-implies-lit-eval-of-nxst

(defthm nxsts-comb-equiv-implies-lit-eval-of-nxst
  (implies (nxsts-comb-equiv aignet aignet2)
           (equal (equal (lit-eval (lookup-reg->nxst n aignet)
                                   invals regvals aignet)
                         (lit-eval (lookup-reg->nxst n aignet2)
                                   invals regvals aignet2))
                  t)))

Theorem: nxsts-comb-equiv-is-an-equivalence

(defthm nxsts-comb-equiv-is-an-equivalence
  (and (booleanp (nxsts-comb-equiv x y))
       (nxsts-comb-equiv x x)
       (implies (nxsts-comb-equiv x y)
                (nxsts-comb-equiv y x))
       (implies (and (nxsts-comb-equiv x y)
                     (nxsts-comb-equiv y z))
                (nxsts-comb-equiv x z)))
  :rule-classes (:equivalence))

Theorem: nxsts-comb-equiv-implies-equal-nxst-eval-4

(defthm nxsts-comb-equiv-implies-equal-nxst-eval-4
  (implies (nxsts-comb-equiv aignet aignet-equiv)
           (equal (nxst-eval n invals regvals aignet)
                  (nxst-eval n invals regvals aignet-equiv)))
  :rule-classes (:congruence))

Theorem: nxsts-comb-equiv-of-node-list-fix-aignet

(defthm nxsts-comb-equiv-of-node-list-fix-aignet
  (equal (nxsts-comb-equiv (node-list-fix aignet)
                           aignet2)
         (nxsts-comb-equiv aignet aignet2)))

Theorem: nxsts-comb-equiv-node-list-equiv-congruence-on-aignet

(defthm nxsts-comb-equiv-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (nxsts-comb-equiv aignet aignet2)
                  (nxsts-comb-equiv aignet-equiv aignet2)))
  :rule-classes :congruence)

Theorem: nxsts-comb-equiv-of-node-list-fix-aignet2

(defthm nxsts-comb-equiv-of-node-list-fix-aignet2
  (equal (nxsts-comb-equiv aignet (node-list-fix aignet2))
         (nxsts-comb-equiv aignet aignet2)))

Theorem: nxsts-comb-equiv-node-list-equiv-congruence-on-aignet2

(defthm nxsts-comb-equiv-node-list-equiv-congruence-on-aignet2
  (implies (node-list-equiv aignet2 aignet2-equiv)
           (equal (nxsts-comb-equiv aignet aignet2)
                  (nxsts-comb-equiv aignet aignet2-equiv)))
  :rule-classes :congruence)