|
|
|---|
|
|
|
|---|
Proof rule for the empty list of constraints expressed as any atom.
The empty list of constraints is always satisfied. Indeed, lists of constraints are conjunctions.
Here we phrase the rule in terms of atom
so that it is more generally applicable to proving other rules
without having to require the list of constraints
to be a true list (of constraints).
The rule constraint-list-satp-of-nil is a specialized version
for the case of an empty list expressed as
Theorem:
(defthm constraint-list-satp-of-atom (implies (atom constrs) (constraint-list-satp constrs defs asg p)))