		Search-engine friendly clone of the ACL2 documentation.

Invert

Invert-outer-loop

Add all parent dependencies to all children.

Signature
(invert-outer-loop nodes graph acc) → acc
Arguments: nodes — The parent nodes we still need to process. Originally the alist-keys of graph. We use this instead of recurring down graph to properly avoid shadowed pairs.; graph — The graph we're inverting, remains constant.; acc — The new, inverted graph we're building.
Returns: acc — Extended by adding parents for each child for the remaining nodes.

Definitions and Theorems

Function: invert-outer-loop

(defun invert-outer-loop (nodes graph acc)
  (declare (xargs :guard t))
  (let ((__function__ 'invert-outer-loop))
    (declare (ignorable __function__))
    (b* (((when (atom nodes)) acc)
         (parent1 (car nodes))
         (children1 (cdr (hons-get parent1 graph)))
         (acc (invert-inner-loop parent1 children1 acc)))
      (invert-outer-loop (cdr nodes)
                         graph acc))))

Theorem: invert-outer-loop-when-atom

(defthm invert-outer-loop-when-atom
  (implies (atom nodes)
           (equal (invert-outer-loop nodes graph acc)
                  acc)))

Theorem: invert-outer-loop-correct

(defthm invert-outer-loop-correct
  (let ((new-acc (invert-outer-loop nodes graph acc)))
    (iff (member par
                 (cdr (hons-assoc-equal child new-acc)))
         (or (member par (cdr (hons-assoc-equal child acc)))
             (and (member par nodes)
                  (member child
                          (cdr (hons-assoc-equal par graph))))))))