		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-satp-of-relation

Proof rule for relation application constraints.

This says that the satisfaction of a relation application constraint reduces to constraint-relation-satp.

This rule lets us dispense with the existentially quantified proof tree, limiting the existential quantification to the extended assignment in constraint-relation-satp. Some existential quantification is unavoidable in general, but the one for the extended assignment is simpler to handle than the one for the whole proof tree.

Definitions and Theorems

Theorem: constraint-satp-of-relation

(defthm constraint-satp-of-relation
 (implies
   (and (assignmentp asg)
        (assignment-wfp asg p)
        (constraint-case constr :relation))
   (equal
        (constraint-satp constr defs asg p)
        (constraint-relation-satp (constraint-relation->name constr)
                                  (constraint-relation->args constr)
                                  defs asg p))))