(vl-edgesynth-sort-edges priority-clks edgetable) → edgelist
Function:
(defun vl-edgesynth-sort-edges (priority-clks edgetable) (declare (xargs :guard (and (string-listp priority-clks) (vl-edgetable-p edgetable)))) (declare (xargs :guard (subsetp-equal priority-clks (alist-keys edgetable)))) (let ((__function__ 'vl-edgesynth-sort-edges)) (declare (ignorable __function__)) (if (atom priority-clks) nil (cons (cdr (hons-assoc-equal (car priority-clks) edgetable)) (vl-edgesynth-sort-edges (cdr priority-clks) edgetable)))))
Theorem:
(defthm vl-edgesynth-edgelist-p-of-vl-edgesynth-sort-edges (implies (and (force (string-listp priority-clks)) (force (vl-edgetable-p edgetable)) (force (subsetp-equal priority-clks (alist-keys edgetable)))) (b* ((edgelist (vl-edgesynth-sort-edges priority-clks edgetable))) (vl-edgesynth-edgelist-p edgelist))) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-edgesynth-sort-edges (equal (len (vl-edgesynth-sort-edges priority-clks edgetable)) (len priority-clks)))
Theorem:
(defthm consp-of-vl-edgesynth-sort-edges (equal (consp (vl-edgesynth-sort-edges priority-clks edgetable)) (consp priority-clks)))
Theorem:
(defthm vl-edgesynth-sort-edges-under-iff (iff (vl-edgesynth-sort-edges priority-clks edgetable) (consp priority-clks)))