		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)