Event: Start with the library "interpreter".

;;;List Operations

Theorem: car-append car (append (a, b)) = if listp (a) then car (a)

else car (b) endif

Theorem: listp-append listp (append (a, b)) = (listp (a) ∨ listp (b))

Theorem: length-append length (append (a, b)) = (length (a) + length (b))

Definition: plistp (list) = if listp (list) then plistp (cdr (list))

else list = nil endif

Theorem: plistp-append-plistp plistp (append (a, b)) = plistp (b)

Theorem: append-plistp-nil (append (a, nil) = a) = plistp (a)

Theorem: not-lessp-count-append (count (x) + count (y)) ≮ count (append (x, y))

Definition: all-numberps (list) = if listp (list)

then if car (list) ∈ N then all-numberps (cdr (list))

else f endif else t endif

Theorem: all-numberps-implies (all-numberps (list) ∧ (e ∈ list)) → (e ∈ N)

;;;Set Operations

Definition: setp (list) = if listp (list)

then if car (list) ∈ cdr (list) then f else setp (cdr (list)) endif

else t endif Theorem: setp-append ((¬ setp (a)) ∨ (¬ setp (b))) → (¬ setp (append (a, b)))

Theorem: setp-member ((x ∈ a) ∧ (x ∈ b)) → (¬ setp (append (a, b)))

Theorem: setp-append-cons setp (append (a, cons (x, b))) = setp (cons (x, append (a, b)))

Theorem: setp-append-not-listp (¬ listp (b)) → (setp (append (a, b)) = setp (a))

Theorem: setp-append-canonicalize setp (append (a, b)) = setp (append (b, a))

Theorem: setp-member-1 (setp (append (a, b)) ∧ (x ∈ b)) → (x ∉ a)

Theorem: setp-member-2 (setp (append (a, b)) ∧ (x ∈ a)) → (x ∉ b)

;;;Subset Operations

Definition: sublistp (sub, list) = if listp (sub) then (car (sub) ∈ list) ∧ sublistp (cdr (sub), list)

else t endif

Theorem: sublistp-append sublistp (append (a, b), list) = (sublistp (a, list) ∧ sublistp (b, list))

Theorem: member-of-sublistp-is-member ((a ∈ b) ∧ sublistp (b, c)) → (a ∈ c)

Theorem: sublistp-of-sublistp-is-sublistp (sublistp (a, b) ∧ sublistp (b, c)) → sublistp (a, c)

Theorem: sublistp-normalize (¬ plistp (b)) → (sublistp (a, b) = sublistp (a, append (b, nil)))

Definition: sei (a, b) = if listp (a) then sei (cdr (a), append (b, list (car (a))))

else t endif Theorem: sublistp-easy sublistp (a, append (b, a))

Theorem: sublistp-reflexive sublistp (a, a)

Theorem: sublistp-in-append (sublistp (x, a) ∨ sublistp (x, b)) → sublistp (x, append (a, b))

Theorem: sublistp-in-cons sublistp (a, y) → sublistp (a, cons (x, y))

;;;Tree Operations

Definition: nodes-rec (flag, tree) = if listp (tree)

then if flag = 'tree then cons (car (tree), nodes-rec ('forest, cdr (tree))) else append (nodes-rec ('tree, car (tree)),

nodes-rec ('forest, cdr (tree))) endif

else nil endif

Definition: nodes (tree) = nodes-rec ('tree, tree)

Definition: roots (forest) = if listp (forest) then cons (caar (forest), roots (cdr (forest)))

else forest endif

Definition: children-rec (flag, node, tree) = if listp (tree)

then if flag = 'tree

then if car (tree) = node

then append (roots (cdr (tree)),

children-rec ('forest, node, cdr (tree)))

else children-rec ('forest, node, cdr (tree)) endif else append (children-rec ('tree, node, car (tree)),

children-rec ('forest, node, cdr (tree))) endif

else nil endif

Definition: children (node, tree) = children-rec ('tree, node, tree)

Definition: parent-rec (flag, node, tree) = if listp (tree)

then if flag = 'tree

then if node ∈ roots (cdr (tree))

then cons (car (tree), parent-rec ('forest, node, cdr (tree))) else parent-rec ('forest, node, cdr (tree)) endif

else append (parent-rec ('tree, node, car (tree)),

parent-rec ('forest, node, cdr (tree))) endif

else nil endif

Definition: parent (node, tree) = car (parent-rec ('tree, node, tree))

Definition: proper-tree (flag, tree) = if flag = 'tree

then if listp (tree) then proper-tree ('forest, cdr (tree))

else f endif elseif listp (tree) then proper-tree ('tree, car (tree))

∧ proper-tree ('forest, cdr (tree)) else tree = nil endif

Theorem: canonicalize-nodes-rec-flag nodes-rec (flag, tree) = if flag = 'tree then nodes-rec ('tree, tree)

else nodes-rec ('forest, tree) endif

Theorem: canonicalize-proper-tree-flag proper-tree (flag, tree) = if flag = 'tree then proper-tree ('tree, tree)

else proper-tree ('forest, tree) endif

Theorem: canonicalize-parent-rec-flag parent-rec (flag, child, tree) = if flag = 'tree then parent-rec ('tree, child, tree)

else parent-rec ('forest, child, tree) endif

Theorem: canonicalize-children-rec-flag children-rec (flag, parent, tree) = if flag = 'tree then children-rec ('tree, parent, tree)

else children-rec ('forest, parent, tree) endif

Theorem: not-flag-tree ((flag ≠ 'tree) ∧ (flag ≠ 'forest)) → ((nodes-rec (flag, tree) = nodes-rec ('forest, tree))

∧ (proper-tree (flag, tree) = proper-tree ('forest, tree)) ∧ (parent-rec (flag, child, tree)

= parent-rec ('forest, child, tree)) ∧ (children-rec (flag, parent, tree)

= children-rec ('forest, parent, tree)))

Theorem: parent-rec-children-rec (child ∈ children-rec (flag, parent, tree)) = (parent ∈ parent-rec (flag, child, tree))

Event: Disable parent-rec-children-rec.

Theorem: plistp-children-rec plistp (children-rec (flag, parent, tree))

Theorem: plistp-parent-rec plistp (parent-rec (flag, child, tree))

Theorem: plistp-roots proper-tree ('forest, forest) → plistp (roots (forest))

Theorem: member-roots-member-forest (proper-tree ('forest, forest) ∧ (node ∈ roots (forest))) → (node ∈ nodes-rec ('forest, forest))

Theorem: not-member-no-parent (proper-tree (flag, tree) ∧ (node ∉ nodes-rec (flag, tree))) → (parent-rec (flag, node, tree) = nil)

Theorem: member-child-tree (proper-tree (flag, tree) ∧ (child ∈ children-rec (flag, node, tree))) → (child ∈ nodes-rec (flag, tree))

Theorem: setp-tree-unique-parent (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree))) → (parent-rec (flag, child, tree)

= if child ∈ nodes-rec (flag, tree)

then if ((flag = 'tree) ∧ (car (tree) = child))

∨ ((flag ≠ 'tree)

∧ (child ∈ roots (tree))) then nil else list (car (parent-rec (flag, child, tree))) endif

else nil endif)

Event: Disable setp-tree-unique-parent.

Theorem: member-parent-parent (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree)) ∧ (parent ∈ parent-rec (flag, child, tree))) → (parent-rec (flag, child, tree) = list (parent))

Theorem: parent-of-child (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree)) ∧ (child ∈ children-rec (flag, parent, tree))) → (parent-rec (flag, child, tree) = list (parent))

Theorem: member-parent-member-tree (parent ∈ parent-rec (flag, child, tree)) → (parent ∈ nodes-rec (flag, tree))

Theorem: node-that-has-child-is-in-tree listp (children-rec (flag, parent, tree)) → (parent ∈ nodes-rec (flag, tree))

Theorem: node-that-has-parent-is-in-tree (proper-tree (flag, tree) ∧ listp (parent-rec (flag, child, tree))) → (child ∈ nodes-rec (flag, tree))

Theorem: sublistp-children-generalized (proper-tree (flag, tree) ∧ sublistp (children, children-rec (flag, parent, tree))) → sublistp (children, nodes-rec (flag, tree))

Event: Disable sublistp-children-generalized.

Theorem: sublistp-children proper-tree (flag, tree) → sublistp (children-rec (flag, parent, tree), nodes-rec (flag, tree))

Definition: subtreep (flag, subtree, tree) = if listp (tree) ∧ listp (subtree)

then if flag = 'tree

then if subtree = tree then t

else subtreep ('forest, subtree, cdr (tree)) endif elseif subtreep ('tree, subtree, car (tree)) then t else subtreep ('forest, subtree, cdr (tree)) endif

else f endif Definition: subtrees (flag, tree) = if listp (tree)

then if flag = 'tree then cons (tree, subtrees ('forest, cdr (tree))) else append (subtrees ('tree, car (tree)),

subtrees ('forest, cdr (tree))) endif

else nil endif

Theorem: subtreep-subtrees (subtree ∈ subtrees (flag, tree)) → subtreep (flag, subtree, tree)

Definition: next-level (subtrees) = if listp (subtrees)

then append (cdar (subtrees), next-level (cdr (subtrees)))

else subtrees endif

Theorem: nodes-rec-forest-append nodes-rec ('forest, append (a, b)) = append (nodes-rec ('forest, a), nodes-rec ('forest, b))

Theorem: next-level-reduces-count listp (subtrees) → (count (next-level (subtrees)) < count (subtrees))

Theorem: next-level-of-tree-in-subtrees proper-tree ('forest, forest) → sublistp (forest, subtrees ('forest, forest))

Theorem: subtrees-of-subtree-in-complete-subtrees (proper-tree ('tree, subtree) ∧ (subtree ∈ subtrees (flag, tree))) → sublistp (subtrees ('tree, subtree), subtrees (flag, tree))

Theorem: subtrees-of-subtrees-in-complete-subtrees (proper-tree ('forest, subtrees) ∧ sublistp (subtrees, subtrees (flag, tree))) → sublistp (subtrees ('forest, subtrees), subtrees (flag, tree))

Theorem: next-level-in-subtrees-forest proper-tree ('forest, subtrees) → sublistp (next-level (subtrees), subtrees ('forest, subtrees))

Theorem: next-level-of-subtrees-in-complete-subtrees (proper-tree ('forest, subtrees) ∧ sublistp (subtrees, subtrees (flag, tree))) → sublistp (next-level (subtrees), subtrees (flag, tree))

Theorem: proper-tree-of-append (proper-tree ('forest, a) ∧ proper-tree ('forest, b)) → proper-tree ('forest, append (a, b))

Theorem: proper-tree-next-level-of-proper-tree proper-tree ('forest, subtrees) → proper-tree ('forest, next-level (subtrees))

Theorem: not-member-subtrees (root ∉ nodes-rec (flag, tree)) → (cons (root, forest) ∉ subtrees (flag, tree))

Theorem: not-member-no-children (parent ∉ nodes-rec (flag, tree)) → (children-rec (flag, parent, tree) = nil)

Theorem: no-children-in-rest-of-forest (setp (append (nodes-rec ('tree, tree), nodes-rec ('forest, forest))) ∧ (parent ∈ nodes-rec ('tree, tree))) → (children-rec ('forest, parent, forest) = nil)

Theorem: no-children-in-rest-of-tree (setp (append (nodes-rec ('tree, tree), nodes-rec ('forest, forest))) ∧ (parent ∈ nodes-rec ('forest, forest))) → (children-rec ('tree, parent, tree) = nil)

Theorem: member-subtree-member-tree (cons (root, forest) ∈ subtrees (flag, tree)) → (root ∈ nodes-rec (flag, tree))

Theorem: children-of-setp-tree (setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ (cons (root, forest) ∈ subtrees (flag, tree))) → (children-rec (flag, root, tree) = roots (forest))

Theorem: node-has-parent ((node ∈ nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ if flag = 'tree then node ≠ car (tree)

else node ∉ roots (tree) endif) → (car (parent-rec (flag, node, tree)) ∈ nodes-rec (flag, tree))

Theorem: parent-is-not-itself-generalized (setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ listp (parent-rec (flag, child, tree))) → (child ≠ car (parent-rec (flag, child, tree)))

Theorem: parent-is-not-itself (setp (nodes-rec ('tree, tree)) ∧ proper-tree ('tree, tree) ∧ (child ∈ cdr (nodes-rec ('tree, tree)))) → (child ≠ car (parent-rec ('tree, child, tree)))

Theorem: listp-parent-rec-equals (setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree)) → (listp (parent-rec (flag, child, tree))

= ((child ∈ nodes-rec (flag, tree))

∧ if flag = 'tree then child ≠ car (tree) else child ∉ roots (tree) endif))

Theorem: parent-is-not-child (setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ listp (parent-rec (flag, child, tree))) → (car (parent-rec (flag, child, tree)) ∉ children-rec (flag, child, tree))

Theorem: parent-not-in-children (setp (nodes-rec ('tree, tree)) ∧ proper-tree ('tree, tree) ∧ (parent ∈ cdr (nodes-rec ('tree, tree)))) → (parent ∉ children-rec ('tree, parent, tree))

;;; Variables and channel operations

Definition: value (key, state) = cdr (assoc (key, state))

Definition: channel (name, state) = value (name, state)

Definition: empty (name, state) = (¬ listp (channel (name, state)))

Definition: head (name, state) = car (channel (name, state))

Definition: send (channel, message, state) = append (channel (channel, state), list (message))

Definition: receive (channel, state) = cdr (channel (channel, state))

;;; Program Specific

Definition: status (node, state) = value (cons ('status, node), state)

Definition: found-value (node, state) = value (cons ('found-value, node), state)

Definition: outstanding (node, state) = value (cons ('outstanding, node), state)

Definition: node-value (node, state) = value (cons ('node-value, node), state)

Definition: send-find (to-children, old, new) = if listp (to-children)

then (channel (car (to-children), new)

= send (car (to-children), 'find, old)) ∧ send-find (cdr (to-children), old, new)

else t endif

;;; The four program statements

Definition: receive-find (old, new, node, from-parent, to-parent, to-children) = if head (from-parent, old) = 'find

then (channel (from-parent, new) = receive (from-parent, old)) ∧ (status (node, new) = 'started) ∧ (found-value (node, new) = node-value (node, old)) ∧ (outstanding (node, new) = length (to-children)) ∧ send-find (to-children, old, new) ∧ (channel (to-parent, new)

= if length (to-children) ≃ 0 then send (to-parent, node-value (node, old), old) else channel (to-parent, old) endif)

∧ changed (old, new, append (list (from-parent,

to-parent,

cons ('status, node),

                               cons ('found-value, node),

cons ('outstanding, node)), to-children))

else changed (old, new, nil) endif Definition: min (x, y) = if x < y then fix (x)

else fix (y) endif

Definition: receive-report (old, new, node, from-child, to-parent) = if empty (from-child, old) then changed (old, new, nil)

else (channel (from-child, new) = receive (from-child, old))

∧ (found-value (node, new)

= min (found-value (node, old),

head (from-child, old)))

∧ (outstanding (node, new)

= (outstanding (node, old) − 1)) ∧ (channel (to-parent, new)

= if outstanding (node, new) ≃ 0 then send (to-parent,

found-value (node, new), old)

else channel (to-parent, old) endif)

∧ changed (old, new, list (from-child, to-parent,

                       cons ('outstanding, node),

cons ('found-value, node))) endif

Definition: start (old, new, root, to-children) = if status (root, old) = 'not-started

then (status (root, new) = 'started)

∧ (found-value (root, new) = node-value (root, old)) ∧ (outstanding (root, new) = length (to-children)) ∧ send-find (to-children, old, new) ∧ changed (old,

new,

append (list (cons ('status, root),

                               cons ('found-value, root),

cons ('outstanding, root)), to-children))

else changed (old, new, nil) endif

Definition: root-receive-report (old, new, root, from-child) = if empty (from-child, old) then changed (old, new, nil) else (channel (from-child, new) = receive (from-child, old))

∧ (found-value (root, new)

= min (found-value (root, old),

head (from-child, old)))

∧ (outstanding (root, new)

= (outstanding (root, old) − 1)) ∧ changed (old,

new,

list (from-child,

                  cons ('outstanding, root),

cons ('found-value, root))) endif

;;; The Program

Definition: rfp (node, children) = if listp (children)

then cons (cons (node, car (children)), rfp (node, cdr (children))) else nil endif

Definition: receive-find-prg (nodes, tree) = if listp (nodes)

then cons (list ('receive-find, car (nodes), cons (parent (car (nodes), tree), car (nodes)), cons (car (nodes), parent (car (nodes), tree)), rfp (car (nodes), children (car (nodes), tree))),

receive-find-prg (cdr (nodes), tree))

else nil endif

Theorem: member-receive-find-prg (statement ∈ receive-find-prg (nodes, tree)) = ((car (statement) = 'receive-find)

∧ (cadr (statement) ∈ nodes) ∧ listp (caddr (statement)) ∧ (caaddr (statement) = parent (cadr (statement), tree)) ∧ (cdaddr (statement) = cadr (statement)) ∧ listp (cadddr (statement)) ∧ (caadddr (statement) = cadr (statement)) ∧ (cdadddr (statement) = parent (cadr (statement), tree)) ∧ (caddddr (statement)

= rfp (cadr (statement), children (cadr (statement), tree))) ∧ (cdddddr (statement) = nil))

Definition: rrp (node, children, parent) = if listp (children)

then cons (list ('receive-report,

node,

cons (car (children), node), cons (node, parent)), rrp (node, cdr (children), parent))

else nil endif

Theorem: member-rrp (statement ∈ rrp (node, children, parent)) = ((car (statement) = 'receive-report)

∧ (cadr (statement) = node) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children) ∧ (cdaddr (statement) = node) ∧ listp (cadddr (statement)) ∧ (caadddr (statement) = node) ∧ (cdadddr (statement) = parent) ∧ (cddddr (statement) = nil))

Definition: receive-report-prg (nodes, tree) = if listp (nodes)

then append (rrp (car (nodes), children (car (nodes), tree), parent (car (nodes), tree)), receive-report-prg (cdr (nodes), tree))

else nil endif

Theorem: member-receive-report-prg (statement ∈ receive-report-prg (nodes, tree)) = ((car (statement) = 'receive-report)

∧ (cadr (statement) ∈ nodes) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children (cadr (statement), tree)) ∧ (cdaddr (statement) = cadr (statement)) ∧ listp (cadddr (statement)) ∧ (caadddr (statement) = cadr (statement)) ∧ (cdadddr (statement) = parent (cadr (statement), tree)) ∧ (cddddr (statement) = nil))

Definition: start-prg (root, tree) = list (list ('start, root, rfp (root, children (root, tree))))

Theorem: member-start-prg (statement ∈ start-prg (root, tree)) = ((car (statement) = 'start)

∧ (cadr (statement) = root) ∧ (caddr (statement) = rfp (root, children (root, tree))) ∧ (cdddr (statement) = nil))

Definition: rrrp (root, children) = if listp (children)

then cons (list ('root-receive-report,

root,

cons (car (children), root)), rrrp (root, cdr (children)))

else nil endif

Theorem: member-rrrp (statement ∈ rrrp (root, children))

= ((car (statement) = 'root-receive-report)

∧ (cadr (statement) = root) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children) ∧ (cdaddr (statement) = root) ∧ (cdddr (statement) = nil))

Definition: root-receive-report-prg (root, tree) = rrrp (root, children (root, tree))

Theorem: member-root-receive-report-prg (statement ∈ root-receive-report-prg (root, tree))

= ((car (statement) = 'root-receive-report)

∧ (cadr (statement) = root) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children (root, tree)) ∧ (cdaddr (statement) = root) ∧ (cdddr (statement) = nil))

Definition: tree-prg (tree) = append (start-prg (car (tree), tree),

append (root-receive-report-prg (car (tree), tree),

append (receive-find-prg (cdr (nodes (tree)), tree), receive-report-prg (cdr (nodes (tree)), tree))))

Theorem: equal-if (if test then p1 else p2 endif = if test then r1

else r2 endif) = if test then p1 = r1

else p2 = r2 endif

Theorem: member-tree-prg (statement ∈ tree-prg (tree)) = (((car (statement) = 'start)

∧ (cadr (statement) = car (tree)) ∧ (caddr (statement)

= rfp (car (tree), children (car (tree), tree))) ∧ (cdddr (statement) = nil))

∨ ((car (statement) = 'root-receive-report)

∧ (cadr (statement) = car (tree)) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children (car (tree), tree)) ∧ (cdaddr (statement) = car (tree)) ∧ (cdddr (statement) = nil))

∨ ((car (statement) = 'receive-find)

∧ (cadr (statement) ∈ cdr (nodes (tree))) ∧ listp (caddr (statement)) ∧ (caaddr (statement) = parent (cadr (statement), tree)) ∧ (cdaddr (statement) = cadr (statement)) ∧ listp (cadddr (statement)) ∧ (caadddr (statement) = cadr (statement)) ∧ (cdadddr (statement) = parent (cadr (statement), tree)) ∧ (caddddr (statement)

= rfp (cadr (statement),

children (cadr (statement), tree)))

∧ (cdddddr (statement) = nil)) ∨ ((car (statement) = 'receive-report)

∧ (cadr (statement) ∈ cdr (nodes (tree))) ∧ listp (caddr (statement)) ∧ (caaddr (statement) ∈ children (cadr (statement), tree)) ∧ (cdaddr (statement) = cadr (statement)) ∧ listp (cadddr (statement)) ∧ (caadddr (statement) = cadr (statement)) ∧ (cdadddr (statement) = parent (cadr (statement), tree)) ∧ (cddddr (statement) = nil)))

;;; Correctness

Definition: treep (tree) = (setp (nodes (tree))

∧ all-numberps (nodes (tree)) ∧ proper-tree ('tree, tree))

Definition: total-outstanding (nodes, tree, state) = if listp (nodes)

then total-outstanding (cdr (nodes), tree, state)

+ if status (car (nodes), state) = 'started then outstanding (car (nodes), state) else 1 + length (children (car (nodes), tree)) endif

else 0 endif

Definition: dl (down-links, state) = if listp (down-links)

then ((empty (car (down-links), state)

∧ (status (caar (down-links), state)

= status (cdar (down-links), state))) ∨ ((channel (car (down-links), state) = list ('find))

∧ (status (caar (down-links), state) = 'started) ∧ (status (cdar (down-links), state)

                  = 'not-started)))

∧ dl (cdr (down-links), state) else t endif

Definition: done (node, state) = ((status (node, state) = 'started)

∧ (outstanding (node, state) ≃ 0))

Definition: ul (up-links, state) = if listp (up-links)

then (empty (car (up-links), state)

∨ ((channel (car (up-links), state)

= list (found-value (caar (up-links), state)))

∧ done (caar (up-links), state))) ∧ ul (cdr (up-links), state)

else t endif

Definition: reported (node, parent, state) = (done (node, state) ∧ empty (cons (node, parent), state))

Definition: number-not-reported (children, parent, state) = if listp (children)

then if reported (car (children), parent, state)

then number-not-reported (cdr (children), parent, state)

else 1 + number-not-reported (cdr (children), parent, state) endif else 0 endif

Definition: min-of-reported (children, parent, state, min) = if listp (children)

then if reported (car (children), parent, state)

then min (found-value (car (children), state),

min-of-reported (cdr (children), parent, state, min))

else min-of-reported (cdr (children), parent, state, min) endif else min endif

Definition: no (nodes, tree, state) = if listp (nodes)

then if status (car (nodes), state) = 'started then (outstanding (car (nodes), state)

= number-not-reported (children (car (nodes), tree), car (nodes), state))

∧ (found-value (car (nodes), state)

= min-of-reported (children (car (nodes), tree), car (nodes), state, node-value (car (nodes), state)))

else t endif

∧ no (cdr (nodes), tree, state) else t endif

Definition: down-links-1 (parent, children) = if listp (children)

then cons (cons (parent, car (children)),

down-links-1 (parent, cdr (children)))

else nil endif

Definition: down-links (nodes, tree) = if listp (nodes)

then append (down-links-1 (car (nodes), children (car (nodes), tree)),

down-links (cdr (nodes), tree))

else nil endif

Definition: up-links (nodes, tree) = if listp (nodes)

then cons (cons (car (nodes), parent (car (nodes), tree)), up-links (cdr (nodes), tree))

else nil endif

Definition: inv (tree, state) = (dl (down-links (nodes (tree), tree), state)

∧ ul (up-links (cdr (nodes (tree)), tree), state)

∧ no (nodes (tree), tree, state))

Definition: not-started (nodes, state) = if listp (nodes)

then (status (car (nodes), state) = 'not-started) ∧ not-started (cdr (nodes), state)

else t endif

Definition: all-channels (tree) = append (up-links (cdr (nodes (tree)), tree), down-links (nodes (tree), tree))

Definition: all-empty (channels, state) = if listp (channels)

then empty (car (channels), state) ∧ all-empty (cdr (channels), state) else t endif

Definition: min-node-value (nodes, state, min) = if listp (nodes)

then min (node-value (car (nodes), state),

min-node-value (cdr (nodes), state, min))

else min endif

Definition: correct (tree, state) = (found-value (car (tree), state)

= min-node-value (cdr (nodes (tree)), state, node-value (car (tree), state)))

;;; Proof of Correctness

Theorem: all-empty-implies-empty (all-empty (channels, state) ∧ (channel ∈ channels)) → (¬ listp (channel (channel, state)))

Theorem: not-started-implies-not-started (not-started (nodes, state) ∧ (node ∈ nodes)) → (cdr (assoc (cons ('status, node), state)) = 'not-started)

Theorem: all-empty-append all-empty (append (a, b), state) = (all-empty (a, state) ∧ all-empty (b, state))

Theorem: all-empty-implies-ul all-empty (up-links, state) → ul (up-links, state)

Definition: nodes-in-channels (channels) = if listp (channels)

then cons (caar (channels),

cons (cdar (channels), nodes-in-channels (cdr (channels))))

else nil endif

Theorem: all-empty-not-started-implies-dl (all-empty (down-links, state) ∧ not-started (nodes-in-channels (down-links), state)) → dl (down-links, state)

Theorem: not-started-implies-no not-started (nodes, state) → no (nodes, tree, state)

Theorem: nodes-in-down-links-1-in-nodes (node ∈ nodes-in-channels (down-links-1 (parent, children))) = if listp (children) then node ∈ cons (parent, children)

else f endif

Theorem: nodes-in-channels-append nodes-in-channels (append (a, b)) = append (nodes-in-channels (a), nodes-in-channels (b))

Theorem: nodes-in-down-links-in-nodes (proper-tree ('tree, tree) ∧ (node ∈ nodes-in-channels (down-links (nodes, tree)))) → (node ∈ nodes (tree))

Theorem: sublistp-not-started (sublistp (sub, list) ∧ not-started (list, state)) → not-started (sub, state)

Theorem: sublistp-down-links-1 (sublistp (children, nodes) ∧ (parent ∈ nodes)) → sublistp (nodes-in-channels (down-links-1 (parent, children)), nodes)

Theorem: children-of-non-node (parent ∉ nodes-rec (flag, tree)) → (children-rec (flag, parent, tree) = nil)

Theorem: down-links-is-sublistp proper-tree ('tree, tree) → sublistp (nodes-in-channels (down-links (nodes, tree)),

nodes-rec ('tree, tree))

Theorem: initial-conditions-imply-invariant (proper-tree ('tree, tree) ∧ all-empty (all-channels (tree), state) ∧ not-started (nodes (tree), state)) → inv (tree, state)

Definition: found-value-node-value (subtrees, state) = if listp (subtrees)

then (found-value (caar (subtrees), state)

= min-node-value (cdr (nodes-rec ('tree, car (subtrees))), state, node-value (caar (subtrees), state)))

∧ found-value-node-value (cdr (subtrees), state) else t endif

Definition: nati (subtrees) = if listp (subtrees) then nati (next-level (subtrees))

else t endif

Theorem: found-value-node-value-append found-value-node-value (append (a, b), state) = (found-value-node-value (a, state) ∧ found-value-node-value (b, state))

;find-value-of-node-value for a subtree is true if
;find-value-of-node-value for the next-level of that subtree is true.

Theorem: no-implies (no (nodes, tree, state) ∧ (node ∈ nodes) ∧ (status (node, state) = 'started)) → ((number-not-reported (children (node, tree), node, state)

= cdr (assoc (cons ('outstanding, node), state))) ∧ (cdr (assoc (cons ('outstanding, node), state)) ∈ N) ∧ (cdr (assoc (cons ('found-value, node), state)) = min-of-reported (children (node, tree),

node, state, node-value (node, state))))

Theorem: total-outstanding-0-implies (((total-outstanding (nodes, tree, state) = 0) ∧ (node ∈ nodes) ∧ (cdr (assoc (cons ('outstanding, node), state)) ∈ N)) → (cdr (assoc (cons ('outstanding, node), state)) = 0)) ∧ (((total-outstanding (nodes, tree, state) = 0) ∧ (node ∈ nodes))

→ (cdr (assoc (cons ('status, node), state)) = 'started))

Theorem: number-not-reported-0-implies ((number-not-reported (children, parent, state) = 0) ∧ (node ∈ children)) → reported (node, parent, state)

Theorem: proper-tree-tree-implies-nodes-exists proper-tree ('tree, tree) → listp (nodes-rec ('tree, tree))

Theorem: min-of-two-nodes-values min (min-node-value (forest-1 ,

state,

cdr (assoc (cons ('node-value, root), state))),

min-node-value (rest-of-forest, state, min)) = min-node-value (cons (root, append (forest-1 , rest-of-forest)), state, min)

Theorem: found-value-min-value-generalized (found-value-node-value (forest, state) ∧ (number-not-reported (roots (forest), root, state) = 0) ∧ proper-tree ('forest, forest)) → (min-of-reported (roots (forest), root, state, min)

= min-node-value (nodes-rec ('forest, forest), state, min))

Theorem: no-at-termination (proper-tree ('tree, tree) ∧ proper-tree ('forest, subtrees)

∧ setp (nodes-rec ('tree, tree)) ∧ no (nodes-rec ('tree, tree), tree, state) ∧ (total-outstanding (nodes-rec ('tree, tree), tree, state) = 0) ∧ sublistp (subtrees, subtrees ('tree, tree))) → found-value-node-value (subtrees, state)

Theorem: inv-implies-augmented-correctness-condition (proper-tree ('tree, tree) ∧ setp (nodes-rec ('tree, tree)) ∧ inv (tree, state) ∧ (total-outstanding (nodes (tree), tree, state) = 0)) → correct (tree, state)

Definition: send-find-func (to-children, old) = if listp (to-children)

then update-assoc (car (to-children), send (car (to-children), 'find, old), send-find-func (cdr (to-children), old))

else old endif

Definition: receive-find-func (old, node, from-parent, to-parent, to-children) = if head (from-parent, old) = 'find

then update-assoc (from-parent, receive (from-parent, old), update-assoc (cons ('status, node),

                               'started,

update-assoc (cons ('found-value,

node), node-value (node, old), update-assoc (cons ('outstanding,

node), length (to-children), if length (to-children) ≃ 0 then update-assoc (to-parent,

send (to-parent,

node-value (node,

old),

old), send-find-func (to-children,

old))

else send-find-func (to-children,

old) endif))))

else old endif Theorem: send-find-func-implements-send-find send-find (to-children, old, send-find-func (to-children, old))

Theorem: nodes-are-not-litatoms (all-numberps (nodes-rec (flag, tree)) ∧ (node ∈ nodes-rec (flag, tree))) → ((pack (x) = node) = f)

Theorem: parent-is-not-a-litatom (all-numberps (nodes-rec ('tree, tree)) ∧ setp (nodes-rec ('tree, tree)) ∧ proper-tree ('tree, tree) ∧ (child ∈ cdr (nodes-rec ('tree, tree)))) → ((pack (x) = car (parent-rec ('tree, child, tree))) = f)

Theorem: children-are-not-litatoms (all-numberps (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ (child ∈ children-rec (flag, parent, tree))) → ((pack (x) = child) = f)

Theorem: children-are-not-litatoms-member (all-numberps (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree)) → ((pack (x) ∈ children-rec (flag, parent, tree)) = f)

Theorem: send-find-of-update-assoc (key ∉ to-children) → (send-find (to-children, old, update-assoc (key, value, state))

= send-find (to-children, old, state))

Theorem: assoc-of-send-find-func (key ∉ to-children) → (assoc (key, send-find-func (to-children, old)) = assoc (key, old))

Theorem: about-rfp (p ∉ c) → (cons (v, p) ∉ rfp (v, c))

Theorem: about-rfp-numberp (a ∈ N) → (cons (pack (x), y) ∉ rfp (a, b))

Theorem: parent-not-in-rfp (setp (nodes-rec ('tree, tree)) ∧ proper-tree ('tree, tree) ∧ (v ∈ cdr (nodes-rec ('tree, tree)))) → (cons (v, car (parent-rec ('tree, v, tree)))

∉ rfp (v, children-rec ('tree, v, tree)))

Theorem: to-node-not-in-rfp (node ∉ children) → (cons (x, node) ∉ rfp (node, children))

Theorem: uc-of-send-find-func sublistp (to-children, excpt) → (uc (old, send-find-func (to-children, state), keys, excpt)

= uc (old, state, keys, excpt))

Theorem: receive-find-func-implements-receive-find (treep (tree) ∧ (statement ∈ receive-find-prg (cdr (nodes (tree)), tree))) → n (old,

receive-find-func (old, cadr (statement), caddr (statement), cadddr (statement), caddddr (statement)),

statement)

Definition: receive-report-func (old, node, from-child, to-parent) = if empty (from-child, old) then old

else update-assoc (from-child, receive (from-child, old), update-assoc (cons ('found-value, node),

min (found-value (node, old), head (from-child, old)), update-assoc (cons ('outstanding,

node), outstanding (node,

old) − 1,

if (outstanding (node,

old) − 1) ≃ 0

then update-assoc (to-parent,

send (to-parent,

min (found-value (node,

old),

head (from-child, old)),

old), old)

else old endif))) endif

Theorem: receive-report-func-implements-receive-report (treep (tree) ∧ (statement ∈ receive-report-prg (cdr (nodes (tree)), tree))) → n (old, receive-report-func (old,

cadr (statement), caddr (statement), cadddr (statement)),

statement)

Definition: start-func (old, root, to-children) = if status (root, old) = 'not-started

then update-assoc (cons ('status, root),

                    'started,

update-assoc (cons ('found-value, root), node-value (root, old), update-assoc (cons ('outstanding,

root), length (to-children), send-find-func (to-children,

old))))

else old endif

Theorem: start-func-implements-start (treep (tree) ∧ (statement ∈ start-prg (car (tree), tree))) → n (old, start-func (old, cadr (statement), caddr (statement)), statement)

Definition: root-receive-report-func (old, root, from-child) = if empty (from-child, old) then old

else update-assoc (from-child, receive (from-child, old), update-assoc (cons ('found-value, root),

min (found-value (root, old), head (from-child, old)), update-assoc (cons ('outstanding,

root), outstanding (root,

old) − 1,

old))) endif

Theorem: root-receive-report-func-implements-root-receive-report (treep (tree) ∧ (statement ∈ root-receive-report-prg (car (tree), tree))) → n (old,

root-receive-report-func (old, cadr (statement), caddr (statement)), statement)

Theorem: receive-find-prg-is-total treep (tree) → total-sufficient (statement,

receive-find-prg (cdr (nodes (tree)), tree),

old,

receive-find-func (old, cadr (statement), caddr (statement), cadddr (statement), caddddr (statement)))

Theorem: receive-report-prg-is-total treep (tree) → total-sufficient (statement,

receive-report-prg (cdr (nodes (tree)), tree),

old,

receive-report-func (old, cadr (statement), caddr (statement), cadddr (statement)))

Theorem: start-prg-is-total treep (tree) → total-sufficient (statement,

start-prg (car (tree), tree),

old,

start-func (old, cadr (statement), caddr (statement)))

Theorem: root-receive-report-prg-is-total treep (tree) → total-sufficient (statement,

root-receive-report-prg (car (tree), tree),

old,

root-receive-report-func (old, cadr (statement), caddr (statement)))

Theorem: total-tree-prg treep (tree) → total (tree-prg (tree))

Theorem: listp-tree-prg listp (tree-prg (tree))

Theorem: node-values-constant-unless-sufficient (treep (tree) ∧ (node ∈ nodes (tree))) → unless-sufficient (statement, tree-prg (tree), old, new,

                  `(equal (node-value ',node state) ',k),
                  '(false))

Theorem: node-values-constant-invariant (initial-condition (`(and

                 (all-empty ',(all-channels tree) state)
                 (and
                  (not-started ',(nodes tree) state)
                  (equal (node-value ',node state) ',k))),

tree-prg (tree))

∧ treep (tree) ∧ (node ∈ nodes (tree)))

→ invariant (`(equal (node-value ',node state) ',k),

tree-prg (tree))

Theorem: dl-implies-instance-of-dl (dl (down-links, state) ∧ (down-link ∈ down-links)) → ((empty (down-link, state)

∧ (status (car (down-link), state)

= status (cdr (down-link), state))) ∨ ((channel (down-link, state) = list ('find))

∧ (status (car (down-link), state) = 'started)

∧ (status (cdr (down-link), state) = 'not-started)))

Event: Disable dl-implies-instance-of-dl.

Theorem: ul-implies-instance-of-ul (ul (uplinks, state) ∧ (uplink ∈ uplinks)) → (empty (uplink, state)

∨ ((channel (uplink, state)

= list (found-value (car (uplink), state)))

∧ done (car (uplink), state)))

Event: Disable ul-implies-instance-of-ul.

Theorem: ul-implies-instance-of-ul-not-empty-uplink (ul (uplinks, state) ∧ (uplink ∈ uplinks) ∧ (¬ empty (uplink, state))) → ((cdr (assoc (uplink, state)) = list (found-value (car (uplink), state)))

∧ (cdr (assoc (cons ('status, car (uplink)), state))

         = 'started)

∧ (cdr (assoc (cons ('outstanding, car (uplink)), state)) ≃ 0))

Theorem: no-implies-instance-of-no (no (nodes, tree, state) ∧ (node ∈ nodes) ∧ (status (node, state) = 'started)) → ((cdr (assoc (cons ('outstanding, node), state))

= number-not-reported (children-rec ('tree, node, tree), node, state))

∧ (cdr (assoc (cons ('found-value, node), state))

= min-of-reported (children-rec ('tree, node, tree), node, state, node-value (node, state))))

Theorem: member-down-links-1 (down-link ∈ down-links-1 (parent, children)) = ((car (down-link) = parent)

∧ (cdr (down-link) ∈ children)

∧ listp (down-link))

Theorem: member-down-links (down-link ∈ down-links (nodes, tree)) = ((car (down-link) ∈ nodes)

∧ (cdr (down-link) ∈ children (car (down-link), tree))

∧ listp (down-link))

Theorem: parent-not-child (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree))) → (parent ∉ children-rec (flag, parent, tree))

Theorem: parent-not-grandchild (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree)) ∧ (child ∈ children-rec (flag, parent, tree))) → (parent ∉ children-rec (flag, child, tree))

Theorem: parent-of-parent-not-node (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree)) ∧ listp (parent-rec (flag, node, tree)) ∧ listp (parent-rec (flag, car (parent-rec (flag, node, tree)), tree))) → (car (parent-rec (flag, car (parent-rec (flag, node, tree)), tree)) ≠ node)

Theorem: member-rfp (channel ∈ rfp (parent, children))

= ((car (channel) = parent)

∧ (cdr (channel) ∈ children)

∧ listp (channel))

Theorem: send-find-implies (send-find (channels, old, new) ∧ (key ∈ channels)) → (cdr (assoc (key, new)) = send (key, 'find, old))

Theorem: assoc-of-channel-preserved-root-receive-report ((w ∉ nodes-rec ('forest, d)) ∧ setp (nodes-rec ('forest, d)) ∧ (z ∈ nodes-rec ('forest, d)) ∧ uc (new,

old,

append (strip-cars (new), strip-cars (old)),

list (cons (v, w), cons ('outstanding, w), cons ('found-value, w)))) → (assoc (cons (x, z), new) = assoc (cons (x, z), old))

Theorem: assoc-equal-cons (assoc (key, alist) = cons (key, value)) = (listp (assoc (key, alist)) ∧ (cdr (assoc (key, alist)) = value))

Theorem: send-find-general (send-find (channels, old, new) ∧ (key ∈ channels)) → (assoc (key, new) = cons (key, send (key, 'find, old)))

Theorem: all-numberps-do-not-contain-litatom all-numberps (list) → (pack (x) ∉ list)

Theorem: all-numberps-append all-numberps (append (x, y)) = (all-numberps (x) ∧ all-numberps (y))

Theorem: all-numberps-nodes-implies-all-numberps-parent all-numberps (nodes-rec (flag, tree)) → all-numberps (parent-rec (flag, child, tree))

Theorem: all-numberps-nodes-implies-all-numberps-car-parent all-numberps (nodes-rec (flag, tree)) → (car (parent-rec (flag, child, tree)) ∈ N)

Theorem: parent-not-litatom all-numberps (nodes-rec (flag, tree)) → ((pack (x) = car (parent-rec (flag, child, tree))) = f)

Theorem: all-numberps-forest-implies-all-numberps-roots all-numberps (nodes-rec ('forest, forest)) → all-numberps (roots (forest))

Theorem: all-numberps-nodes-implies-all-numberps-children all-numberps (nodes-rec (flag, tree)) → all-numberps (children-rec (flag, parent, tree))

Theorem: dl-preserves-instance-of-dl (treep (tree) ∧ (down-link ∈ down-links (nodes (tree), tree)) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old)) → ((empty (down-link, new)

∧ (status (car (down-link), new) = status (cdr (down-link), new))) ∨ ((channel (down-link, new) = list ('find))

∧ (status (car (down-link), new) = 'started)

∧ (status (cdr (down-link), new) = 'not-started)))

Theorem: dl-preserves-sublist (dl (down-links (nodes (tree), tree), old) ∧ treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ sublistp (sublist, down-links (nodes (tree), tree))) → dl (sublist, new)

Theorem: dl-preserves-dl (dl (down-links (nodes (tree), tree), old) ∧ treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree))) → dl (down-links (nodes (tree), tree), new)

Theorem: member-up-links (up-link ∈ up-links (nodes, tree)) = ((car (up-link) ∈ nodes)

∧ (cdr (up-link) = parent (car (up-link), tree))

∧ listp (up-link))

Theorem: zero-not-reported-implies-children-reported ((number-not-reported (children, parent, state) ≃ 0) ∧ (child ∈ children)) → ((cdr (assoc (cons ('status, child), state)) = 'started)

∧ (outstanding (child, state) ≃ 0)

∧ (¬ listp (cdr (assoc (cons (child, parent), state)))))

Theorem: dl-ul-no-preserves-instance-of-ul (treep (tree)

∧ (up-link ∈ up-links (cdr (nodes (tree)), tree)) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old)) → (empty (up-link, new)

∨ ((channel (up-link, new) = list (found-value (car (up-link), new))) ∧ done (car (up-link), new)))

Theorem: dl-ul-no-preserves-ul-sublist (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old) ∧ sublistp (sublist, up-links (cdr (nodes (tree)), tree))) → ul (sublist, new)

Theorem: dl-ul-no-preserves-ul (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old)) → ul (up-links (cdr (nodes (tree)), tree), new)

Theorem: parent-not-started-implies-all-empty-and-not-started ((status (parent, state) = 'not-started) ∧ dl (rfp (parent, children), state)) → (all-empty (rfp (parent, children), state)

∧ not-started (children, state))

Theorem: start-preserves-no-for-parent ((parent ∈ N) ∧ (parent ∉ children) ∧ not-started (children, old) ∧ sublistp (rfp (parent, children), rfp (parent, excpt)) ∧ changed (old,

new,

append (list (cons ('status, parent), cons ('found-value, parent),

cons ('outstanding, parent)), rfp (parent, excpt))))

→ ((number-not-reported (children, parent, new) = length (children)) ∧ (min-of-reported (children, parent, new, value) = value))

Theorem: unchanged-preserves-no changed (old, new, nil) → ((number-not-reported (children, parent, new)

= number-not-reported (children, parent, old)) ∧ (min-of-reported (children, parent, new, value)

= min-of-reported (children, parent, old, value)))

Theorem: start-preserves-no-for-rest-of-tree ((root ∈ N) ∧ (parent ∈ N) ∧ (parent ∉ children) ∧ (root ∉ children) ∧ (root ≠ parent) ∧ changed (old,

new,

append (list (cons ('status, root),

                      cons ('found-value, root),

cons ('outstanding, root)), rfp (root, excpt))))

→ ((number-not-reported (children, parent, new)

= number-not-reported (children, parent, old)) ∧ (min-of-reported (children, parent, new, value)

= min-of-reported (children, parent, old, value)))

Theorem: length-rfp length (rfp (parent, children)) = length (children)

Theorem: start-preserves-instance-of-no (treep (tree) ∧ start (old, new, car (tree), rfp (car (tree), children (car (tree), tree))) ∧ (node ∈ nodes (tree)) ∧ dl (rfp (car (tree), children (car (tree), tree)), old) ∧ (status (node, new) = 'started) ∧ ((status (node, old) = 'started)

→ ((outstanding (node, old) = number-not-reported (children (node, tree), node, old)) ∧ (found-value (node, old)

= min-of-reported (children (node, tree), node, old,

node-value (node, old))))))

→ ((outstanding (node, new)

= number-not-reported (children (node, tree), node, new)) ∧ (found-value (node, new)

= min-of-reported (children (node, tree), node, new, node-value (node, new))))

Theorem: min-commutative min (a, b) = min (b, a)

Theorem: min-associative min (min (a, b), c) = min (a, min (b, c))

Theorem: min-commutative-1 min (a, min (b, c)) = min (b, min (a, c))

Theorem: min-of-reported-of-min min-of-reported (children, parent, state, min (value, x)) = min (min-of-reported (children, parent, state, value), x)

Theorem: update-min-of-reported ((parent ∈ N) ∧ (child ∈ N) ∧ (parent ≠ child) ∧ all-numberps (children) ∧ setp (children) ∧ (parent ∉ children) ∧ (channel (cons (child, parent), old) = list (found-value (child, old))) ∧ done (child, old) ∧ (channel (cons (child, parent), new) = receive (cons (child, parent), old)) ∧ changed (old,

new,

list (cons (child, parent), cons ('outstanding, parent), cons ('found-value, parent))))

→ (min-of-reported (children, parent, new, value)

= if child ∈ children

then min (found-value (child, old),

min-of-reported (children, parent, old, value))

else min-of-reported (children, parent, old, value) endif)

Theorem: min-of-reported-of-non-root ((root ∈ N)

∧ (child ∈ N) ∧ (parent ∈ N) ∧ all-numberps (children) ∧ setp (children) ∧ (parent ∉ children) ∧ (root ≠ parent) ∧ (root ∉ children) ∧ changed (old,

new,

list (cons (child, root),

               cons ('outstanding, root),

cons ('found-value, root))))

→ (min-of-reported (children, parent, new, value) = min-of-reported (children, parent, old, value))

Theorem: number-not-reported-of-non-root ((root ∈ N) ∧ (child ∈ N) ∧ (parent ∈ N) ∧ all-numberps (children) ∧ setp (children) ∧ (parent ∉ children) ∧ (root ≠ parent) ∧ (root ∉ children) ∧ changed (old,

new,

list (cons (child, root),

               cons ('outstanding, root),

cons ('found-value, root))))

→ (number-not-reported (children, parent, new) = number-not-reported (children, parent, old))

Theorem: number-not-reported-of-root ((parent ∈ N) ∧ (child ∈ N) ∧ (parent ≠ child) ∧ all-numberps (children) ∧ setp (children) ∧ (parent ∉ children) ∧ (channel (cons (child, parent), old) = list (found-value (child, old))) ∧ done (child, old) ∧ (channel (cons (child, parent), new) = receive (cons (child, parent), old)) ∧ changed (old,

new, list (cons (child, parent),

cons ('outstanding, parent), cons ('found-value, parent))))

→ (number-not-reported (children, parent, new)

= if child ∈ children then number-not-reported (children, parent, old) − 1 else number-not-reported (children, parent, old) endif)

Theorem: setp-nodes-implies-setp-roots (proper-tree ('forest, forest) ∧ setp (nodes-rec ('forest, forest))) → setp (roots (forest))

Theorem: setp-nodes-setp-children (proper-tree (flag, tree) ∧ setp (nodes-rec (flag, tree))) → setp (children-rec (flag, parent, tree))

Theorem: root-receive-report-preserves-instance-of-no (treep (tree) ∧ (child ∈ children (car (tree), tree)) ∧ root-receive-report (old, new, car (tree), cons (child, car (tree))) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ (node ∈ nodes (tree)) ∧ (status (node, new) = 'started) ∧ ((status (node, old) = 'started)

→ ((outstanding (node, old) = number-not-reported (children (node, tree), node, old)) ∧ (found-value (node, old)

= min-of-reported (children (node, tree), node, old, node-value (node, old))))))

→ ((outstanding (node, new)

= number-not-reported (children (node, tree), node, new)) ∧ (found-value (node, new)

= min-of-reported (children (node, tree), node, new, node-value (node, new))))

Theorem: receive-find-preserves-no-for-rest-of-tree ((node ∈ N) ∧ (parent-of-node ∈ N) ∧ (parent ∈ N) ∧ (parent ≠ node) ∧ (node ∉ children)

∧ changed (old, new, append (list (cons (parent-of-node, node),

cons (node, parent-of-node), cons ('status, node),

                      cons ('found-value, node),

cons ('outstanding, node)), rfp (node, excpt))))

→ ((number-not-reported (children, parent, new)

= number-not-reported (children, parent, old)) ∧ (min-of-reported (children, parent, new, value)

= min-of-reported (children, parent, old, value)))

Theorem: receive-find-preserves-no-for-node ((node ∈ N) ∧ (parent-of-node ∈ N) ∧ (node ∉ children) ∧ not-started (children, old) ∧ sublistp (rfp (node, children), rfp (node, excpt)) ∧ changed (old,

new,

append (list (cons (parent-of-node, node), cons (node, parent-of-node), cons ('status, node),

                      cons ('found-value, node),

cons ('outstanding, node)), rfp (node, excpt))))

→ ((number-not-reported (children, node, new) = length (children))

∧ (min-of-reported (children, node, new, value) = min-of-reported (children, node, old, value)))

Theorem: receive-find-preserves-no-for-parent-of-node ((node ∈ N) ∧ (parent-of-node ∈ N) ∧ (node ≠ parent-of-node) ∧ (status (node, old) ≠ 'started) ∧ ((outstanding (node, new) ≃ 0)

→ (¬ empty (cons (node, parent-of-node), new))) ∧ changed (old,

new,

append (list (cons (parent-of-node, node), cons (node, parent-of-node), cons ('status, node),

                      cons ('found-value, node),

cons ('outstanding, node)), rfp (node, excpt))))

→ ((number-not-reported (children, parent-of-node, new) = number-not-reported (children, parent-of-node, old)) ∧ (min-of-reported (children, parent-of-node, new, value)

= min-of-reported (children, parent-of-node, old, value)))

Theorem: dl-of-append dl (append (a, b), state) = (dl (a, state) ∧ dl (b, state))

Theorem: down-links-1-rfp down-links-1 (parent, children) = rfp (parent, children)

Theorem: dl-down-links-implies-dl-rfp (dl (down-links (nodes, tree), state) ∧ (node ∈ nodes)) → dl (rfp (node, children (node, tree)), state)

Event: Disable dl-down-links-implies-dl-rfp.

Event: Disable down-links-1-rfp.

Event: Disable dl-of-append.

Theorem: receive-find-preserves-instance-of-no (treep (tree) ∧ (node ∈ cdr (nodes (tree))) ∧ receive-find (old,

new, node, cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree)))

∧ dl (down-links (nodes (tree), tree), old) ∧ (n ∈ nodes (tree)) ∧ (status (n, new) = 'started) ∧ ((status (n, old) = 'started)

→ ((outstanding (n, old) = number-not-reported (children (n, tree), n, old)) ∧ (found-value (n, old)

= min-of-reported (children (n, tree), n, old, node-value (n, old))))))

→ ((outstanding (n, new) = number-not-reported (children (n, tree), n, new))

∧ (found-value (n, new)

= min-of-reported (children (n, tree), n, new, node-value (n, new))))

Theorem: receive-report-preserves-no-for-rest-of-tree ((node ∈ N) ∧ (parent-of-node ∈ N) ∧ (child-of-node ∈ N) ∧ (parent ∈ N) ∧ (parent ≠ node) ∧ (node ∉ children) ∧ changed (old,

new,

list (cons (child-of-node, node), cons (node, parent-of-node),

               cons ('outstanding, node),

cons ('found-value, node))))

→ ((number-not-reported (children, parent, new)

= number-not-reported (children, parent, old)) ∧ (min-of-reported (children, parent, new, value)

= min-of-reported (children, parent, old, value)))

Theorem: receive-report-preserves-no-for-node ((node ∈ N) ∧ (parent ∈ N) ∧ (child ∈ N) ∧ (node ∉ children) ∧ all-numberps (children) ∧ setp (children) ∧ (channel (cons (child, node), old) = list (found-value (child, old))) ∧ done (child, old) ∧ (channel (cons (child, node), new) = receive (cons (child, node), old)) ∧ changed (old,

new,

list (cons (child, node), cons (node, parent),

               cons ('outstanding, node),

cons ('found-value, node))))

→ ((number-not-reported (children, node, new)

= if child ∈ children then number-not-reported (children, node, old) − 1

else number-not-reported (children, node, old) endif) ∧ (min-of-reported (children, node, new, value)

= if child ∈ children

then min (found-value (child, old),

min-of-reported (children, node, old, value))

else min-of-reported (children, node, old, value) endif))

Theorem: receive-report-preserves-no-for-parent ((node ∈ N) ∧ (parent ∈ N) ∧ (node ≠ parent) ∧ ((outstanding (node, new) ≃ 0) → (¬ empty (cons (node, parent), new))) ∧ (outstanding (node, old) ≄ 0) ∧ changed (old,

new,

list (cons (child, node), cons (node, parent),

               cons ('outstanding, node),

cons ('found-value, node))))

→ ((number-not-reported (children, parent, new)

= number-not-reported (children, parent, old)) ∧ (min-of-reported (children, parent, new, value)

= min-of-reported (children, parent, old, value)))

Theorem: child-member-cdr-nodes (proper-tree ('tree, tree) ∧ setp (nodes-rec ('tree, tree)) ∧ (child ∈ children-rec ('tree, node, tree))) → (child ∈ cdr (nodes-rec ('tree, tree)))

Theorem: receive-report-preserves-instance-of-no (treep (tree) ∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)) ∧ (n ∈ nodes (tree)) ∧ receive-report (old,

new, node, cons (child, node), cons (node, parent (node, tree)))

∧ (status (n, new) = 'started) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old) ∧ dl (down-links (nodes (tree), tree), old)) → ((outstanding (n, new) = number-not-reported (children (n, tree), n, new))

∧ (found-value (n, new)

= min-of-reported (children (n, tree), n, new, node-value (n, new))))

Theorem: dl-ul-no-preserves-instance-of-no (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old) ∧ (node ∈ nodes (tree)) ∧ (status (node, new) = 'started)) → ((outstanding (node, new)

= number-not-reported (children (node, tree), node, new)) ∧ (found-value (node, new)

= min-of-reported (children (node, tree), node, new, node-value (node, new))))

Theorem: dl-ul-no-preserves-no-sublist (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ dl (down-links (nodes (tree), tree), old) ∧ ul (up-links (cdr (nodes (tree)), tree), old) ∧ no (nodes (tree), tree, old) ∧ sublistp (sublist, nodes (tree))) → no (sublist, tree, new)

Theorem: inv-preserves-inv (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ inv (tree, old)) → inv (tree, new)

Theorem: inv-is-invariant (initial-condition (`(and

                (all-empty ',(all-channels tree) state)
                (not-started ',(nodes tree) state)),

tree-prg (tree))

∧ treep (tree)) → invariant (`(inv ',tree state), tree-prg (tree))

Theorem: outstanding-non-increasing (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement) ∧ dl (down-links (nodes (tree), tree), old) ∧ (node ∈ nodes (tree))) → (if status (node, old) = 'started then outstanding (node, old)

else 1 + length (children (node, tree)) endif ≮ if status (node, new) = 'started then outstanding (node, new) else 1 + length (children (node, tree)) endif)

Theorem: total-outstanding-non-increasing-sublist (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement) ∧ dl (down-links (nodes (tree), tree), old) ∧ sublistp (sublist, nodes (tree))) → (total-outstanding (sublist, tree, old)

≮ total-outstanding (sublist, tree, new))

Theorem: total-outstanding-non-increasing (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement) ∧ dl (down-links (nodes (tree), tree), old)) → (total-outstanding (nodes (tree), tree, old)

≮ total-outstanding (nodes (tree), tree, new))

Theorem: position-append position (append (a, b), e) = if e ∈ a then position (a, e)

else length (a) + position (b, e) endif

Theorem: parents-position-decreases ((node ∈ nodes-rec (flag, tree)) ∧ setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ if flag = 'tree then car (tree) ≠ node

else node ∉ roots (tree) endif) → (position (nodes-rec (flag, tree), car (parent-rec (flag, node, tree)))

< position (nodes-rec (flag, tree), node))

Definition: parent-to-root-induction (node, tree) = if (node ∈ nodes (tree))

∧ setp (nodes (tree))

∧ proper-tree ('tree, tree) then if car (tree) = node then t

else parent-to-root-induction (parent (node, tree), tree) endif else t endif

Theorem: dl-and-all-empty-implies-root-defines-status (dl (down-links (nodes (tree), tree), state) ∧ all-empty (down-links (nodes (tree), tree), state) ∧ setp (nodes (tree)) ∧ proper-tree ('tree, tree) ∧ (node ∈ nodes (tree))) → (cdr (assoc (cons ('status, node), state)) = status (car (tree), state))

Definition: suffix (s, l) = if listp (l)

then if s = l then t

else suffix (s, cdr (l)) endif else ¬ listp (s) endif

Theorem: suffix-implies-suffix-cdr suffix (s, l) → suffix (cdr (s), l)

Theorem: member-suffix-member-list ((e ∈ s) ∧ suffix (s, l)) → (e ∈ l)

Theorem: childs-position-increases ((node ∈ nodes-rec (flag, tree)) ∧ setp (nodes-rec (flag, tree)) ∧ proper-tree (flag, tree) ∧ (child ∈ children-rec (flag, node, tree))) → (position (nodes-rec (flag, tree), node)

< position (nodes-rec (flag, tree), child))

Theorem: setp-list-setp-suffix (setp (l) ∧ suffix (s, l)) → setp (s)

Theorem: later-positions-are-in-suffix (setp (l) ∧ suffix (s, l) ∧ (x ∈ s)

∧ (y ∈ l) ∧ (position (l, x) < position (l, y))) → (y ∈ s)

Definition: all-done (nodes, state) = if listp (nodes)

then if done (car (nodes), state) then all-done (cdr (nodes), state)

else f endif else t endif

Theorem: all-done-implies-done (all-done (nodes, state) ∧ (node ∈ nodes)) → done (node, state)

Theorem: all-done-implies-all-done-sublist (all-done (nodes, state) ∧ sublistp (sublist, nodes)) → all-done (sublist, state)

Definition: ulnks (children, parent) = if listp (children)

then cons (cons (car (children), parent), ulnks (cdr (children), parent)) else nil endif

Theorem: all-done-and-all-empty-implies-number-not-reported-0 (all-done (children, state) ∧ all-empty (ulnks (children, parent), state)) → (number-not-reported (children, parent, state) = 0)

Theorem: all-empty-implies-all-empty-sublist (all-empty (channels, state) ∧ sublistp (sublist, channels)) → all-empty (sublist, state)

Theorem: sublist-ulnks (proper-tree ('tree, tree) ∧ sublistp (sublist, children (parent, tree)) ∧ setp (nodes (tree))) → sublistp (ulnks (sublist, parent), up-links (cdr (nodes (tree)), tree))

Theorem: child-of-node-in-suffix-is-in-suffix (proper-tree ('tree, tree) ∧ setp (nodes (tree)) ∧ (child ∈ children (node, tree)) ∧ suffix (nodes, nodes (tree)) ∧ (node ∈ nodes)) → (child ∈ cdr (nodes))

Theorem: children-are-suffix-of-sublist-generalized (proper-tree ('tree, tree) ∧ setp (nodes (tree)) ∧ suffix (nodes, nodes (tree)) ∧ (node ∈ nodes) ∧ sublistp (sublist, children-rec ('tree, node, tree))) → sublistp (sublist, cdr (nodes))

Theorem: all-nodes-are-done (proper-tree ('tree, tree) ∧ setp (nodes (tree)) ∧ all-empty (down-links (nodes (tree), tree), state) ∧ all-empty (up-links (cdr (nodes (tree)), tree), state) ∧ dl (down-links (nodes (tree), tree), state) ∧ ul (up-links (cdr (nodes (tree)), tree), state) ∧ no (nodes (tree), tree, state) ∧ (status (car (tree), state) = 'started) ∧ suffix (nodes, nodes (tree))) → all-done (nodes, state)

Theorem: all-done-implies-total-outstanding-0 all-done (nodes, state) → (total-outstanding (nodes, tree, state) = 0)

Theorem: all-empty-root-started-implies-total-outstanding-0 (proper-tree ('tree, tree) ∧ setp (nodes (tree)) ∧ inv (tree, state) ∧ all-empty (down-links (nodes (tree), tree), state) ∧ all-empty (up-links (cdr (nodes (tree)), tree), state) ∧ (status (car (tree), state) = 'started)) → (total-outstanding (nodes (tree), tree, state) = 0)

Definition: full-channel (channels, state) = if listp (channels)

then if empty (car (channels), state) then full-channel (cdr (channels), state) else car (channels) endif

else f endif

Theorem: not-all-empty-implies-full-channel-full ((¬ all-empty (channels, state)) ∧ (f ∉ channels)) → (listp (cdr (assoc (full-channel (channels, state), state)))

∧ (full-channel (channels, state) ∈ channels) ∧ full-channel (channels, state))

Theorem: not-total-outstanding-0-implies-full-channel (proper-tree ('tree, tree) ∧ setp (nodes (tree)) ∧ inv (tree, state) ∧ ((status (car (tree), state) = 'started)

∨ (status (car (tree), state) = 'not-started)) ∧ (total-outstanding (nodes (tree), tree, state) ≠ 0)) → ((status (car (tree), state) = 'not-started)

∨ full-channel (down-links (nodes (tree), tree), state) ∨ full-channel (up-links (cdr (nodes (tree)), tree), state))

Theorem: status-root-becomes-started-or-unchanged (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement)) → ((status (car (tree), new) = 'started)

∨ (status (car (tree), new) = status (car (tree), old)))

Theorem: root-started-or-not-started-is-invariant (initial-condition (`(and

                (all-empty ',(all-channels tree) state)
                (not-started ',(nodes tree) state)),

tree-prg (tree))

∧ treep (tree)) → invariant (`(or

              (equal
               (status ',(car tree) state)
               'started)
              (equal
               (status ',(car tree) state)
               'not-started)),

tree-prg (tree))

Theorem: total-outstanding-decreases-sublist (treep (tree) ∧ dl (down-links (nodes (tree), tree), old) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ sublistp (nodes, nodes (tree)) ∧ (node ∈ nodes) ∧ (if status (node, new) = 'started then outstanding (node, new)

else 1 + length (children (node, tree)) endif < if status (node, old) = 'started then outstanding (node, old) else 1 + length (children (node, tree)) endif))

→ (total-outstanding (nodes, tree, new)

< total-outstanding (nodes, tree, old))

Definition: tou (old, new, node, tree) = (if status (node, new) = 'started then outstanding (node, new)

else 1 + length (children (node, tree)) endif < if status (node, old) = 'started

then outstanding (node, old)

else 1 + length (children (node, tree)) endif)

Theorem: total-outstanding-decreases (treep (tree) ∧ dl (down-links (nodes (tree), tree), old) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ (node ∈ nodes (tree)) ∧ tou (old, new, node, tree)) → (total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old))

Theorem: start-decreases-tou (treep (tree) ∧ (status (car (tree), old) = 'not-started) ∧ n (old,

new,

list ('start, car (tree), rfp (car (tree), children (car (tree), tree))))) → tou (old, new, car (tree), tree)

Theorem: others-preserve-root-not-started (treep (tree) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ (statement ≠ list ('start,

car (tree),

rfp (car (tree), children (car (tree), tree)))))

→ (cdr (assoc (cons ('status, car (tree)), new)) = status (car (tree), old))

Theorem: root-receive-report-decreases-tou (treep (tree) ∧ listp (channel (cons (child, car (tree)), old)) ∧ (child ∈ children (car (tree), tree)) ∧ n (old,

new,

list ('root-receive-report, car (tree), cons (child, car (tree)))) ∧ inv (tree, old)) → tou (old, new, car (tree), tree)

Theorem: others-preserve-up-to-root-full (treep (tree) ∧ listp (channel (cons (child, car (tree)), old)) ∧ (child ∈ children (car (tree), tree)) ∧ (statement ∈ tree-prg (tree))

∧ (statement ≠ list ('root-receive-report,

car (tree),

cons (child, car (tree))))

∧ n (old, new, statement)) → listp (cdr (assoc (cons (child, car (tree)), new)))

Theorem: receive-find-decreases-tou (treep (tree) ∧ listp (channel (cons (parent (node, tree), node), old)) ∧ (node ∈ cdr (nodes (tree))) ∧ n (old,

new,

     list ('receive-find,

node,

cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree))))

∧ inv (tree, old)) → tou (old, new, node, tree)

Theorem: others-preserve-down-to-node-full (treep (tree) ∧ listp (channel (cons (parent (node, tree), node), old)) ∧ (node ∈ cdr (nodes (tree))) ∧ (statement ∈ tree-prg (tree)) ∧ (statement ≠ list ('receive-find,

node,

cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree))))

∧ n (old, new, statement)) → listp (cdr (assoc (cons (car (parent-rec ('tree, node, tree)), node), new)))

Theorem: receive-report-decreases-tou (treep (tree) ∧ listp (channel (cons (child, node), old)) ∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)) ∧ n (old,

new,

       list ('receive-report,

node,

cons (child, node),

cons (node, parent (node, tree))))

∧ inv (tree, old)) → tou (old, new, node, tree)

Theorem: others-preserve-up-to-node-full (treep (tree) ∧ listp (channel (cons (child, node), old)) ∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)) ∧ (statement ≠ list ('receive-report,

node,

cons (child, node),

cons (node, parent (node, tree))))

∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement)) → listp (cdr (assoc (cons (child, node), new)))

Event: Disable total-outstanding-decreases.

Event: Disable tou.

Event: Disable total-outstanding-decreases-sublist.

Event: Disable status-root-becomes-started-or-unchanged.

Event: Disable not-total-outstanding-0-implies-full-channel.

Event: Disable not-all-empty-implies-full-channel-full.

Event: Disable full-channel.

Event: Disable all-empty-root-started-implies-total-outstanding-0.

Event: Disable all-done-implies-total-outstanding-0.

Event: Disable all-nodes-are-done.

Event: Disable children-are-suffix-of-sublist-generalized. Event: Disable child-of-node-in-suffix-is-in-suffix. Event: Disable sublist-ulnks. Event: Disable all-empty-implies-all-empty-sublist. Event: Disable all-done-and-all-empty-implies-number-not-reported-0. Event: Disable ulnks. Event: Disable all-done-implies-all-done-sublist. Event: Disable all-done-implies-done. Event: Disable all-done. Event: Disable later-positions-are-in-suffix. Event: Disable setp-list-setp-suffix. Event: Disable childs-position-increases. Event: Disable member-suffix-member-list. Event: Disable suffix-implies-suffix-cdr. Event: Disable suffix. Event: Disable dl-and-all-empty-implies-root-defines-status. Event: Disable parent-to-root-induction. Event: Disable parents-position-decreases.

Event: Disable position-append. Event: Disable total-outstanding-non-increasing. Event: Disable total-outstanding-non-increasing-sublist. Event: Disable outstanding-non-increasing. Event: Disable dl-ul-no-preserves-no-sublist. Event: Disable dl-ul-no-preserves-instance-of-no. Event: Disable receive-report-preserves-instance-of-no. Event: Disable child-member-cdr-nodes. Event: Disable receive-report-preserves-no-for-parent. Event: Disable receive-report-preserves-no-for-node. Event: Disable receive-report-preserves-no-for-rest-of-tree. Event: Disable receive-find-preserves-instance-of-no. Event: Disable dl-down-links-implies-dl-rfp. Event: Disable down-links-1-rfp. Event: Disable dl-of-append. Event: Disable receive-find-preserves-no-for-parent-of-node. Event: Disable receive-find-preserves-no-for-node. Event: Disable receive-find-preserves-no-for-rest-of-tree.

Event: Disable root-receive-report-preserves-instance-of-no. Event: Disable setp-nodes-setp-children. Event: Disable setp-nodes-implies-setp-roots. Event: Disable number-not-reported-of-root. Event: Disable number-not-reported-of-non-root. Event: Disable min-of-reported-of-non-root. Event: Disable update-min-of-reported. Event: Disable min-of-reported-of-min. Event: Disable min-commutative-1. Event: Disable min-associative. Event: Disable min-commutative. Event: Disable start-preserves-instance-of-no. Event: Disable length-rfp. Event: Disable start-preserves-no-for-rest-of-tree. Event: Disable unchanged-preserves-no. Event: Disable start-preserves-no-for-parent. Event: Disable parent-not-started-implies-all-empty-and-not-started. Event: Disable dl-ul-no-preserves-ul.

Event: Disable dl-ul-no-preserves-ul-sublist. Event: Disable dl-ul-no-preserves-instance-of-ul. Event: Disable zero-not-reported-implies-children-reported. Event: Disable member-up-links. Event: Disable dl-preserves-dl. Event: Disable dl-preserves-sublist. Event: Disable dl-preserves-instance-of-dl. Event: Disable all-numberps-nodes-implies-all-numberps-children. Event: Disable all-numberps-forest-implies-all-numberps-roots. Event: Disable parent-not-litatom. Event: Disable all-numberps-nodes-implies-all-numberps-car-parent. Event: Disable all-numberps-nodes-implies-all-numberps-parent. Event: Disable all-numberps-append. Event: Disable send-find-general. Event: Disable assoc-equal-cons. Event: Disable send-find-implies. Event: Disable member-rfp. Event: Disable parent-of-parent-not-node.

Event: Disable parent-not-grandchild. Event: Disable parent-not-child. Event: Disable member-down-links. Event: Disable member-down-links-1. Event: Disable ul-implies-instance-of-ul-not-empty-uplink. Event: Disable no-implies-instance-of-no. Event: Disable ul-implies-instance-of-ul. Event: Disable dl-implies-instance-of-dl. Event: Disable inv-implies-augmented-correctness-condition. Event: Disable initial-conditions-imply-invariant. Event: Disable all-empty-not-started-implies-dl. Event: Disable inv. Event: Disable dl. Event: Disable node-values-constant-invariant. Event: Disable node-values-constant-unless-sufficient. Event: Disable listp-tree-prg. Event: Disable root-receive-report-prg-is-total. Event: Disable start-prg-is-total.

Event: Disable receive-report-prg-is-total. Event: Disable receive-find-prg-is-total. Event: Disable root-receive-report-func-implements-root-receive-report. Event: Disable root-receive-report-func. Event: Disable start-func-implements-start. Event: Disable start-func. Event: Disable receive-report-func-implements-receive-report. Event: Disable receive-report-func. Event: Disable receive-find-func-implements-receive-find. Event: Disable uc-of-send-find-func. Event: Disable to-node-not-in-rfp. Event: Disable parent-not-in-rfp. Event: Disable about-rfp-numberp. Event: Disable about-rfp. Event: Disable assoc-of-send-find-func. Event: Disable send-find-of-update-assoc. Event: Disable children-are-not-litatoms-member. Event: Disable children-are-not-litatoms.

Event: Disable parent-is-not-a-litatom. Event: Disable nodes-are-not-litatoms. Event: Disable send-find-func-implements-send-find. Event: Disable receive-find-func. Event: Disable send-find-func. Event: Disable no-at-termination. Event: Disable found-value-min-value-generalized. Event: Disable min-of-two-nodes-values. Event: Disable proper-tree-tree-implies-nodes-exists. Event: Disable number-not-reported-0-implies. Event: Disable total-outstanding-0-implies. Event: Disable no-implies. Event: Disable found-value-node-value-append. Event: Disable nati. Event: Disable found-value-node-value. Event: Disable down-links-is-sublistp. Event: Disable children-of-non-node. Event: Disable sublistp-down-links-1.

Event: Disable sublistp-not-started. Event: Disable nodes-in-down-links-in-nodes. Event: Disable nodes-in-channels-append. Event: Disable nodes-in-down-links-1-in-nodes. Event: Disable not-started-implies-no. Event: Disable nodes-in-channels. Event: Disable all-empty-implies-ul. Event: Disable all-empty-append. Event: Disable not-started-implies-not-started. Event: Disable all-empty-implies-empty. Event: Disable correct. Event: Disable min-node-value. Event: Disable all-empty. Event: Disable all-channels. Event: Disable not-started. Event: Disable up-links. Event: Disable down-links. Event: Disable down-links-1.

Event: Disable no. Event: Disable min-of-reported. Event: Disable number-not-reported. Event: Disable reported. Event: Disable ul. Event: Disable done. Event: Disable total-outstanding. Event: Disable treep. Event: Disable member-tree-prg. Event: Disable equal-if. Event: Disable tree-prg. Event: Disable member-root-receive-report-prg. Event: Disable root-receive-report-prg. Event: Disable member-rrrp. Event: Disable rrrp. Event: Disable member-start-prg. Event: Disable start-prg. Event: Disable member-receive-report-prg.

Event: Disable receive-report-prg. Event: Disable member-rrp. Event: Disable rrp. Event: Disable member-receive-find-prg. Event: Disable receive-find-prg. Event: Disable rfp. Event: Disable root-receive-report. Event: Disable start. Event: Disable receive-report. Event: Disable min. Event: Disable receive-find. Event: Disable send-find. Event: Disable node-value. Event: Disable outstanding. Event: Disable found-value. Event: Disable status. Event: Disable receive. Event: Disable send.

Event: Disable head. Event: Disable empty. Event: Disable channel. Event: Disable value. Event: Disable parent-not-in-children. Event: Disable parent-is-not-child. Event: Disable listp-parent-rec-equals. Event: Disable parent-is-not-itself. Event: Disable parent-is-not-itself-generalized. Event: Disable node-has-parent. Event: Disable children-of-setp-tree. Event: Disable member-subtree-member-tree. Event: Disable no-children-in-rest-of-tree. Event: Disable no-children-in-rest-of-forest. Event: Disable not-member-no-children. Event: Disable not-member-subtrees. Event: Disable proper-tree-next-level-of-proper-tree. Event: Disable proper-tree-of-append.

Event: Disable next-level-of-subtrees-in-complete-subtrees. Event: Disable next-level-in-subtrees-forest. Event: Disable subtrees-of-subtrees-in-complete-subtrees. Event: Disable subtrees-of-subtree-in-complete-subtrees. Event: Disable next-level-of-tree-in-subtrees. Event: Disable next-level-reduces-count. Event: Disable nodes-rec-forest-append. Event: Disable next-level. Event: Disable subtreep-subtrees. Event: Disable subtrees. Event: Disable subtreep. Event: Disable sublistp-children. Event: Disable sublistp-children-generalized. Event: Disable node-that-has-parent-is-in-tree. Event: Disable node-that-has-child-is-in-tree. Event: Disable member-parent-member-tree. Event: Disable parent-of-child. Event: Disable member-parent-parent.

Event: Disable member-child-tree. Event: Disable not-member-no-parent. Event: Disable plistp-roots. Event: Disable plistp-parent-rec. Event: Disable plistp-children-rec. Event: Disable member-roots-member-forest. Event: Disable parent-rec-children-rec. Event: Disable not-flag-tree. Event: Disable canonicalize-children-rec-flag. Event: Disable canonicalize-parent-rec-flag. Event: Disable canonicalize-proper-tree-flag. Event: Disable canonicalize-nodes-rec-flag. Event: Disable proper-tree. Event: Disable parent. Event: Disable parent-rec. Event: Disable children. Event: Disable children-rec. Event: Disable roots.

Event: Disable nodes. Event: Disable nodes-rec. Event: Disable sublistp-in-cons. Event: Disable sublistp-in-append. Event: Disable sublistp-reflexive. Event: Disable sublistp-easy. Event: Disable sei. Event: Disable sublistp-normalize. Event: Disable sublistp-of-sublistp-is-sublistp. Event: Disable member-of-sublistp-is-member. Event: Disable sublistp-append. Event: Disable sublistp. Event: Disable setp-member-2. Event: Disable setp-member-1. Event: Disable setp-append-canonicalize. Event: Disable setp-append-not-listp. Event: Disable setp-append-cons. Event: Disable setp-member.

Event: Disable setp-append. Event: Disable setp. Event: Disable all-numberps-implies. Event: Disable all-numberps. Event: Disable not-lessp-count-append. Event: Disable append-plistp-nil. Event: Disable plistp-append-plistp. Event: Disable plistp. Event: Disable length-append. Event: Disable listp-append. Event: Disable car-append. Event: Disable n. Theorem: member-cdr-nodes-member-nodes ((node ∈ cdr (nodes (tree))) ∧ treep (tree)) → (node ∈ nodes (tree)) Theorem: total-outstanding-decreases-expanded (treep (tree) ∧ inv (tree, old) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ (node ∈ nodes (tree)) ∧ tou (old, new, node, tree)) → (((total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old)) = t) ∧ (total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old)))

Theorem: total-outstanding-decreases-expanded-count (treep (tree) ∧ inv (tree, old) ∧ n (old, new, statement) ∧ (statement ∈ tree-prg (tree)) ∧ (node ∈ nodes (tree)) ∧ tou (old, new, node, tree) ∧ (total-outstanding (nodes (tree), tree, old) = (1 + count))) → (((total-outstanding (nodes (tree), tree, new) < (1 + count)) = t)

∧ (total-outstanding (nodes (tree), tree, new) < (1 + count)))

Theorem: total-outstanding-non-increasing-expanded (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement) ∧ inv (tree, old)) → (((total-outstanding (nodes (tree), tree, old)

< total-outstanding (nodes (tree), tree, new))

= f)

∧ (total-outstanding (nodes (tree), tree, old)

≮ total-outstanding (nodes (tree), tree, new)))

Theorem: total-outstanding-non-increasing-expanded-count (treep (tree) ∧ (statement ∈ tree-prg (tree)) ∧ n (old, new, statement) ∧ inv (tree, old) ∧ (total-outstanding (nodes (tree), tree, old) = (1 + count))) → ((((1 + count) < total-outstanding (nodes (tree), tree, old)) = f)

∧ ((1 + count) ≮ total-outstanding (nodes (tree), tree, new)))

Theorem: key-statements-member-tree-prg (treep (tree) → (list ('start, car (tree), rfp (car (tree), children (car (tree), tree)))

∈ tree-prg (tree))) ∧ ((treep (tree) ∧ (child ∈ children (car (tree), tree)))

   → (list ('root-receive-report,

car (tree),

cons (child, car (tree))) ∈ tree-prg (tree)))

∧ ((treep (tree) ∧ (node ∈ cdr (nodes (tree))))

   → (list ('receive-find,

node, cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree)))

∈ tree-prg (tree)))

∧ ((treep (tree)

∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)))

   → (list ('receive-report,

node,

cons (child, node),

cons (node, parent (node, tree))) ∈ tree-prg (tree)))

Theorem: down-link-full-decreases-total-outstanding-ensures (treep (tree) ∧ (node ∈ cdr (nodes (tree))) ∧ inv (tree, old) ∧ listp (channel (cons (parent (node, tree), node), old)) ∧ n (old,

new,

     list ('receive-find,

node,

cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree)))))

→ (total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old))

Theorem: down-link-full-unless (treep (tree) ∧ (node ∈ cdr (nodes (tree))) ∧ listp (channel (cons (parent (node, tree), node), old)) ∧ (statement ∈ tree-prg (tree)) ∧ (statement ≠ list ('receive-find,

node,

cons (parent (node, tree), node), cons (node, parent (node, tree)), rfp (node, children (node, tree))))

∧ n (old, new, statement)) → listp (channel (cons (parent (node, tree), node), new))

Theorem: down-link-full-decreases-total-outstanding (treep (tree) ∧ (node ∈ cdr (nodes (tree)))) → leads-to (`(and

             (inv ',tree state)

             (and
              (listp
               (channel
                ',(cons (parent node tree) node)
                state))
              (equal
               (total-outstanding
                ',(nodes tree)
                ',tree
                state)
               ',(add1 count)))),
           `(lessp
             (total-outstanding
              ',(nodes tree)
              ',tree
              state)
             ',(add1 count)),

tree-prg (tree))

Theorem: member-car-tree-nodes-tree treep (tree) → (car (tree) ∈ nodes (tree))

Theorem: root-up-link-full-decreases-total-outstanding-ensures (treep (tree) ∧ inv (tree, old) ∧ (child ∈ children (car (tree), tree)) ∧ listp (channel (cons (child, car (tree)), old)) ∧ n (old,

new,

list ('root-receive-report, car (tree), cons (child, car (tree))))) → (total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old))

Theorem: root-up-link-full-unless (treep (tree) ∧ (child ∈ children (car (tree), tree)) ∧ listp (channel (cons (child, car (tree)), old)) ∧ (statement ∈ tree-prg (tree))

∧ (statement ≠ list ('root-receive-report,

car (tree),

cons (child, car (tree))))

∧ n (old, new, statement)) → listp (channel (cons (child, car (tree)), new))

Theorem: up-link-full-decreases-total-outstanding-ensures (treep (tree) ∧ inv (tree, old) ∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)) ∧ listp (channel (cons (child, node), old)) ∧ n (old,

new,

     list ('receive-report,

node,

cons (child, node),

cons (node, parent (node, tree)))))

→ (total-outstanding (nodes (tree), tree, new)

< total-outstanding (nodes (tree), tree, old))

Theorem: up-link-full-unless (treep (tree) ∧ (node ∈ cdr (nodes (tree))) ∧ (child ∈ children (node, tree)) ∧ listp (channel (cons (child, node), old)) ∧ (statement ∈ tree-prg (tree)) ∧ (statement ≠ list ('receive-report,

node,

cons (child, node),

cons (node, parent (node, tree))))

∧ n (old, new, statement)) → listp (channel (cons (child, node), new))

Theorem: member-cdr-nodes-equals (treep (tree) ∧ (node ≠ car (tree))) → ((node ∈ nodes (tree)) = (node ∈ cdr (nodes (tree))))

Theorem: up-link-full-decreases-total-outstanding (treep (tree) ∧ (node ∈ nodes (tree)) ∧ (child ∈ children (node, tree))) → leads-to (`(and

             (inv ',tree state)
             (and
              (listp
               (channel ',(cons child node) state))
              (equal
               (total-outstanding
                ',(nodes tree)
                ',tree
                state)
               ',(add1 count)))),
           `(lessp

(total-outstanding
',(nodes tree)
',tree
state)
',(add1 count)),

tree-prg (tree))

Theorem: not-started-root-decreases-total-outstanding-ensures (treep (tree) ∧ inv (tree, old) ∧ (status (car (tree), old) = 'not-started) ∧ n (old,

new, list ('start, car (tree), rfp (car (tree), children (car (tree), tree)))))

→ (total-outstanding (nodes (tree), tree, new) < total-outstanding (nodes (tree), tree, old))

Theorem: not-started-root-unless (treep (tree) ∧ (status (car (tree), old) = 'not-started) ∧ (statement ∈ tree-prg (tree)) ∧ (statement ≠ list ('start,

car (tree),

rfp (car (tree), children (car (tree), tree))))

∧ n (old, new, statement)) → (status (car (tree), new) = 'not-started)

Theorem: not-started-root-decreases-total-outstanding treep (tree) → leads-to (`(and

(inv ',tree state)
(and
(equal
 (status ',(car tree) state)
 'not-started)
(equal
 (total-outstanding
  ',(nodes tree)
  ',tree
  state)
 ',(add1 count)))),
`(lessp
(total-outstanding
',(nodes tree)
',tree

state)
',(add1 count)),

tree-prg (tree))

Theorem: full-channel-not-f-implies full-channel (channels, state) → ((full-channel (channels, state) ∈ channels)

∧ listp (channel (full-channel (channels, state), state)))

Theorem: total-outstanding-decreases-leads-to (treep (tree) ∧ initial-condition (`(and

      (all-empty
       ',(all-channels tree)
       state)
      (not-started ',(nodes tree) state)),

tree-prg (tree)))

→ leads-to (`(equal

(total-outstanding
',(nodes tree)
',tree
state)
',(add1 count)),
`(lessp
(total-outstanding
',(nodes tree)
',tree
state)
',(add1 count)),

tree-prg (tree))

Theorem: termination-induction (treep (tree) ∧ initial-condition (`(and

      (all-empty
       ',(all-channels tree)
       state)
      (not-started ',(nodes tree) state)),

tree-prg (tree)))

→ leads-to (`(lessp

(total-outstanding
',(nodes tree)
',tree
state)
',(add1 count)),

`(equal
(total-outstanding
',(nodes tree)
',tree
state)
0),

tree-prg (tree))

Theorem: termination (treep (tree) ∧ initial-condition (`(and

      (all-empty
       ',(all-channels tree)
       state)
      (not-started ',(nodes tree) state)),

tree-prg (tree)))

→ leads-to ('(true),

`(equal
(total-outstanding
',(nodes tree)
',tree
state)
0),

tree-prg (tree))

Theorem: correctness-condition (treep (tree) ∧ initial-condition (`(and

      (all-empty
       ',(all-channels tree)
       state)
      (not-started ',(nodes tree) state)),

tree-prg (tree)))

→ leads-to ('(true), `(correct ',tree state), tree-prg (tree))

Index

about-rfp, 23 about-rfp-numberp, 23 all-channels, 18, 20 all-done, 43, 44 all-done-and-all-empty-implies-

number-not-reported-0, 43 all-done-implies-all-done-subli

st, 43 all-done-implies-done, 43 all-done-implies-total-outstandi

ng-0, 44 all-empty, 18–20, 31, 42–44 all-empty-append, 19 all-empty-implies-all-empty-sub

list, 43 all-empty-implies-empty, 19 all-empty-implies-ul, 19 all-empty-not-started-implies-d

l, 19 all-empty-root-started-implies-t

otal-outstanding-0, 44 all-nodes-are-done, 44 all-numberps, 1, 16, 23, 29, 30, 33,

34, 38 all-numberps-append, 29 all-numberps-do-not-contain-lit

atom, 29 all-numberps-forest-implies-all

-numberps-roots, 29 all-numberps-implies, 1 all-numberps-nodes-implies-all-

numberps-car-parent, 29 numberps-children, 30 numberps-parent, 29

append-plistp-nil, 1 assoc-equal-cons, 29 assoc-of-channel-preserved-root

-receive-report, 29 assoc-of-send-find-func, 23

canonicalize-children-rec-flag, 4 canonicalize-nodes-rec-flag, 4 canonicalize-parent-rec-flag, 4 canonicalize-proper-tree-flag, 4 car-append, 1 changed, 10–12, 32–39 channel, 9–12, 16, 19, 27, 30, 31, 33,

34, 38, 46–48, 65–67, 69 child-member-cdr-nodes, 39 child-of-node-in-suffix-is-in-s

uffix, 43 children, 3, 12–17, 21, 28, 32, 33, 35,

37–41, 43, 45–48, 64–68 children-are-not-litatoms, 23 children-are-not-litatoms-membe

r, 23 children-are-suffix-of-sublist-

generalized, 44 children-of-non-node, 20 children-of-setp-tree, 8 children-rec, 3–6, 8, 9, 20, 23, 28,

30, 35, 39, 42, 44 childs-position-increases, 42 correct, 18, 22 correctness-condition, 70

dl, 16, 18, 19, 27, 30–32, 37, 39–42,

44–46 dl-and-all-empty-implies-root-de

fines-status, 42 dl-down-links-implies-dl-rfp, 37 dl-implies-instance-of-dl, 27 dl-of-append, 37 dl-preserves-dl, 30 dl-preserves-instance-of-dl, 30 dl-preserves-sublist, 30 dl-ul-no-preserves-instance-of-

no, 40 ul, 30

dl-ul-no-preserves-no-sublist, 40 dl-ul-no-preserves-ul, 31 dl-ul-no-preserves-ul-sublist, 31 done, 16, 27, 31, 33, 34, 38, 43 down-link-full-decreases-total-

outstanding, 65 outstanding-ensures, 65

down-link-full-unless, 65 down-links, 17–20, 28, 30, 31, 37,

39–42, 44–46 down-links-1, 17, 19, 20, 28, 37 down-links-1-rfp, 37 down-links-is-sublistp, 20

empty, 9, 11, 16, 18, 24, 25, 27, 30,

31, 36, 39, 44 equal-if, 15

found-value, 10–12, 16–18, 20, 24,

25, 27, 31–35, 37–40 found-value-min-value-generalize

d, 21 found-value-node-value, 20–22 found-value-node-value-append, 20 full-channel, 44, 45, 69 full-channel-not-f-implies, 69

head, 9–12, 22, 24, 25

initial-condition, 27, 40, 45, 69, 70 initial-conditions-imply-invari

ant, 20 inv, 18, 20, 22, 40, 44–48, 63–68 inv-implies-augmented-correctne

ss-condition, 22 inv-is-invariant, 40 inv-preserves-inv, 40 invariant, 27, 41, 45

key-statements-member-tree-prg, 64

later-positions-are-in-suffix, 42 leads-to, 66, 68–70 length, 1, 10, 11, 16, 22, 25, 32, 36,

41, 45, 46 length-append, 1 length-rfp, 32 listp-append, 1 listp-parent-rec-equals, 9 listp-tree-prg, 26

member-car-tree-nodes-tree, 66 member-cdr-nodes-equals, 67 member-cdr-nodes-member-nodes, 63 member-child-tree, 5 member-down-links, 28 member-down-links-1, 28 member-of-sublistp-is-member, 2 member-parent-member-tree, 6 member-parent-parent, 6 member-receive-find-prg, 12 member-receive-report-prg, 13 member-rfp, 28 member-root-receive-report-prg, 14 member-roots-member-forest, 5 member-rrp, 13 member-rrrp, 14 member-start-prg, 14 member-subtree-member-tree, 8 member-suffix-member-list, 42 member-tree-prg, 15 member-up-links, 30 min, 11, 12, 17, 18, 21, 24, 25, 33,

39 min-associative, 33 min-commutative, 33 min-commutative-1, 33 min-node-value, 18, 20, 21 min-of-reported, 17, 21, 28, 32–40 min-of-reported-of-min, 33 min-of-reported-of-non-root, 33 min-of-two-nodes-values, 21

n, 24, 25, 30, 31, 40, 41, 45–48, 63–

68 nati, 20 next-level, 7, 8, 20 next-level-in-subtrees-forest, 7 next-level-of-subtrees-in-complete

-subtrees, 7 next-level-of-tree-in-subtrees, 7 next-level-reduces-count, 7 no, 17–19, 21, 22, 28, 31, 39, 40, 44 no-at-termination, 21 no-children-in-rest-of-forest, 8 no-children-in-rest-of-tree, 8 no-implies, 21 no-implies-instance-of-no, 28 node-has-parent, 8 node-that-has-child-is-in-tree, 6 node-that-has-parent-is-in-tree, 6 node-value, 10, 11, 17, 18, 20–22,

25, 28, 33, 35, 37, 38, 40 node-values-constant-invariant, 27 node-values-constant-unless-suf

ficient, 26 nodes, 3, 14–16, 18–20, 22, 24, 26,

27, 30–32, 35, 37, 39–48, 63–68

nodes-are-not-litatoms, 23 nodes-in-channels, 19, 20 nodes-in-channels-append, 19 nodes-in-down-links-1-in-nodes, 19 nodes-in-down-links-in-nodes, 19 nodes-rec, 3–9, 20–23, 28–30, 35, 39,

41, 42 nodes-rec-forest-append, 7 not-all-empty-implies-full-chan

nel-full, 44 not-flag-tree, 5 not-lessp-count-append, 1 not-member-no-children, 8 not-member-no-parent, 5 not-member-subtrees, 8 not-started, 18–20, 31, 36 not-started-implies-no, 19 not-started-implies-not-started, 19 not-started-root-decreases-tota

l-outstanding, 68

l-outstanding-ensures, 68 not-started-root-unless, 68 not-total-outstanding-0-implies

-full-channel, 45 number-not-reported, 17, 21, 28, 30,

32–40, 43 number-not-reported-0-implies, 21 number-not-reported-of-non-root, 34 number-not-reported-of-root, 34

others-preserve-down-to-node-fu

ll, 47 others-preserve-root-not-starte

d, 46 others-preserve-up-to-node-full, 48 others-preserve-up-to-root-full, 47 outstanding, 10–12, 16, 17, 24, 25,

30, 32, 33, 35–41, 45, 46 outstanding-non-increasing, 41

parent, 4, 12, 13, 15, 18, 30, 37, 39, 42, 47, 48, 65, 67

parent-is-not-a-litatom, 23

parent-is-not-child, 9 parent-is-not-itself, 9 parent-is-not-itself-generalize

d, 8 parent-not-child, 28 parent-not-grandchild, 28 parent-not-in-children, 9 parent-not-in-rfp, 23 parent-not-litatom, 29 parent-not-started-implies-all-e mpty-and-not-started, 31

parent-of-child, 6

parent-of-parent-not-node, 28

parent-rec, 4–6, 8, 9, 23, 28, 29, 41,

47 parent-rec-children-rec, 5 parent-to-root-induction, 42 parents-position-decreases, 41 plistp, 1, 2, 5 plistp-append-plistp, 1 plistp-children-rec, 5 plistp-parent-rec, 5 plistp-roots, 5 position, 41–43 position-append, 41 proper-tree, 4–9, 16, 19–23, 28, 35,

39, 41–45 proper-tree-next-level-of-prope

r-tree, 8 proper-tree-of-append, 8 proper-tree-tree-implies-nodes-e

xists, 21

receive, 9–12, 22, 24, 25, 33, 34, 38 receive-find, 10, 37 receive-find-decreases-tou, 47 receive-find-func, 22, 24, 26 receive-find-func-implements-re

ceive-find, 24 receive-find-preserves-instance

-of-no, 37 receive-find-preserves-no-for-n

ode, 36 receive-find-preserves-no-for-p

arent-of-node, 36 receive-find-preserves-no-for-re

st-of-tree, 35 receive-find-prg, 12, 14, 24, 26 receive-find-prg-is-total, 26 receive-report, 11, 39 receive-report-decreases-tou, 47 receive-report-func, 24–26 receive-report-func-implements-

receive-report, 24 receive-report-preserves-instan

ce-of-no, 39 receive-report-preserves-no-for

-node, 38 -parent, 39 -rest-of-tree, 38

receive-report-prg, 13, 14, 24, 26 receive-report-prg-is-total, 26 reported, 16, 17, 21 rfp, 12–15, 23, 24, 28, 31, 32, 36, 37,

46, 47, 64, 65, 68 root-receive-report, 11, 35 root-receive-report-decreases-t

ou, 46 root-receive-report-func, 25, 26 root-receive-report-func-impleme

nts-root-receive-report, 25 root-receive-report-preserves-i

nstance-of-no, 35 root-receive-report-prg, 14, 25, 26 root-receive-report-prg-is-tota

l, 26 root-started-or-not-started-is-i

nvariant, 45 root-up-link-full-decreases-tot

al-outstanding-ensures, 66 root-up-link-full-unless, 66 roots, 3–5, 8, 9, 21, 29, 35, 41 rrp, 13 rrrp, 14

sei, 2 send, 9–11, 22, 24, 29 send-find, 10, 11, 23, 29 send-find-func, 22–25 send-find-func-implements-send-

find, 23 send-find-general, 29 send-find-implies, 29 send-find-of-update-assoc, 23 setp, 1, 2, 5, 6, 8, 9, 16, 22, 23, 28,

29, 33–35, 38, 39, 41–45 setp-append, 2 setp-append-canonicalize, 2 setp-append-cons, 2 setp-append-not-listp, 2 setp-list-setp-suffix, 42 setp-member, 2 setp-member-1, 2 setp-member-2, 2 setp-nodes-implies-setp-roots, 35 setp-nodes-setp-children, 35 setp-tree-unique-parent, 5 start, 11, 32 start-decreases-tou, 46 start-func, 25, 26 start-func-implements-start, 25 start-preserves-instance-of-no, 32 start-preserves-no-for-parent, 31 start-preserves-no-for-rest-of-t

ree, 32 start-prg, 13, 14, 25, 26 start-prg-is-total, 26 status, 10, 11, 16–18, 21, 25, 27, 28,

30–32, 35–37, 39–42, 44– 46, 68

status-root-becomes-started-or-

unchanged, 45 sublist-ulnks, 43 sublistp, 2, 3, 6, 7, 20, 22, 24, 30,

31, 36, 40, 41, 43–45 sublistp-append, 2 sublistp-children, 6 sublistp-children-generalized, 6 sublistp-down-links-1, 20 sublistp-easy, 3 sublistp-in-append, 3 sublistp-in-cons, 3 sublistp-normalize, 2 sublistp-not-started, 20 sublistp-of-sublistp-is-sublistp, 2 sublistp-reflexive, 3 subtreep, 6, 7 subtreep-subtrees, 7 subtrees, 7, 8, 22 subtrees-of-subtree-in-complete

-subtrees, 7 subtrees-of-subtrees-in-complete

-subtrees, 7 suffix, 42–44 suffix-implies-suffix-cdr, 42

termination, 70 termination-induction, 69 to-node-not-in-rfp, 24 total, 26 total-outstanding, 16, 21, 22, 41, 44–

46, 63–68 total-outstanding-0-implies, 21 total-outstanding-decreases, 46 total-outstanding-decreases-exp

anded, 63

anded-count, 64 total-outstanding-decreases-lea

ds-to, 69 total-outstanding-decreases-sub

list, 45 total-outstanding-non-increasin

g, 41

g-expanded, 64

g-expanded-count, 64 g-sublist, 41 total-sufficient, 26 total-tree-prg, 26 tou, 46–48, 63, 64 tree-prg, 14, 15, 26, 27, 30, 31, 40, 41, 45–48, 63–70 treep, 16, 24–27, 30–32, 35, 37, 39– 41, 45–48, 63–70

uc, 24, 29

uc-of-send-find-func, 24

ul, 16, 18, 19, 27, 31, 35, 39, 40, 44 ul-implies-instance-of-ul, 27 ul-implies-instance-of-ul-not-e mpty-uplink, 27

ulnks, 43

unchanged-preserves-no, 32

unless-sufficient, 27

up-link-full-decreases-total-out standing, 67 standing-ensures, 67

up-link-full-unless, 67

up-links, 18, 30, 31, 35, 39, 40, 43–

45 update-assoc, 22–25 update-min-of-reported, 33

value, 9, 10

zero-not-reported-implies-child ren-reported, 30