		Search-engine friendly clone of the ACL2 documentation.

Program-equivalence

Program-equivp

Equivalence of two programs.

This binary relation is indeed an equivalence: reflexive, symmetric, and transitive.

Definitions and Theorems

Theorem: program-equivp-necc

(defthm program-equivp-necc
  (implies
       (program-equivp program1 program2)
       (implies (and (symbol-valuep function)
                     (value-listp arguments))
                (equal (exec-call function arguments program1)
                       (exec-call function arguments program2)))))

Theorem: booleanp-of-program-equivp

(defthm booleanp-of-program-equivp
  (b* ((yes/no (program-equivp program1 program2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: program-equivp-reflexive

(defthm program-equivp-reflexive
  (program-equivp program program))

Theorem: program-equivp-symmetic

(defthm program-equivp-symmetic
  (implies (program-equivp program1 program2)
           (program-equivp program2 program1))
  :rule-classes nil)

Theorem: program-equivp-transitive

(defthm program-equivp-transitive
  (implies (and (program-equivp program1 program2)
                (program-equivp program2 program3))
           (program-equivp program1 program3)))