|
|
|---|
|
|
|
|---|
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.
Theorem:
(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))))