		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)