diff options
Diffstat (limited to 'src/proof/proof_rule.h')
| -rw-r--r-- | src/proof/proof_rule.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 173e4df9a..78e773bdc 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -713,6 +713,15 @@ enum class PfRule : uint32_t // Conclusion: (not (= (select a k) (select b k))) // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). ARRAYS_EXT, + // ======== EQ_RANGE expansion + // Children: none + // Arguments: ((eqrange a b i j)) + // ---------------------------------------- + // Conclusion: (= + // (eqrange a b i j) + // (forall ((x T)) + // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) + ARRAYS_EQ_RANGE_EXPAND, // ======== Array Trust // Children: (P1 ... Pn) // Arguments: (F) |