|
(in-package :pvs)
(defun split-rewrite* (form vars dir)
(cond ((or (equation? form)(iff? form))
;;checks if rhs freevars are in given + lhs freevars.
(let ((lhs (if (string-equal dir 'rl)(args2 form)(args1 form)))
(rhs (if (string-equal dir 'rl)(args1 form)(args2 form))))
(if
(subsetp (freevars rhs)
(append vars
(freevars lhs))
:test #'same-declaration);;NSH(11.2.94)
(values lhs rhs nil)
(values form *true* nil))))
((implication? form)
(multiple-value-bind (lhs rhs hyp)
(split-rewrite* (args2 form) vars dir)
(values lhs rhs
(if (null hyp) (args1 form)
(make-conjunction (list (args1 form) hyp))))))
((negation? form)
(values (args1 form) *false* nil))
(t (values form *true* nil))))
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
