(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))))
¤ 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.0.24Bemerkung:
(vorverarbeitet)
¤
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.
