Function-variable-dependency
Notion of dependency on function variables.
A term term depends on
a function variable fvar
iff fvar occurs in term
or fvar is one of the function variables that
a second-order
function that occurs in term depends on..
A second-order function
sofun depends on a function variable fvar
iff its body, guard, or (if present) measure depends on fvar.
A second-order theorem
sothm depends on a function variable fvar
iff its formula depends on fvar.
Examples
Example 1
Given
(defunvar ?f (*) => *)
(defunvar ?g (*) => *)
(defun2 h[?f] (x) (?f (cons x 3)))
the term (h[?f] (?g a)) depends exactly on ?g and ?f.
Example 2
Given
(defunvar ?f (*) => *)
(defunvar ?g (*) => *)
(defun2 h[?f] (x) (?f (cons x 3)))
(defun2 k[?f][?g] (a) (h[?f] (?g a)))
the function k[?f][?g] depends exactly on ?g and ?f.
Example 3
Given
(defunvar ?f (*) => *)
(defunvar ?g (*) => *)
(defun2 h[?f] (x) (?f (cons x 3)))
(defthm th (h[?f] (?g a)))
the theorem th depends exactly on ?g and ?f.
