Create a list of doublets for functional instantiation.
(sothm-inst-pairs fsbs wrld) → pairs
From a function substitution obtained by extending an instantiation
via ext-fun-subst-term/terms/function,
the list of pairs to supply to
In addition, when a dotted pair is encountered
whose car is the name of a quantifier second-order function,
an extra pair for instantiating the associated witness is inserted.
The witnesses of quantifier second-order functions
must also be part of the
Function:
(defun sothm-inst-pairs (fsbs wrld) (declare (xargs :guard (and (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'sothm-inst-pairs)) (declare (ignorable __function__)) (if (endp fsbs) nil (let* ((pair (car fsbs)) (1st (car pair)) (2nd (cdr pair))) (if (quant-sofunp 1st wrld) (let ((1st-wit (defun-sk-witness 1st wrld)) (2nd-wit (defun-sk-witness 2nd wrld))) (cons (list 1st 2nd) (cons (list 1st-wit 2nd-wit) (sothm-inst-pairs (cdr fsbs) wrld)))) (cons (list 1st 2nd) (sothm-inst-pairs (cdr fsbs) wrld)))))))