(note-lib "interpreter") ;;;List Operations (prove-lemma car-append (rewrite) (equal (car (append a b)) (if (listp a) (car a) (car b)))) (prove-lemma listp-append (rewrite) (equal (listp (append a b)) (or (listp a) (listp b)))) (prove-lemma length-append (rewrite) (equal (length (append a b)) (plus (length a) (length b)))) (defn plistp (list) (if (listp list) (plistp (cdr list)) (equal list nil))) (prove-lemma plistp-append-plistp (rewrite) (equal (plistp (append a b)) (plistp b))) (prove-lemma append-plistp-nil (rewrite) (equal (equal (append a nil) a) (plistp a))) (prove-lemma not-lessp-count-append (rewrite) (not (lessp (plus (count x) (count y)) (count (append x y))))) (defn all-numberps (list) (if (listp list) (if (numberp (car list)) (all-numberps (cdr list)) f) t)) (prove-lemma all-numberps-implies (rewrite) (implies (and (all-numberps list) (member e list)) (numberp e))) ;;;Set Operations (defn setp (list) (if (listp list) (if (member (car list) (cdr list)) f (setp (cdr list))) t)) (prove-lemma setp-append (rewrite) (implies (or (not (setp a)) (not (setp b))) (not (setp (append a b))))) (prove-lemma setp-member (rewrite) (implies (and (member x a) (member x b)) (not (setp (append a b))))) (prove-lemma setp-append-cons (rewrite) (equal (setp (append a (cons x b))) (setp (cons x (append a b))))) (prove-lemma setp-append-not-listp (rewrite) (implies (not (listp b)) (equal (setp (append a b)) (setp a)))) (prove-lemma setp-append-canonicalize (rewrite) (equal (setp (append a b)) (setp (append b a)))) (prove-lemma setp-member-1 (rewrite) (implies (and (setp (append a b)) (member x b)) (not (member x a)))) (prove-lemma setp-member-2 (rewrite) (implies (and (setp (append a b)) (member x a)) (not (member x b)))) ;;;Subset Operations (defn sublistp (sub list) (if (listp sub) (and (member (car sub) list) (sublistp (cdr sub) list)) t)) (prove-lemma sublistp-append (rewrite) (equal (sublistp (append a b) list) (and (sublistp a list) (sublistp b list)))) (prove-lemma member-of-sublistp-is-member (rewrite) (implies (and (member a b) (sublistp b c)) (member a c))) (prove-lemma sublistp-of-sublistp-is-sublistp (rewrite) (implies (and (sublistp a b) (sublistp b c)) (sublistp a c))) (prove-lemma sublistp-normalize (rewrite) (implies (not (plistp b)) (equal (sublistp a b) (sublistp a (append b nil))))) (defn sei (a b) (if (listp a) (sei (cdr a) (append b (list (car a)))) t)) (prove-lemma sublistp-easy (rewrite) (sublistp a (append b a)) ((induct (sei a b)))) (prove-lemma sublistp-reflexive (rewrite) (sublistp a a) ((use (sublistp-easy (b nil))))) (prove-lemma sublistp-in-append (rewrite) (implies (or (sublistp x a) (sublistp x b)) (sublistp x (append a b)))) (prove-lemma sublistp-in-cons (rewrite) (implies (sublistp a y) (sublistp a (cons x y)))) ;;;Tree Operations (defn nodes-rec (flag tree) (if (listp tree) (if (equal flag 'tree) (cons (car tree) (nodes-rec 'forest (cdr tree))) (append (nodes-rec 'tree (car tree)) (nodes-rec 'forest (cdr tree)))) nil)) (defn nodes (tree) (nodes-rec 'tree tree)) (defn roots (forest) (if (listp forest) (cons (caar forest) (roots (cdr forest))) forest)) (defn children-rec (flag node tree) (if (listp tree) (if (equal flag 'tree) (if (equal (car tree) node) (append (roots (cdr tree)) (children-rec 'forest node (cdr tree))) (children-rec 'forest node (cdr tree))) (append (children-rec 'tree node (car tree)) (children-rec 'forest node (cdr tree)))) nil)) (defn children (node tree) (children-rec 'tree node tree)) (defn parent-rec (flag node tree) (if (listp tree) (if (equal flag 'tree) (if (member node (roots (cdr tree))) (cons (car tree) (parent-rec 'forest node (cdr tree))) (parent-rec 'forest node (cdr tree))) (append (parent-rec 'tree node (car tree)) (parent-rec 'forest node (cdr tree)))) nil)) (defn parent (node tree) (car (parent-rec 'tree node tree))) (defn proper-tree (flag tree) (if (equal flag 'tree) (if (listp tree) (proper-tree 'forest (cdr tree)) f) (if (listp tree) (and (proper-tree 'tree (car tree)) (proper-tree 'forest (cdr tree))) (equal tree nil)))) (prove-lemma canonicalize-nodes-rec-flag () (equal (nodes-rec flag tree) (if (equal flag 'tree) (nodes-rec 'tree tree) (nodes-rec 'forest tree)))) (prove-lemma canonicalize-proper-tree-flag () (equal (proper-tree flag tree) (if (equal flag 'tree) (proper-tree 'tree tree) (proper-tree 'forest tree)))) (prove-lemma canonicalize-parent-rec-flag () (equal (parent-rec flag child tree) (if (equal flag 'tree) (parent-rec 'tree child tree) (parent-rec 'forest child tree)))) (prove-lemma canonicalize-children-rec-flag () (equal (children-rec flag parent tree) (if (equal flag 'tree) (children-rec 'tree parent tree) (children-rec 'forest parent tree)))) (prove-lemma not-flag-tree (rewrite) (implies (and (not (equal flag 'tree)) (not (equal flag 'forest))) (and (equal (nodes-rec flag tree) (nodes-rec 'forest tree)) (equal (proper-tree flag tree) (proper-tree 'forest tree)) (equal (parent-rec flag child tree) (parent-rec 'forest child tree)) (equal (children-rec flag parent tree) (children-rec 'forest parent tree)))) ((use (canonicalize-nodes-rec-flag) (canonicalize-proper-tree-flag) (canonicalize-parent-rec-flag) (canonicalize-children-rec-flag)))) (prove-lemma parent-rec-children-rec (rewrite) (equal (member child (children-rec flag parent tree)) (member parent (parent-rec flag child tree)))) (disable parent-rec-children-rec) (prove-lemma plistp-children-rec (rewrite) (plistp (children-rec flag parent tree))) (prove-lemma plistp-parent-rec (rewrite) (plistp (parent-rec flag child tree))) (prove-lemma plistp-roots (rewrite) (implies (proper-tree 'forest forest) (plistp (roots forest)))) (prove-lemma member-roots-member-forest (rewrite) (implies (and (proper-tree 'forest forest) (member node (roots forest))) (member node (nodes-rec 'forest forest)))) (prove-lemma not-member-no-parent (rewrite) (implies (and (proper-tree flag tree) (not (member node (nodes-rec flag tree)))) (equal (parent-rec flag node tree) nil))) (prove-lemma member-child-tree (rewrite) (implies (and (proper-tree flag tree) (member child (children-rec flag node tree))) (member child (nodes-rec flag tree)))) (prove-lemma setp-tree-unique-parent (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree))) (equal (parent-rec flag child tree) (if (member child (nodes-rec flag tree)) (if (or (and (equal flag 'tree) (equal (car tree) child)) (and (not (equal flag 'tree)) (member child (roots tree)))) nil (list (car (parent-rec flag child tree)))) nil)))) (disable setp-tree-unique-parent) (prove-lemma member-parent-parent (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree)) (member parent (parent-rec flag child tree))) (equal (parent-rec flag child tree) (list parent))) ((INSTRUCTIONS PROMOTE (DIVE 1) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP (DEMOTE 3) (DIVE 1) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE))) (prove-lemma parent-of-child (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree)) (member child (children-rec flag parent tree))) (equal (parent-rec flag child tree) (list parent))) ((enable parent-rec-children-rec))) (prove-lemma member-parent-member-tree (rewrite) (implies (member parent (parent-rec flag child tree)) (member parent (nodes-rec flag tree)))) (prove-lemma node-that-has-child-is-in-tree (rewrite) (implies (listp (children-rec flag parent tree)) (member parent (nodes-rec flag tree)))) (prove-lemma node-that-has-parent-is-in-tree (rewrite) (implies (and (proper-tree flag tree) (listp (parent-rec flag child tree))) (member child (nodes-rec flag tree)))) (prove-lemma sublistp-children-generalized (rewrite) (implies (and (proper-tree flag tree) (sublistp children (children-rec flag parent tree))) (sublistp children (nodes-rec flag tree))) ((induct (length children)))) (disable sublistp-children-generalized) (prove-lemma sublistp-children (rewrite) (implies (proper-tree flag tree) (sublistp (children-rec flag parent tree) (nodes-rec flag tree))) ((use (sublistp-children-generalized (children (children-rec flag parent tree)))))) (defn subtreep (flag subtree tree) (if (and (listp tree) (listp subtree)) (if (equal flag 'tree) (if (equal subtree tree) t (subtreep 'forest subtree (cdr tree))) (if (subtreep 'tree subtree (car tree)) t (subtreep 'forest subtree (cdr tree)))) f)) (defn subtrees (flag tree) (if (listp tree) (if (equal flag 'tree) (cons tree (subtrees 'forest (cdr tree))) (append (subtrees 'tree (car tree)) (subtrees 'forest (cdr tree)))) nil)) (prove-lemma subtreep-subtrees (rewrite) (implies (member subtree (subtrees flag tree)) (subtreep flag subtree tree))) (defn next-level (subtrees) (if (listp subtrees) (append (cdar subtrees) (next-level (cdr subtrees))) subtrees)) (prove-lemma nodes-rec-forest-append (rewrite) (equal (nodes-rec 'forest (append a b)) (append (nodes-rec 'forest a) (nodes-rec 'forest b)))) (prove-lemma next-level-reduces-count (rewrite) (implies (listp subtrees) (lessp (count (next-level subtrees)) (count subtrees)))) (prove-lemma next-level-of-tree-in-subtrees (rewrite) (implies (proper-tree 'forest forest) (sublistp forest (subtrees 'forest forest))) ((expand (subtrees 'tree (car forest))))) (prove-lemma subtrees-of-subtree-in-complete-subtrees (rewrite) (implies (and (proper-tree 'tree subtree) (member subtree (subtrees flag tree))) (sublistp (subtrees 'tree subtree) (subtrees flag tree)))) (prove-lemma subtrees-of-subtrees-in-complete-subtrees (rewrite) (implies (and (proper-tree 'forest subtrees) (sublistp subtrees (subtrees flag tree))) (sublistp (subtrees 'forest subtrees) (subtrees flag tree))) ((induct (length subtrees)))) (prove-lemma next-level-in-subtrees-forest (rewrite) (implies (proper-tree 'forest subtrees) (sublistp (next-level subtrees) (subtrees 'forest subtrees)))) (prove-lemma next-level-of-subtrees-in-complete-subtrees (rewrite) (implies (and (proper-tree 'forest subtrees) (sublistp subtrees (subtrees flag tree))) (sublistp (next-level subtrees) (subtrees flag tree))) ((use (sublistp-of-sublistp-is-sublistp (a (next-level subtrees)) (b (subtrees 'forest subtrees)) (c (subtrees flag tree)))))) (prove-lemma proper-tree-of-append (rewrite) (implies (and (proper-tree 'forest a) (proper-tree 'forest b)) (proper-tree 'forest (append a b)))) (prove-lemma proper-tree-next-level-of-proper-tree (rewrite) (implies (proper-tree 'forest subtrees) (proper-tree 'forest (next-level subtrees)))) (prove-lemma not-member-subtrees (rewrite) (implies (not (member root (nodes-rec flag tree))) (not (member (cons root forest) (subtrees flag tree))))) (prove-lemma not-member-no-children (rewrite) (implies (not (member parent (nodes-rec flag tree))) (equal (children-rec flag parent tree) nil))) (prove-lemma no-children-in-rest-of-forest (rewrite) (implies (and (setp (append (nodes-rec 'tree tree) (nodes-rec 'forest forest))) (member parent (nodes-rec 'tree tree))) (equal (children-rec 'forest parent forest) nil))) (prove-lemma no-children-in-rest-of-tree (rewrite) (implies (and (setp (append (nodes-rec 'tree tree) (nodes-rec 'forest forest))) (member parent (nodes-rec 'forest forest))) (equal (children-rec 'tree parent tree) nil))) (prove-lemma member-subtree-member-tree (rewrite) (implies (member (cons root forest) (subtrees flag tree)) (member root (nodes-rec flag tree)))) (prove-lemma children-of-setp-tree (rewrite) (implies (and (setp (nodes-rec flag tree)) (proper-tree flag tree) (member (cons root forest) (subtrees flag tree))) (equal (children-rec flag root tree) (roots forest))) ((induct (children-rec flag root tree)))) (prove-lemma node-has-parent (rewrite) (implies (and (member node (nodes-rec flag tree)) (proper-tree flag tree) (if (equal flag 'tree) (not (equal node (car tree))) (not (member node (roots tree))))) (member (car (parent-rec flag node tree)) (nodes-rec flag tree)))) (prove-lemma parent-is-not-itself-generalized (rewrite) (implies (and (setp (nodes-rec flag tree)) (proper-tree flag tree) (listp (parent-rec flag child tree))) (not (equal child (car (parent-rec flag child tree)))))) (prove-lemma parent-is-not-itself (rewrite) (implies (and (setp (nodes-rec 'tree tree)) (proper-tree 'tree tree) (member child (cdr (nodes-rec 'tree tree)))) (not (equal child (car (parent-rec 'tree child tree))))) ((use (setp-tree-unique-parent (child child) (tree tree) (flag 'tree)) (parent-is-not-itself-generalized (flag 'tree))) (disable parent-is-not-itself-generalized))) (prove-lemma listp-parent-rec-equals (rewrite) (implies (and (setp (nodes-rec flag tree)) (proper-tree flag tree)) (equal (listp (parent-rec flag child tree)) (and (member child (nodes-rec flag tree)) (if (equal flag 'tree) (not (equal child (car tree))) (not (member child (roots tree))))))) ((use (setp-tree-unique-parent)))) (prove-lemma parent-is-not-child (rewrite) (implies (and (setp (nodes-rec flag tree)) (proper-tree flag tree) (listp (parent-rec flag child tree))) (not (member (car (parent-rec flag child tree)) (children-rec flag child tree))))) (prove-lemma parent-not-in-children (rewrite) (implies (and (setp (nodes-rec 'tree tree)) (proper-tree 'tree tree) (member parent (cdr (nodes-rec 'tree tree)))) (not (member parent (children-rec 'tree parent tree)))) ((INSTRUCTIONS PROMOTE (DIVE 1) (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) (DIVE 1) (DIVE 2) X TOP bash))) ;;; Variables and channel operations (defn value (key state) (cdr (assoc key state))) (defn channel (name state) (value name state)) (defn empty (name state) (not (listp (channel name state)))) (defn head (name state) (car (channel name state))) (defn send (channel message state) (append (channel channel state) (list message))) (defn receive (channel state) (cdr (channel channel state))) ;;; Program Specific (defn status (node state) (value (cons 'status node) state)) (defn found-value (node state) (value (cons 'found-value node) state)) (defn outstanding (node state) (value (cons 'outstanding node) state)) (defn node-value (node state) (value (cons 'node-value node) state)) (defn send-find (to-children old new) (if (listp to-children) (and (equal (channel (car to-children) new) (send (car to-children) 'find old)) (send-find (cdr to-children) old new)) t)) ;;; The four program statements (defn receive-find (old new node from-parent to-parent to-children) (if (equal (head from-parent old) 'find) (and (equal (channel from-parent new) (receive from-parent old)) (equal (status node new) 'started) (equal (found-value node new) (node-value node old)) (equal (outstanding node new) (length to-children)) (send-find to-children old new) (equal (channel to-parent new) (if (zerop (length to-children)) (send to-parent (node-value node old) old) (channel to-parent old))) (changed old new (append (list from-parent to-parent (cons 'status node) (cons 'found-value node) (cons 'outstanding node)) to-children))) (changed old new nil))) (defn min (x y) (if (lessp x y) (fix x) (fix y))) (defn receive-report (old new node from-child to-parent) (if (empty from-child old) (changed old new nil) (and (equal (channel from-child new) (receive from-child old)) (equal (found-value node new) (min (found-value node old) (head from-child old))) (equal (outstanding node new) (sub1 (outstanding node old))) (equal (channel to-parent new) (if (zerop (outstanding node new)) (send to-parent (found-value node new) old) (channel to-parent old))) (changed old new (list from-child to-parent (cons 'outstanding node) (cons 'found-value node)))))) (defn start (old new root to-children) (if (equal (status root old) 'not-started) (and (equal (status root new) 'started) (equal (found-value root new) (node-value root old)) (equal (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))) (changed old new nil))) (defn root-receive-report (old new root from-child) (if (empty from-child old) (changed old new nil) (and (equal (channel from-child new) (receive from-child old)) (equal (found-value root new) (min (found-value root old) (head from-child old))) (equal (outstanding root new) (sub1 (outstanding root old))) (changed old new (list from-child (cons 'outstanding root) (cons 'found-value root)))))) ;;; The Program (defn rfp (node children) (if (listp children) (cons (cons node (car children)) (rfp node (cdr children))) nil)) (defn receive-find-prg (nodes tree) (if (listp nodes) (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)) nil)) (prove-lemma member-receive-find-prg (rewrite) (equal (member statement (receive-find-prg nodes tree)) (and (equal (car statement) 'receive-find) (member (cadr statement) nodes) (listp (caddr statement)) (equal (caaddr statement) (parent (cadr statement) tree)) (equal (cdaddr statement) (cadr statement)) (listp (cadddr statement)) (equal (caadddr statement) (cadr statement)) (equal (cdadddr statement) (parent (cadr statement) tree)) (equal (caddddr statement) (rfp (cadr statement) (children (cadr statement) tree))) (equal (cdddddr statement) nil))) ((disable children parent))) (defn rrp (node children parent) (if (listp children) (cons (list 'receive-report node (cons (car children) node) (cons node parent)) (rrp node (cdr children) parent)) nil)) (prove-lemma member-rrp (rewrite) (equal (member statement (rrp node children parent)) (and (equal (car statement) 'receive-report) (equal (cadr statement) node) (listp (caddr statement)) (member (caaddr statement) children) (equal (cdaddr statement) node) (listp (cadddr statement)) (equal (caadddr statement) node) (equal (cdadddr statement) parent) (equal (cddddr statement) nil)))) (defn receive-report-prg (nodes tree) (if (listp nodes) (append (rrp (car nodes) (children (car nodes) tree) (parent (car nodes) tree)) (receive-report-prg (cdr nodes) tree)) nil)) (prove-lemma member-receive-report-prg (rewrite) (equal (member statement (receive-report-prg nodes tree)) (and (equal (car statement) 'receive-report) (member (cadr statement) nodes) (listp (caddr statement)) (member (caaddr statement) (children (cadr statement) tree)) (equal (cdaddr statement) (cadr statement)) (listp (cadddr statement)) (equal (caadddr statement) (cadr statement)) (equal (cdadddr statement) (parent (cadr statement) tree)) (equal (cddddr statement) nil))) ((disable parent children))) (defn start-prg (root tree) (list (list 'start root (rfp root (children root tree))))) (prove-lemma member-start-prg (rewrite) (equal (member statement (start-prg root tree)) (and (equal (car statement) 'start) (equal (cadr statement) root) (equal (caddr statement) (rfp root (children root tree))) (equal (cdddr statement) nil))) ((disable children))) (defn rrrp (root children) (if (listp children) (cons (list 'root-receive-report root (cons (car children) root)) (rrrp root (cdr children))) nil)) (prove-lemma member-rrrp (rewrite) (equal (member statement (rrrp root children)) (and (equal (car statement) 'root-receive-report) (equal (cadr statement) root) (listp (caddr statement)) (member (caaddr statement) children) (equal (cdaddr statement) root) (equal (cdddr statement) nil)))) (defn root-receive-report-prg (root tree) (rrrp root (children root tree))) (prove-lemma member-root-receive-report-prg (rewrite) (equal (member statement (root-receive-report-prg root tree)) (and (equal (car statement) 'root-receive-report) (equal (cadr statement) root) (listp (caddr statement)) (member (caaddr statement) (children root tree)) (equal (cdaddr statement) root) (equal (cdddr statement) nil))) ((disable children))) (defn 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))))) (prove-lemma equal-if (rewrite) (equal (equal (if test p1 p2) (if test r1 r2)) (if test (equal p1 r1) (equal p2 r2)))) (prove-lemma member-tree-prg (rewrite) (equal (member statement (tree-prg tree)) ;(start root to-children) (or (and (equal (car statement) 'start) (equal (cadr statement) (car tree)) (equal (caddr statement) (rfp (car tree) (children (car tree) tree))) (equal (cdddr statement) nil)) ;(root-receive-report root from-child) (and (equal (car statement) 'root-receive-report) (equal (cadr statement) (car tree)) (listp (caddr statement)) (member (caaddr statement) (children (car tree) tree)) (equal (cdaddr statement) (car tree)) (equal (cdddr statement) nil)) ;(receive-find node from-parent to-parent to-children) (and (equal (car statement) 'receive-find) (member (cadr statement) (cdr (nodes tree))) (listp (caddr statement)) (equal (caaddr statement) (parent (cadr statement) tree)) (equal (cdaddr statement) (cadr statement)) (listp (cadddr statement)) (equal (caadddr statement) (cadr statement)) (equal (cdadddr statement) (parent (cadr statement) tree)) (equal (caddddr statement) (rfp (cadr statement) (children (cadr statement) tree))) (equal (cdddddr statement) nil)) ;(receive-report node from-child to-parent) (and (equal (car statement) 'receive-report) (member (cadr statement) (cdr (nodes tree))) (listp (caddr statement)) (member (caaddr statement) (children (cadr statement) tree)) (equal (cdaddr statement) (cadr statement)) (listp (cadddr statement)) (equal (caadddr statement) (cadr statement)) (equal (cdadddr statement) (parent (cadr statement) tree)) (equal (cddddr statement) nil)))) ((disable parent children nodes root-receive-report-prg start-prg))) ;;; Correctness (defn treep (tree) (and (setp (nodes tree)) (all-numberps (nodes tree)) (proper-tree 'tree tree))) (defn total-outstanding (nodes tree state) (if (listp nodes) (plus (total-outstanding (cdr nodes) tree state) (if (equal (status (car nodes) state) 'started) (outstanding (car nodes) state) (add1 (length (children (car nodes) tree))))) 0)) (defn dl (down-links state) (if (listp down-links) (and (or (and (empty (car down-links) state) (equal (status (caar down-links) state) (status (cdar down-links) state))) (and (equal (channel (car down-links) state) (list 'find)) (equal (status (caar down-links) state) 'started) (equal (status (cdar down-links) state) 'not-started))) (dl (cdr down-links) state)) t)) (defn done (node state) (and (equal (status node state) 'started) (zerop (outstanding node state)))) (defn ul (up-links state) (if (listp up-links) (and (or (empty (car up-links) state) (and (equal (channel (car up-links) state) (list (found-value (caar up-links) state))) (done (caar up-links) state))) (ul (cdr up-links) state)) t)) (defn reported (node parent state) (and (done node state) (empty (cons node parent) state))) (defn number-not-reported (children parent state) (if (listp children) (if (reported (car children) parent state) (number-not-reported (cdr children) parent state) (add1 (number-not-reported (cdr children) parent state))) 0)) (defn min-of-reported (children parent state min) (if (listp children) (if (reported (car children) parent state) (min (found-value (car children) state) (min-of-reported (cdr children) parent state min)) (min-of-reported (cdr children) parent state min)) min)) (defn no (nodes tree state) (if (listp nodes) (and (if (equal (status (car nodes) state) 'started) (and (equal (outstanding (car nodes) state) (number-not-reported (children (car nodes) tree) (car nodes) state)) (equal (found-value (car nodes) state) (min-of-reported (children (car nodes) tree) (car nodes) state (node-value (car nodes) state)))) t) (no (cdr nodes) tree state)) t)) (defn down-links-1 (parent children) (if (listp children) (cons (cons parent (car children)) (down-links-1 parent (cdr children))) nil)) (defn down-links (nodes tree) (if (listp nodes) (append (down-links-1 (car nodes) (children (car nodes) tree)) (down-links (cdr nodes) tree)) nil)) (defn up-links (nodes tree) (if (listp nodes) (cons (cons (car nodes) (parent (car nodes) tree)) (up-links (cdr nodes) tree)) nil)) (defn inv (tree state) (and (dl (down-links (nodes tree) tree) state) (ul (up-links (cdr (nodes tree)) tree) state) (no (nodes tree) tree state))) (defn not-started (nodes state) (if (listp nodes) (and (equal (status (car nodes) state) 'not-started) (not-started (cdr nodes) state)) t)) (defn all-channels (tree) (append (up-links (cdr (nodes tree)) tree) (down-links (nodes tree) tree))) (defn all-empty (channels state) (if (listp channels) (and (empty (car channels) state) (all-empty (cdr channels) state)) t)) (defn min-node-value (nodes state min) (if (listp nodes) (min (node-value (car nodes) state) (min-node-value (cdr nodes) state min)) min)) (defn correct (tree state) (equal (found-value (car tree) state) (min-node-value (cdr (nodes tree)) state (node-value (car tree) state)))) ;;; Proof of Correctness (prove-lemma all-empty-implies-empty (rewrite) (implies (and (all-empty channels state) (member channel channels)) (not (listp (channel channel state))))) (prove-lemma not-started-implies-not-started (rewrite) (implies (and (not-started nodes state) (member node nodes)) (equal (cdr (assoc (cons 'status node) state)) 'not-started))) (prove-lemma all-empty-append (rewrite) (equal (all-empty (append a b) state) (and (all-empty a state) (all-empty b state)))) (prove-lemma all-empty-implies-ul (rewrite) (implies (all-empty up-links state) (ul up-links state))) (defn nodes-in-channels (channels) (if (listp channels) (cons (caar channels) (cons (cdar channels) (nodes-in-channels (cdr channels)))) nil)) (prove-lemma all-empty-not-started-implies-dl (rewrite) (implies (and (all-empty down-links state) (not-started (nodes-in-channels down-links) state)) (dl down-links state))) (prove-lemma not-started-implies-no (rewrite) (implies (not-started nodes state) (no nodes tree state))) (prove-lemma nodes-in-down-links-1-in-nodes (rewrite) (equal (member node (nodes-in-channels (down-links-1 parent children))) (if (listp children) (member node (cons parent children)) f))) (prove-lemma nodes-in-channels-append (rewrite) (equal (nodes-in-channels (append a b)) (append (nodes-in-channels a) (nodes-in-channels b)))) (prove-lemma nodes-in-down-links-in-nodes (rewrite) (implies (and (proper-tree 'tree tree) (member node (nodes-in-channels (down-links nodes tree)))) (member node (nodes tree)))) (prove-lemma sublistp-not-started (rewrite) (implies (and (sublistp sub list) (not-started list state)) (not-started sub state))) (prove-lemma sublistp-down-links-1 (rewrite) (implies (and (sublistp children nodes) (member parent nodes)) (sublistp (nodes-in-channels (down-links-1 parent children)) nodes))) (prove-lemma children-of-non-node (rewrite) (implies (not (member parent (nodes-rec flag tree))) (equal (children-rec flag parent tree) nil))) (prove-lemma down-links-is-sublistp (rewrite) (implies (proper-tree 'tree tree) (sublistp (nodes-in-channels (down-links nodes tree)) (nodes-rec 'tree tree))) ((INSTRUCTIONS (INDUCT (LENGTH NODES)) (CLAIM (MEMBER (CAR NODES) (NODES-REC 'TREE TREE)) 0) BASH BASH BASH))) (prove-lemma initial-conditions-imply-invariant (rewrite) (implies (and (proper-tree 'tree tree) (all-empty (all-channels tree) state) (not-started (nodes tree) state)) (inv tree state)) ((INSTRUCTIONS BASH PROMOTE (REWRITE ALL-EMPTY-NOT-STARTED-IMPLIES-DL) (REWRITE SUBLISTP-NOT-STARTED (($LIST (NODES-REC 'TREE TREE)))) (REWRITE DOWN-LINKS-IS-SUBLISTP)))) (defn found-value-node-value (subtrees state) (if (listp subtrees) (and (equal (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)) t)) (defn nati (subtrees) (if (listp subtrees) (nati (next-level subtrees)) t)) (prove-lemma found-value-node-value-append (rewrite) (equal (found-value-node-value (append a b) state) (and (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. (prove-lemma no-implies (rewrite) (implies (and (no nodes tree state) (member node nodes) (equal (status node state) 'started)) (and (equal (number-not-reported (children node tree) node state) (cdr (assoc (cons 'outstanding node) state))) (numberp (cdr (assoc (cons 'outstanding node) state))) (equal (cdr (assoc (cons 'found-value node) state)) (min-of-reported (children node tree) node state (node-value node state)))))) (prove-lemma total-outstanding-0-implies (rewrite) (and (implies (and (equal (total-outstanding nodes tree state) 0) (member node nodes) (numberp (cdr (assoc (cons 'outstanding node) state)))) (equal (cdr (assoc (cons 'outstanding node) state)) 0)) (implies (and (equal (total-outstanding nodes tree state) 0) (member node nodes)) (equal (cdr (assoc (cons 'status node) state)) 'started)))) (prove-lemma number-not-reported-0-implies (rewrite) (implies (and (equal (number-not-reported children parent state) 0) (member node children)) (reported node parent state)) ((disable reported))) (prove-lemma proper-tree-tree-implies-nodes-exists (rewrite) (implies (proper-tree 'tree tree) (listp (nodes-rec 'tree tree)))) (prove-lemma min-of-two-nodes-values (rewrite) (equal (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))) (prove-lemma found-value-min-value-generalized (rewrite) (implies (and (found-value-node-value forest state) (equal (number-not-reported (roots forest) root state) 0) (proper-tree 'forest forest)) (equal (min-of-reported (roots forest) root state min) (min-node-value (nodes-rec 'forest forest) state min))) ((INSTRUCTIONS (INDUCT (LENGTH FOREST)) (BASH T (DISABLE MIN REPORTED)) PROMOTE (DIVE 1) (DIVE 1) = UP (REWRITE MIN-OF-TWO-NODES-VALUES) TOP DROP (BASH (DISABLE MIN)) PROVE))) (prove-lemma no-at-termination (rewrite) (implies (and (proper-tree 'tree tree) (proper-tree 'forest subtrees) (setp (nodes-rec 'tree tree)) (no (nodes-rec 'tree tree) tree state) (equal (total-outstanding (nodes-rec 'tree tree) tree state) 0) (sublistp subtrees (subtrees 'tree tree))) (found-value-node-value subtrees state)) ((INSTRUCTIONS (INDUCT (NATI SUBTREES)) CHANGE-GOAL PROVE (BASH T) (INDUCT (FOUND-VALUE-NODE-VALUE SUBTREES STATE)) CHANGE-GOAL PROVE (BASH T) PROMOTE (DIVE 1) (REWRITE FOUND-VALUE-MIN-VALUE-GENERALIZED) TOP S (DIVE 1) (DIVE 1) (= (CHILDREN W TREE)) UP (REWRITE NO-IMPLIES (($NODES (NODES-REC 'TREE TREE)))) (REWRITE TOTAL-OUTSTANDING-0-IMPLIES (($NODES (NODES-REC 'TREE TREE)) ($TREE TREE))) TOP S (REWRITE MEMBER-SUBTREE-MEMBER-TREE) (REWRITE NO-IMPLIES (($NODES (NODES-REC 'TREE TREE)) ($TREE TREE))) (REWRITE MEMBER-SUBTREE-MEMBER-TREE) (DIVE 1) S (REWRITE TOTAL-OUTSTANDING-0-IMPLIES (($NODES (NODES-REC 'TREE TREE)) ($TREE TREE))) TOP S (REWRITE MEMBER-SUBTREE-MEMBER-TREE) (REWRITE MEMBER-SUBTREE-MEMBER-TREE) (DIVE 1) S (REWRITE TOTAL-OUTSTANDING-0-IMPLIES (($NODES (NODES-REC 'TREE TREE)) ($TREE TREE))) TOP S (REWRITE MEMBER-SUBTREE-MEMBER-TREE)))) (prove-lemma inv-implies-augmented-correctness-condition (rewrite) (implies (and (proper-tree 'tree tree) (setp (nodes-rec 'tree tree)) (inv tree state) (equal (total-outstanding (nodes tree) tree state) 0)) (correct tree state)) ((use (no-at-termination (subtrees (list tree)) (tree tree) (state state))) (disable no-at-termination))) (defn send-find-func (to-children old) (if (listp to-children) (update-assoc (car to-children) (send (car to-children) 'find old) (send-find-func (cdr to-children) old)) old)) (defn receive-find-func (old node from-parent to-parent to-children) (if (equal (head from-parent old) 'find) (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 (zerop (length to-children)) (update-assoc to-parent (send to-parent (node-value node old) old) (send-find-func to-children old)) (send-find-func to-children old)))))) old)) (prove-lemma send-find-func-implements-send-find (rewrite) (send-find to-children old (send-find-func to-children old))) (prove-lemma nodes-are-not-litatoms (rewrite) (implies (and (all-numberps (nodes-rec flag tree)) (member node (nodes-rec flag tree))) (equal (equal (pack x) node) f)) ((use (all-numberps-implies (list (nodes-rec flag tree)) (e node))) (disable all-numberps-implies))) (prove-lemma parent-is-not-a-litatom (rewrite) (implies (and (all-numberps (nodes-rec 'tree tree)) (setp (nodes-rec 'tree tree)) (proper-tree 'tree tree) (member child (cdr (nodes-rec 'tree tree)))) (equal (equal (pack x) (car (parent-rec 'tree child tree))) f)) ((INSTRUCTIONS PROMOTE (DIVE 1) (REWRITE NODES-ARE-NOT-LITATOMS (($FLAG 'TREE) ($TREE TREE))) TOP S (REWRITE NODE-HAS-PARENT) (DROP 1 2) (DIVE 2) X TOP PROVE (DROP 1) (DEMOTE 1) (DIVE 1) (DIVE 1) X TOP PROVE))) (prove-lemma children-are-not-litatoms (rewrite) (implies (and (all-numberps (nodes-rec flag tree)) (proper-tree flag tree) (member child (children-rec flag parent tree))) (equal (equal (pack x) child) f)) ((INSTRUCTIONS PROMOTE (DIVE 1) (REWRITE NODES-ARE-NOT-LITATOMS (($FLAG FLAG) ($TREE TREE))) TOP S (REWRITE MEMBER-CHILD-TREE (($NODE PARENT)))))) (prove-lemma children-are-not-litatoms-member (rewrite) (implies (and (all-numberps (nodes-rec flag tree)) (proper-tree flag tree)) (equal (member (pack x) (children-rec flag parent tree)) f)) ((use (children-are-not-litatoms (child (pack x)))))) (prove-lemma send-find-of-update-assoc (rewrite) (implies (not (member key to-children)) (equal (send-find to-children old (update-assoc key value state)) (send-find to-children old state)))) (prove-lemma assoc-of-send-find-func (rewrite) (implies (not (member key to-children)) (equal (assoc key (send-find-func to-children old)) (assoc key old)))) (prove-lemma about-rfp (rewrite) (implies (not (member p c)) (not (member (cons v p) (rfp v c))))) (prove-lemma about-rfp-numberp (rewrite) (implies (numberp a) (not (member (cons (pack x) y) (rfp a b))))) (prove-lemma parent-not-in-rfp (rewrite) (implies (and (setp (nodes-rec 'tree tree)) (proper-tree 'tree tree) (member v (cdr (nodes-rec 'tree tree)))) (not (member (cons v (car (parent-rec 'tree v tree))) (rfp v (children-rec 'tree v tree))))) ((INSTRUCTIONS PROMOTE (DIVE 1) (REWRITE ABOUT-RFP) TOP S (DIVE 1) (REWRITE PARENT-IS-NOT-CHILD) TOP S (BASH T)))) (prove-lemma to-node-not-in-rfp (rewrite) (implies (not (member node children)) (not (member (cons x node) (rfp node children))))) (prove-lemma uc-of-send-find-func (rewrite) (implies (sublistp to-children excpt) (equal (uc old (send-find-func to-children state) keys excpt) (uc old state keys excpt)))) (prove-lemma receive-find-func-implements-receive-find (rewrite) (implies (and (treep tree) (member statement (receive-find-prg (cdr (nodes tree)) tree))) (n old (receive-find-func old (cadr statement) (caddr statement) (cadddr statement) (caddddr statement)) statement))) (defn receive-report-func (old node from-child to-parent) (if (empty from-child old) old (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) (sub1 (outstanding node old)) (if (zerop (sub1 (outstanding node old))) (update-assoc to-parent (send to-parent (min (found-value node old) (head from-child old)) old) old) old)))))) (prove-lemma receive-report-func-implements-receive-report (rewrite) (implies (and (treep tree) (member statement (receive-report-prg (cdr (nodes tree)) tree))) (n old (receive-report-func old (cadr statement) (caddr statement) (cadddr statement)) statement)) ((disable min))) (defn start-func (old root to-children) (if (equal (status root old) 'not-started) (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)))) old)) (prove-lemma start-func-implements-start (rewrite) (implies (and (treep tree) (member statement (start-prg (car tree) tree))) (n old (start-func old (cadr statement) (caddr statement)) statement))) (defn root-receive-report-func (old root from-child) (if (empty from-child old) old (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) (sub1 (outstanding root old)) old))))) (prove-lemma root-receive-report-func-implements-root-receive-report (rewrite) (implies (and (treep tree) (member statement (root-receive-report-prg (car tree) tree))) (n old (root-receive-report-func old (cadr statement) (caddr statement)) statement)) ((disable min))) (prove-lemma receive-find-prg-is-total (rewrite) (implies (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)))) ((disable n receive-find receive-find-func member-receive-find-prg nodes setp proper-tree all-numberps) (use (receive-find-func-implements-receive-find)))) (prove-lemma receive-report-prg-is-total (rewrite) (implies (treep tree) (total-sufficient statement (receive-report-prg (cdr (nodes tree)) tree) old (receive-report-func old (cadr statement) (caddr statement) (cadddr statement)))) ((disable n receive-report receive-report-func member-receive-report-prg nodes setp proper-tree all-numberps) (use (receive-report-func-implements-receive-report)))) (prove-lemma start-prg-is-total (rewrite) (implies (treep tree) (total-sufficient statement (start-prg (car tree) tree) old (start-func old (cadr statement) (caddr statement)))) ((disable n start start-func start-prg nodes setp proper-tree all-numberps) (use (start-func-implements-start)))) (prove-lemma root-receive-report-prg-is-total (rewrite) (implies (treep tree) (total-sufficient statement (root-receive-report-prg (car tree) tree) old (root-receive-report-func old (cadr statement) (caddr statement)))) ((disable n root-receive-report root-receive-report-func root-receive-report-prg member-root-receive-report-prg nodes setp proper-tree all-numberps) (use (root-receive-report-func-implements-root-receive-report)))) (prove-lemma total-tree-prg (rewrite) (implies (treep tree) (total (tree-prg tree))) ((INSTRUCTIONS (BASH (DISABLE N ROOT-RECEIVE-REPORT-PRG-IS-TOTAL START-PRG-IS-TOTAL RECEIVE-REPORT-PRG-IS-TOTAL RECEIVE-FIND-PRG-IS-TOTAL MEMBER-ROOT-RECEIVE-REPORT-PRG MEMBER-START-PRG MEMBER-RECEIVE-REPORT-PRG MEMBER-RECEIVE-FIND-PRG ROOT-RECEIVE-REPORT-FUNC START-FUNC RECEIVE-REPORT-FUNC RECEIVE-FIND-FUNC ROOT-RECEIVE-REPORT-PRG START-PRG RECEIVE-REPORT-PRG RECEIVE-FIND-PRG PROPER-TREE ALL-NUMBERPS SETP NODES TREEP MEMBER-TREE-PRG TOTAL-SUFFICIENT)) PROMOTE (REWRITE HELP-PROVE-TOTAL) (PUT (NEW (RECEIVE-REPORT-FUNC (OLDT (RECEIVE-REPORT-PRG (CDR (NODES TREE)) TREE)) (CADR (ET (RECEIVE-REPORT-PRG (CDR (NODES TREE)) TREE))) (CADDR (ET (RECEIVE-REPORT-PRG (CDR (NODES TREE)) TREE))) (CADDDR (ET (RECEIVE-REPORT-PRG (CDR (NODES TREE)) TREE)))))) (REWRITE RECEIVE-REPORT-PRG-IS-TOTAL) PROMOTE (REWRITE HELP-PROVE-TOTAL) (PUT (NEW (RECEIVE-FIND-FUNC (OLDT (RECEIVE-FIND-PRG (CDR (NODES TREE)) TREE)) (CADR (ET (RECEIVE-FIND-PRG (CDR (NODES TREE)) TREE))) (CADDR (ET (RECEIVE-FIND-PRG (CDR (NODES TREE)) TREE))) (CADDDR (ET (RECEIVE-FIND-PRG (CDR (NODES TREE)) TREE))) (CADDDDR (ET (RECEIVE-FIND-PRG (CDR (NODES TREE)) TREE)))))) (REWRITE RECEIVE-FIND-PRG-IS-TOTAL) PROMOTE (REWRITE HELP-PROVE-TOTAL) (PUT (NEW (ROOT-RECEIVE-REPORT-FUNC (OLDT (ROOT-RECEIVE-REPORT-PRG (CAR TREE) TREE)) (CADR (ET (ROOT-RECEIVE-REPORT-PRG (CAR TREE) TREE))) (CADDR (ET (ROOT-RECEIVE-REPORT-PRG (CAR TREE) TREE)))))) (REWRITE ROOT-RECEIVE-REPORT-PRG-IS-TOTAL) PROMOTE (REWRITE HELP-PROVE-TOTAL) (PUT (NEW (START-FUNC (OLDT (START-PRG (CAR TREE) TREE)) (CADR (ET (START-PRG (CAR TREE) TREE))) (CADDR (ET (START-PRG (CAR TREE) TREE)))))) (REWRITE START-PRG-IS-TOTAL)))) (prove-lemma listp-tree-prg (rewrite) (listp (tree-prg tree))) (prove-lemma node-values-constant-unless-sufficient (rewrite) (implies (and (treep tree) (member node (nodes tree))) (unless-sufficient statement (tree-prg tree) old new `(equal (node-value (quote ,node) state) (quote ,k)) '(false))) ((disable tree-prg))) (prove-lemma node-values-constant-invariant (rewrite) (implies (and (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (and (not-started (quote ,(nodes tree)) state) (equal (node-value (quote ,node) state) (quote ,k)))) (tree-prg tree)) (treep tree) (member node (nodes tree))) (invariant `(equal (node-value (quote ,node) state) (quote ,k)) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE UNLESS-PROVES-INVARIANT (($IC (LIST 'AND (LIST 'ALL-EMPTY (LIST 'QUOTE (ALL-CHANNELS TREE)) 'STATE) (LIST 'AND (LIST 'NOT-STARTED (LIST 'QUOTE (NODES TREE)) 'STATE) (LIST 'EQUAL (LIST 'NODE-VALUE (LIST 'QUOTE NODE) 'STATE) (LIST 'QUOTE K))))))) (REWRITE HELP-PROVE-UNLESS) (REWRITE NODE-VALUES-CONSTANT-UNLESS-SUFFICIENT) (BASH (DISABLE EVAL TREE-PRG))))) (prove-lemma dl-implies-instance-of-dl (rewrite) (implies (and (dl down-links state) (member down-link down-links)) (or (and (empty down-link state) (equal (status (car down-link) state) (status (cdr down-link) state))) (and (equal (channel down-link state) (list 'find)) (equal (status (car down-link) state) 'started) (equal (status (cdr down-link) state) 'not-started))))) (disable dl-implies-instance-of-dl) (prove-lemma ul-implies-instance-of-ul (rewrite) (implies (and (ul uplinks state) (member uplink uplinks)) (or (empty uplink state) (and (equal (channel uplink state) (list (found-value (car uplink) state))) (done (car uplink) state))))) (disable ul-implies-instance-of-ul) (prove-lemma ul-implies-instance-of-ul-not-empty-uplink (rewrite) (implies (and (ul uplinks state) (member uplink uplinks) (not (empty uplink state))) (and (equal (cdr (assoc uplink state)) (list (found-value (car uplink) state))) (equal (cdr (assoc (cons 'status (car uplink)) state)) 'started) (zerop (cdr (assoc (cons 'outstanding (car uplink)) state))))) ((use (ul-implies-instance-of-ul)))) (prove-lemma no-implies-instance-of-no (rewrite) (implies (and (no nodes tree state) (member node nodes) (equal (status node state) 'started)) (and (equal (cdr (assoc (cons 'outstanding node) state)) (number-not-reported (children-rec 'tree node tree) node state)) (equal (cdr (assoc (cons 'found-value node) state)) (min-of-reported (children-rec 'tree node tree) node state (node-value node state)))))) (prove-lemma member-down-links-1 (rewrite) (equal (member down-link (down-links-1 parent children)) (and (equal (car down-link) parent) (member (cdr down-link) children) (listp down-link)))) (prove-lemma member-down-links (rewrite) (equal (member down-link (down-links nodes tree)) (and (member (car down-link) nodes) (member (cdr down-link) (children (car down-link) tree)) (listp down-link))) ((disable children))) (prove-lemma parent-not-child (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree))) (not (member parent (children-rec flag parent tree))))) (prove-lemma parent-not-grandchild (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree)) (member child (children-rec flag parent tree))) (not (member parent (children-rec flag child tree))))) (prove-lemma parent-of-parent-not-node (rewrite) (implies (and (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))) (not (equal (car (parent-rec flag (car (parent-rec flag node tree)) tree)) node))) ((INSTRUCTIONS (USE-LEMMA PARENT-NOT-GRANDCHILD ((CHILD (CAR (PARENT-REC FLAG NODE TREE))) (PARENT (CAR (PARENT-REC FLAG (CAR (PARENT-REC FLAG NODE TREE)) TREE))))) PROMOTE (DEMOTE 1) (DIVE 1) (DIVE 1) S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) UP UP (DIVE 2) (DIVE 1) (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROMOTE PROVE))) (prove-lemma member-rfp (rewrite) (equal (member channel (rfp parent children)) (and (equal (car channel) parent) (member (cdr channel) children) (listp channel)))) (prove-lemma send-find-implies (rewrite) (implies (and (send-find channels old new) (member key channels)) (equal (cdr (assoc key new)) (send key 'find old)))) (prove-lemma assoc-of-channel-preserved-root-receive-report (rewrite) (implies (and (not (member w (nodes-rec 'forest d))) (setp (nodes-rec 'forest d)) (member 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)))) (equal (assoc (cons x z) new) (assoc (cons x z) old))) ((use (about-uc (a new) (b old) (excpt (list (cons v w) (cons 'outstanding w) (cons 'found-value w))) (key (cons x z)))) (disable about-uc))) (prove-lemma assoc-equal-cons (rewrite) (equal (equal (assoc key alist) (cons key value)) (and (listp (assoc key alist)) (equal (cdr (assoc key alist)) value)))) (prove-lemma send-find-general (rewrite) (implies (and (send-find channels old new) (member key channels)) (equal (assoc key new) (cons key (send key 'find old))))) (prove-lemma all-numberps-do-not-contain-litatom (rewrite) (implies (all-numberps list) (not (member (pack x) list)))) (prove-lemma all-numberps-append (rewrite) (equal (all-numberps (append x y)) (and (all-numberps x) (all-numberps y)))) (prove-lemma all-numberps-nodes-implies-all-numberps-parent (rewrite) (implies (all-numberps (nodes-rec flag tree)) (all-numberps (parent-rec flag child tree)))) (prove-lemma all-numberps-nodes-implies-all-numberps-car-parent (rewrite) (implies (all-numberps (nodes-rec flag tree)) (numberp (car (parent-rec flag child tree)))) ((use (all-numberps-nodes-implies-all-numberps-parent)) (disable all-numberps-nodes-implies-all-numberps-parent))) (prove-lemma parent-not-litatom (rewrite) (implies (all-numberps (nodes-rec flag tree)) (equal (equal (pack x) (car (parent-rec flag child tree))) f)) ((use (all-numberps-nodes-implies-all-numberps-car-parent)) (disable all-numberps-nodes-implies-all-numberps-car-parent))) (prove-lemma all-numberps-forest-implies-all-numberps-roots (rewrite) (implies (all-numberps (nodes-rec 'forest forest)) (all-numberps (roots forest)))) (prove-lemma all-numberps-nodes-implies-all-numberps-children (rewrite) (implies (all-numberps (nodes-rec flag tree)) (all-numberps (children-rec flag parent tree)))) (prove-lemma dl-preserves-instance-of-dl (rewrite) (implies (and (treep tree) (member down-link (down-links (nodes tree) tree)) (n old new statement) (member statement (tree-prg tree)) (dl (down-links (nodes tree) tree) old)) (or (and (empty down-link new) (equal (status (car down-link) new) (status (cdr down-link) new))) (and (equal (channel down-link new) (list 'find)) (equal (status (car down-link) new) 'started) (equal (status (cdr down-link) new) 'not-started)))) ((INSTRUCTIONS PROMOTE (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINK DOWN-LINK) (STATE OLD) (DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)))) (DEMOTE 6) (DIVE 1) (DIVE 1) S-PROP UP (S-PROP IMPLIES) TOP PROMOTE (CLAIM (EQUAL (CAR STATEMENT) 'START) 0) (DROP 5) (BASH T (DISABLE TREE-PRG)) PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS 'STATUS C) (CONS (CONS 'FOUND-VALUE C) (CONS (CONS 'OUTSTANDING C) (RFP C (APPEND (ROOTS W) NIL)))))))) TOP S PROVE PROMOTE (CLAIM (NOT (EQUAL Z C))) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (APPEND (ROOTS W) NIL)))))))) TOP S PROVE (CLAIM (EQUAL (CAR STATEMENT) 'ROOT-RECEIVE-REPORT) 0) (DROP 5) (PROVE (DISABLE TREE-PRG)) (CLAIM (EQUAL (CAR STATEMENT) 'RECEIVE-REPORT) 0) (DROP 5) (CLAIM (AND (EQUAL (STATUS (CAR DOWN-LINK) NEW) (STATUS (CAR DOWN-LINK) OLD)) (EQUAL (STATUS (CDR DOWN-LINK) NEW) (STATUS (CDR DOWN-LINK) OLD)) (EQUAL (CHANNEL DOWN-LINK NEW) (CHANNEL DOWN-LINK OLD))) 0) (DROP 1 2 3 4 6 7 8) PROVE (CONTRADICT 9) (DROP 5 6 7 9) SPLIT (PROVE (DISABLE TREE-PRG)) (PROVE (DISABLE TREE-PRG)) (CLAIM (AND (NOT (EQUAL DOWN-LINK (CADDR STATEMENT))) (NOT (EQUAL DOWN-LINK (CADDDR STATEMENT)))) 0) (PROVE (DISABLE TREE-PRG)) (CONTRADICT 6) (DROP 3 6) SPLIT (PROVE (DISABLE TREE-PRG)) (BASH T (DISABLE TREE-PRG)) PROMOTE (CONTRADICT 4) (DIVE 1) (REWRITE PARENT-NOT-GRANDCHILD) TOP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE (CLAIM (EQUAL DOWN-LINK (CADDDR STATEMENT)) 0) (CONTRADICT 10) (DROP 3 5 6 10) (BASH T (DISABLE TREE-PRG)) PROMOTE (CONTRADICT 4) (DIVE 1) (REWRITE PARENT-NOT-GRANDCHILD) TOP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE (CLAIM (EQUAL DOWN-LINK (CADDR STATEMENT)) 0) (CLAIM (MEMBER DOWN-LINK (CADDDDR STATEMENT)) 0) (CONTRADICT 12) (DROP 3 5 6 10 12) (BASH T (DISABLE TREE-PRG)) (DROP 5) (BASH T (DISABLE TREE-PRG)) (CLAIM (MEMBER DOWN-LINK (CADDDDR STATEMENT)) 0) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINK (CONS (PARENT (CAR DOWN-LINK) TREE) (CAR DOWN-LINK))) (STATE OLD) (DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)))) (DEMOTE 13) (DIVE 1) (DIVE 1) (= * T IFF) TOP (DROP 5) (BASH T (DISABLE TREE-PRG)) PROMOTE (CLAIM (NOT (EQUAL Z C))) PROVE S-PROP (CLAIM (MEMBER (CAR DOWN-LINK) (CDR (NODES TREE))) 0) (DROP 3 4 5 6 7 8 9 10 11 12) (REWRITE MEMBER-DOWN-LINKS) S (DIVE 1) (REWRITE NODE-HAS-PARENT) TOP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE PROVE PROVE PROVE PROVE PROVE (CONTRADICT 13) (DROP 3 5 6 10 11 13) PROVE (CLAIM (AND (EQUAL (STATUS (CAR DOWN-LINK) NEW) (STATUS (CAR DOWN-LINK) OLD)) (EQUAL (STATUS (CDR DOWN-LINK) NEW) (STATUS (CDR DOWN-LINK) OLD)) (EQUAL (CHANNEL DOWN-LINK NEW) (CHANNEL DOWN-LINK OLD))) 0) (DROP 1 2 3 4 5 7 8 9 10 11 12) PROVE (CONTRADICT 13) (DROP 5 6 13) (DEMOTE 3) (DIVE 1) (= * (RECEIVE-FIND OLD NEW (CADR STATEMENT) (CADDR STATEMENT) (CADDDR STATEMENT) (CADDDDR STATEMENT)) ((DISABLE TREE-PRG MEMBER-DOWN-LINKS))) X-DUMB TOP PROMOTE (CLAIM (EQUAL (HEAD (CADDR STATEMENT) OLD) 'FIND) 0) (DIVE 1) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CADDR STATEMENT) (CADDDR STATEMENT) (CONS 'STATUS (CADR STATEMENT)) (CONS 'FOUND-VALUE (CADR STATEMENT)) (CONS 'OUTSTANDING (CADR STATEMENT))) (CADDDDR STATEMENT))))) TOP (DIVE 2) (DIVE 1) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CADDR STATEMENT) (CADDDR STATEMENT) (CONS 'STATUS (CADR STATEMENT)) (CONS 'FOUND-VALUE (CADR STATEMENT)) (CONS 'OUTSTANDING (CADR STATEMENT))) (CADDDDR STATEMENT))))) TOP (DIVE 2) (DIVE 2) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CADDR STATEMENT) (CADDDR STATEMENT) (CONS 'STATUS (CADR STATEMENT)) (CONS 'FOUND-VALUE (CADR STATEMENT)) (CONS 'OUTSTANDING (CADR STATEMENT))) (CADDDDR STATEMENT))))) TOP S (BASH T (DISABLE TREE-PRG)) (DROP 3 4 5 6 10 11) PROVE (BASH T (DISABLE TREE-PRG)) (CLAIM (NOT (EQUAL (CDR DOWN-LINK) (CADR STATEMENT)))) (DROP 10 11) PROVE PROVE (DROP 10 11) (CLAIM (NOT (EQUAL (CAR DOWN-LINK) (CADR STATEMENT)))) (PROVE (DISABLE TREE-PRG)) (DROP 1 2 3 4 5 6 7 8 9) PROVE))) (prove-lemma dl-preserves-sublist (rewrite) (implies (and (dl (down-links (nodes tree) tree) old) (treep tree) (n old new statement) (member statement (tree-prg tree)) (sublistp sublist (down-links (nodes tree) tree))) (dl sublist new)) ((INSTRUCTIONS (INDUCT (DL SUBLIST NEW)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) (= * T ((DISABLE N TREE-PRG MEMBER-TREE-PRG))) UP S TOP PROMOTE X (DROP 7) (USE-LEMMA DL-PRESERVES-INSTANCE-OF-DL ((TREE TREE) (DOWN-LINK (CAR SUBLIST)) (STATEMENT STATEMENT) (OLD OLD) (NEW NEW))) (DEMOTE 7) (DIVE 1) (DIVE 1) (= * T ((DISABLE TREEP N TREE-PRG MEMBER-TREE-PRG NODES))) TOP S prove))) (prove-lemma dl-preserves-dl (rewrite) (implies (and (dl (down-links (nodes tree) tree) old) (treep tree) (n old new statement) (member statement (tree-prg tree))) (dl (down-links (nodes tree) tree) new)) ((use (dl-preserves-sublist (sublist (down-links (nodes tree) tree)))) (disable tree-prg member-tree-prg))) (prove-lemma member-up-links (rewrite) (equal (member up-link (up-links nodes tree)) (and (member (car up-link) nodes) (equal (cdr up-link) (parent (car up-link) tree)) (listp up-link)))) (prove-lemma zero-not-reported-implies-children-reported (rewrite) (implies (and (zerop (number-not-reported children parent state)) (member child children)) (and (equal (cdr (assoc (cons 'status child) state)) 'started) (zerop (outstanding child state)) (not (listp (cdr (assoc (cons child parent) state)))))) ((induct (member child children)))) (prove-lemma dl-ul-no-preserves-instance-of-ul (rewrite) (implies (and (treep tree) (member up-link (up-links (cdr (nodes tree)) tree)) (n old new statement) (member statement (tree-prg tree)) (dl (down-links (nodes tree) tree) old) (ul (up-links (cdr (nodes tree)) tree) old) (no (nodes tree) tree old)) (or (empty up-link new) (and (equal (channel up-link new) (list (found-value (car up-link) new))) (done (car up-link) new)))) ((INSTRUCTIONS PROMOTE (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (UPLINK UP-LINK) (STATE OLD))) (DEMOTE 8) (DIVE 1) (DIVE 1) S-PROP UP (S-PROP IMPLIES) TOP PROMOTE (CLAIM (EQUAL (CAR STATEMENT) 'START) 0) (DROP 5 6 7) (CLAIM (AND (EQUAL (FOUND-VALUE (CAR UP-LINK) NEW) (FOUND-VALUE (CAR UP-LINK) OLD)) (EQUAL (CHANNEL UP-LINK NEW) (CHANNEL UP-LINK OLD)) (EQUAL (STATUS (CAR UP-LINK) NEW) (STATUS (CAR UP-LINK) OLD)) (EQUAL (OUTSTANDING (CAR UP-LINK) NEW) (OUTSTANDING (CAR UP-LINK) OLD))) 0) (DROP 1 2 3 4 6) PROVE (CONTRADICT 7) (DROP 5 7) (BASH T (DISABLE TREE-PRG)) PROMOTE (CLAIM (NOT (EQUAL X D))) PROVE PROMOTE (CLAIM (NOT (EQUAL X D))) PROVE PROMOTE (CLAIM (NOT (MEMBER (CONS X D) (RFP D (APPEND (ROOTS V) NIL))))) PROVE PROMOTE (CLAIM (NOT (MEMBER (CONS X (CAR (PARENT-REC 'FOREST X V))) (RFP D (APPEND (ROOTS V) NIL))))) PROVE PROMOTE (CLAIM (NOT (EQUAL X D))) PROVE (CLAIM (EQUAL (CAR STATEMENT) 'ROOT-RECEIVE-REPORT) 0) (CLAIM (NOT (EQUAL (CAR UP-LINK) (CAR TREE))) 0) CHANGE-GOAL (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (CLAIM (EQUAL UP-LINK (CADDR STATEMENT)) 0) (DROP 5 6 7 9) (BASH T (DISABLE TREE-PRG)) (CLAIM (AND (EQUAL (FOUND-VALUE (CAR UP-LINK) NEW) (FOUND-VALUE (CAR UP-LINK) OLD)) (EQUAL (CHANNEL UP-LINK NEW) (CHANNEL UP-LINK OLD)) (EQUAL (STATUS (CAR UP-LINK) NEW) (STATUS (CAR UP-LINK) OLD)) (EQUAL (OUTSTANDING (CAR UP-LINK) NEW) (OUTSTANDING (CAR UP-LINK) OLD))) 0) (DROP 1 2 3 4 5 6 7 9 10 11 12) PROVE (CONTRADICT 13) (DROP 5 6 7 8 9 13) (BASH T (DISABLE TREE-PRG)) (CLAIM (EQUAL (CAR STATEMENT) 'RECEIVE-FIND) 0) (CLAIM (EQUAL (CADR STATEMENT) (CAR UP-LINK)) 0) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((STATE OLD) (DOWN-LINK (CONS (PARENT (CAR UP-LINK) TREE) (CAR UP-LINK))) (DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)))) (DEMOTE 13) (DIVE 1) (DIVE 1) S-PROP (REWRITE MEMBER-DOWN-LINKS) S (DIVE 1) (= * T IFF) UP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) UP S (= * T IFF) CHANGE-GOAL (DROP 3 4 5 6 7 8 9 10 11 12) S (DIVE 2) (DIVE 1) (= T) UP S (DIVE 1) (= F) UP S TOP X CHANGE-GOAL (DEMOTE 1) S CHANGE-GOAL (DEMOTE 1) S CHANGE-GOAL (DROP 3 4 5 6 7 8 9 10 11 12) S (REWRITE NODE-HAS-PARENT) PROVE DEMOTE S S PROVE UP (S-PROP IMPLIES) TOP PROMOTE (DROP 5 6 7 9 10) (BASH T (DISABLE TREE-PRG)) (CLAIM (AND (EQUAL (FOUND-VALUE (CAR UP-LINK) NEW) (FOUND-VALUE (CAR UP-LINK) OLD)) (EQUAL (CHANNEL UP-LINK NEW) (CHANNEL UP-LINK OLD)) (EQUAL (STATUS (CAR UP-LINK) NEW) (STATUS (CAR UP-LINK) OLD)) (EQUAL (OUTSTANDING (CAR UP-LINK) NEW) (OUTSTANDING (CAR UP-LINK) OLD))) 0) (DROP 1 2 3 4 5 6 7 9 10 11 12) PROVE (CONTRADICT 13) (DROP 5 6 7 8 9 10 13) (BASH T (DISABLE TREE-PRG)) PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 12 14 15) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 12 14 15) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 12 14 15) (BASH T) PROMOTE (DIVE 1) (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE (REWRITE LISTP-PARENT-REC-EQUALS) PROVE PROVE (REWRITE LISTP-PARENT-REC-EQUALS) PROVE PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 12 14 15) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 13 14) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 13 14) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 13 14) (BASH T) PROMOTE (CLAIM (SETP (NODES-REC 'TREE TREE))) (DIVE 1) (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (CAR (PARENT-REC 'TREE D TREE)) D) (CONS (CONS D (CAR (PARENT-REC 'TREE D TREE))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN-REC 'TREE D TREE)))))))))) TOP S (DROP 7 8 9 10 11 13 14) PROVE (CLAIM (EQUAL UP-LINK (CADDR STATEMENT)) 0) (CLAIM (NOT (EQUAL (CADDR STATEMENT) (CADDDR STATEMENT))) 0) (DROP 5 6 7) (BASH T (DISABLE TREE-PRG)) (CONTRADICT 13) (DROP 3 5 6 7 8 13) (PROVE (DISABLE TREE-PRG)) (CLAIM (EQUAL UP-LINK (CADDDR STATEMENT)) 0) (CLAIM (EMPTY (CADDR STATEMENT) OLD) 0) (CLAIM (CHANGED OLD NEW NIL) 0) (DROP 1 2 3 4 5 6 7 9 10 11 12 13 14) PROVE (CONTRADICT 15) (DROP 1 2 5 6 7 8 12 13 15) (PROVE (DISABLE TREE-PRG)) (CLAIM (EMPTY UP-LINK OLD) 0) (CLAIM (EQUAL (STATUS (CADR STATEMENT) OLD) 'STARTED) 0) (DROP 5 6 7) (BASH T (DISABLE TREE-PRG MIN)) PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (CAR (PARENT-REC 'TREE W TREE))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (DROP 6 7 8 9 10 11 14 15 16) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (CAR (PARENT-REC 'TREE W TREE))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (DROP 6 7 8 9 10 11 14 15 16) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (CAR (PARENT-REC 'TREE W TREE))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (DROP 6 7 8 9 10 11 14 15 16) PROVE (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (STATE OLD) (UPLINK (CADDR STATEMENT)))) (DEMOTE 17) (DIVE 1) (DIVE 1) S-PROP (= * T IFF) UP (S-PROP IMPLIES) (S-PROP OR) UP PROMOTE (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (STATE OLD) (DOWN-LINK (CONS (CADR STATEMENT) (CAADDR STATEMENT))))) (DEMOTE 19) (DIVE 1) (DIVE 1) S-PROP (= * T IFF) UP (S-PROP IMPLIES) TOP PROMOTE (CONTRADICT 16) (DROP 1 2 3 4 5 6 7 8 9 10 11 16) PROVE (DROP 3 5 6 7 8 14 15 16 17 18) (BASH T (DISABLE TREE-PRG)) (DROP 3 5 6 7 8 14 15 16) (BASH T (DISABLE TREE-PRG)) PROMOTE (CONTRADICT 7) (DIVE 1) (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE PROVE (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE (CADR STATEMENT)))) (DEMOTE 16) (DIVE 1) (DIVE 1) (= * T IFF) UP (S-PROP IMPLIES) TOP PROMOTE (USE-LEMMA ZERO-NOT-REPORTED-IMPLIES-CHILDREN-REPORTED ((CHILDREN (CHILDREN (CADR STATEMENT) TREE)) (PARENT (CADR STATEMENT)) (STATE OLD) (CHILD (CAADDR STATEMENT)))) (CONTRADICT 14) (DROP 3 5 6 7 14) (BASH T (DISABLE TREE-PRG)) S-PROP (CLAIM (EQUAL (CADR STATEMENT) (CAR UP-LINK)) ((DISABLE TREE-PRG))) (DROP 3 4 5 6 7 9 10 11 12 13 14) PROVE (CLAIM (AND (EQUAL (CHANNEL UP-LINK NEW) (CHANNEL UP-LINK OLD)) (EQUAL (STATUS (CAR UP-LINK) NEW) (STATUS (CAR UP-LINK) OLD)) (EQUAL (FOUND-VALUE (CAR UP-LINK) NEW) (FOUND-VALUE (CAR UP-LINK) OLD)) (EQUAL (OUTSTANDING (CAR UP-LINK) NEW) (OUTSTANDING (CAR UP-LINK) OLD))) 0) (DROP 1 2 3 4 5 6 7 9 10 11 12 13) PROVE (CONTRADICT 14) (CLAIM (NOT (EQUAL (CAR UP-LINK) (CADR STATEMENT))) ((DISABLE TREE-PRG))) (DROP 5 6 7 8 14) (CLAIM (NUMBERP (CAR UP-LINK))) (DROP 2) (BASH T (DISABLE TREE-PRG MIN))))) (prove-lemma dl-ul-no-preserves-ul-sublist (rewrite) (implies (and (treep tree) (n old new statement) (member 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)) ((INSTRUCTIONS (INDUCT (UL SUBLIST NEW)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= * T ((DISABLE N TREE-PRG MEMBER-TREE-PRG TREEP NODES))) UP S TOP PROMOTE X (DROP 9) (USE-LEMMA DL-UL-NO-PRESERVES-INSTANCE-OF-UL ((TREE TREE) (UP-LINK (CAR SUBLIST)) (STATEMENT STATEMENT) (OLD OLD) (NEW NEW))) (DEMOTE 9) (DIVE 1) (DIVE 1) S-PROP (= * T ((DISABLE N TREE-PRG MEMBER-TREE-PRG TREEP NODES))) TOP S PROMOTE PROMOTE X))) (prove-lemma dl-ul-no-preserves-ul (rewrite) (implies (and (treep tree) (n old new statement) (member 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)) ((use (dl-ul-no-preserves-ul-sublist (sublist (up-links (cdr (nodes tree)) tree)))) (disable treep tree-prg member-tree-prg member-up-links nodes n))) (prove-lemma parent-not-started-implies-all-empty-and-not-started (rewrite) (implies (and (equal (status parent state) 'not-started) (dl (rfp parent children) state)) (and (all-empty (rfp parent children) state) (not-started children state)))) (prove-lemma start-preserves-no-for-parent (rewrite) (implies (and (numberp parent) (not (member 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)))) (and (equal (number-not-reported children parent new) (length children)) (equal (min-of-reported children parent new value) value))) ((INSTRUCTIONS (INDUCT (LENGTH CHILDREN)) (CLAIM (EQUAL (CDR (ASSOC (CONS 'STATUS (CAR CHILDREN)) NEW)) 'STARTED) 0) PROMOTE PROMOTE (CONTRADICT 1) (DIVE 1) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS 'STATUS PARENT) (CONS 'FOUND-VALUE PARENT) (CONS 'OUTSTANDING PARENT)) (RFP PARENT EXCPT))))) TOP PROVE PROVE PROVE PROVE PROVE))) (prove-lemma unchanged-preserves-no (rewrite) (implies (changed old new nil) (and (equal (number-not-reported children parent new) (number-not-reported children parent old)) (equal (min-of-reported children parent new value) (min-of-reported children parent old value))))) (prove-lemma start-preserves-no-for-rest-of-tree (rewrite) (implies (and (numberp root) (numberp parent) (not (member parent children)) (not (member root children)) (not (equal root parent)) (changed old new (append (list (cons 'status root) (cons 'found-value root) (cons 'outstanding root)) (rfp root excpt)))) (and (equal (number-not-reported children parent new) (number-not-reported children parent old)) (equal (min-of-reported children parent new value) (min-of-reported children parent old value))))) (prove-lemma length-rfp (rewrite) (equal (length (rfp parent children)) (length children))) (prove-lemma start-preserves-instance-of-no (rewrite) (implies (and (treep tree) (start old new (car tree) (rfp (car tree) (children (car tree) tree))) (member node (nodes tree)) (dl (rfp (car tree) (children (car tree) tree)) old) (equal (status node new) 'started) (implies (equal (status node old) 'started) (and (equal (outstanding node old) (number-not-reported (children node tree) node old)) (equal (found-value node old) (min-of-reported (children node tree) node old (node-value node old)))))) (and (equal (outstanding node new) (number-not-reported (children node tree) node new)) (equal (found-value node new) (min-of-reported (children node tree) node new (node-value node new))))) ((INSTRUCTIONS PROMOTE (DEMOTE 2) (DIVE 1) X-DUMB (CLAIM (EQUAL (STATUS (CAR TREE) OLD) 'NOT-STARTED) 0) (DIVE 1) (DIVE 1) = UP UP S-PROP TOP PROMOTE (CLAIM (EQUAL NODE (CAR TREE)) 0) (CLAIM (NUMBERP NODE) 0) (CLAIM (NOT (MEMBER NODE (CHILDREN NODE TREE))) 0) (CLAIM (NOT-STARTED (CHILDREN NODE TREE) OLD) 0) (CLAIM (SUBLISTP (RFP NODE (CHILDREN NODE TREE)) (RFP NODE (CHILDREN (CAR TREE) TREE))) 0) (DIVE 1) (DIVE 2) (CLAIM (CHANGED OLD NEW (APPEND (LIST (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN (CAR TREE) TREE)))) 0) (REWRITE START-PRESERVES-NO-FOR-PARENT (($OLD OLD) ($EXCPT (CHILDREN (CAR TREE) TREE)))) TOP (DIVE 2) (DIVE 2) (REWRITE START-PRESERVES-NO-FOR-PARENT (($OLD OLD) ($EXCPT (CHILDREN (CAR TREE) TREE)))) TOP (DROP 3 9 10 11 12 13) PROVE TOP (CONTRADICT 13) (DROP 1 2 3 4 5 6 9 10 11 12 13) PROVE (CONTRADICT 12) (DIVE 2) (DIVE 2) (DIVE 1) = TOP (REWRITE SUBLISTP-REFLEXIVE) (CONTRADICT 11) (REWRITE PARENT-NOT-STARTED-IMPLIES-ALL-EMPTY-AND-NOT-STARTED (($PARENT (CAR TREE)))) (DIVE 1) (DIVE 2) (DIVE 1) = TOP S-PROP (CONTRADICT 10) (DROP 3 4 5 6 7 8 9 10) PROVE (CONTRADICT 9) (DROP 2 3 4 5 6 7 9) PROVE (CLAIM (NUMBERP (CAR TREE)) 0) (CLAIM (NUMBERP NODE) 0) (CLAIM (NOT (MEMBER NODE (CHILDREN NODE TREE))) 0) (CLAIM (NOT (MEMBER (CAR TREE) (CHILDREN NODE TREE))) 0) (DIVE 1) (DIVE 2) (CLAIM (CHANGED OLD NEW (APPEND (LIST (CONS 'STATUS (CAR TREE)) (CONS 'FOUND-VALUE (CAR TREE)) (CONS 'OUTSTANDING (CAR TREE))) (RFP (CAR TREE) (CHILDREN (CAR TREE) TREE)))) 0) (REWRITE START-PRESERVES-NO-FOR-REST-OF-TREE (($OLD OLD) ($ROOT (CAR TREE)) ($EXCPT (CHILDREN (CAR TREE) TREE)))) TOP (DIVE 2) (DIVE 2) (REWRITE START-PRESERVES-NO-FOR-REST-OF-TREE (($OLD OLD) ($ROOT (CAR TREE)) ($EXCPT (CHILDREN (CAR TREE) TREE)))) TOP (CLAIM (AND (EQUAL (STATUS NODE NEW) (STATUS NODE OLD)) (EQUAL (OUTSTANDING NODE NEW) (OUTSTANDING NODE OLD)) (EQUAL (FOUND-VALUE NODE NEW) (FOUND-VALUE NODE OLD)) (EQUAL (NODE-VALUE NODE NEW) (NODE-VALUE NODE OLD))) 0) (DROP 1 2 3 6 7 9 10 11 12 13) (PROVE (DISABLE STATUS OUTSTANDING FOUND-VALUE NODE-VALUE CHILDREN)) (CONTRADICT 14) (DROP 3 4 5 6 7 11 12 14) PROVE TOP (CONTRADICT 13) (DROP 1 2 3 4 5 6 8 9 10 11 12 13) PROVE (CONTRADICT 12) (DROP 3 4 5 6 7 9 10 11 12) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (CONTRADICT 10) (DROP 3 4 5 6 7 8 9 10) PROVE (CONTRADICT 9) (DROP 2 3 4 5 6 7 8 9) PROVE S-PROP TOP PROMOTE (DIVE 1) (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DIVE 2) (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP PROVE))) (prove-lemma min-commutative (rewrite) (equal (min a b) (min b a))) (prove-lemma min-associative (rewrite) (equal (min (min a b) c) (min a (min b c)))) (prove-lemma min-commutative-1 (rewrite) (equal (min a (min b c)) (min b (min a c)))) (prove-lemma min-of-reported-of-min (rewrite) (equal (min-of-reported children parent state (min value x)) (min (min-of-reported children parent state value) x)) ((disable reported found-value min))) (prove-lemma update-min-of-reported (rewrite) (implies (and (numberp parent) (numberp child) (not (equal parent child)) (all-numberps children) (setp children) (not (member parent children)) (equal (channel (cons child parent) old) (list (found-value child old))) (done child old) (equal (channel (cons child parent) new) (receive (cons child parent) old)) (changed old new (list (cons child parent) (cons 'outstanding parent) (cons 'found-value parent)))) (equal (min-of-reported children parent new value) (if (member child children) (min (found-value child old) (min-of-reported children parent old value)) (min-of-reported children parent old value)))) ((INSTRUCTIONS (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DISABLE REPORTED FOUND-VALUE HEAD CHANNEL RECEIVE MIN DONE) (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= T) UP TOP SPLIT (DIVE 1) X (DIVE 2) (DIVE 2) = UP UP (DIVE 3) = TOP (DROP 12) (CLAIM (EQUAL CHILD (CAR CHILDREN)) 0) (CLAIM (AND (NOT (MEMBER CHILD (CDR CHILDREN))) (MEMBER CHILD CHILDREN)) 0) S S-PROP SPLIT (DIVE 2) (DIVE 2) X (DIVE 1) (= F) UP S TOP (DIVE 1) (DIVE 1) (DIVE 1) = UP (= (FOUND-VALUE CHILD OLD)) TOP S (CONTRADICT 15) (DROP 1 5 6 7 13 14 15) PROVE (CONTRADICT 13) (DROP 2 3 4 5 7 8 9 10 11 13) PROVE (CLAIM (MEMBER CHILD (CDR CHILDREN)) 0) (CLAIM (MEMBER CHILD CHILDREN) 0) S S-PROP SPLIT (DIVE 2) (DIVE 2) X (DIVE 1) (= T) TOP S (DIVE 1) (DIVE 1) (= (FOUND-VALUE (CAR CHILDREN) OLD)) TOP DROP (PROVE (DISABLE DONE MIN RECEIVE CHANNEL HEAD FOUND-VALUE REPORTED)) (DIVE 2) (DIVE 2) X (DIVE 1) (= F) TOP S (CONTRADICT 14) (DROP 1 2 3 4 5 6 7 8 9 10 11 12 14) PROVE (CLAIM (NOT (MEMBER CHILD CHILDREN)) 0) S (DIVE 2) X (DIVE 1) (= (REPORTED (CAR CHILDREN) PARENT NEW)) UP (DIVE 2) (DIVE 1) (= (FOUND-VALUE (CAR CHILDREN) NEW)) TOP S (CONTRADICT 14) (DROP 1 2 3 4 5 6 7 8 9 10 11 14) PROVE (PROVE (DISABLE DONE MIN RECEIVE CHANNEL HEAD FOUND-VALUE REPORTED))))) (prove-lemma min-of-reported-of-non-root (rewrite) (implies (and (numberp root) (numberp child) (numberp parent) (all-numberps children) (setp children) (not (member parent children)) (not (equal root parent)) (not (member root children)) (changed old new (list (cons child root) (cons 'outstanding root) (cons 'found-value root)))) (equal (min-of-reported children parent new value) (min-of-reported children parent old value))) ((INSTRUCTIONS (DISABLE MIN REPORTED DONE FOUND-VALUE OUTSTANDING STATUS) (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) (= T) UP S TOP PROMOTE (DIVE 1) X (DIVE 2) (DIVE 2) = UP UP (DIVE 3) = TOP (DROP 11) (DIVE 1) (DIVE 1) (= (REPORTED (CAR CHILDREN) PARENT OLD)) UP (DIVE 2) (DIVE 1) (= (FOUND-VALUE (CAR CHILDREN) OLD)) TOP (DIVE 2) X TOP S (PROVE (DISABLE STATUS OUTSTANDING FOUND-VALUE DONE REPORTED MIN))))) (prove-lemma number-not-reported-of-non-root (rewrite) (implies (and (numberp root) (numberp child) (numberp parent) (all-numberps children) (setp children) (not (member parent children)) (not (equal root parent)) (not (member root children)) (changed old new (list (cons child root) (cons 'outstanding root) (cons 'found-value root)))) (equal (number-not-reported children parent new) (number-not-reported children parent old))) ((INSTRUCTIONS (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) (= T) UP S TOP PROMOTE (DIVE 1) (DISABLE REPORTED) X (DIVE 1) (= (REPORTED (CAR CHILDREN) PARENT OLD)) UP (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP (DROP 11) (DIVE 2) X TOP S (PROVE (DISABLE REPORTED))))) (prove-lemma number-not-reported-of-root (rewrite) (implies (and (numberp parent) (numberp child) (not (equal parent child)) (all-numberps children) (setp children) (not (member parent children)) (equal (channel (cons child parent) old) (list (found-value child old))) (done child old) (equal (channel (cons child parent) new) (receive (cons child parent) old)) (changed old new (list (cons child parent) (cons 'outstanding parent) (cons 'found-value parent)))) (equal (number-not-reported children parent new) (if (member child children) (sub1 (number-not-reported children parent old)) (number-not-reported children parent old)))) ((INSTRUCTIONS (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (CLAIM (EQUAL CHILD (CAR CHILDREN)) 0) (CLAIM (AND (MEMBER CHILD CHILDREN) (NOT (MEMBER CHILD (CDR CHILDREN)))) 0) S (DEMOTE 2) (DIVE 1) (DIVE 1) (= T) UP S TOP PROMOTE (DIVE 1) (DISABLE REPORTED) X (DIVE 1) (= T) UP S = TOP (DIVE 2) (DIVE 1) X (DIVE 1) (= F) TOP S (CONTRADICT 14) (DROP 2 3 4 5 6 8 9 10 11 12 14) PROVE (DEMOTE 2) (DIVE 1) (DIVE 1) (= T) UP S TOP (DIVE 2) (DIVE 2) (DIVE 1) X TOP S-PROP SPLIT (DIVE 1) X (DIVE 1) (= (REPORTED (CAR CHILDREN) PARENT OLD)) UP (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP (DIVE 2) (DIVE 1) X TOP CHANGE-GOAL (DIVE 1) X (DIVE 1) (= (REPORTED (CAR CHILDREN) PARENT OLD)) TOP (DIVE 2) X TOP (DIVE 1) (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP S (CLAIM (NOT (ZEROP (NUMBER-NOT-REPORTED (CDR CHILDREN) PARENT OLD))) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14) (PROVE (DISABLE REPORTED)) (CONTRADICT 15) (DROP 1 2 3 4 5 6 7 9 10 11 12 14 15) (GENERALIZE (((CDR CHILDREN) L))) (INDUCT (MEMBER CHILD L)) PROVE PROVE PROVE (PROVE (DISABLE REPORTED))))) (prove-lemma setp-nodes-implies-setp-roots (rewrite) (implies (and (proper-tree 'forest forest) (setp (nodes-rec 'forest forest))) (setp (roots forest))) ((induct (roots forest)))) (prove-lemma setp-nodes-setp-children (rewrite) (implies (and (proper-tree flag tree) (setp (nodes-rec flag tree))) (setp (children-rec flag parent tree))) ((INSTRUCTIONS (INDUCT (CHILDREN-REC FLAG PARENT TREE)) PROMOTE PROMOTE (DIVE 1) X (DIVE 2) (= NIL) TOP PROVE PROMOTE PROMOTE PROVE PROMOTE PROMOTE (DIVE 1) X (CLAIM (EQUAL (CHILDREN-REC 'TREE PARENT (CAR TREE)) NIL) 0) TOP PROVE (DIVE 2) (CLAIM (MEMBER PARENT (NODES-REC 'TREE (CAR TREE)))) (= NIL) TOP PROVE PROVE))) (prove-lemma root-receive-report-preserves-instance-of-no (rewrite) (implies (and (treep tree) (member child (children (car tree) tree)) (root-receive-report old new (car tree) (cons child (car tree))) (ul (up-links (cdr (nodes tree)) tree) old) (member node (nodes tree)) (equal (status node new) 'started) (implies (equal (status node old) 'started) (and (equal (outstanding node old) (number-not-reported (children node tree) node old)) (equal (found-value node old) (min-of-reported (children node tree) node old (node-value node old)))))) (and (equal (outstanding node new) (number-not-reported (children node tree) node new)) (equal (found-value node new) (min-of-reported (children node tree) node new (node-value node new))))) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (STATUS NODE OLD) 'STARTED)) (DEMOTE 7) (DIVE 1) (DIVE 1) S-PROP UP (S-PROP IMPLIES) TOP PROMOTE (CLAIM (EQUAL NODE (CAR TREE)) 0) (DEMOTE 3) (DIVE 1) X-DUMB TOP SPLIT (DIVE 2) (REWRITE NUMBER-NOT-REPORTED-OF-ROOT (($CHILD CHILD) ($OLD OLD))) TOP (DIVE 1) (DIVE 1) = UP = (DIVE 1) (DIVE 1) = UP = UP UP (DROP 1 3 4 5 6 7 8 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 3 4 5 6 7 8 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DIVE 1) S (REWRITE UL-IMPLIES-INSTANCE-OF-UL-NOT-EMPTY-UPLINK (($UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)))) TOP S (DROP 3 5 6 7 8 10 11 12 13 14) PROVE (DIVE 1) (DIVE 1) (DIVE 2) = TOP S-PROP (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL-NOT-EMPTY-UPLINK ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (UPLINK (CONS CHILD (CAR TREE))) (STATE OLD))) (DEMOTE 15) (DIVE 1) (DIVE 1) S-PROP (DROP 3 4 5 6 7 8 9 10 11 12 13 14) (= T) TOP S (DROP 1 2 3 4 5 6 7 8 10 12 13 14) PROVE (DROP 1 2 3 4 5 6 7 8 10 11 12 13) PROVE (DEMOTE 1 2 3 4 5 6 7 8 10 11 12 13 14) (BOOKMARK (BEGIN (EQSUB 1))) (= NODE (CAR TREE) 0) (CLAIM (EQUAL NODE (CAR TREE)) TAUT) (DROP 1) (BOOKMARK (END (EQSUB 1))) DROP PROMOTE (DIVE 2) (REWRITE UPDATE-MIN-OF-REPORTED (($CHILD CHILD) ($OLD OLD))) TOP S-PROP (DIVE 1) = (DIVE 2) X-DUMB (DIVE 1) S (REWRITE UL-IMPLIES-INSTANCE-OF-UL-NOT-EMPTY-UPLINK (($UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)))) TOP (DIVE 2) (DIVE 2) (DIVE 4) (= * (NODE-VALUE (CAR TREE) OLD) 0) UP = TOP DROP (PROVE (DISABLE MIN)) (DROP 3 4 5 6 7 8 9 10 11 12) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 2 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 2 3 4 5 6 7 8 9 10 11 12 13) PROVE (DROP 2 3 4 5 6 7 8 9 10 11 12 13) PROVE (DIVE 1) S (REWRITE UL-IMPLIES-INSTANCE-OF-UL-NOT-EMPTY-UPLINK (($UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)))) TOP S (DROP 4 5 6 7 8 9 10 11 12 13) PROVE (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL-NOT-EMPTY-UPLINK ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (UPLINK (CONS CHILD (CAR TREE))) (STATE OLD))) (DEMOTE 14) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP S (DROP 3 4 5 6 7 8 9 10 11 12 13) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DROP 1 2 3 4 5 6 8 9 11 12 13 14) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DROP 1 2 3 4 5 6 7 9 11 12 13 14) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DROP 1 2 3 4 5 6 8 9 11) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DROP 1 2 3 4 5 6 7 9 11) PROVE (DEMOTE 3) (DIVE 1) X-DUMB TOP SPLIT (DIVE 2) (REWRITE NUMBER-NOT-REPORTED-OF-NON-ROOT (($ROOT (CAR TREE)) ($CHILD CHILD) ($OLD OLD))) TOP (DIVE 1) (= * (OUTSTANDING NODE OLD) 0) = TOP S (DROP 2 3 5 6 7 8 10 11 12 13) PROVE (DROP 2 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DIVE 1) (= * (FOUND-VALUE NODE OLD) 0) UP (DIVE 2) (REWRITE MIN-OF-REPORTED-OF-NON-ROOT (($OLD OLD) ($CHILD CHILD) ($ROOT (CAR TREE)))) TOP (DIVE 1) = TOP (DIVE 2) (DIVE 4) (= * (NODE-VALUE NODE OLD) 0) TOP S (DROP 1 2 3 4 5 6 7 8 10 11 12 13) PROVE (DROP 2 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 2 3 5 6 7 8 9 10 11 12 13 14) PROVE (DROP 1 2 3 4 5 6 7 8 10 11 12 13) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DIVE 1) (= * (OUTSTANDING NODE OLD) 0) = TOP S (DROP 1 2 3 4 5 6 7 8 9 11 12 13 14) PROVE (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) (DIVE 4) (= * (NODE-VALUE NODE OLD) 0) TOP (DIVE 1) (= * (FOUND-VALUE NODE OLD) 0) = TOP S (DROP 1 2 3 4 5 6 7 8 9 11 12 13 14) PROVE (DROP 1 2 3 4 5 6 7 8 9 11 12 13 14) PROVE (DIVE 1) (= * (OUTSTANDING NODE OLD) 0) = TOP (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP S (DROP 1 2 3 4 5 6 7 8 9 11) PROVE (DIVE 1) (= * (FOUND-VALUE NODE OLD) 0) = TOP (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) (DIVE 4) (= * (NODE-VALUE NODE OLD) 0) TOP S (DROP 1 2 3 4 5 6 7 8 9 11) PROVE (DROP 1 2 3 4 5 6 7 8 9 11) PROVE))) (prove-lemma receive-find-preserves-no-for-rest-of-tree (rewrite) (implies (and (numberp node) (numberp parent-of-node) (numberp parent) (not (equal parent node)) (not (member 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)))) (and (equal (number-not-reported children parent new) (number-not-reported children parent old)) (equal (min-of-reported children parent new value) (min-of-reported children parent old value)))) ((disable min) (induct (length children)))) (prove-lemma receive-find-preserves-no-for-node (rewrite) (implies (and (numberp node) (numberp parent-of-node) (not (member 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)))) (and (equal (number-not-reported children node new) (length children)) (equal (min-of-reported children node new value) (min-of-reported children node old value)))) ((INSTRUCTIONS (DISABLE MIN) (INDUCT (LENGTH CHILDREN)) (CLAIM (EQUAL (CDR (ASSOC (CONS 'STATUS (CAR CHILDREN)) NEW)) 'STARTED) 0) PROMOTE PROMOTE (CONTRADICT 1) (DIVE 1) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (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))))) TOP PROVE (DROP 1 2 3 4 5 6 7 8) PROVE (DROP 1 3 9) PROVE PROVE PROVE))) (prove-lemma receive-find-preserves-no-for-parent-of-node (rewrite) (implies (and (numberp node) (numberp parent-of-node) (not (equal node parent-of-node)) (not (equal (status node old) 'started)) (implies (zerop (outstanding node new)) (not (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)))) (and (equal (number-not-reported children parent-of-node new) (number-not-reported children parent-of-node old)) (equal (min-of-reported children parent-of-node new value) (min-of-reported children parent-of-node old value)))) ((INSTRUCTIONS (DISABLE MIN) (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= * T ((DISABLE ZEROP OUTSTANDING EMPTY))) UP (S-PROP IMPLIES) TOP PROMOTE (DIVE 1) (DIVE 1) X-DUMB S-PROP (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP (DIVE 2) (DIVE 1) X-DUMB S-PROP (DIVE 2) (DIVE 2) = UP UP (DIVE 3) = TOP (DROP 8 9) (CLAIM (EQUAL (CAR CHILDREN) NODE) 0) (PROVE (DISABLE MIN)) (CLAIM (EQUAL (REPORTED (CAR CHILDREN) PARENT-OF-NODE NEW) (REPORTED (CAR CHILDREN) PARENT-OF-NODE OLD)) 0) (PROVE (DISABLE MIN REPORTED)) (CONTRADICT 9) (DROP 5 6 9) (PROVE (DISABLE MIN)) PROVE))) (prove-lemma dl-of-append (rewrite) (equal (dl (append a b) state) (and (dl a state) (dl b state)))) (prove-lemma down-links-1-rfp (rewrite) (equal (down-links-1 parent children) (rfp parent children))) (prove-lemma dl-down-links-implies-dl-rfp (rewrite) (implies (and (dl (down-links nodes tree) state) (member node nodes)) (dl (rfp node (children node tree)) state))) (disable dl-down-links-implies-dl-rfp) (disable down-links-1-rfp) (disable dl-of-append) (prove-lemma receive-find-preserves-instance-of-no (rewrite) (implies (and (treep tree) (member 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) (member n (nodes tree)) (equal (status n new) 'started) (implies (equal (status n old) 'started) (and (equal (outstanding n old) (number-not-reported (children n tree) n old)) (equal (found-value n old) (min-of-reported (children n tree) n old (node-value n old)))))) (and (equal (outstanding n new) (number-not-reported (children n tree) n new)) (equal (found-value n new) (min-of-reported (children n tree) n new (node-value n new))))) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (HEAD (CONS (PARENT NODE TREE) NODE) OLD) 'FIND) 0) (CLAIM (EQUAL N NODE) 0) (CLAIM (NOT-STARTED (CHILDREN NODE TREE) OLD) 0) (DEMOTE 3) (DIVE 1) X-DUMB S-PROP TOP (DROP 6) PROMOTE (DIVE 1) (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-NODE (($OLD OLD) ($PARENT-OF-NODE (PARENT NODE TREE)) ($EXCPT (CHILDREN NODE TREE)))) TOP (DIVE 2) (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-NODE (($OLD OLD) ($PARENT-OF-NODE (PARENT NODE TREE)) ($EXCPT (CHILDREN NODE TREE)))) TOP (BASH T) PROMOTE (GENERALIZE (((CHILDREN-REC 'TREE NODE TREE) CHILDREN))) (DROP 1 2 3 4 5 6 7 8 9 11 12 13 14 16 17) (INDUCT (LENGTH CHILDREN)) PROVE PROVE (DROP 2 3 5 6 7 8 9) PROVE (DROP 3 4 5 6 7 8 9) PROVE (DROP 2 3 5 6 7 8 9) PROVE (DIVE 1) (DIVE 1) = TOP S-PROP (DIVE 1) (DIVE 2) (DIVE 1) = TOP (REWRITE SUBLISTP-REFLEXIVE) PROVE (DROP 2 3 5 6 7 8 9) PROVE (DROP 3 4 5 6 7 8 9) PROVE (DROP 2 3 5 6 7 8 9) PROVE (DIVE 1) (DIVE 1) = TOP S-PROP (DIVE 1) (DIVE 2) (DIVE 1) = TOP (REWRITE SUBLISTP-REFLEXIVE) PROVE (CONTRADICT 10) (REWRITE PARENT-NOT-STARTED-IMPLIES-ALL-EMPTY-AND-NOT-STARTED (($PARENT NODE))) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)) (STATE OLD))) (DEMOTE 11) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DROP 1 2 3 4 5 6 7 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) S (REWRITE MEMBER-DOWN-LINKS) S (DIVE 2) (REWRITE PARENT-REC-CHILDREN-REC) TOP (DIVE 1) (REWRITE NODE-HAS-PARENT) TOP S (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE PROVE PROVE PROVE PROVE PROVE (REWRITE DL-DOWN-LINKS-IMPLIES-DL-RFP (($NODES (NODES TREE)))) PROVE (CLAIM (EQUAL N (PARENT NODE TREE)) 0) (DEMOTE 3) (DIVE 1) X-DUMB S-PROP TOP PROMOTE (DIVE 1) (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-PARENT-OF-NODE (($OLD OLD) ($NODE NODE) ($EXCPT (CHILDREN NODE TREE)))) UP TOP (DIVE 2) (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-PARENT-OF-NODE (($OLD OLD) ($NODE NODE) ($EXCPT (CHILDREN NODE TREE)))) TOP (DIVE 1) (DIVE 1) (= * (OUTSTANDING N OLD) 0) TOP (DIVE 2) (DIVE 1) (= * (FOUND-VALUE N OLD) 0) TOP (DIVE 2) (DIVE 2) (DIVE 4) (= * (NODE-VALUE N OLD) 0) TOP (DEMOTE 6) (DIVE 1) (DIVE 1) (= * T 0) TOP S (DEMOTE 5) (DIVE 1) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP S (DROP 1 2 3 4 5 6 7) PROVE (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 7 8) PROVE (CONTRADICT 9) (DROP 3 4 5 6 7 8 9) PROVE (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP S (DROP 1 2 3 4 5 6 7 8 9) PROVE (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP S (DROP 1 2 3 4 5 6 7 8 9) PROVE (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP S (DROP 1 2 3 4 5 6 7 8 9) PROVE (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 5 6 7 8 9 10) PROVE (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)) (STATE OLD))) (DEMOTE 11) (DIVE 1) (DIVE 1) S-PROP (REWRITE MEMBER-DOWN-LINKS) (DIVE 1) S (REWRITE NODE-HAS-PARENT) UP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) S UP (= * T 0) TOP (DROP 1 2 3 4 5 6 8 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE S (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 1 2 3 4 5 6 7 8) (PROVE (DISABLE OUTSTANDING LENGTH-RFP FOUND-VALUE STATUS NODE-VALUE CHANGED)) (DROP 1 2 3 4 5 6 7 8) (PROVE (DISABLE CHANGED OUTSTANDING FOUND-VALUE STATUS RECEIVE SEND LENGTH-RFP)) (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 5 6 7 8 9 10) PROVE (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)) (STATE OLD))) (DEMOTE 11) (DIVE 1) (DIVE 1) S-PROP (REWRITE MEMBER-DOWN-LINKS) (DIVE 1) S (REWRITE NODE-HAS-PARENT) UP S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) UP S (= * T 0) TOP (DROP 1 2 3 4 5 6 8 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 4 5 6 7 8 9 10) PROVE S (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 1 2 3 4 5 6 7 8) (PROVE (DISABLE SEND LENGTH-RFP OUTSTANDING NODE-VALUE FOUND-VALUE STATUS RECEIVE CHANGED)) (DROP 1 2 3 4 5 6 7 8) (PROVE (DISABLE LENGTH-RFP CHANGED FOUND-VALUE NODE-VALUE SEND RECEIVE OUTSTANDING)) (DEMOTE 3) (DIVE 1) X-DUMB S-PROP TOP PROMOTE (DIVE 1) (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-REST-OF-TREE (($OLD OLD) ($NODE NODE) ($PARENT-OF-NODE (PARENT NODE TREE)) ($EXCPT (CHILDREN NODE TREE)))) UP (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP (DIVE 2) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) UP UP (DIVE 2) (REWRITE RECEIVE-FIND-PRESERVES-NO-FOR-REST-OF-TREE (($OLD OLD) ($NODE NODE) ($PARENT-OF-NODE (PARENT NODE TREE)) ($EXCPT (CHILDREN NODE TREE)))) (DIVE 4) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP (DEMOTE 6) (DEMOTE 5) (DIVE 1) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (APPEND (LIST (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'STATUS NODE) (CONS 'FOUND-VALUE NODE) (CONS 'OUTSTANDING NODE)) (RFP NODE (CHILDREN NODE TREE)))))) TOP S (DROP 1 2 3 4 5 6 7) (PROVE (DISABLE FOUND-VALUE STATUS OUTSTANDING NODE-VALUE SEND RECEIVE CHANNEL EMPTY HEAD LENGTH-RFP)) (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 7 8) PROVE (CONTRADICT 9) (DROP 3 4 5 6 7 8 9) PROVE (DROP 1 2 3 4 5 6 7 8 9) (PROVE (DISABLE LENGTH-RFP STATUS OUTSTANDING NODE-VALUE FOUND-VALUE SEND RECEIVE CHANNEL EMPTY HEAD CHILDREN PARENT)) (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 5 6 7 8 9 10) PROVE (DROP 3 5 6 7 10) PROVE (DROP 1 2 3 4 5 6 7 8 9) (PROVE (DISABLE LENGTH-RFP CHANGED STATUS FOUND-VALUE OUTSTANDING NODE-VALUE SEND RECEIVE CHANNEL EMPTY CHILDREN PARENT)) (DROP 1 2 3 4 5 6 7 8 9) (PROVE (DISABLE LENGTH-RFP STATUS OUTSTANDING NODE-VALUE FOUND-VALUE CHANNEL EMPTY SEND RECEIVE CHILDREN PARENT)) (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DROP 1 2 3 4 5 6 7 8 9) (PROVE (DISABLE LENGTH-RFP CHILDREN PARENT STATUS OUTSTANDING NODE-VALUE FOUND-VALUE SEND RECEIVE CHANNEL EMPTY)) (CLAIM (NUMBERP NODE) 0) (DROP 1 2 3 4 5 6 7 9 10) PROVE (CONTRADICT 11) (DROP 3 4 5 6 7 8 9 10 11) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 3 4 5 6 7 8 9 10) PROVE (DROP 2 3 5 6 7 8 9 10) PROVE (DROP 3 5 6 7 10) PROVE (DROP 1 2 3 4 5 6 7 8 9) (PROVE (DISABLE PARENT CHILDREN OUTSTANDING NODE-VALUE FOUND-VALUE STATUS LENGTH-RFP RECEIVE SEND CHANNEL EMPTY HEAD)) (DEMOTE 3) (DIVE 1) X-DUMB S-PROP TOP PROMOTE (DROP 7) (DIVE 1) (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DIVE 2) (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DROP 1 2 3 4) (PROVE (DISABLE PARENT CHILDREN))))) (prove-lemma receive-report-preserves-no-for-rest-of-tree (rewrite) (implies (and (numberp node) (numberp parent-of-node) (numberp child-of-node) (numberp parent) (not (equal parent node)) (not (member node children)) (changed old new (list (cons child-of-node node) (cons node parent-of-node) (cons 'outstanding node) (cons 'found-value node)))) (and (equal (number-not-reported children parent new) (number-not-reported children parent old)) (equal (min-of-reported children parent new value) (min-of-reported children parent old value)))) ((disable min) (induct (length children)))) (prove-lemma receive-report-preserves-no-for-node (rewrite) (implies (and (numberp node) (numberp parent) (numberp child) (not (member node children)) (all-numberps children) (setp children) (equal (channel (cons child node) old) (list (found-value child old))) (done child old) (equal (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)))) (and (equal (number-not-reported children node new) (if (member child children) (sub1 (number-not-reported children node old)) (number-not-reported children node old))) (equal (min-of-reported children node new value) (if (member child children) (min (found-value child old) (min-of-reported children node old value)) (min-of-reported children node old value))))) ((INSTRUCTIONS (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DISABLE REPORTED FOUND-VALUE HEAD CHANNEL RECEIVE MIN DONE) (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= T) TOP (CLAIM (EQUAL CHILD (CAR CHILDREN)) 0) (CLAIM (AND (MEMBER CHILD CHILDREN) (NOT (MEMBER CHILD (CDR CHILDREN)))) 0) S SPLIT (DIVE 1) X (DIVE 1) (= * T 0) UP S (DIVE 1) (= * (FOUND-VALUE CHILD OLD) 0) UP (DIVE 2) = TOP (DIVE 2) (DIVE 2) X (DIVE 1) (= * F ((DISABLE DONE CHANNEL))) TOP S (DROP 8 9 10 15 16 17) PROVE (DROP 15 16 17) PROVE (DIVE 1) X (DIVE 1) (= * T 0) UP S = TOP (DIVE 2) (DIVE 1) X (DIVE 1) (= * F ((DISABLE DONE CHANNEL))) TOP S (DROP 15 16) PROVE (CONTRADICT 13) (DROP 2 3 4 5 6 8 9 10 11 13) PROVE (CLAIM (AND (MEMBER CHILD (CDR CHILDREN)) (MEMBER CHILD CHILDREN)) 0) S SPLIT (DIVE 1) X (DIVE 1) (= * (REPORTED (CAR CHILDREN) NODE OLD) 0) UP (DIVE 2) (DIVE 1) (= * (FOUND-VALUE (CAR CHILDREN) OLD) 0) UP (DIVE 2) = UP UP (DIVE 3) = TOP (DIVE 2) (DIVE 2) X TOP DROP (PROVE (DISABLE DONE MIN RECEIVE CHANNEL HEAD FOUND-VALUE REPORTED)) (DROP 8 9 10 15 16 17) PROVE (DROP 8 9 10 15 16 17) PROVE (DIVE 1) X (DIVE 1) (= * (REPORTED (CAR CHILDREN) NODE OLD) 0) UP (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP (DIVE 2) (DIVE 1) X TOP S-PROP S S-PROP SPLIT (CONTRADICT 18) (DROP 1 2 3 4 5 6 7 10 11 12 14 15 16 17 18) (GENERALIZE (((CDR CHILDREN) L))) (PROVE (DISABLE CHANNEL DONE)) (DROP 8 9 10 13 14 15 16) PROVE (DEMOTE 13) (DIVE 1) (DIVE 1) (DIVE 2) X UP S TOP PROMOTE (CLAIM (NOT (MEMBER CHILD CHILDREN)) 0) S SPLIT (DIVE 1) X (DIVE 1) (= * (REPORTED (CAR CHILDREN) NODE OLD) 0) UP (DIVE 2) (DIVE 2) = UP (DIVE 1) (= * (FOUND-VALUE (CAR CHILDREN) OLD) 0) UP UP (DIVE 3) = TOP (DIVE 2) X TOP S (DROP 8 9 10 15 16 17 18) PROVE (DROP 8 9 10 15 16 17) PROVE (DIVE 1) X (DIVE 1) (= * (REPORTED (CAR CHILDREN) NODE OLD) 0) UP (DIVE 2) = UP (DIVE 3) (DIVE 1) = TOP (DIVE 2) X TOP S (DROP 8 9 10 15 16) PROVE (CONTRADICT 14) (DROP 2 3 4 5 6 8 9 10 11 14) PROVE PROVE))) (prove-lemma receive-report-preserves-no-for-parent (rewrite) (implies (and (numberp node) (numberp parent) (not (equal node parent)) (implies (zerop (outstanding node new)) (not (empty (cons node parent) new))) (not (zerop (outstanding node old))) (changed old new (list (cons child node) (cons node parent) (cons 'outstanding node) (cons 'found-value node)))) (and (equal (number-not-reported children parent new) (number-not-reported children parent old)) (equal (min-of-reported children parent new value) (min-of-reported children parent old value)))) ((INSTRUCTIONS (DISABLE MIN REPORTED) (INDUCT (LENGTH CHILDREN)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) (S-PROP AND) S UP (S-PROP IMPLIES) TOP PROMOTE (CLAIM (EQUAL (CAR CHILDREN) NODE) 0) PROVE PROVE PROVE))) (prove-lemma child-member-cdr-nodes (rewrite) (implies (and (proper-tree 'tree tree) (setp (nodes-rec 'tree tree)) (member child (children-rec 'tree node tree))) (member child (cdr (nodes-rec 'tree tree)))) ((INSTRUCTIONS PROMOTE (CONTRADICT 3) (DIVE 1) (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP (BASH T)))) (prove-lemma receive-report-preserves-instance-of-no (rewrite) (implies (and (treep tree) (member node (cdr (nodes tree))) (member child (children node tree)) (member n (nodes tree)) (receive-report old new node (cons child node) (cons node (parent node tree))) (equal (status n new) 'started) (ul (up-links (cdr (nodes tree)) tree) old) (no (nodes tree) tree old) (dl (down-links (nodes tree) tree) old)) (and (equal (outstanding n new) (number-not-reported (children n tree) n new)) (equal (found-value n new) (min-of-reported (children n tree) n new (node-value n new))))) ((INSTRUCTIONS PROMOTE (CLAIM (AND (NUMBERP NODE) (NUMBERP (PARENT NODE TREE)) (NUMBERP N) (NUMBERP CHILD) (NOT (EQUAL CHILD NODE)) (NOT (EQUAL (PARENT NODE TREE) NODE)) (NOT (MEMBER NODE (CHILDREN NODE TREE))) (NOT (MEMBER N (CHILDREN N TREE))) (ALL-NUMBERPS (CHILDREN NODE TREE)) (ALL-NUMBERPS (CHILDREN N TREE)) (SETP (CHILDREN NODE TREE)) (SETP (CHILDREN N TREE))) 0) (CLAIM (AND (EQUAL (STATUS N OLD) (STATUS N NEW)) (EQUAL (NODE-VALUE N OLD) (NODE-VALUE N NEW))) 0) (CLAIM (EQUAL (CHANNEL (CONS CHILD NODE) OLD) (LIST (FOUND-VALUE CHILD OLD))) 0) (CLAIM (DONE CHILD OLD) 0) (CLAIM (EQUAL (STATUS NODE OLD) 'STARTED) 0) (CLAIM (EQUAL N NODE) 0) (DEMOTE 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26) (= N NODE) DROP PROMOTE (USE-LEMMA RECEIVE-REPORT-PRESERVES-NO-FOR-NODE ((NODE NODE) (PARENT (PARENT NODE TREE)) (CHILD CHILD) (CHILDREN (CHILDREN NODE TREE)) (OLD OLD) (NEW NEW) (VALUE (NODE-VALUE NODE OLD)))) (DEMOTE 23) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP (S-PROP IMPLIES) TOP PROMOTE (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE NODE))) (DEMOTE 25) (DIVE 1) (DIVE 1) S-PROP UP (S-PROP IMPLIES) TOP PROMOTE (DIVE 1) (DIVE 2) = TOP (DIVE 2) (DIVE 2) (DIVE 4) = UP = TOP (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 21 22 23 24) (PROVE (DISABLE CHANGED MIN ZEROP CHANNEL)) (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 21 22) (PROVE (DISABLE CHANNEL RECEIVE MIN ZEROP CHANGED)) (CLAIM (EQUAL N (PARENT NODE TREE)) 0) (DEMOTE 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27) (= N (PARENT NODE TREE)) DROP PROMOTE (USE-LEMMA RECEIVE-REPORT-PRESERVES-NO-FOR-PARENT ((NODE NODE) (PARENT (PARENT NODE TREE)) (OLD OLD) (NEW NEW) (CHILD CHILD) (CHILDREN (CHILDREN (PARENT NODE TREE) TREE)) (VALUE (NODE-VALUE (PARENT NODE TREE) OLD)))) (DEMOTE 26) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP (S-PROP IMPLIES) TOP PROMOTE (CLAIM (AND (EQUAL (OUTSTANDING (PARENT NODE TREE) NEW) (OUTSTANDING (PARENT NODE TREE) OLD)) (EQUAL (FOUND-VALUE (PARENT NODE TREE) NEW) (FOUND-VALUE (PARENT NODE TREE) OLD))) 0) (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE (PARENT NODE TREE)))) (DEMOTE 30) (DIVE 1) (DIVE 1) S-PROP (DIVE 1) = = UP S UP (S-PROP IMPLIES) TOP PROMOTE (DIVE 1) (DIVE 1) = UP (DIVE 2) = TOP (DIVE 2) (DIVE 1) = UP (DIVE 2) (DIVE 4) = UP = TOP (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 2 6 27 28 29) PROVE (CONTRADICT 28) (DROP 1 2 3 4 6 7 8 9 12 13 14 15 16 17 18 19 20 21 23 24 26 27 28) (PROVE (DISABLE CHANNEL MIN ZEROP)) (DIVE 1) (DIVE 1) (= * F 0) UP S-PROP (DIVE 2) (DIVE 3) (DIVE 3) (= * T 0) TOP (DIVE 1) (DIVE 3) (DIVE 3) (= * T 0) TOP (CLAIM (NOT (ZEROP (OUTSTANDING NODE OLD))) 0) S-PROP (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 23 24 25 26) (PROVE (DISABLE MIN CHANGED CHANNEL)) (CONTRADICT 26) (DIVE 1) (DIVE 1) S (REWRITE NO-IMPLIES-INSTANCE-OF-NO (($NODES (NODES TREE)) ($TREE TREE))) TOP S (CLAIM (NOT (REPORTED CHILD NODE OLD)) 0) (CONTRADICT 27) (REWRITE NUMBER-NOT-REPORTED-0-IMPLIES (($CHILDREN (CHILDREN NODE TREE)))) (DEMOTE 27) DROP PROVE (CONTRADICT 27) (DIVE 1) X-DUMB S-PROP X-DUMB (DIVE 1) (DIVE 1) = TOP S (DROP 3 4 5 6 7 8 9 10 11 12 13 14 15 1 17 18 19 20 21 22 23 24 25 26) PROVE (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 23 24 25 26 27) (PROVE (DISABLE CHANGED CHANNEL ZEROP MIN)) (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 23 24 25 26 27 28) (PROVE (DISABLE CHANNEL CHANGED MIN ZEROP)) (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24) PROVE (CLAIM (AND (EQUAL (FOUND-VALUE N OLD) (FOUND-VALUE N NEW)) (EQUAL (OUTSTANDING N OLD) (OUTSTANDING N NEW))) 0) (USE-LEMMA RECEIVE-REPORT-PRESERVES-NO-FOR-REST-OF-TREE ((NODE NODE) (CHILD-OF-NODE CHILD) (PARENT-OF-NODE (PARENT NODE TREE)) (PARENT N) (CHILDREN (CHILDREN N TREE)) (VALUE (NODE-VALUE N OLD)))) (DEMOTE 31) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP (S-PROP IMPLIES) TOP PROMOTE (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE N))) (DEMOTE 33) (DIVE 1) (DIVE 1) S-PROP (DIVE 1) = = UP S UP (S-PROP IMPLIES) TOP PROMOTE (DIVE 1) (DIVE 1) = UP (DIVE 2) = TOP (DIVE 2) (DIVE 1) = UP (DIVE 2) (DIVE 4) = UP = TOP (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32) PROVE S-PROP SPLIT (DROP 3 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 29 30) PROVE (DROP 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 25 26 27 28 29 30 31) (PROVE (DISABLE CHANGED CHANNEL MIN ZEROP)) (CONTRADICT 29) (DROP 1 2 3 4 6 7 8 9 16 17 18 19 20 21 22 23 25 26 29) (PROVE (DISABLE MIN ZEROP CHANNEL)) (CLAIM (EQUAL (STATUS CHILD OLD) 'STARTED) 0) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (DOWN-LINK (CONS NODE CHILD)) (STATE OLD))) (CONTRADICT 26) (DEMOTE 28) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DEMOTE 27) DROP PROVE (DROP 5 6 7 8 9 18 19 20 21 22 23 24 25 26 27) PROVE (CONTRADICT 27) (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (STATE OLD) (UPLINK (CONS CHILD NODE)))) (DEMOTE 28) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP (S-PROP IMPLIES) TOP (DEMOTE 24) DROP PROVE (DROP 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27) PROVE (CONTRADICT 25) (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (STATE OLD) (UPLINK (CONS CHILD NODE)))) (DEMOTE 26) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DEMOTE 24) DROP PROVE (DROP 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25) PROVE (DEMOTE 5) (DIVE 1) X-DUMB (DIVE 1) (= * T 0) UP S-PROP TOP PROMOTE (DIVE 1) (DIVE 2) (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (DIVE 2) (DIVE 2) (DIVE 4) = UP (REWRITE UNCHANGED-PRESERVES-NO (($OLD OLD))) TOP (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE N))) (DEMOTE 25) (DIVE 1) (DIVE 1) S-PROP (DIVE 1) = = UP S UP (S-PROP IMPLIES) TOP (DEMOTE 24) DROP PROVE (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (STATE OLD) (UPLINK (CONS CHILD NODE)))) (DEMOTE 24) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DEMOTE 23) DROP PROVE (DROP 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23) PROVE (CONTRADICT 22) (DROP 1 2 3 4 6 7 8 9 16 17 18 19 20 21 22) (PROVE (DISABLE MIN ZEROP CHANNEL SEND RECEIVE HEAD PARENT CHILDREN NODES)) (CONTRADICT 10) (DROP 5 6 7 8 9 10) PROVE))) (prove-lemma dl-ul-no-preserves-instance-of-no (rewrite) (implies (and (treep tree) (n old new statement) (member statement (tree-prg tree)) (dl (down-links (nodes tree) tree) old) (ul (up-links (cdr (nodes tree)) tree) old) (no (nodes tree) tree old) (member node (nodes tree)) (equal (status node new) 'started)) (and (equal (outstanding node new) (number-not-reported (children node tree) node new)) (equal (found-value node new) (min-of-reported (children node tree) node new (node-value node new))))) ((INSTRUCTIONS PROMOTE (USE-LEMMA NO-IMPLIES-INSTANCE-OF-NO ((NODES (NODES TREE)) (TREE TREE) (STATE OLD) (NODE NODE))) (DEMOTE 9) (DIVE 1) (DIVE 1) S-PROP UP (DIVE 2) (DIVE 1) (DIVE 1) (= (OUTSTANDING NODE OLD)) UP UP (DIVE 2) (DIVE 1) (= (FOUND-VALUE NODE OLD)) TOP PROMOTE (CLAIM (EQUAL (CAR STATEMENT) 'START) 0) (USE-LEMMA START-PRESERVES-INSTANCE-OF-NO ((TREE TREE) (OLD OLD) (NEW NEW) (NODE NODE))) (DEMOTE 11) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DROP 3 4 5 6 7 8 9) (PROVE (DISABLE TREE-PRG START)) (DROP 8) (DEMOTE 8) (DISABLE STATUS OUTSTANDING FOUND-VALUE NODE-VALUE START ROOT-RECEIVE-REPORT RECEIVE-FIND RECEIVE-REPORT) S SPLIT (DROP 2 3 5 6 7 8 9 10 11 12) (DIVE 1) (DIVE 2) (= (CHILDREN (CAR TREE) TREE)) TOP (REWRITE DL-DOWN-LINKS-IMPLIES-DL-RFP (($NODES (NODES TREE)))) PROVE (DROP 4 5 6 7 9 10 11) (PROVE (DISABLE TREE-PRG START)) (DIVE 1) (DIVE 2) (= (CHILDREN (CAR TREE) TREE)) TOP (REWRITE DL-DOWN-LINKS-IMPLIES-DL-RFP (($NODES (NODES TREE)))) (DROP 2 3 4 5 6 7 8 9 10) PROVE (DROP 4 5 6 7 9) (PROVE (DISABLE TREE-PRG START)) (CLAIM (EQUAL (CAR STATEMENT) 'ROOT-RECEIVE-REPORT) 0) (USE-LEMMA ROOT-RECEIVE-REPORT-PRESERVES-INSTANCE-OF-NO ((TREE TREE) (CHILD (CAADDR STATEMENT)) (OLD OLD) (NEW NEW) (NODE NODE))) (DEMOTE 9) (DEMOTE 11) (DIVE 1) (DIVE 1) S-PROP (DIVE 1) (= * T 0) UP (DIVE 2) (DIVE 1) (= * T 0) TOP S (DROP 4 5 6 7 8 9) (PROVE (DISABLE TREE-PRG ROOT-RECEIVE-REPORT)) (DROP 2 4 5 6 7 8 9) (PROVE (DISABLE TREE-PRG)) (DEMOTE 9) (CLAIM (EQUAL (CAR STATEMENT) 'RECEIVE-FIND) 0) (USE-LEMMA RECEIVE-FIND-PRESERVES-INSTANCE-OF-NO ((TREE TREE) (NODE (CADR STATEMENT)) (PARENT (CAADDR STATEMENT)) (N NODE) (OLD OLD) (NEW NEW))) (DEMOTE 12) (DIVE 1) (DIVE 1) S-PROP S (DIVE 1) (= * T 0) UP (DIVE 2) (DIVE 1) (= * T 0) TOP S (DROP 4 5 6 7 8 9 10) (PROVE (DISABLE TREE-PRG RECEIVE-FIND)) (DROP 2 4 5 6 7 8 9 10) (PROVE (DISABLE TREE-PRG)) (USE-LEMMA RECEIVE-REPORT-PRESERVES-INSTANCE-OF-NO ((TREE TREE) (NODE (CADR STATEMENT)) (CHILD (CAADDR STATEMENT)) (N NODE) (OLD OLD) (NEW NEW))) (DEMOTE 12) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP S S-PROP S SPLIT (DROP 4 5 6 7 8 12 13) (PROVE (DISABLE RECEIVE-REPORT TREE-PRG)) (DROP 2 4 5 6 7 8 12) (PROVE (DISABLE TREE-PRG)) (DROP 2 4 5 6 7 8) (PROVE (DISABLE TREE-PRG))))) (prove-lemma dl-ul-no-preserves-no-sublist (rewrite) (implies (and (treep tree) (n old new statement) (member 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)) ((INSTRUCTIONS (INDUCT (NO SUBLIST TREE NEW)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP S TOP PROMOTE X (DROP 9) (USE-LEMMA DL-UL-NO-PRESERVES-INSTANCE-OF-NO ((TREE TREE) (OLD OLD) (NEW NEW) (STATEMENT STATEMENT) (NODE (CAR SUBLIST)))) (DEMOTE 9) (DIVE 1) (DIVE 1) S-PROP (DIVE 1) (= * T 0) TOP S (DROP 3 4 5 6 7) PROVE (DROP 2 3 4 5 6 7) PROVE PROMOTE PROMOTE X))) (prove-lemma inv-preserves-inv (rewrite) (implies (and (treep tree) (n old new statement) (member statement (tree-prg tree)) (inv tree old)) (inv tree new)) ((INSTRUCTIONS (DISABLE NODES N MEMBER-TREE-PRG TREE-PRG TREEP) S SPLIT (REWRITE DL-UL-NO-PRESERVES-NO-SUBLIST) (REWRITE SUBLISTP-REFLEXIVE) (REWRITE DL-UL-NO-PRESERVES-UL) (REWRITE DL-PRESERVES-DL)))) (prove-lemma inv-is-invariant (rewrite) (implies (and (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree)) (treep tree)) (invariant `(inv (quote ,tree) state) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE UNLESS-PROVES-INVARIANT (($IC (LIST 'AND (LIST 'ALL-EMPTY (LIST 'QUOTE (ALL-CHANNELS TREE)) 'STATE) (LIST 'NOT-STARTED (LIST 'QUOTE (NODES TREE)) 'STATE))))) (BASH (DISABLE INV TREEP N MEMBER-TREE-PRG TREE-PRG)) (BASH (DISABLE INV TREE-PRG))))) (prove-lemma outstanding-non-increasing (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement) (dl (down-links (nodes tree) tree) old) (member node (nodes tree))) (not (lessp (if (equal (status node old) 'started) (outstanding node old) (add1 (length (children node tree)))) (if (equal (status node new) 'started) (outstanding node new) (add1 (length (children node tree))))))) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (CADR STATEMENT) NODE) 0) (CLAIM (EQUAL (CAR STATEMENT) 'RECEIVE-FIND) 0) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (STATE OLD) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)))) (DEMOTE 8) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DROP 4) (BASH T (DISABLE MIN ZEROP TREE-PRG)) (DROP 3 4) (CLAIM (LISTP (PARENT-REC 'TREE NODE TREE)) 0) (DROP 2 4 5) (PROVE (ENABLE PARENT-REC-CHILDREN-REC)) (CONTRADICT 6) (DIVE 1) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP (PROVE (DISABLE TREE-PRG)) PROVE PROVE (DROP 4) (BASH T (DISABLE TREE-PRG MIN ZEROP)) PROMOTE (DIVE 1) (DIVE 2) = TOP DROP PROVE PROMOTE (DIVE 1) (DIVE 2) = TOP DROP PROVE (DROP 4) (BASH T (DISABLE TREE-PRG MIN ZEROP))))) (prove-lemma total-outstanding-non-increasing-sublist (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement) (dl (down-links (nodes tree) tree) old) (sublistp sublist (nodes tree))) (not (lessp (total-outstanding sublist tree old) (total-outstanding sublist tree new)))) ((INSTRUCTIONS (INDUCT (TOTAL-OUTSTANDING SUBLIST TREE OLD)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP (S-PROP IMPLIES) TOP PROMOTE (USE-LEMMA OUTSTANDING-NON-INCREASING ((TREE TREE) (STATEMENT STATEMENT) (OLD OLD) (NEW NEW) (NODE (CAR SUBLIST)))) (DEMOTE 8) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DROP 2 3 4 5 6) (PROVE (DISABLE OUTSTANDING STATUS CHILDREN)) (DROP 2 3 4 5 7) PROVE (DROP 2 3 4 5) PROVE (PROVE (DISABLE TREEP TREE-PRG MEMBER-TREE-PRG NODES N))))) (prove-lemma total-outstanding-non-increasing (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement) (dl (down-links (nodes tree) tree) old)) (not (lessp (total-outstanding (nodes tree) tree old) (total-outstanding (nodes tree) tree new)))) ((disable nodes treep tree-prg member-tree-prg))) (prove-lemma position-append (rewrite) (equal (position (append a b) e) (if (member e a) (position a e) (plus (length a) (position b e))))) (prove-lemma parents-position-decreases (rewrite) (implies (and (member node (nodes-rec flag tree)) (setp (nodes-rec flag tree)) (proper-tree flag tree) (if (equal flag 'tree) (not (equal (car tree) node)) (not (member node (roots tree))))) (lessp (position (nodes-rec flag tree) (car (parent-rec flag node tree))) (position (nodes-rec flag tree) node)))) (defn parent-to-root-induction (node tree) (if (and (member node (nodes tree)) (setp (nodes tree)) (proper-tree 'tree tree)) (if (equal (car tree) node) t (parent-to-root-induction (parent node tree) tree)) t) ((lessp (position (nodes tree) node)))) (prove-lemma dl-and-all-empty-implies-root-defines-status (rewrite) (implies (and (dl (down-links (nodes tree) tree) state) (all-empty (down-links (nodes tree) tree) state) (setp (nodes tree)) (proper-tree 'tree tree) (member node (nodes tree))) (equal (cdr (assoc (cons 'status node) state)) (status (car tree) state))) ((INSTRUCTIONS (INDUCT (PARENT-TO-ROOT-INDUCTION NODE TREE)) PROVE (CLAIM (MEMBER NODE (CHILDREN-REC 'TREE (CAR (PARENT-REC 'TREE NODE TREE)) TREE)) 0) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (STATE STATE) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)))) (USE-LEMMA ALL-EMPTY-IMPLIES-EMPTY ((CHANNELS (DOWN-LINKS (NODES TREE) TREE)) (STATE STATE) (CHANNEL (CONS (PARENT NODE TREE) NODE)))) PROVE (CONTRADICT 1) (REWRITE PARENT-REC-CHILDREN-REC) PROVE PROVE))) (defn suffix (s l) (if (listp l) (if (equal s l) t (suffix s (cdr l))) (not (listp s)))) (prove-lemma suffix-implies-suffix-cdr (rewrite) (implies (suffix s l) (suffix (cdr s) l))) (prove-lemma member-suffix-member-list (rewrite) (implies (and (member e s) (suffix s l)) (member e l))) (prove-lemma childs-position-increases (rewrite) (implies (and (member node (nodes-rec flag tree)) (setp (nodes-rec flag tree)) (proper-tree flag tree) (member child (children-rec flag node tree))) (lessp (position (nodes-rec flag tree) node) (position (nodes-rec flag tree) child))) ((enable parent-rec-children-rec) (use (parents-position-decreases (node child))))) (prove-lemma setp-list-setp-suffix (rewrite) (implies (and (setp l) (suffix s l)) (setp s))) (prove-lemma later-positions-are-in-suffix (rewrite) (implies (and (setp l) (suffix s l) (member x s) (member y l) (lessp (position l x) (position l y))) (member y s))) (defn all-done (nodes state) (if (listp nodes) (if (done (car nodes) state) (all-done (cdr nodes) state) f) t)) (prove-lemma all-done-implies-done (rewrite) (implies (and (all-done nodes state) (member node nodes)) (done node state)) ((disable done))) (prove-lemma all-done-implies-all-done-sublist (rewrite) (implies (and (all-done nodes state) (sublistp sublist nodes)) (all-done sublist state)) ((disable done))) (defn ulnks (children parent) (if (listp children) (cons (cons (car children) parent) (ulnks (cdr children) parent)) nil)) (prove-lemma all-done-and-all-empty-implies-number-not-reported-0 (rewrite) (implies (and (all-done children state) (all-empty (ulnks children parent) state)) (equal (number-not-reported children parent state) 0)) ((disable done))) (prove-lemma all-empty-implies-all-empty-sublist (rewrite) (implies (and (all-empty channels state) (sublistp sublist channels)) (all-empty sublist state)) ((disable channel))) (prove-lemma sublist-ulnks (rewrite) (implies (and (proper-tree 'tree tree) (sublistp sublist (children parent tree)) (setp (nodes tree))) (sublistp (ulnks sublist parent) (up-links (cdr (nodes tree)) tree))) ((induct (ulnks sublist parent)))) (prove-lemma child-of-node-in-suffix-is-in-suffix (rewrite) (implies (and (proper-tree 'tree tree) (setp (nodes tree)) (member child (children node tree)) (suffix nodes (nodes tree)) (member node nodes)) (member child (cdr nodes))) ((INSTRUCTIONS PROMOTE (CLAIM (MEMBER CHILD NODES)) PROVE))) (prove-lemma children-are-suffix-of-sublist-generalized (rewrite) (implies (and (proper-tree 'tree tree) (setp (nodes tree)) (suffix nodes (nodes tree)) (member node nodes) (sublistp sublist (children-rec 'tree node tree))) (sublistp sublist (cdr nodes))) ((INSTRUCTIONS (INDUCT (LENGTH SUBLIST)) PROMOTE PROMOTE X (DIVE 1) (REWRITE CHILD-OF-NODE-IN-SUFFIX-IS-IN-SUFFIX (($NODE NODE) ($TREE TREE))) TOP PROVE PROVE PROVE))) (prove-lemma all-nodes-are-done (rewrite) (implies (and (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) (equal (status (car tree) state) 'started) (suffix nodes (nodes tree))) (all-done nodes state)) ((INSTRUCTIONS (INDUCT (LENGTH NODES)) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP (REWRITE SUFFIX-IMPLIES-SUFFIX-CDR) UP S TOP PROMOTE X (DIVE 1) (DIVE 1) (REWRITE DL-AND-ALL-EMPTY-IMPLIES-ROOT-DEFINES-STATUS (($TREE TREE))) = TOP S (DIVE 1) (DIVE 1) (REWRITE NO-IMPLIES-INSTANCE-OF-NO (($NODES (NODES TREE)) ($TREE TREE))) (REWRITE ALL-DONE-AND-ALL-EMPTY-IMPLIES-NUMBER-NOT-REPORTED-0) TOP S (REWRITE ALL-DONE-IMPLIES-ALL-DONE-SUBLIST (($NODES (CDR NODES)))) (REWRITE CHILDREN-ARE-SUFFIX-OF-SUBLIST-GENERALIZED (($TREE TREE) ($NODE (CAR NODES)))) X (REWRITE SUBLISTP-REFLEXIVE) (REWRITE ALL-EMPTY-IMPLIES-ALL-EMPTY-SUBLIST (($CHANNELS (UP-LINKS (CDR (NODES TREE)) TREE)))) (REWRITE SUBLIST-ULNKS) S (REWRITE SUBLISTP-REFLEXIVE) (REWRITE MEMBER-SUFFIX-MEMBER-LIST (($S NODES))) X S (DIVE 1) (REWRITE DL-AND-ALL-EMPTY-IMPLIES-ROOT-DEFINES-STATUS (($TREE TREE))) = TOP S (REWRITE MEMBER-SUFFIX-MEMBER-LIST (($S NODES))) X (REWRITE MEMBER-SUFFIX-MEMBER-LIST (($S NODES))) X PROMOTE X))) (prove-lemma all-done-implies-total-outstanding-0 (rewrite) (implies (all-done nodes state) (equal (total-outstanding nodes tree state) 0))) (prove-lemma all-empty-root-started-implies-total-outstanding-0 (rewrite) (implies (and (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) (equal (status (car tree) state) 'started)) (equal (total-outstanding (nodes tree) tree state) 0)) ((INSTRUCTIONS PROMOTE (DEMOTE 3) (DIVE 1) X-DUMB TOP PROMOTE (DIVE 1) (REWRITE ALL-DONE-IMPLIES-TOTAL-OUTSTANDING-0) TOP S (REWRITE ALL-NODES-ARE-DONE (($TREE TREE))) X))) (defn full-channel (channels state) (if (listp channels) (if (empty (car channels) state) (full-channel (cdr channels) state) (car channels)) f)) (prove-lemma not-all-empty-implies-full-channel-full (rewrite) (implies (and (not (all-empty channels state)) (not (member f channels))) (and (listp (cdr (assoc (full-channel channels state) state))) (member (full-channel channels state) channels) (full-channel channels state)))) (prove-lemma not-total-outstanding-0-implies-full-channel (rewrite) (implies (and (proper-tree 'tree tree) (setp (nodes tree)) (inv tree state) (or (equal (status (car tree) state) 'started) (equal (status (car tree) state) 'not-started)) (not (equal (total-outstanding (nodes tree) tree state) 0))) (or (equal (status (car tree) state) 'not-started) (full-channel (down-links (nodes tree) tree) state) (full-channel (up-links (cdr (nodes tree)) tree) state))) ((INSTRUCTIONS PROMOTE (CONTRADICT 5) (DIVE 1) (REWRITE ALL-EMPTY-ROOT-STARTED-IMPLIES-TOTAL-OUTSTANDING-0) TOP S SPLIT (CONTRADICT 6) (REWRITE NOT-ALL-EMPTY-IMPLIES-FULL-CHANNEL-FULL) (DROP 3 4 5 6 7) PROVE SPLIT (CONTRADICT 7) (REWRITE NOT-ALL-EMPTY-IMPLIES-FULL-CHANNEL-FULL) (DROP 3 4 5 6 7) PROVE SPLIT))) (prove-lemma status-root-becomes-started-or-unchanged (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement)) (or (equal (status (car tree) new) 'started) (equal (status (car tree) new) (status (car tree) old)))) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (CADR STATEMENT) (CAR TREE)) 0) (PROVE (DISABLE TREE-PRG MIN)) (PROVE (DISABLE TREE-PRG MIN))))) (prove-lemma root-started-or-not-started-is-invariant (rewrite) (implies (and (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree)) (treep tree)) (invariant `(or (equal (status (quote ,(car tree)) state) 'started) (equal (status (quote ,(car tree)) state) 'not-started)) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE UNLESS-PROVES-INVARIANT (($IC (LIST 'AND (LIST 'ALL-EMPTY (LIST 'QUOTE (ALL-CHANNELS TREE)) 'STATE) (LIST 'NOT-STARTED (LIST 'QUOTE (NODES TREE)) 'STATE))))) (REWRITE HELP-PROVE-UNLESS) (DROP 1) (GENERALIZE (((EU (LIST 'OR (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('STARTED))) (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('NOT-STARTED)))) (TREE-PRG TREE) '(FALSE)) STATEMENT) ((OLDU (LIST 'OR (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('STARTED))) (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('NOT-STARTED)))) (TREE-PRG TREE) '(FALSE)) OLD) ((NEWU (LIST 'OR (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('STARTED))) (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('NOT-STARTED)))) (TREE-PRG TREE) '(FALSE)) NEW))) (USE-LEMMA STATUS-ROOT-BECOMES-STARTED-OR-UNCHANGED ((TREE TREE) (OLD OLD) (NEW NEW))) (PROVE (DISABLE TREE-PRG MEMBER-TREE-PRG N)) (PROVE (DISABLE TREE-PRG) (EXPAND (NOT-STARTED (NODES-REC 'TREE TREE) (S (TREE-PRG TREE) 0))))))) (prove-lemma total-outstanding-decreases-sublist (rewrite) (implies (and (treep tree) (dl (down-links (nodes tree) tree) old) (n old new statement) (member statement (tree-prg tree)) (sublistp nodes (nodes tree)) (member node nodes) (lessp (if (equal (status node new) 'started) (outstanding node new) (add1 (length (children node tree)))) (if (equal (status node old) 'started) (outstanding node old) (add1 (length (children node tree)))))) (lessp (total-outstanding nodes tree new) (total-outstanding nodes tree old))) ((INSTRUCTIONS (INDUCT (MEMBER NODE NODES)) (PROVE (DISABLE TREE-PRG MEMBER-TREE-PRG TREEP STATUS OUTSTANDING CHILDREN)) (PROVE (DISABLE TREE-PRG MEMBER-TREE-PRG TREEP STATUS OUTSTANDING CHILDREN NODES N) (EXPAND (TOTAL-OUTSTANDING NODES TREE OLD) (TOTAL-OUTSTANDING NODES TREE NEW))) PROMOTE PROMOTE (DEMOTE 3) (DIVE 1) (DIVE 1) S-PROP (= * T 0) UP S TOP PROMOTE (DROP 8 9) (USE-LEMMA OUTSTANDING-NON-INCREASING ((TREE TREE) (STATEMENT STATEMENT) (OLD OLD) (NEW NEW) (NODE (CAR NODES)))) (PROVE (DISABLE TREE-PRG MEMBER-TREE-PRG TREEP STATUS OUTSTANDING CHILDREN NODES N) (EXPAND (TOTAL-OUTSTANDING NODES TREE OLD) (TOTAL-OUTSTANDING NODES TREE NEW))) (DROP 3 4 5 6) (PROVE (DISABLE STATUS OUTSTANDING NODES CHILDREN))))) (defn tou (old new node tree) (lessp (if (equal (status node new) 'started) (outstanding node new) (add1 (length (children node tree)))) (if (equal (status node old) 'started) (outstanding node old) (add1 (length (children node tree)))))) (prove-lemma total-outstanding-decreases (rewrite) (implies (and (treep tree) (dl (down-links (nodes tree) tree) old) (n old new statement) (member statement (tree-prg tree)) (member node (nodes tree)) (tou old new node tree)) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old))) ((INSTRUCTIONS PROMOTE (DEMOTE 6) (DIVE 1) X TOP PROMOTE (PROVE (DISABLE TREE-PRG MEMBER-TREE-PRG N TREEP NODES))))) (prove-lemma start-decreases-tou (rewrite) (implies (and (treep tree) (equal (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))) (prove-lemma others-preserve-root-not-started (rewrite) (implies (and (treep tree) (n old new statement) (member statement (tree-prg tree)) (not (equal statement (list 'start (car tree) (rfp (car tree) (children (car tree) tree)))))) (equal (cdr (assoc (cons 'status (car tree)) new)) (status (car tree) old))) ((INSTRUCTIONS (BASH T (DISABLE TREE-PRG MIN ZEROP PARENT CHILDREN NODES)) PROMOTE (CLAIM (AND (NUMBERP W) (NUMBERP (PARENT W (CONS X Z)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT W (CONS X Z)) W) (CONS (CONS W (PARENT W (CONS X Z))) (CONS (CONS 'STATUS W) (CONS (CONS 'FOUND-VALUE W) (CONS (CONS 'OUTSTANDING W) (RFP W (CHILDREN W (CONS X Z))))))))))) TOP S (DROP 4 5 6 7 8 9 11 12) (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (CONTRADICT 7) (DROP 3 4 6 7) PROVE (CONTRADICT 14) (DROP 4 5 6 7 8 9 10 11 12 14) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT W (CONS X Z)) W) (CONS (CONS W (PARENT W (CONS X Z))) (CONS (CONS 'STATUS W) (CONS (CONS 'FOUND-VALUE W) (CONS (CONS 'OUTSTANDING W) (RFP W (CHILDREN W (CONS X Z))))))))))) TOP S (CLAIM (AND (NUMBERP W) (NUMBERP (PARENT W (CONS X Z)))) 0) (DROP 4 5 6 7 8 10 11) (BASH T (DISABLE CHILDREN PARENT NODES)) PROMOTE (CONTRADICT 7) (DROP 3 4 5 6 7) PROVE (CONTRADICT 13) (DROP 4 5 6 7 8 9 10 11) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (PARENT W (CONS X Z))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (CLAIM (AND (NUMBERP Z1) (NUMBERP W) (NOT (EQUAL X W))) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11 12) PROVE (CONTRADICT 13) (DROP 4 5 6 7 8 9 10 13) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (PARENT W (CONS X Z))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (CLAIM (AND (NUMBERP Z1) (NUMBERP W)) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11 12) (PROVE (DISABLE PARENT)) (CONTRADICT 13) (DROP 4 5 6 7 8 9 10 13) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (PARENT W (CONS X Z))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (CLAIM (AND (NUMBERP Z1) (NUMBERP W)) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11 12) (PROVE (DISABLE PARENT)) (CONTRADICT 13) (DROP 4 5 6 7 8 9 10 13) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS Z1 W) (CONS W (PARENT W (CONS X Z))) (CONS 'OUTSTANDING W) (CONS 'FOUND-VALUE W))))) TOP S (CLAIM (AND (NUMBERP Z1) (NUMBERP W)) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11 12) (PROVE (DISABLE PARENT)) (CONTRADICT 13) (DROP 4 5 6 7 8 9 10 13) PROVE PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS V X) (CONS 'OUTSTANDING X) (CONS 'FOUND-VALUE X))))) TOP S (CLAIM (NUMBERP V) 0) (DROP 1 2 3 4 5 6 7 8 9) PROVE (CONTRADICT 10) (DROP 4 5 6 7 8 10) PROVE))) (prove-lemma root-receive-report-decreases-tou (rewrite) (implies (and (treep tree) (listp (channel (cons child (car tree)) old)) (member 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)) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (STATUS (CAR TREE) OLD) 'STARTED) 0) (CLAIM (NOT (ZEROP (OUTSTANDING (CAR TREE) OLD))) 0) (DROP 5) PROVE (USE-LEMMA NUMBER-NOT-REPORTED-0-IMPLIES ((CHILDREN (CHILDREN (CAR TREE) TREE)) (PARENT (CAR TREE)) (STATE OLD) (NODE CHILD))) (CONTRADICT 2) (DROP 2) (DEMOTE 6) (DIVE 1) (DIVE 1) S (REWRITE NO-IMPLIES-INSTANCE-OF-NO (($TREE TREE) ($NODES (NODES TREE)))) TOP (DROP 4) DEMOTE S (DEMOTE 4) S (DROP 2 3 4 5 6) PROVE (CONTRADICT 6) (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (UPLINK (CONS CHILD (CAR TREE))) (STATE OLD))) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (STATE OLD) (DOWN-LINK (CONS (CAR TREE) CHILD)))) (DROP 4 6) (DEMOTE 5) (DIVE 1) (DIVE 1) (= * T 0) TOP (DEMOTE 5) (DIVE 1) (DIVE 1) (= * T 0) TOP (DROP 1 3 4) DEMOTE PROVE (DROP 2) (DIVE 1) (DIVE 1) (= T) TOP (DROP 3) S-PROP (DIVE 1) (REWRITE MEMBER-DOWN-LINKS) TOP PROVE (DIVE 1) (DIVE 1) (DROP 5) (= T) UP (DIVE 2) (REWRITE MEMBER-UP-LINKS) (DROP 2 4) (DIVE 2) (DIVE 1) (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT (CAR TREE)))) TOP PROVE PROVE PROVE PROVE))) (prove-lemma others-preserve-up-to-root-full (rewrite) (implies (and (treep tree) (listp (channel (cons child (car tree)) old)) (member child (children (car tree) tree)) (member statement (tree-prg tree)) (not (equal statement (list 'root-receive-report (car tree) (cons child (car tree))))) (n old new statement)) (listp (cdr (assoc (cons child (car tree)) new)))) ((INSTRUCTIONS PROMOTE (CLAIM (AND (NUMBERP CHILD) (NUMBERP (CAR TREE))) 0) (BASH T (DISABLE TREE-PRG MIN ZEROP PARENT CHILDREN NODES)) PROMOTE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS 'STATUS W) (CONS (CONS 'FOUND-VALUE W) (CONS (CONS 'OUTSTANDING W) (RFP W (CHILDREN W (CONS W Z))))))))) TOP S (CLAIM (NOT (EQUAL W CHILD)) 0) (DROP 1 2 3 4 5 6 7 8 9 10 11) (PROVE (DISABLE CHILDREN)) (CONTRADICT 14) (DROP 4 6 7 8 9 10 11) PROVE PROMOTE (CLAIM (AND (EQUAL D CHILD) (EQUAL X (PARENT D (CONS X Z)))) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT D (CONS X Z)) D) (CONS (CONS D (PARENT D (CONS X Z))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN D (CONS X Z))))))))))) TOP S (DROP 4 7 8 9 10 11 12 13 14 15) (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DIVE 1) S (REWRITE PARENT-NOT-GRANDCHILD) TOP S X (DEMOTE 1 2) DROP PROVE (DEMOTE 6) S PROMOTE (CONTRADICT 7) (DEMOTE 1 2) DROP PROVE PROMOTE (DIVE 1) (DIVE 1) (CLAIM (EQUAL D CHILD) 0) (CLAIM (EQUAL X (PARENT D (CONS X Z))) 0) (DIVE 1) (DIVE 1) = UP (DIVE 2) = UP UP UP = TOP S TOP (CONTRADICT 18) (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DIVE 1) = TOP (DEMOTE 5) S (CLAIM (NOT (EQUAL D X)) 0) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT D (CONS X Z)) D) (CONS (CONS D (PARENT D (CONS X Z))) (CONS (CONS 'STATUS D) (CONS (CONS 'FOUND-VALUE D) (CONS (CONS 'OUTSTANDING D) (RFP D (CHILDREN D (CONS X Z))))))))))) TOP S (DROP 4 7 8 9 10 11 12 13 14) (PROVE (DISABLE NODES CHILDREN PARENT)) TOP (CONTRADICT 18) (DEMOTE 1 6) DROP PROVE PROMOTE (CLAIM (EQUAL D CHILD) 0) (CLAIM (EQUAL X (PARENT D (CONS X Z))) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP (DIVE 2) = UP UP UP = TOP S (CONTRADICT 18) (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DIVE 1) = TOP (DEMOTE 5) S (CLAIM (NOT (EQUAL C CHILD)) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS C D) (CONS D (PARENT D (CONS X Z))) (CONS 'OUTSTANDING D) (CONS 'FOUND-VALUE D))))) TOP S (DROP 5 8 9 10 11 12 13 14) (PROVE (DISABLE CHILDREN PARENT NODES)) (CLAIM (EQUAL D X) 0) (CONTRADICT 6) (DIVE 1) (DIVE 1) = TOP (DEMOTE 1) DROP PROVE (CONTRADICT 19) (DIVE 1) (= * (PARENT CHILD (CONS X Z)) 0) TOP (DIVE 1) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DEMOTE 5) S (DIVE 2) S (DIVE 1) (DIVE 2) = UP (REWRITE PARENT-OF-CHILD (($PARENT D))) TOP S X (DEMOTE 1) S (DEMOTE 7) S PROMOTE (CLAIM (EQUAL D CHILD) 0) (CLAIM (EQUAL (PARENT D (CONS X Z)) X) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP (DIVE 2) = TOP (DIVE 1) = TOP S (CONTRADICT 18) (DIVE 1) (DIVE 1) = UP S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DEMOTE 5) S (CLAIM (EQUAL C CHILD) 0) (CONTRADICT 6) (DIVE 1) (DIVE 1) (= * X 0) TOP (DEMOTE 1) DROP PROVE (DIVE 1) (= * (PARENT CHILD (CONS X Z)) 0) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DEMOTE 5) S (DIVE 2) (DIVE 1) = UP S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT D))) TOP S X (DEMOTE 1) S (DEMOTE 7) S (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS C D) (CONS D (PARENT D (CONS X Z))) (CONS 'OUTSTANDING D) (CONS 'FOUND-VALUE D))))) TOP S (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14) PROVE PROMOTE (CLAIM (EQUAL C CHILD) 0) (CONTRADICT 17) (DROP 4 8 9 10 11 12 13 14 17) (BASH T) PROMOTE (CONTRADICT 8) (DIVE 1) (REWRITE PARENT-REC-CHILDREN-REC) TOP PROVE (CLAIM (EQUAL D CHILD) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP (DIVE 2) (= * (PARENT D (CONS X Z)) 0) UP UP UP = TOP S (DIVE 2) (DIVE 1) = UP S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DEMOTE 5) S (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS C D) (CONS D (PARENT D (CONS X Z))) (CONS 'OUTSTANDING D) (CONS 'FOUND-VALUE D))))) TOP S (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14) (PROVE (DISABLE PARENT)) PROMOTE (CLAIM (EQUAL C CHILD) 0) (DROP 4 8 9 10 11 12 13 14) (DEMOTE 6) (DIVE 1) S (REWRITE PARENT-REC-CHILDREN-REC) TOP (BASH T) (CLAIM (EQUAL D CHILD) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP (DIVE 2) (= * (PARENT D (CONS X Z)) 0) UP UP UP = TOP S (DEMOTE 4) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 2) (= * (PARENT D (CONS X Z)) 0) UP (DIVE 1) = TOP S (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DIVE 1) = TOP (DEMOTE 4) S (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT X))) TOP S X (DEMOTE 1) S (DIVE 1) = TOP (DEMOTE 5) S (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS C D) (CONS D (PARENT D (CONS X Z))) (CONS 'OUTSTANDING D) (CONS 'FOUND-VALUE D))))) TOP S (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14) PROVE (CONTRADICT 7) (DROP 2 4 5 6 7) PROVE))) (prove-lemma receive-find-decreases-tou (rewrite) (implies (and (treep tree) (listp (channel (cons (parent node tree) node) old)) (member 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)) ((INSTRUCTIONS PROMOTE (CLAIM (AND (EQUAL (STATUS NODE OLD) 'NOT-STARTED) (EQUAL (HEAD (CONS (PARENT NODE TREE) NODE) OLD) 'FIND)) 0) (DROP 5) (PROVE (DISABLE CHILDREN PARENT NODES)) (CONTRADICT 6) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (DOWN-LINK (CONS (PARENT NODE TREE) NODE)) (STATE OLD))) (DEMOTE 7) (DIVE 1) (DIVE 1) (= * T 0) (DROP 1 3 4 5 6) TOP DEMOTE (PROVE (DISABLE PARENT NODES)) S SPLIT (DROP 2 4 5 6 7) (REWRITE MEMBER-DOWN-LINKS) (DIVE 2) (DIVE 1) S (REWRITE PARENT-REC-CHILDREN-REC) TOP S (CLAIM (MEMBER NODE (NODES-REC 'TREE TREE))) (DIVE 1) (REWRITE NODE-HAS-PARENT) TOP S (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE PROVE PROVE PROVE PROVE PROVE))) (prove-lemma others-preserve-down-to-node-full (rewrite) (implies (and (treep tree) (listp (channel (cons (parent node tree) node) old)) (member node (cdr (nodes tree))) (member statement (tree-prg tree)) (not (equal 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)))) ((INSTRUCTIONS PROMOTE (CLAIM (AND (NUMBERP NODE) (NUMBERP (PARENT NODE TREE))) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) (= (PARENT NODE TREE)) TOP (BASH T (DISABLE TREE-PRG MIN ZEROP PARENT CHILDREN NODES)) PROMOTE (CLAIM (EQUAL (PARENT NODE (CONS X Z)) X) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP UP (REWRITE SEND-FIND-GENERAL (($OLD OLD) ($CHANNELS (RFP X (CHILDREN X (CONS X Z)))))) TOP S (REWRITE MEMBER-RFP) S (DIVE 2) (DIVE 2) = TOP (REWRITE PARENT-REC-CHILDREN-REC) (DROP 3 4 6 8 9 10 11 12 13 14 15) PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS 'STATUS X) (CONS (CONS 'FOUND-VALUE X) (CONS (CONS 'OUTSTANDING X) (RFP X (CHILDREN X (CONS X Z))))))))) TOP S-PROP (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13) (PROVE (DISABLE PARENT CHILDREN)) PROMOTE (CLAIM (EQUAL V NODE) 0) (CONTRADICT 9) (= V NODE) S (CLAIM (EQUAL V (PARENT NODE TREE)) 0) (CLAIM (MEMBER NODE (CHILDREN V TREE)) 0) (DIVE 1) (DIVE 1) (DIVE 1) (DIVE 1) = UP UP (REWRITE SEND-FIND-GENERAL (($OLD OLD) ($CHANNELS (RFP V (CHILDREN V TREE))))) TOP S (REWRITE MEMBER-RFP) S (DEMOTE 22) S (CONTRADICT 22) S (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 1) = TOP S (DROP 3 4 6 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22) PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DROP 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18) (PROVE (DISABLE CHILDREN PARENT)) PROMOTE (CLAIM (EQUAL V NODE) 0) (CONTRADICT 9) (DIVE 1) (DIVE 1) = TOP S-PROP (CLAIM (EQUAL V (PARENT NODE TREE)) 0) (DIVE 1) (DIVE 1) (REWRITE SEND-FIND-GENERAL (($OLD OLD) ($CHANNELS (RFP V (CHILDREN V TREE))))) TOP S (DIVE 1) (DIVE 1) = TOP (REWRITE MEMBER-RFP) S (DIVE 2) (DIVE 2) = TOP (REWRITE PARENT-REC-CHILDREN-REC) (DROP 3 4 6 8 9 10 11 12 13 14 15 16 17 18 19 20 21) PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DROP 1 2 3 4 5 6 7 8 10 11 12 13 14 15 16 17 18) (PROVE (DISABLE PARENT CHILDREN)) PROMOTE (CLAIM (EQUAL NODE (PARENT V TREE)) 0) (CLAIM (EQUAL V (PARENT NODE TREE)) 0) (CONTRADICT 21) (DIVE 1) (DIVE 2) (DIVE 1) = TOP (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S (DEMOTE 1 2) DROP PROVE (REWRITE LISTP-PARENT-REC-EQUALS) (DEMOTE 1 2 5 8) DROP PROVE (DEMOTE 1 2) DROP PROVE (DROP 3 4 6 8 9 10 11 12 13 14 15 16 17 18 19 21) PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DROP 1 2 3 4 5 6 7 8 10 11 12 13 14 15 16 17 18) (PROVE (DISABLE PARENT CHILDREN)) (CLAIM (EQUAL V (PARENT NODE TREE)) 0) (DIVE 1) (DIVE 1) (REWRITE SEND-FIND-GENERAL (($OLD OLD) ($CHANNELS (RFP V (CHILDREN V TREE))))) TOP S (REWRITE MEMBER-RFP) S (DIVE 1) (DIVE 2) = TOP S (DIVE 2) (DIVE 2) = TOP (REWRITE PARENT-REC-CHILDREN-REC) (DEMOTE 1 2 5 7) DROP PROMOTE (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) TOP PROVE PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DEMOTE 9 19 20 21) DROP (PROVE (DISABLE PARENT CHILDREN)) PROMOTE (CLAIM (AND (NOT (EQUAL V NODE)) (NOT (MEMBER NODE (CHILDREN V TREE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DEMOTE 9 18 19 20 21) DROP (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 19) (DEMOTE 1 2 5 7 8 9 15 18) DROP (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DROP 6 7 8) (DIVE 1) (DIVE 1) S UP (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE PROVE PROVE PROMOTE (DEMOTE 6) (DIVE 1) (DIVE 1) (DIVE 1) X-DUMB TOP DROP (PROVE (DISABLE CHILDREN)) PROMOTE (CLAIM (AND (NOT (MEMBER NODE (CHILDREN V TREE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DEMOTE 9 18 19 20) DROP (PROVE (DISABLE PARENT CHILDREN)) (CONTRADICT 19) (DEMOTE 1 2 5 7 8 15) DROP PROMOTE SPLIT (DEMOTE 6) (DIVE 1) (DIVE 1) (DIVE 1) X-DUMB TOP DROP (PROVE (DISABLE CHILDREN)) (DROP 6) (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE PROVE PROVE PROMOTE (CLAIM (AND (NOT (MEMBER NODE (CHILDREN V TREE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V TREE) V) (CONS (CONS V (PARENT V TREE)) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V TREE)))))))))) TOP S-PROP (DEMOTE 9 18 19 20) DROP (PROVE (DISABLE PARENT CHILDREN)) (CONTRADICT 19) (DEMOTE 1 2 5 7 8 9 15) DROP PROMOTE SPLIT (DEMOTE 7) (DIVE 1) (DIVE 1) (DIVE 1) X-DUMB TOP DROP (PROVE (DISABLE CHILDREN)) (DROP 7) (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE PROVE PROVE PROMOTE (CLAIM (AND (NOT (EQUAL (CONS W V) (CONS (PARENT NODE TREE) NODE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V TREE)) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DEMOTE 17 18 19) DROP (PROVE (DISABLE CHILDREN PARENT)) (CONTRADICT 18) (DEMOTE 1 2 5 7 8 9) DROP PROMOTE (BASH T (DISABLE PARENT CHILDREN)) PROMOTE (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S PROVE PROVE PROVE PROMOTE (DIVE 1) S (REWRITE PARENT-IS-NOT-CHILD) TOP S PROVE PROVE PROMOTE (CLAIM (AND (NOT (EQUAL (CONS (PARENT NODE TREE) NODE) (CONS W V))) (NOT (EQUAL (CONS (PARENT NODE TREE) NODE) (CONS V (PARENT V TREE))))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V TREE)) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DEMOTE 17 18 19) DROP (PROVE (DISABLE PARENT)) (CONTRADICT 18) (DEMOTE 1 2 5 7 8 9) DROP (BASH T) PROMOTE (DIVE 1) (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S X (BASH T) PROVE PROMOTE (DIVE 1) (REWRITE PARENT-IS-NOT-CHILD) TOP S X PROVE PROMOTE (CLAIM (AND (NOT (EQUAL (CONS W V) (CONS (PARENT NODE TREE) NODE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V TREE)) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DEMOTE 17 18 19) DROP (PROVE (DISABLE PARENT)) (CONTRADICT 18) (DEMOTE 1 2 5 7 8 9) DROP (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S (DROP 4 5 6) PROVE PROVE PROVE (BASH T) PROMOTE (DIVE 1) (REWRITE PARENT-IS-NOT-CHILD) TOP S (DROP 4) PROVE PROVE PROMOTE (CLAIM (AND (NOT (EQUAL (CONS W V) (CONS (PARENT NODE TREE) NODE))) (NOT (EQUAL (CONS V (PARENT V TREE)) (CONS (PARENT NODE TREE) NODE)))) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V TREE)) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DEMOTE 17 18 19) DROP (PROVE (DISABLE PARENT)) (CONTRADICT 18) (DEMOTE 1 2 5 7 8 9) DROP (BASH T (DISABLE PARENT CHILDREN NODES)) PROMOTE (DIVE 1) S (REWRITE PARENT-OF-PARENT-NOT-NODE) TOP S (DROP 4 5 6) PROVE PROVE PROVE (BASH T) PROMOTE (DIVE 1) (REWRITE PARENT-IS-NOT-CHILD) TOP S (DROP 4) PROVE PROVE PROMOTE (CLAIM (NOT (EQUAL NODE X)) 0) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W X) (CONS 'OUTSTANDING X) (CONS 'FOUND-VALUE X))))) TOP S-PROP (DEMOTE 14 15) DROP (PROVE (DISABLE PARENT)) (CONTRADICT 15) (DEMOTE 1 2 5 7) DROP PROVE (CONTRADICT 7) (DROP 2 5 6 7) PROVE))) (prove-lemma receive-report-decreases-tou (rewrite) (implies (and (treep tree) (listp (channel (cons child node) old)) (member node (cdr (nodes tree))) (member 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)) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL (STATUS NODE OLD) 'STARTED) 0) (CLAIM (EQUAL (STATUS NODE NEW) 'STARTED) 0) (CLAIM (NOT (ZEROP (OUTSTANDING NODE OLD))) 0) (DROP 1 3 4 6) (PROVE (DISABLE CHANGED MIN)) (CONTRADICT 9) S (DIVE 1) (DIVE 1) (REWRITE NO-IMPLIES-INSTANCE-OF-NO (($NODES (NODES TREE)) ($TREE TREE))) TOP (USE-LEMMA NUMBER-NOT-REPORTED-0-IMPLIES ((CHILDREN (CHILDREN NODE TREE)) (PARENT NODE) (NODE CHILD) (STATE OLD))) (DIVE 3) (DIVE 1) (REWRITE NO-IMPLIES-INSTANCE-OF-NO (($NODES (NODES TREE)) ($TREE TREE))) TOP (DROP 1 3 5 6 7 8 9) (DIVE 1) (DIVE 1) (DIVE 1) (= (CHILDREN NODE TREE)) TOP (PROVE (DISABLE CHILDREN)) (DEMOTE 6) S (DROP 2 4 5 6 7 8 9 10) PROVE (DEMOTE 6) S (DROP 2 4 5 6 7 8 9) PROVE (CONTRADICT 8) (DROP 6 8) (DIVE 1) S (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS CHILD NODE) (CONS NODE (PARENT NODE TREE)) (CONS 'OUTSTANDING NODE) (CONS 'FOUND-VALUE NODE))))) TOP (DEMOTE 6) S (DROP 1 3 4 6) (PROVE (DISABLE ZEROP MIN)) (DROP 2 5 6) PROVE (CONTRADICT 7) (DEMOTE 6) (DIVE 1) X-DUMB TOP PROMOTE (DROP 5 6 9) (USE-LEMMA UL-IMPLIES-INSTANCE-OF-UL ((UPLINKS (UP-LINKS (CDR (NODES TREE)) TREE)) (UPLINK (CONS CHILD NODE)) (STATE OLD))) (USE-LEMMA DL-IMPLIES-INSTANCE-OF-DL ((DOWN-LINKS (DOWN-LINKS (NODES TREE) TREE)) (STATE OLD) (DOWN-LINK (CONS NODE CHILD)))) (DEMOTE 8) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DEMOTE 7) (DIVE 1) (DIVE 1) S-PROP (= * T 0) TOP (DROP 1 3 4 5 6) PROVE S (REWRITE MEMBER-UP-LINKS) (DIVE 2) (DIVE 1) (DIVE 2) S (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT NODE))) TOP (DROP 5 6) PROVE (DEMOTE 1) S (DEMOTE 1) S (DEMOTE 4) S S (REWRITE MEMBER-DOWN-LINKS) (DROP 2 5 6 7) PROVE))) (prove-lemma others-preserve-up-to-node-full (rewrite) (implies (and (treep tree) (listp (channel (cons child node) old)) (member node (cdr (nodes tree))) (member child (children node tree)) (not (equal statement (list 'receive-report node (cons child node) (cons node (parent node tree))))) (member statement (tree-prg tree)) (n old new statement)) (listp (cdr (assoc (cons child node) new)))) ((INSTRUCTIONS PROMOTE (CLAIM (MEMBER CHILD (CDR (NODES TREE))) 0) (CLAIM (EQUAL NODE (PARENT CHILD TREE)) 0) (DEMOTE 1 2 3 4 5 6 7 8) (= NODE (PARENT CHILD TREE)) DROP PROMOTE (CLAIM (AND (NUMBERP CHILD) (NUMBERP (PARENT CHILD TREE)) (NOT (EQUAL CHILD (CAR TREE))) (NOT (EQUAL (PARENT CHILD TREE) (CAR TREE))) (NUMBERP (PARENT (PARENT CHILD TREE) TREE))) 0) (BASH T (DISABLE TREE-PRG MIN ZEROP PARENT CHILDREN NODES)) PROMOTE (CLAIM (EQUAL V CHILD) 0) (DEMOTE 6 17 22) DROP PROVE (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V (CONS X Z)) V) (CONS (CONS V (PARENT V (CONS X Z))) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V (CONS X Z))))))))))) TOP S-PROP (DROP 6 10 11 12 13 14 15 16 17 18) (BASH T) PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (CONS (CONS (PARENT V (CONS X Z)) V) (CONS (CONS V (PARENT V (CONS X Z))) (CONS (CONS 'STATUS V) (CONS (CONS 'FOUND-VALUE V) (CONS (CONS 'OUTSTANDING V) (RFP V (CHILDREN V (CONS X Z))))))))))) TOP S-PROP (DROP 6 10 11 12 13 14 15 16 17) PROVE PROMOTE (CLAIM (EQUAL CHILD V) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (PROVE (DISABLE PARENT CHILDREN NODES)) PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (AND (NUMBERP X) (NUMBERP CHILD)) 0) (BASH T (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (CLAIM (NUMBERP CHILD) 0) (DROP 6 12 13 14 15 16 17 18) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 23) (DROP 6 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE CHILDREN NODES PARENT)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE CHILDREN PARENT NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (CLAIM (NUMBERP CHILD) 0) (DROP 6 12 13 14 15 16 17 18) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 23) (DROP 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23) PROVE PROMOTE (CLAIM (EQUAL V CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (DIVE 1) (DIVE 1) (REWRITE ABOUT-UC (($B OLD) ($EXCPT (LIST (CONS W V) (CONS V (PARENT V (CONS X Z))) (CONS 'OUTSTANDING V) (CONS 'FOUND-VALUE V))))) TOP S-PROP (DROP 6 12 13 14 15 16 17 18) (CLAIM (NUMBERP CHILD) 0) (PROVE (DISABLE PARENT CHILDREN NODES)) (CONTRADICT 15) (DROP 8 9 10 11 12 13 14 15) PROVE (CONTRADICT 9) (DROP 2 5 6 7 9) PROVE (CONTRADICT 9) (DROP 2 5 6 7 9) PROVE (CONTRADICT 8) (DROP 2 5 6 7 8) PROVE))) (disable total-outstanding-decreases) (disable tou) (disable total-outstanding-decreases-sublist) (disable status-root-becomes-started-or-unchanged) (disable not-total-outstanding-0-implies-full-channel) (disable not-all-empty-implies-full-channel-full) (disable full-channel) (disable all-empty-root-started-implies-total-outstanding-0) (disable all-done-implies-total-outstanding-0) (disable all-nodes-are-done) (disable children-are-suffix-of-sublist-generalized) (disable child-of-node-in-suffix-is-in-suffix) (disable sublist-ulnks) (disable all-empty-implies-all-empty-sublist) (disable all-done-and-all-empty-implies-number-not-reported-0) (disable ulnks) (disable all-done-implies-all-done-sublist) (disable all-done-implies-done) (disable all-done) (disable later-positions-are-in-suffix) (disable setp-list-setp-suffix) (disable childs-position-increases) (disable member-suffix-member-list) (disable suffix-implies-suffix-cdr) (disable suffix) (disable dl-and-all-empty-implies-root-defines-status) (disable parent-to-root-induction) (disable parents-position-decreases) (disable position-append) (disable total-outstanding-non-increasing) (disable total-outstanding-non-increasing-sublist) (disable outstanding-non-increasing) (disable dl-ul-no-preserves-no-sublist) (disable dl-ul-no-preserves-instance-of-no) (disable receive-report-preserves-instance-of-no) (disable child-member-cdr-nodes) (disable receive-report-preserves-no-for-parent) (disable receive-report-preserves-no-for-node) (disable receive-report-preserves-no-for-rest-of-tree) (disable receive-find-preserves-instance-of-no) (disable dl-down-links-implies-dl-rfp) (disable down-links-1-rfp) (disable dl-of-append) (disable receive-find-preserves-no-for-parent-of-node) (disable receive-find-preserves-no-for-node) (disable receive-find-preserves-no-for-rest-of-tree) (disable root-receive-report-preserves-instance-of-no) (disable setp-nodes-setp-children) (disable setp-nodes-implies-setp-roots) (disable number-not-reported-of-root) (disable number-not-reported-of-non-root) (disable min-of-reported-of-non-root) (disable update-min-of-reported) (disable min-of-reported-of-min) (disable min-commutative-1) (disable min-associative) (disable min-commutative) (disable start-preserves-instance-of-no) (disable length-rfp) (disable start-preserves-no-for-rest-of-tree) (disable unchanged-preserves-no) (disable start-preserves-no-for-parent) (disable parent-not-started-implies-all-empty-and-not-started) (disable dl-ul-no-preserves-ul) (disable dl-ul-no-preserves-ul-sublist) (disable dl-ul-no-preserves-instance-of-ul) (disable zero-not-reported-implies-children-reported) (disable member-up-links) (disable dl-preserves-dl) (disable dl-preserves-sublist) (disable dl-preserves-instance-of-dl) (disable all-numberps-nodes-implies-all-numberps-children) (disable all-numberps-forest-implies-all-numberps-roots) (disable parent-not-litatom) (disable all-numberps-nodes-implies-all-numberps-car-parent) (disable all-numberps-nodes-implies-all-numberps-parent) (disable all-numberps-append) (disable send-find-general) (disable assoc-equal-cons) (disable send-find-implies) (disable member-rfp) (disable parent-of-parent-not-node) (disable parent-not-grandchild) (disable parent-not-child) (disable member-down-links) (disable member-down-links-1) (disable ul-implies-instance-of-ul-not-empty-uplink) (disable no-implies-instance-of-no) (disable ul-implies-instance-of-ul) (disable dl-implies-instance-of-dl) (disable inv-implies-augmented-correctness-condition) (disable initial-conditions-imply-invariant) (disable all-empty-not-started-implies-dl) (disable inv) (disable dl) (disable node-values-constant-invariant) (disable node-values-constant-unless-sufficient) (disable listp-tree-prg) (disable root-receive-report-prg-is-total) (disable start-prg-is-total) (disable receive-report-prg-is-total) (disable receive-find-prg-is-total) (disable root-receive-report-func-implements-root-receive-report) (disable root-receive-report-func) (disable start-func-implements-start) (disable start-func) (disable receive-report-func-implements-receive-report) (disable receive-report-func) (disable receive-find-func-implements-receive-find) (disable uc-of-send-find-func) (disable to-node-not-in-rfp) (disable parent-not-in-rfp) (disable about-rfp-numberp) (disable about-rfp) (disable assoc-of-send-find-func) (disable send-find-of-update-assoc) (disable children-are-not-litatoms-member) (disable children-are-not-litatoms) (disable parent-is-not-a-litatom) (disable nodes-are-not-litatoms) (disable send-find-func-implements-send-find) (disable receive-find-func) (disable send-find-func) (disable no-at-termination) (disable found-value-min-value-generalized) (disable min-of-two-nodes-values) (disable proper-tree-tree-implies-nodes-exists) (disable number-not-reported-0-implies) (disable total-outstanding-0-implies) (disable no-implies) (disable found-value-node-value-append) (disable nati) (disable found-value-node-value) (disable down-links-is-sublistp) (disable children-of-non-node) (disable sublistp-down-links-1) (disable sublistp-not-started) (disable nodes-in-down-links-in-nodes) (disable nodes-in-channels-append) (disable nodes-in-down-links-1-in-nodes) (disable not-started-implies-no) (disable nodes-in-channels) (disable all-empty-implies-ul) (disable all-empty-append) (disable not-started-implies-not-started) (disable all-empty-implies-empty) (disable correct) (disable min-node-value) (disable all-empty) (disable all-channels) (disable not-started) (disable up-links) (disable down-links) (disable down-links-1) (disable no) (disable min-of-reported) (disable number-not-reported) (disable reported) (disable ul) (disable done) (disable total-outstanding) (disable treep) (disable member-tree-prg) (disable equal-if) (disable tree-prg) (disable member-root-receive-report-prg) (disable root-receive-report-prg) (disable member-rrrp) (disable rrrp) (disable member-start-prg) (disable start-prg) (disable member-receive-report-prg) (disable receive-report-prg) (disable member-rrp) (disable rrp) (disable member-receive-find-prg) (disable receive-find-prg) (disable rfp) (disable root-receive-report) (disable start) (disable receive-report) (disable min) (disable receive-find) (disable send-find) (disable node-value) (disable outstanding) (disable found-value) (disable status) (disable receive) (disable send) (disable head) (disable empty) (disable channel) (disable value) (disable parent-not-in-children) (disable parent-is-not-child) (disable listp-parent-rec-equals) (disable parent-is-not-itself) (disable parent-is-not-itself-generalized) (disable node-has-parent) (disable children-of-setp-tree) (disable member-subtree-member-tree) (disable no-children-in-rest-of-tree) (disable no-children-in-rest-of-forest) (disable not-member-no-children) (disable not-member-subtrees) (disable proper-tree-next-level-of-proper-tree) (disable proper-tree-of-append) (disable next-level-of-subtrees-in-complete-subtrees) (disable next-level-in-subtrees-forest) (disable subtrees-of-subtrees-in-complete-subtrees) (disable subtrees-of-subtree-in-complete-subtrees) (disable next-level-of-tree-in-subtrees) (disable next-level-reduces-count) (disable nodes-rec-forest-append) (disable next-level) (disable subtreep-subtrees) (disable subtrees) (disable subtreep) (disable sublistp-children) (disable sublistp-children-generalized) (disable node-that-has-parent-is-in-tree) (disable node-that-has-child-is-in-tree) (disable member-parent-member-tree) (disable parent-of-child) (disable member-parent-parent) (disable member-child-tree) (disable not-member-no-parent) (disable plistp-roots) (disable plistp-parent-rec) (disable plistp-children-rec) (disable member-roots-member-forest) (disable parent-rec-children-rec) (disable not-flag-tree) (disable canonicalize-children-rec-flag) (disable canonicalize-parent-rec-flag) (disable canonicalize-proper-tree-flag) (disable canonicalize-nodes-rec-flag) (disable proper-tree) (disable parent) (disable parent-rec) (disable children) (disable children-rec) (disable roots) (disable nodes) (disable nodes-rec) (disable sublistp-in-cons) (disable sublistp-in-append) (disable sublistp-reflexive) (disable sublistp-easy) (disable sei) (disable sublistp-normalize) (disable sublistp-of-sublistp-is-sublistp) (disable member-of-sublistp-is-member) (disable sublistp-append) (disable sublistp) (disable setp-member-2) (disable setp-member-1) (disable setp-append-canonicalize) (disable setp-append-not-listp) (disable setp-append-cons) (disable setp-member) (disable setp-append) (disable setp) (disable all-numberps-implies) (disable all-numberps) (disable not-lessp-count-append) (disable append-plistp-nil) (disable plistp-append-plistp) (disable plistp) (disable length-append) (disable listp-append) (disable car-append) (disable n) (prove-lemma member-cdr-nodes-member-nodes (rewrite) (implies (and (member node (cdr (nodes tree))) (treep tree)) (member node (nodes tree))) ((enable treep proper-tree))) (prove-lemma total-outstanding-decreases-expanded (rewrite) (implies (and (treep tree) (inv tree old) (n old new statement) (member statement (tree-prg tree)) (member node (nodes tree)) (tou old new node tree)) (and (equal (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old)) t) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old)))) ((enable inv) (use (total-outstanding-decreases)))) (prove-lemma total-outstanding-decreases-expanded-count (rewrite) (implies (and (treep tree) (inv tree old) (n old new statement) (member statement (tree-prg tree)) (member node (nodes tree)) (tou old new node tree) (equal (total-outstanding (nodes tree) tree old) (add1 count))) (and (equal (lessp (total-outstanding (nodes tree) tree new) (add1 count)) t) (lessp (total-outstanding (nodes tree) tree new) (add1 count))))) (prove-lemma total-outstanding-non-increasing-expanded (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement) (inv tree old)) (and (equal (lessp (total-outstanding (nodes tree) tree old) (total-outstanding (nodes tree) tree new)) f) (not (lessp (total-outstanding (nodes tree) tree old) (total-outstanding (nodes tree) tree new))))) ((enable inv) (use (total-outstanding-non-increasing)))) (prove-lemma total-outstanding-non-increasing-expanded-count (rewrite) (implies (and (treep tree) (member statement (tree-prg tree)) (n old new statement) (inv tree old) (equal (total-outstanding (nodes tree) tree old) (add1 count))) (and (equal (lessp (add1 count) (total-outstanding (nodes tree) tree old)) f) (not (lessp (add1 count) (total-outstanding (nodes tree) tree new)))))) (prove-lemma key-statements-member-tree-prg (rewrite) (and (implies (treep tree) (member (list 'start (car tree) (rfp (car tree) (children (car tree) tree))) (tree-prg tree))) (implies (and (treep tree) (member child (children (car tree) tree))) (member (list 'root-receive-report (car tree) (cons child (car tree))) (tree-prg tree))) (implies (and (treep tree) (member node (cdr (nodes tree)))) (member (list 'receive-find node (cons (parent node tree) node) (cons node (parent node tree)) (rfp node (children node tree))) (tree-prg tree))) (implies (and (treep tree) (member node (cdr (nodes tree))) (member child (children node tree))) (member (list 'receive-report node (cons child node) (cons node (parent node tree))) (tree-prg tree)))) ((enable member-tree-prg))) (prove-lemma down-link-full-decreases-total-outstanding-ensures (rewrite) (implies (and (treep tree) (member 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))))) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old))) ((INSTRUCTIONS PROMOTE (REWRITE TOTAL-OUTSTANDING-DECREASES-EXPANDED (($STATEMENT (LIST 'RECEIVE-FIND NODE (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (RFP NODE (CHILDREN NODE TREE)))) ($NODE NODE))) PROVE PROVE PROVE))) (prove-lemma down-link-full-unless (rewrite) (implies (and (treep tree) (member node (cdr (nodes tree))) (listp (channel (cons (parent node tree) node) old)) (member statement (tree-prg tree)) (not (equal 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))) ((INSTRUCTIONS PROMOTE (DIVE 1) (DIVE 1) (DIVE 1) X UP UP X X TOP PROVE))) (prove-lemma down-link-full-decreases-total-outstanding (rewrite) (implies (and (treep tree) (member node (cdr (nodes tree)))) (leads-to `(and (inv (quote ,tree) state) (and (listp (channel (quote ,(cons (parent node tree) node)) state)) (equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))))) `(lessp (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE UNCONDITIONAL-FAIRNESS) (REWRITE HELP-PROVE-UNLESS) (CLAIM (EQUAL (EU (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (LIST 'LISTP (CONS 'CHANNEL (CONS (LIST 'QUOTE (CONS (PARENT NODE TREE) NODE)) '(STATE)))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))) (LIST 'RECEIVE-FIND NODE (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (RFP NODE (CHILDREN NODE TREE)))) 0) PROVE PROVE (REWRITE HELP-PROVE-ENSURES (($STATEMENT (LIST 'RECEIVE-FIND NODE (CONS (PARENT NODE TREE) NODE) (CONS NODE (PARENT NODE TREE)) (RFP NODE (CHILDREN NODE TREE)))))) PROVE PROVE))) (prove-lemma member-car-tree-nodes-tree (rewrite) (implies (treep tree) (member (car tree) (nodes tree))) ((enable treep proper-tree nodes nodes-rec))) (prove-lemma root-up-link-full-decreases-total-outstanding-ensures (rewrite) (implies (and (treep tree) (inv tree old) (member 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))))) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old))) ((INSTRUCTIONS PROMOTE (REWRITE TOTAL-OUTSTANDING-DECREASES-EXPANDED (($STATEMENT (LIST 'ROOT-RECEIVE-REPORT (CAR TREE) (CONS CHILD (CAR TREE)))) ($NODE (CAR TREE)))) PROVE PROVE PROVE))) (prove-lemma root-up-link-full-unless (rewrite) (implies (and (treep tree) (member child (children (car tree) tree)) (listp (channel (cons child (car tree)) old)) (member statement (tree-prg tree)) (not (equal statement (list 'root-receive-report (car tree) (cons child (car tree))))) (n old new statement)) (listp (channel (cons child (car tree)) new))) ((INSTRUCTIONS PROMOTE (DIVE 1) X X TOP PROVE))) (prove-lemma up-link-full-decreases-total-outstanding-ensures (rewrite) (implies (and (treep tree) (inv tree old) (member node (cdr (nodes tree))) (member 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))))) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old))) ((INSTRUCTIONS PROMOTE (REWRITE TOTAL-OUTSTANDING-DECREASES-EXPANDED (($STATEMENT (LIST 'RECEIVE-REPORT NODE (CONS CHILD NODE) (CONS NODE (PARENT NODE TREE)))))) PROVE PROVE PROVE))) (prove-lemma up-link-full-unless (rewrite) (implies (and (treep tree) (member node (cdr (nodes tree))) (member child (children node tree)) (listp (channel (cons child node) old)) (member statement (tree-prg tree)) (not (equal statement (list 'receive-report node (cons child node) (cons node (parent node tree))))) (n old new statement)) (listp (channel (cons child node) new))) ((INSTRUCTIONS PROMOTE (DIVE 1) X X TOP PROVE))) (prove-lemma member-cdr-nodes-equals (rewrite) (implies (and (treep tree) (not (equal node (car tree)))) (equal (member node (nodes tree)) (member node (cdr (nodes tree))))) ((enable treep proper-tree nodes nodes-rec))) (prove-lemma up-link-full-decreases-total-outstanding (rewrite) (implies (and (treep tree) (member node (nodes tree)) (member child (children node tree))) (leads-to `(and (inv (quote ,tree) state) (and (listp (channel (quote ,(cons child node)) state)) (equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))))) `(lessp (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (CLAIM (EQUAL NODE (CAR TREE)) 0) (REWRITE UNCONDITIONAL-FAIRNESS) (REWRITE HELP-PROVE-UNLESS) (CLAIM (EQUAL (EU (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (LIST 'LISTP (CONS 'CHANNEL (CONS (LIST 'QUOTE (CONS CHILD NODE)) '(STATE)))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))) (LIST 'ROOT-RECEIVE-REPORT (CAR TREE) (CONS CHILD (CAR TREE)))) 0) PROVE PROVE (REWRITE HELP-PROVE-ENSURES (($STATEMENT (LIST 'ROOT-RECEIVE-REPORT (CAR TREE) (CONS CHILD (CAR TREE)))))) PROVE PROVE (REWRITE UNCONDITIONAL-FAIRNESS) (REWRITE HELP-PROVE-UNLESS) (CLAIM (EQUAL (EU (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (LIST 'LISTP (CONS 'CHANNEL (CONS (LIST 'QUOTE (CONS CHILD NODE)) '(STATE)))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))) (LIST 'RECEIVE-REPORT NODE (CONS CHILD NODE) (CONS NODE (PARENT NODE TREE)))) 0) PROVE PROVE (REWRITE HELP-PROVE-ENSURES (($STATEMENT (LIST 'RECEIVE-REPORT NODE (CONS CHILD NODE) (CONS NODE (PARENT NODE TREE)))))) PROVE PROVE))) (prove-lemma not-started-root-decreases-total-outstanding-ensures (rewrite) (implies (and (treep tree) (inv tree old) (equal (status (car tree) old) 'not-started) (n old new (list 'start (car tree) (rfp (car tree) (children (car tree) tree))))) (lessp (total-outstanding (nodes tree) tree new) (total-outstanding (nodes tree) tree old))) ((INSTRUCTIONS PROMOTE (REWRITE TOTAL-OUTSTANDING-DECREASES-EXPANDED (($STATEMENT (LIST 'START (CAR TREE) (RFP (CAR TREE) (CHILDREN (CAR TREE) TREE)))) ($NODE (CAR TREE)))) PROVE PROVE PROVE))) (prove-lemma not-started-root-unless (rewrite) (implies (and (treep tree) (equal (status (car tree) old) 'not-started) (member statement (tree-prg tree)) (not (equal statement (list 'start (car tree) (rfp (car tree) (children (car tree) tree))))) (n old new statement)) (equal (status (car tree) new) 'not-started)) ((enable status value))) (prove-lemma not-started-root-decreases-total-outstanding (rewrite) (implies (treep tree) (leads-to `(and (inv (quote ,tree) state) (and (equal (status (quote ,(car tree)) state) 'not-started) (equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))))) `(lessp (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE UNCONDITIONAL-FAIRNESS) (REWRITE HELP-PROVE-UNLESS) (CLAIM (EQUAL (EU (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'EQUAL (CONS (CONS 'STATUS (CONS (LIST 'QUOTE (CAR TREE)) '(STATE))) '('NOT-STARTED))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))) (LIST 'START (CAR TREE) (RFP (CAR TREE) (CHILDREN (CAR TREE) TREE)))) 0) PROVE PROVE (REWRITE HELP-PROVE-ENSURES (($STATEMENT (LIST 'START (CAR TREE) (RFP (CAR TREE) (CHILDREN (CAR TREE) TREE)))))) PROVE PROVE))) (prove-lemma full-channel-not-f-implies (rewrite) (implies (full-channel channels state) (and (member (full-channel channels state) channels) (listp (channel (full-channel channels state) state)))) ((enable full-channel empty channel value))) (prove-lemma total-outstanding-decreases-leads-to (rewrite) (implies (and (treep tree) (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree))) (leads-to `(equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) `(lessp (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'OR (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'AND (LIST 'EQUAL (LIST 'STATUS (LIST 'QUOTE (CAR TREE)) 'STATE) ''NOT-STARTED) (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 COUNT))))) (LIST 'OR (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'AND (LIST 'FULL-CHANNEL (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) 'STATE) (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 COUNT))))) (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'AND (LIST 'FULL-CHANNEL (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) 'STATE) (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 COUNT)))))))))) (CLAIM (EVAL (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'OR (LIST 'EQUAL (LIST 'STATUS (LIST 'QUOTE (CAR TREE)) 'STATE) ''STARTED) (LIST 'EQUAL (LIST 'STATUS (LIST 'QUOTE (CAR TREE)) 'STATE) ''NOT-STARTED))) (S (TREE-PRG TREE) (ILEADS (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))))) 0) (DROP 2) (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (USE-LEMMA NOT-TOTAL-OUTSTANDING-0-IMPLIES-FULL-CHANNEL) (PROVE (ENABLE TREEP PROPER-TREE)) (CONTRADICT 3) (DROP 3) (PROVE (DISABLE EVAL-OR EVAL) (ENABLE INV-IS-INVARIANT)) (REWRITE DISJOIN-LEFT) (REWRITE NOT-STARTED-ROOT-DECREASES-TOTAL-OUTSTANDING) (REWRITE DISJOIN-LEFT) (CLAIM (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))))) 0) (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'AND (LIST 'LISTP (LIST 'CHANNEL (LIST 'QUOTE (CONS (PARENT (CDR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))))) TREE) (CDR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))))))) 'STATE)) (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 COUNT)))))))) (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (DROP 2) BASH PROMOTE (CLAIM (EQUAL (CONS (PARENT (CDR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE)) TREE) (CDR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE))) (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE)) 0) PROVE (CONTRADICT 5) (DROP 4 5) (CLAIM (MEMBER (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE) (DOWN-LINKS (NODES TREE) TREE)) 0) (DEMOTE 4) (DIVE 1) (REWRITE MEMBER-DOWN-LINKS) TOP (DROP 2 3) (CLAIM (EQUAL (PARENT (CDR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE)) TREE) (CAR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE))) 0) PROVE PROMOTE (CONTRADICT 2) (DROP 2) (DIVE 1) X (DIVE 1) (REWRITE PARENT-OF-CHILD (($PARENT (CAR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE))))) TOP S (DEMOTE 1) (DIVE 1) X TOP S (DEMOTE 1) (DIVE 1) X (DIVE 1) (DIVE 1) X TOP S (DEMOTE 2) (DIVE 1) (DIVE 2) (DIVE 1) (DIVE 2) X TOP S (CONTRADICT 4) (REWRITE FULL-CHANNEL-NOT-F-IMPLIES) (REWRITE DOWN-LINK-FULL-DECREASES-TOTAL-OUTSTANDING) (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (DOWN-LINKS (NODES TREE) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (DROP 2) (CLAIM (MEMBER (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE) (DOWN-LINKS (NODES TREE) TREE)) 0) (DEMOTE 3) (DIVE 1) (REWRITE MEMBER-DOWN-LINKS) TOP SPLIT (REWRITE MEMBER-OF-SUBLISTP-IS-MEMBER (($B (CHILDREN (CAR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE)) TREE)))) (REWRITE CHILDREN-ARE-SUFFIX-OF-SUBLIST-GENERALIZED (($TREE TREE) ($NODE (CAR (FULL-CHANNEL (DOWN-LINKS (NODES TREE) TREE) STATE))))) (DEMOTE 1) (DIVE 1) X TOP S (DEMOTE 1) (DIVE 1) X TOP S X (DIVE 1) X TOP (REWRITE SUBLISTP-REFLEXIVE) (CONTRADICT 3) (REWRITE FULL-CHANNEL-NOT-F-IMPLIES) (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P '(FALSE)))) PROVE (REWRITE FALSE-LEADS-TO-ANYTHING) (CLAIM (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT)))))) 0) (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'AND (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (LIST 'AND (LIST 'LISTP (LIST 'CHANNEL (LIST 'QUOTE (CONS (CAR (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))))) (CDR (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) (S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))))))) 'STATE)) (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 COUNT)))))))) (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (DROP 2) BASH PROMOTE (CONTRADICT 5) (DROP 3 4 5) (CLAIM (MEMBER (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) STATE) (UP-LINKS (CDR (NODES TREE)) TREE))) (DEMOTE 3) (DIVE 1) (REWRITE MEMBER-UP-LINKS) TOP S (REWRITE UP-LINK-FULL-DECREASES-TOTAL-OUTSTANDING) (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (DROP 2) (CLAIM (MEMBER (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) STATE) (UP-LINKS (CDR (NODES TREE)) TREE))) (DEMOTE 3) (DIVE 1) (REWRITE MEMBER-UP-LINKS) TOP SPLIT (DIVE 1) = X TOP (DIVE 2) X TOP (REWRITE NODE-HAS-PARENT) (DIVE 2) (= * (NODES TREE) ((ENABLE NODES))) TOP (REWRITE MEMBER-CDR-NODES-MEMBER-NODES) (DEMOTE 1) (DIVE 1) X TOP S S (DIVE 1) (DROP 2 3 4) TOP (DIVE 1) (DIVE 2) (= * (CAR (NODES TREE)) ((ENABLE NODES NODES-REC))) TOP (= (NOT (EQUAL (CAR (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) STATE)) (CAR (NODES TREE))))) (CONTRADICT 2) (DIVE 1) (DIVE 1) = TOP (DEMOTE 1) (DIVE 1) X (DIVE 1) X TOP PROVE (GENERALIZE (((S (TREE-PRG TREE) (ILEADS (LIST 'AND (CONS 'INV (CONS (LIST 'QUOTE TREE) '(STATE))) (LIST 'AND (CONS 'FULL-CHANNEL (CONS (LIST 'QUOTE (UP-LINKS (CDR (NODES TREE)) TREE)) '(STATE))) (LIST 'EQUAL (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))))) STATE))) (DROP 2) (CLAIM (MEMBER (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) STATE) (UP-LINKS (CDR (NODES TREE)) TREE))) (DEMOTE 3) (DIVE 1) (REWRITE MEMBER-UP-LINKS) TOP SPLIT (DIVE 2) (DIVE 1) = X UP X TOP (REWRITE PARENT-REC-CHILDREN-REC) (DIVE 2) (REWRITE SETP-TREE-UNIQUE-PARENT) (DIVE 1) (DIVE 2) (= * (NODES TREE) ((ENABLE NODES))) UP (REWRITE MEMBER-CDR-NODES-MEMBER-NODES) UP S (DIVE 1) (= * F 0) TOP S X (= * (NOT (EQUAL (CAR (NODES TREE)) (CAR (FULL-CHANNEL (UP-LINKS (CDR (NODES TREE)) TREE) STATE)))) ((ENABLE NODES NODES-REC))) (CONTRADICT 5) (DIVE 1) (DIVE 1) = TOP (DEMOTE 1) (DIVE 1) X (DIVE 1) X TOP S (DEMOTE 1) (DIVE 1) X TOP S (DEMOTE 1) (DIVE 1) X (DIVE 1) (DIVE 1) X TOP S (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P '(FALSE)))) PROVE (REWRITE FALSE-LEADS-TO-ANYTHING)))) (prove-lemma termination-induction (rewrite) (implies (and (treep tree) (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree))) (leads-to `(lessp (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) (quote ,(add1 count))) `(equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) 0) (tree-prg tree))) ((INSTRUCTIONS (INDUCT (PLUS COUNT J)) PROMOTE PROMOTE (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (CONS 'EQUAL (CONS (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) '(0)))))) PROVE (REWRITE Q-LEADS-TO-Q) PROMOTE PROMOTE (DEMOTE 2) (DIVE 1) (DIVE 1) S-PROP TOP SPLIT (REWRITE LEADS-TO-TRANSITIVE (($Q (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 (SUB1 COUNT))))))) (DROP 4) (CLAIM (NOT (LESSP (TOTAL-OUTSTANDING (NODES TREE) TREE (S (TREE-PRG TREE) (ILEADS (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 COUNT))) (TREE-PRG TREE) (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 (SUB1 COUNT))))))) (ADD1 (SUB1 COUNT)))) 0) (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 (SUB1 COUNT))))))) (DROP 2 3) PROVE (REWRITE TOTAL-OUTSTANDING-DECREASES-LEADS-TO) (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'LESSP (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) (LIST 'QUOTE (ADD1 (SUB1 COUNT))))))) (DROP 3) PROVE (REWRITE Q-LEADS-TO-Q)))) (prove-lemma termination (rewrite) (implies (and (treep tree) (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree))) (leads-to '(true) `(equal (total-outstanding (quote ,(nodes tree)) (quote ,tree) state) 0) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE LEADS-TO-STRENGTHEN-LEFT (($P (LIST 'LESSP (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) (LIST 'QUOTE (ADD1 (TOTAL-OUTSTANDING (NODES TREE) TREE (S (TREE-PRG TREE) (ILEADS '(TRUE) (TREE-PRG TREE) (CONS 'EQUAL (CONS (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) '(0)))))))))))) PROVE (REWRITE TERMINATION-INDUCTION)))) (prove-lemma correctness-condition (rewrite) (implies (and (treep tree) (initial-condition `(and (all-empty (quote ,(all-channels tree)) state) (not-started (quote ,(nodes tree)) state)) (tree-prg tree))) (leads-to '(true) `(correct (quote ,tree) state) (tree-prg tree))) ((INSTRUCTIONS PROMOTE (REWRITE LEADS-TO-WEAKEN-RIGHT (($Q (LIST 'EQUAL (LIST 'TOTAL-OUTSTANDING (LIST 'QUOTE (NODES TREE)) (LIST 'QUOTE TREE) 'STATE) 0)))) BASH PROMOTE (REWRITE INV-IMPLIES-AUGMENTED-CORRECTNESS-CONDITION) (DEMOTE 1) (DIVE 1) X TOP S (DEMOTE 1) (DIVE 1) X (DIVE 1) (DIVE 1) X TOP S (CLAIM (EVAL (LIST 'INV (LIST 'QUOTE TREE) 'STATE) (S (TREE-PRG TREE) (JLEADS (ILEADS '(TRUE) (TREE-PRG TREE) (CONS 'CORRECT (CONS (LIST 'QUOTE TREE) '(STATE)))) (TREE-PRG TREE) (CONS 'EQUAL (CONS (CONS 'TOTAL-OUTSTANDING (CONS (LIST 'QUOTE (NODES TREE)) (CONS (LIST 'QUOTE TREE) '(STATE)))) '(0)))))) ((DISABLE EVAL) (ENABLE INV-IS-INVARIANT))) PROVE (REWRITE TERMINATION))))