		Search-engine friendly clone of the ACL2 documentation.

Semantics

Outs-comb-equiv

Combinational equivalence of aignets, considering only primary outputs

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

Definitions and Theorems

Theorem: outs-comb-equiv-necc

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

Theorem: outs-comb-equiv-implies-lit-eval-of-fanin

(defthm
 outs-comb-equiv-implies-lit-eval-of-fanin
 (implies
      (outs-comb-equiv aignet aignet2)
      (equal (equal (lit-eval (fanin 0 (lookup-stype n :po aignet))
                              invals regvals aignet)
                    (lit-eval (fanin 0 (lookup-stype n :po aignet2))
                              invals regvals aignet2))
             t)))

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

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

Theorem: outs-comb-equiv-implies-equal-output-eval-4

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

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

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

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

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

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

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

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

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