%Patch files loaded: patch2 version 1.2.2.36 $$$pvs-strategies ;;NSH(5.27.95) : From JMR ;;added exclude argument to grind and if-match argument to use. (defstep use (lemma &optional subst (if-match best) (polarity? nil)) (then@ (lemma lemma subst) (if *new-fmla-nums* (let ((fnum (car *new-fmla-nums*))) (then (beta fnum) (repeat (inst? fnum :if-match if-match :polarity? polarity?)))) (skip))) "Introduces lemma LEMMA, then does BETA and INST? (repeatedly) on the lemma." "Using lemma ~a") ;;; ---------------------------------------------------------------------- ;;; Strategies for ttp.pvs ;;; ---------------------------------------------------------------------- ;;; Added :split-fnums argument to 'bash' and 'reduce' in order to pass it to ;;; 'bddsimp'. -hp, 29.11.99 (defstep bash (&optional (if-match T)(updates? T) polarity? (instantiator inst?) (split-fnums *)) (then (assert) (bddsimp :fnums split-fnums) (if if-match (let ((command (generate-instantiator-command if-match polarity? instantiator))) command)(skip)) (repeat (then (skolem-typepred)(flatten))) (lift-if :updates? updates?)) " Core of REDUCE. Does ASSERT, BDDSIMP, INST?, SKOLEM-TYPEPRED, FLATTEN, and LIFT-IF once and in that order. The IF-MATCH option can be NIL, T, ALL, or BEST for no, some, all, or the best instantiation. If the UPDATES? option is NIL, update applications are not if-lifted. When the POLARITY? flag is T, INST? matches templates against complementary subexpressions. The INSTANTIATOR argument can be used to specify use of an alternative instantiation mechanism. This defaults to the (INST?) strategy." "Simplifying with decision procedures, rewriting, propositional reasoning, quantifier instantiation, skolemization, if-lifting.," ) (defstep reduce (&optional (if-match t) (updates? t) polarity? (instantiator inst?) (split-fnums *)) (REPEAT* (TRY (BASH$ :IF-MATCH IF-MATCH :UPDATES? UPDATES? :POLARITY? POLARITY? :INSTANTIATOR INSTANTIATOR :split-fnums split-fnums) (REPLACE*) (SKIP))) "Core of GRIND (ASSERT, BDDSIMP, INST?, SKOLEM-TYPEPRED, FLATTEN, LIFT-IF, i.e., BASH then REPLACE*) without reestablishing all the rewrites. See BASH for more explanation." "Repeatedly simplifying with decision procedures, rewriting, propositional reasoning, quantifier instantiation, skolemization, if-lifting and equality replacement," ) (defstep REW () (then (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES ("the_mem" "faults_latch" "set_prop1a" "set_prop2" "member_remove[proc]" "none_before_current" "before_irreflexive" "CRC1a_char" "CRC1b_char" "CRC2a_char" "CRC2b_char")) (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev")) "TTP: Installs special-purpose rewrites and does some forward chaining" "TTP: Installing rewrites and doing some forward reasoning,") ; ---------------------------------------------------------------------- (defstep lazy-reduce () (TRY (repeat* (THEN (LIFT-IF) (ASSERT) (REPLACE*))) (lazy-reduce) (TRY (BDDSIMP +) (lazy-reduce) (TRY (BDDSIMP) (lazy-reduce) (TRY (APPLY-EXTENSIONALITY :HIDE? T) (THEN (IFF) (lazy-reduce)) (TRY (APPLY-EXTENSIONALITY :HIDE? T :fnum 2) (THEN (IFF) (lazy-reduce)) (TRY (APPLY-EXTENSIONALITY :HIDE? T :fnum 3) (THEN (IFF) (lazy-reduce)) (TRY (APPLY-EXTENSIONALITY :HIDE? T :fnum 4) (THEN (IFF) (lazy-reduce)) (TRY (APPLY-EXTENSIONALITY :HIDE? T :fnum 5) (THEN (IFF) (lazy-reduce)) (TRY (APPLY-EXTENSIONALITY :HIDE? T :fnum 6) (THEN (IFF) (lazy-reduce)) (skip)))))))))) "TTP: Repeatedly applies (THEN (LIFT-IF) (ASSERT) (REPLACE)), (BDDSIMP +), (BDDSIMP), and (APPLY-EXTENSIONALITY). As soon as one of these succeeds, starts from beginning." "" ) ; ---------------------------------------------------------------------- (defstep mem (&optional (term) (split *)) ; version for "real" ttp (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (inst-cp - "broadcaster(t!1)") (if term (inst - term) (inst?)) (rewrite "newmem") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) ; (use "arrival" :polarity? t) ; (if term (use "arrival" :subst ("p" term)) (skip)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "mem strategy" "mem strategy" ) (defstep mem- (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newmem") (assert) (use "fail_silence" :subst ("t" "t!1")) (if term (use "nonarrival" :subst ("p" term "t" "t!1")) (use "nonarrival" :subst ("p" term) :polarity? t)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "mem- strategy" "mem- strategy" ) (defstep prev (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newprev") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "prev strategy" "prev strategy" ) (defstep prev- (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newprev") (assert) (use "fail_silence" :subst ("t" "t!1")) (if term (use "nonarrival" :subst ("p" term "t" "t!1")) (use "nonarrival" :subst ("p" term) :polarity? t)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "prev- strategy" "prev- strategy" ) (defstep doubt (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newdoubt") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "doubt strategy" "doubt strategy" ) (defstep doubt- (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newdoubt") (assert) (use "fail_silence" :subst ("t" "t!1")) (if term (use "nonarrival" :subst ("p" term "t" "t!1")) (use "nonarrival" :subst ("p" term) :polarity? t)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "doubt- strategy" "doubt- strategy" ) (defstep prev-doubt (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newprev") (rewrite "newdoubt") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "prev-doubt strategy" "prev-doubt strategy" ) (defstep rej (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newrejected") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "rej strategy" "rej strategy" ) (defstep acc-rej (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newaccepted") (REWRITE "newrejected") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "acc-rej strategy" "acc-rej strategy" ) (defstep acc-rej- (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newaccepted") (REWRITE "newrejected") (assert) (use "fail_silence" :subst ("t" "t!1")) (if term (use "nonarrival" :subst ("p" term "t" "t!1")) (use "nonarrival" :subst ("p" term) :polarity? t)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "acc-rej strategy" "acc-rej strategy" ) (defstep mysucc (&optional (term) (split *)) (then (FORWARD-CHAIN "faulty_mem") (FORWARD-CHAIN "faults_latch_rev") (INST-CP - "broadcaster(t!1)") (IF term (inst - term) (inst?)) (REWRITE "newmy_succ") (assert) (use "sending" :subst ("t" "t!1")) (if term (use "arrival" :subst ("p" term "t" "t!1")) (use "arrival" :subst ("t" "t!1") :polarity? T)) (assert) ; (reduce :split-fnums split)) (lazy-reduce)) "mysucc strategy" "mysucc strategy" ) $$$ttp.pvs % --------------------------------------------------------------------------- % % Group Membership Algorithm of the Time-Triggered Protocol (TTP) % % accompanying paper available at % http://www.informatik.uni-ulm.de/ki/PVS/membership.html % % Author: % Holger Pfeifer Tel.: (+49) 731 / 502-4124 % Universitaet Ulm Fax: (+49) 731 / 502-4119 % Abt. Kuenstliche Intelligenz pfeifer@ki.informatik.uni-ulm.de % D-89069 Ulm http://www.informatik.uni-ulm.de/ki/pfeifer.html % % Acknowledgment: % Several basic lemmas (e.g. about 'before') and the original version % of the proof strategies are due to John Rushby, SRI International. % % --------------------------------------------------------------------------- ttp [n:upfrom(4)] : THEORY BEGIN IMPORTING mod_props time : TYPE+ = nat postime : TYPE+ = posnat proc : TYPE+ = below(n) % -- processors numbered 0 .. n-1 memvec : TYPE+ = [proc -> bool] % -- membership vector p,q,r,a,b, x,y,z,xs : VAR proc S : VAR set[proc] j : VAR postime i,s,t : VAR time v,w : VAR memvec broadcaster(t) : proc = mod(t,n) % -- broadcaster at time t membership(t,p) : memvec % -- membership vector of processor p accepted : [time,proc -> nat] % -- #messages a proc. has accepted rejected : [time,proc -> nat] % -- #messages a proc. has rejected prev(t,p) : bool % -- p was previous active sender doubt(t,p) : bool % -- p is in doubt on whether it's previous % transmission was ok my_succ(t,p) : proc % -- successor of a node that has prev faulty(t,p) : bool % -- p is faulty at time t the_mem(t)(p) : bool = % -- the "global" membership: set of NOT faulty(t,p) % non-faulty processors sends(t,b) : bool % -- broadcaster b sends a message at time t arrives(t,p) : bool % -- message sent at time t arrives at p sending : AXIOM % -- a non-faulty braodcaster will produce LET b = broadcaster(t) IN % some activity on the bus NOT faulty(t,b) AND membership(t,b)(b) IMPLIES sends(t,b) faulty_broadcaster: AXIOM % -- a newly send-faulty broadcaster will LET b = broadcaster(t+1) IN % not be able to send a message NOT faulty(t,b) AND faulty(t+1,b) IMPLIES NOT sends(t+1,b) shutdown : AXIOM % -- the broadcaster has just diagnosed its LET b = broadcaster(t) IN % fault and thus will not send accepted(t,b) <= rejected(t,b) IMPLIES NOT sends(t,b) fail_silence : AXIOM % -- a processor that has diagnosed its LET b = broadcaster(t) IN % fault will not send anymore NOT membership(t,b)(b) IMPLIES NOT sends(t,b) arrival : AXIOM % -- a non-faulty receiver will receive the LET b = broadcaster(t) IN % message sent by the broadcaster sends(t,b) AND NOT faulty(t,p) IMPLIES arrives(t,p) faulty_receiver: AXIOM % -- a newly receive-faulty broadcaster will LET b = broadcaster(t+1) IN % not be able to receive the message NOT faulty(t,p) AND faulty(t+1,p) AND p /= b IMPLIES NOT faulty(t+1,b) AND NOT arrives(t+1,p) nonarrival: AXIOM % -- no generation of spontaneous messages LET b = broadcaster(t) IN NOT sends(t,b) IMPLIES NOT arrives(t,p) all_or_none: COROLLARY NOT faulty(t,p) AND NOT faulty(t,q) IMPLIES arrives(t,p) = arrives(t,q) faults_latch : AXIOM faulty(t,p) => faulty(t+1,p) faults_latch_always : COROLLARY forall i: faulty(t, p) => faulty(t+i,p) faults_latch_rev : COROLLARY NOT faulty(1+t,p) => NOT faulty(t,p) % ---------------------------------------------------------------------- at_least_four_nodes : LEMMA EXISTS p,x,y,z : p /= x AND p /= y AND p /= z AND x /= y AND x /= z AND y /= z at_least_three_nodes : COROLLARY EXISTS x,y,z : x /= y AND y /= z AND z /= x another_node_exists : LEMMA EXISTS y: x /= y three_non_faulty_exist : AXIOM EXISTS x, y, z: NOT faulty(t,x) AND NOT faulty(t,y) AND NOT faulty(t,z) AND x /= y AND x /= z AND y /= z two_non_faulty_exist : COROLLARY EXISTS p, q: NOT faulty(t,p) AND NOT faulty(t,q) AND p /= q non_faulty_exists : COROLLARY EXISTS p: NOT faulty(t,p) two_other_nonfaulty_exist : COROLLARY EXISTS p, q: NOT faulty(t,p) AND NOT faulty(t,q) AND p /= q AND p /= x AND q /= x another_nonfaulty_exists : COROLLARY EXISTS p: NOT faulty(t,p) AND p /= x % -------------------------------------------------------------------------- mono : LEMMA the_mem(t+i) = the_mem(t) AND faulty(t+i,p) => faulty(t,p) mono2 : LEMMA the_mem(i+t) = the_mem(t) AND faulty(i+t,p) => faulty(t,p) faulty_mem : COROLLARY faulty(1+t,p) AND the_mem(1+t) = the_mem(t) => faulty(t,p) faulty_x : LEMMA the_mem(t) = remove(x,v) => faulty(t,x) not_faulty_y : LEMMA the_mem(t) = remove(x,v) AND member(y,v) AND x /= y => NOT faulty(t,y) useful : LEMMA membership(t,x) = the_mem(t) AND membership(t,x)(p) => NOT faulty(t,p) set_prop1 : LEMMA v(x) OR remove(x,add(x,v)) = v set_prop1a : LEMMA NOT v(x) => remove(x,add(x,v)) = v set_prop2 : LEMMA v(x) => add(x,remove(x,v)) = v set_prop_3 : LEMMA remove(x,remove(y,v)) = remove(y,remove(x,v)) % -------------------------------------------------------------------------- % -- x will broadcast before y, at time t or later before(t,x,y) : bool = FORALL i: y = broadcaster(t+i) => EXISTS s: s NOT before(t,x,y) round_prop : LEMMA broadcaster(t) > broadcaster(s) => broadcaster(t) - broadcaster(s) < n cycle : lemma broadcaster(t) = broadcaster(t+j) IFF (EXISTS (i:nat): j=i*n) next_broadcast_slot : COROLLARY x = broadcaster(t) => x = broadcaster(t+n) bcast_prop : lemma broadcaster(t) <= t broadcaster_not_next_broadcaster : LEMMA broadcaster(t) /= broadcaster(t+1) before_prop : LEMMA x = broadcaster(s + broadcaster(x) - broadcaster(s)) before_prop1 : LEMMA x = broadcaster(t - broadcaster(t) + x) before_prop1n : LEMMA LET k = IF x >= broadcaster(t) THEN x - broadcaster(t) ELSE n + x - broadcaster(t) ENDIF IN x = broadcaster(t + k) AND FORALL i: i < k => x /= broadcaster(t+i) next_b_prop : LEMMA EXISTS s: s < n AND x = broadcaster(t + s) AND FORALL i: i x /= broadcaster(t+i) nonfaulty_broadcaster_exists : LEMMA EXISTS s: NOT faulty(t,broadcaster(t+s)) before_prop2 : LEMMA broadcaster(t) = broadcaster(1 + i + t) => i >= n-1 before0 : LEMMA broadcaster(x) - broadcaster(1 + t) = n - 1 => x = broadcaster(t) before0a : LEMMA broadcaster(x) - broadcaster(1+t) = -1 => x=broadcaster(t) % -- main properties of 'before': before1 : LEMMA x /= broadcaster(t) => before(t+1,x, broadcaster(t)) before2 : LEMMA before(t,x,y) => x = broadcaster(t) or before(t+1,x,y) before_previous : LEMMA before(t+1,x,y) AND y /= broadcaster(t) => before(t,x,y) before3 : LEMMA before(t,x,y) => y /= broadcaster(t) before3_rev : LEMMA y /= broadcaster(t) => EXISTS x: before(t,x,y) before_irreflexive : LEMMA NOT before(t,x,x) before_asymmetric : LEMMA before(t,x,y) => NOT before(t,y,x) before_transitive : LEMMA before(t,x,y) AND before(t,y,z) => before(t,x,z) before_total : LEMMA x /= y => before(t,x,y) OR before(t,y,x) not_prev_broadcaster_before : LEMMA NOT before(t+1,broadcaster(t),p) % -- properties of 'before' with faulty processors involved: two_nonfaulty_before_broadcaster_exist : LEMMA EXISTS p,q: NOT faulty(t+1,p) AND NOT faulty(t+1,q) AND p /= q AND before(t+1,p,broadcaster(t)) AND before(t+1,q,broadcaster(t)) nonfaulty_before_broadcaster_exists : COROLLARY EXISTS p: NOT faulty(t+1,p) AND before(t+1,p,broadcaster(t)) another_nonfaulty_before_broadcaster_exists : COROLLARY FORALL z: EXISTS p: NOT faulty(t+1,p) AND p /= z AND before(t+1,p,broadcaster(t)) three_nonfaulty_before_faulty_broadbaster : LEMMA faulty(t, broadcaster(t)) => EXISTS x,y,z: x /= y AND y /= z AND z /= x AND NOT faulty(t+1,x) AND NOT faulty(t+1,y) AND NOT faulty(t+1,z) AND before(t+1,x,broadcaster(t)) AND before(t+1,y,broadcaster(t)) AND before(t+1,z,broadcaster(t)) two_other_nonfaulty_before_faulty_broadcaster : COROLLARY FORALL z: faulty(t,broadcaster(t)) => EXISTS x,y: x /= y AND x /= z AND y /= z AND NOT faulty(t+1,x) AND NOT faulty(t+1,y) AND before(t+1,x,broadcaster(t)) AND before(t+1,y,broadcaster(t)) nonfaulty_before_broadcaster_not_prev_exists : LEMMA before(t,y,z) AND NOT faulty(t,y) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND the_mem(t+1) = the_mem(t) => EXISTS p: p /= z AND NOT faulty(t+1,p) AND before(t+1,p,broadcaster(t)) nonfaulty_before_prev_exists_invariant : LEMMA before(t,y,z) AND NOT faulty(t,y) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND the_mem(t+1) = the_mem(t) => EXISTS p: NOT faulty(t+1,p) AND before(t+1,p,z) all_faulty_after_prev_invariant : LEMMA (FORALL p: before(t,z,p) => faulty(t,p)) => FORALL p: before(t+1,z,p) AND before(t+1,p,broadcaster(t)) => faulty(t+1,p) nonfaulty_before_prev_not_prevprev_exists_invariant : LEMMA (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND faulty(t,broadcaster(t)) AND the_mem(t+1) = the_mem(t) => EXISTS p: p /= y AND NOT faulty(t+1,p) AND before(t+1,p,z) all_faulty_after_prev_faulty_broadcaster_invariant : LEMMA (FORALL p: before(t,z,p) => faulty(t,p)) AND faulty(t,broadcaster(t)) => FORALL p: before(t+1,z,p) => faulty(t+1,p) non_faulty_before_exists_invariant : LEMMA (EXISTS p: NOT faulty(t,p) AND before(t,p,x)) AND faulty(t,broadcaster(t)) AND the_mem(t+1) = the_mem(t) => EXISTS p: NOT faulty(t+1,p) AND before(t+1,p,x) all_faulty_between_prev_and_prevprev_invariant : LEMMA (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND faulty(t, broadcaster(t)) AND NOT faulty(t,z) => FORALL p: before(t+1,y,p) AND before(t+1,p,z) => faulty(t+1,p) % -------------------------------------------------------------------------- CRC(v,w) : bool = % -- CRC check of membership vectors FORALL p: v(p) = w(p) CRC1a(t)(p,b) : bool = LET v = membership(t,p), w = membership(t,b) IN CRC(v WITH [(p) := TRUE, (b) := TRUE], w) CRC1a_char : LEMMA CRC1a(t)(p,b) <=> membership(t,b) = add(p,add(b,membership(t,p))) CRC1a_char2 : COROLLARY CRC1a(t)(p,b) => membership(t,b)(p) CRC1b(t)(p,b) : bool = LET v = membership(t,p), w = membership(t,b) IN CRC(v WITH [(p) := FALSE, (b) := TRUE], w) CRC1b_char : LEMMA CRC1b(t)(p,b) <=> membership(t,b) = add(b,remove(p,membership(t,p))) CRC1b_char2 : COROLLARY p /= b => CRC1b(t)(p,b) => NOT membership(t,b)(p) CRC2a(t)(p,q,b) : bool = % -- set mem(t,p)(b) to TRUE, too. LET u = membership(t,p), v = membership(t,q), w = membership(t,b) IN CRC(u WITH [(p) := TRUE, (q) := FALSE, (b) := TRUE], w) CRC2a_char : LEMMA CRC2a(t)(p,q,b) <=> membership(t,b) = add(b,remove(q,add(p,membership(t,p)))) CRC2a_char2 : COROLLARY p /= q AND q /= b => CRC2a(t)(p,q,b) => membership(t,b)(p) AND NOT membership(t,b)(q) CRC2b(t)(p,q,b) : bool = % -- set mem(t,p)(b) to TRUE, too. LET u = membership(t,p), v = membership(t,q), w = membership(t,b) IN CRC(u WITH [(p) := FALSE, (q) := TRUE, (b) := TRUE], w) CRC2b_char : LEMMA CRC2b(t)(p,q,b) <=> membership(t,b) = add(b,add(q,remove(p,membership(t,p)))) CRC2b_char2 : COROLLARY p /= q AND p /= b => CRC2b(t)(p,q,b) => NOT membership(t,b)(p) AND membership(t,b)(q) % -------------------------------------------------------------------------- algorithm : AXIOM LET b = broadcaster(t) IN IF p = b THEN IF accepted(t,p) <= rejected(t,p) % -- clique avoidance THEN membership(t+1,p) = remove(p,membership(t,p)) ELSE membership(t+1,p) = membership(t,p) ENDIF AND accepted(t+1,p) = 1 AND rejected(t+1,p) = 0 AND prev(t+1,p) = TRUE AND doubt(t+1,p) = doubt(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF NOT membership(t,p)(p) THEN membership(t+1,p) = membership(t,p) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF prev(t,p) AND arrives(t,p) AND CRC1a(t)(p,b) THEN membership(t+1,p) = membership(t,p) AND prev(t+1,p) = FALSE AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) + 1 AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF prev(t,p) AND arrives(t,p) AND CRC1b(t)(p,b) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = FALSE AND doubt(t+1,p) = TRUE AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) + 1 AND my_succ(t+1,p) = b ELSIF prev(t,p) AND sends(t,b) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = TRUE AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) + 1 AND my_succ(t+1,p) = my_succ(t,p) ELSIF prev(t,p) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = TRUE AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF doubt(t,p) AND arrives(t,p) AND CRC2a(t)(p,my_succ(t,p),b) THEN membership(t+1,p) = membership(t,p) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = FALSE AND accepted(t+1,p) = accepted(t,p) + 1 AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF doubt(t,p) AND arrives(t,p) AND CRC2b(t)(p,my_succ(t,p),b) THEN membership(t+1,p) = remove(p,add(my_succ(t,p),membership(t,p))) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = FALSE AND accepted(t+1,p) = accepted(t,p) + 1 AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF doubt(t,p) AND sends(t,b) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) + 1 AND my_succ(t+1,p) = my_succ(t,p) ELSIF doubt(t,p) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF arrives(t,p) AND membership(t,p) = membership(t,b) THEN membership(t+1,p) = membership(t,p) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) + 1 AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSIF NOT sends(t,b) THEN membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) AND my_succ(t+1,p) = my_succ(t,p) ELSE membership(t+1,p) = remove(b,membership(t,p)) AND prev(t+1,p) = prev(t,p) AND doubt(t+1,p) = doubt(t,p) AND accepted(t+1,p) = accepted(t,p) AND rejected(t+1,p) = rejected(t,p) + 1 AND my_succ(t+1,p) = my_succ(t,p) ENDIF % -------------------------------------------------------------------------- newmem : LEMMA membership(t+1,p) = LET b = broadcaster(t) IN IF p = b AND accepted(t,p) > rejected(t,p) THEN membership(t,p) ELSIF p = b THEN remove(p,membership(t,p)) ELSIF NOT membership(t,p)(p) OR (prev(t,p) AND arrives(t,p) AND CRC1a(t)(p,b)) OR (NOT prev(t,p) AND doubt(t,p) AND arrives(t,p) AND CRC2a(t)(p,my_succ(t,p),b)) OR (NOT prev(t,p) AND NOT doubt(t,p) AND membership(t,p) = membership(t,b) AND arrives(t,p)) THEN membership(t,p) ELSIF NOT prev(t,p) AND doubt(t,p) AND arrives(t,p) AND CRC2b(t)(p,my_succ(t,p),b) THEN remove(p,add(my_succ(t,p),membership(t,p))) ELSE remove(b,membership(t,p)) ENDIF % -------------------------------------------------------------------------- newprev : LEMMA prev(t+1,p) = LET b = broadcaster(t) IN IF p = b THEN TRUE ELSIF membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND (CRC1a(t)(p,b) OR CRC1b(t)(p,b)) THEN FALSE ELSE prev(t,p) ENDIF newdoubt : LEMMA doubt(t+1,p) = LET b = broadcaster(t) IN IF NOT p = b AND membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND NOT CRC1a(t)(p,b) AND CRC1b(t)(p,b) THEN TRUE ELSIF NOT p = b AND membership(t,p)(p) AND NOT prev(t,p) AND doubt(t,p) AND arrives(t,p) AND (CRC2a(t)(p,my_succ(t,p),b) OR CRC2b(t)(p,my_succ(t,p),b)) THEN FALSE ELSE doubt(t,p) ENDIF newaccepted : LEMMA accepted(t+1,p) = LET b = broadcaster(t) IN IF p = b THEN 1 ELSIF (membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND CRC1a(t)(p,b)) OR (membership(t,p)(p) AND NOT prev(t,p) AND doubt(t,p) AND arrives(t,p) AND (CRC2a(t)(p,my_succ(t,p),b) OR CRC2b(t)(p,my_succ(t,p),b))) OR (membership(t,p)(p) AND NOT prev(t,p) AND NOT doubt(t,p) AND membership(t,p) = membership(t,b) AND arrives(t,p)) THEN accepted(t,p) + 1 ELSE accepted(t,p) ENDIF newrejected : LEMMA rejected(t+1,p) = LET b = broadcaster(t) IN IF p = b THEN 0 ELSIF (membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND NOT CRC1a(t)(p,b) AND CRC1b(t)(p,b)) OR (membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND NOT CRC1a(t)(p,b) AND CRC1b(t)(p,b)) OR (membership(t,p)(p) AND prev(t,p) AND sends(t,b) AND (NOT (arrives(t,p) AND CRC1a(t)(p,b))) AND (NOT (arrives(t,p) AND CRC1b(t)(p,b)))) OR (membership(t,p)(p) AND NOT prev(t,p) AND doubt(t,p) AND sends(t,b) AND (NOT (arrives(t,p) AND CRC2a(t)(p,my_succ(t,p),b))) AND (NOT (arrives(t,p) AND CRC2b(t)(p,my_succ(t,p),b)))) OR (membership(t,p)(p) AND NOT prev(t,p) AND NOT doubt(t,p) AND sends(t,b) AND (NOT membership(t,p) = membership(t,b) OR NOT arrives(t,p))) THEN rejected(t,p) + 1 ELSE rejected(t,p) ENDIF newmy_succ : LEMMA my_succ(t+1,p) = LET b = broadcaster(t) IN IF b /= p AND membership(t,p)(p) AND prev(t,p) AND arrives(t,p) AND NOT CRC1a(t)(p,b) AND CRC1b(t)(p,b) THEN b ELSE my_succ(t,p) ENDIF % -------------------------------------------------------------------------- % -- stable(t,y,z): % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z stable(t,y,z) : bool = NOT faulty(t,y) AND NOT faulty(t,z) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND (accepted(t,p) = rejected(t,p) + 1 <=> (p = z)) AND (accepted(t,p) > rejected(t,p) + 1 WHEN (p /= z)) AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF stable_to_stable_non_faulty : LEMMA LET b = broadcaster(t) IN stable(t,y,z) AND NOT faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,z,b) stable_to_stable_faulty : LEMMA LET b = broadcaster(t) IN stable(t,y,z) AND faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,y,z) % ---------------------------------------------------------------------- % -- latent(t,x,y,z): % x ... becomes faulty at time t (was non-faulty at time t-1) % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z latent(t|t>0,x,y,z) : bool = NOT faulty(t-1,x) AND the_mem(t) = remove(x,the_mem(t-1)) AND (x /= y => NOT faulty(t,y)) AND (x /= z => NOT faulty(t,z)) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF p = x THEN membership(t,x) = add(x,the_mem(t)) AND IF x = z THEN accepted(t,x) = rejected(t,x) + 1 ELSE accepted(t,x) > rejected(t,x) + 1 ENDIF AND prev(t,x) = (x = z) AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = add(x,the_mem(t)) AND IF p = z THEN accepted(t,z) = rejected(t,z) + 1 ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF latent_x_is_faulty : LEMMA FORALL (t|t>0): latent(t,x,y,z) IMPLIES faulty(t,x) stable_to_latent_non_faulty : LEMMA LET b = broadcaster(t) IN stable(t,y,z) AND NOT faulty(t,x) AND NOT faulty(t,b) AND the_mem(t+1) = remove(x,the_mem(t)) IMPLIES latent(t+1,x,z,b) stable_to_latent_faulty : LEMMA LET b = broadcaster(t) IN stable(t,y,z) AND NOT faulty(t,x) AND faulty(t,b) AND the_mem(t+1) = remove(x,the_mem(t)) IMPLIES latent(t+1,x,y,z) % ---------------------------------------------------------------------- % -- excluded(t,y,z,x,S): % x ... fails to broadcast, has PREV and ACC<=REJ+1 % z ... last non-faulty broadcaster before x: has PREV and ACC>REJ % y ... last non-faulty broadcaster before z: has ACC>REJ, but not PREV % S ... set of good processors x has wrongly removed from own membership % i ... time since x last broadcast, i.e. x = broadcaster(t-i) excluded(t,y,z,x,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,z) AND NOT faulty(t,y) AND x = broadcaster(t-i) AND 0 < i AND i <= n AND NOT S(x) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,x)) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) <= rejected(t,x) + 1 AND prev(t,x) = TRUE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND IF (p = z) OR (p = y) THEN accepted(t,p) > rejected(t,p) ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF latent_to_excluded : LEMMA FORALL (t|t>0): latent(t,x,y,z) AND x = broadcaster(t) AND the_mem(t+1) = the_mem(t) IMPLIES excluded(t+1,y,z,x,emptyset,1) x_not_broadcaster_in_excluded : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) IMPLIES broadcaster(t) /= x excluded_loop : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded(t,y,z,x,S,i) AND faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES excluded(t+1,y,z,x,S,i+1) % ---------------------------------------------------------------------- % -- excluded_doubt(t,x,xs,y,z,S): % x ... is not acknowledged by successor (xs), has DOUBT, ACC<=REJ % xs... x's successor % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time since x last broadcast, i.e. x = broadcaster(t-i) excluded_doubt(t,x,xs,y,z,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,z) AND NOT faulty(t,y) AND NOT faulty(t,xs) AND x = broadcaster(t-i) AND 1 < i AND i <= n AND NOT S(x) AND before(t,y,z) AND before(t,x,xs) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) <= rejected(t,x) AND prev(t,x) = FALSE AND doubt(t,x) = TRUE AND my_succ(t,x) = xs ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND IF p = z THEN accepted(t,z) = rejected(t,z) + 1 ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF excluded_to_excluded_doubt : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded(t,y,z,x,S,i) AND NOT faulty(t,b) AND (NOT EXISTS q: NOT faulty(t,q) AND q /= b AND S(q)) AND arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_doubt(t+1,x,b,z,b,add(b,S),i+1) excluded_doubt_loop_on_missed : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) AND NOT faulty(t,b) AND NOT arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_doubt(t+1,x,xs,z,b,add(b,S),i+1) excluded_doubt_loop_on_disagree : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) AND NOT faulty(t,b) AND (EXISTS q: NOT faulty(t,q) AND q /= xs AND q /= b AND S(q)) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_doubt(t+1,x,xs,z,b,add(b,S),i+1) excluded_doubt_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) AND faulty(t,b) AND b /= x AND the_mem(t+1) = the_mem(t) IMPLIES excluded_doubt(t+1,x,xs,y,z,S,i+1) excluded_doubt_to_stable_on_x : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) AND b = x AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,y,z) excluded_doubt_to_stable : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) AND NOT faulty(t,b) AND (NOT EXISTS q: NOT faulty(t,q) AND q /= xs AND q /= b AND S(q)) AND arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,z,b) % ------------------------------------------------------------------------ % -- pending_selfdiag(t,x,y,z,S): % x ... fails to receive or rejects broadcaster, has PREV and ACC<=REJ % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time since x last broadcast, i.e. x = broadcaster(t-i) pending_selfdiag(t,x,y,z,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,z) AND NOT faulty(t,y) AND x = broadcaster(t-i) AND 1 < i AND i <= n AND NOT S(x) AND (EXISTS q: NOT faulty(t,q) AND S(q)) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) <= rejected(t,x) AND prev(t,x) = TRUE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND IF p = z THEN accepted(t,z) = rejected(t,z) + 1 ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF excluded_to_pending_selfdiag_on_disagree : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded(t,y,z,x,S,i) AND NOT faulty(t,b) AND (EXISTS q: NOT faulty(t,q) AND q /= b AND S(q)) AND the_mem(t+1) = the_mem(t) IMPLIES pending_selfdiag(t+1,x,z,b,add(b,S),i+1) excluded_to_pending_selfdiag_on_missed : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded(t,y,z,x,S,i) AND NOT faulty(t,b) AND NOT arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES pending_selfdiag(t+1,x,z,b,add(b,S),i+1) pending_selfdiag_loop : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) AND NOT faulty(t,b) AND (EXISTS q: NOT faulty(t,q) AND q /= b AND S(q)) AND the_mem(t+1) = the_mem(t) IMPLIES pending_selfdiag(t+1,x,z,b,add(b,S),i+1) pending_selfdiag_loop_on_missed : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) AND NOT faulty(t,b) AND NOT arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES pending_selfdiag(t+1,x,z,b,add(b,S),i+1) pending_selfdiag_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) AND faulty(t,b) AND b /= x AND the_mem(t+1) = the_mem(t) IMPLIES pending_selfdiag(t+1,x,y,z,S,i+1) pending_selfdiag_to_excluded_doubt : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) AND NOT faulty(t,b) AND (NOT EXISTS q: NOT faulty(t,q) AND q /= b AND S(q)) AND arrives(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_doubt(t+1,x,b,z,b,add(b,S),i+1) pending_selfdiag_to_stable : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) AND b = x AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,y,z) % ---------------------------------------------------------------------- % -- missed_rcv(t,x,y,z,S,i): % x ... fails to receive message: wronlgy excludes good broadcaster % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time during which x was not the broadcaster missed_rcv(t,x,y,z,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,y) AND NOT faulty(t,z) AND NOT S(x) AND S(z) AND 0 < i AND i < n AND (FORALL s: 0 x /= broadcaster(t-s)) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND prev(t,x) = FALSE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = add(x,the_mem(t)) AND IF p = z THEN accepted(t,p) = rejected(t,p) + 1 ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF missed_rcv_x_not_broadcaster_since : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) => FORALL s: 0 x /= broadcaster(t-s) latent_to_missed_rcv : LEMMA FORALL (t|t>0): LET b = broadcaster(t) IN latent(t,x,y,z) AND x /= b AND x /= z AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv(t+1,x,z,b,singleton(b),1) missed_rcv_loop_on_other_broadcaster : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND NOT faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv(t+1,x,z,b,add(b,S),i+1) missed_rcv_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND faulty(t,b) AND b /= x AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv(t+1,x,y,z,S,i+1) missed_rcv_to_excluded : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND b = x AND accepted(t,x) > rejected(t,x) AND NOT sends(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded(t+1,y,z,x,S,1) missed_rcv_to_stable : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND b = x AND accepted(t,x) <= rejected(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,y,z) % ---------------------------------------------------------------------- % -- excluded_z_not_ack(t,y,z,x,S): % x ... sends message that won't be accepted, has PREV and ACC=1, REJ=0 % z ... last non-faulty broadcaster before x: has PREV and ACC=REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time since x last broadcast, i.e. x = broadcaster(t-i) excluded_z_not_ack(t,y,z,x,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,z) AND NOT faulty(t,y) AND x = broadcaster(t-i) AND 0 < i AND i <= n AND NOT S(x) AND S(z) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND before(t,z,x) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) = rejected(t,x) + 1 AND prev(t,x) = TRUE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND IF p = z THEN accepted(t,z) = rejected(t,z) ELSE accepted(t,p) > rejected(t,p) ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF missed_rcv_to_excluded_z_not_ack : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND b = x AND accepted(t,x) > rejected(t,x) AND (EXISTS q: NOT faulty(t,q) AND S(q) AND q /= z) AND sends(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_z_not_ack(t+1,y,z,x,S,1) x_not_broadcaster_in_excluded_z_not_ack : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) IMPLIES broadcaster(t) /= x excluded_z_not_ack_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_not_ack(t,y,z,x,S,i) AND faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_z_not_ack(t+1,y,z,x,S,i+1) excluded_z_not_ack_to_excluded : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_not_ack(t,y,z,x,S,i) AND NOT faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES excluded(t+1,z,b,x,add(b,S),i+1) % ---------------------------------------------------------------------- % -- excluded_z_doubt(t,y,z,x,S): % x ... sends, doesn't ack z, but otherwise OK, has PREV and ACC=1, REJ=0 % z ... last non-faulty broadcaster before x: has DOUBT and ACC=REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time since x last broadcast, i.e. x = broadcaster(t-i) excluded_z_doubt(t,y,z,x,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,z) AND NOT faulty(t,y) AND x = broadcaster(t-i) AND 0 < i AND i <= n AND NOT S(x) AND S(z) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND before(t,z,x) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) = rejected(t,x) + 1 AND prev(t,x) = TRUE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = the_mem(t) AND IF p = z THEN accepted(t,z) = rejected(t,z) ELSE accepted(t,p) > rejected(t,p) ENDIF AND prev(t,p) = FALSE AND doubt(t,p) = (p = z) AND my_succ(t,z) = x ENDIF missed_rcv_to_excluded_z_doubt : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) AND b = x AND accepted(t,x) > rejected(t,x) AND (NOT EXISTS q: NOT faulty(t,q) AND S(q) AND q /= z) AND sends(t,x) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_z_doubt(t+1,y,z,x,S,1) x_not_broadcaster_in_excluded_z_doubt : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) IMPLIES broadcaster(t) /= x excluded_z_doubt_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_doubt(t,y,z,x,S,i) AND faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES excluded_z_doubt(t+1,y,z,x,S,i+1) excluded_z_doubt_to_excluded : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_doubt(t,y,z,x,S,i) AND NOT faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES excluded(t+1,z,b,x,add(b,S),i+1) % ---------------------------------------------------------------------- % -- missed_rcv_x_not_ack(t,y,x,z,S): % x ... fails to receive or rejects broadcaster, has PREV and ACC<=REJ % z ... last non-faulty broadcaster: has PREV and ACC=1, REJ=0 % y ... last non-faulty broadcaster before z % S ... set of good processors x has wrongly removed from own membership % i ... time during which x was not the broadcaster missed_rcv_x_not_ack(t,y,x,z,S,(i|i<=t)) : bool = faulty(t,x) AND NOT faulty(t,y) AND NOT faulty(t,z) AND NOT S(x) AND S(z) AND 0 < i AND i <= n AND (FORALL s: 0 x /= broadcaster(t-s)) AND before(t,y,z) AND (EXISTS p: p /= y AND NOT faulty(t,p) AND before(t,p,z)) AND (FORALL p: before(t,z,p) => faulty(t,p)) AND (EXISTS p: NOT faulty(t,p) AND before(t,p,y)) AND (FORALL p: before(t,y,p) AND before(t,p,z) => faulty(t,p)) AND FORALL p: IF p = x THEN membership(t,x) = difference(add(x,the_mem(t)),S) AND accepted(t,x) <= rejected(t,x) AND prev(t,x) = TRUE AND doubt(t,x) = FALSE ELSIF faulty(t,p) THEN NOT membership(t,p)(p) ELSE membership(t,p) = add(x,the_mem(t)) AND IF p = z THEN accepted(t,p) = rejected(t,p) + 1 ELSE accepted(t,p) > rejected(t,p) + 1 ENDIF AND prev(t,p) = (p = z) AND doubt(t,p) = FALSE ENDIF latent_to_missed_rcv_x_not_ack : LEMMA FORALL (t|t>0): LET b = broadcaster(t) IN latent(t,x,y,z) AND x /= b AND x = z AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv_x_not_ack(t+1,y,x,b,singleton(b),1) missed_rcv_x_not_ack_loop_on_ignore : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv_x_not_ack(t,y,x,z,S,i) AND NOT faulty(t,b) AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv_x_not_ack(t+1,z,x,b,add(b,S),i+1) missed_rcv_x_not_ack_loop_on_dead : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv_x_not_ack(t,y,x,z,S,i) AND faulty(t,b) AND b /= x AND the_mem(t+1) = the_mem(t) IMPLIES missed_rcv_x_not_ack(t+1,y,x,z,S,i+1) missed_rcv_x_not_ack_to_stable : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv_x_not_ack(t,y,x,z,S,i) AND b = x AND the_mem(t+1) = the_mem(t) IMPLIES stable(t+1,y,z) % ---------------------------------------------------------------------- latent_is_nonstable : LEMMA FORALL (t|t>0): latent(t,x,y,z) => NOT stable(t,a,b) excluded_is_nonstable : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) => NOT stable(t,a,b) excluded_doubt_is_nonstable : LEMMA FORALL (i|i<=t): excluded_doubt(t,x,xs,y,z,S,i) => NOT stable(t,a,b) pending_selfdiag_is_nonstable : LEMMA FORALL (i|i<=t): pending_selfdiag(t,x,y,z,S,i) => NOT stable(t,a,b) missed_rcv_is_nonstable : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) => NOT stable(t,a,b) excluded_z_not_ack_is_nonstable : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) => NOT stable(t,a,b) excluded_z_doubt_is_nonstable : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) => NOT stable(t,a,b) missed_rcv_x_not_ack_is_nonstable : LEMMA FORALL (i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i) => NOT stable(t,a,b) % ---------------------------------------------------------------------- no_faults_when_not_stable : AXIOM NOT stable(t,y,z) => the_mem(t+1) = the_mem(t) always_non_stable_is_no_more_faults : COROLLARY (FORALL s: NOT stable(t+s,y,z)) => (FORALL s: the_mem(t+s) = the_mem(t)) fault_may_occur_when_stable : AXIOM stable(t,y,z) => (the_mem(t+1) = the_mem(t) OR EXISTS x: NOT faulty(t,x) AND the_mem(t+1) = remove(x,the_mem(t))) initial : AXIOM EXISTS y,z: stable(0,y,z) % ---------------------------------------------------------------------- stable_successors : LEMMA LET b = broadcaster(t) IN stable(t,y,z) IMPLIES stable(t+1,z,b) OR stable(t+1,y,z) OR (EXISTS x: latent(t+1,x,z,b)) OR (EXISTS x: latent(t+1,x,y,z)) latent_successors : LEMMA FORALL (t|t>0): LET b = broadcaster(t) IN latent(t,x,y,z) IMPLIES excluded(t+1,y,z,x,emptyset,1) OR missed_rcv(t+1,x,z,b,singleton(b),1) OR missed_rcv_x_not_ack(t+1,y,x,b,singleton(b),1) excluded_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded(t,y,z,x,S,i) IMPLIES excluded(t+1,y,z,x,S,i+1) OR excluded(t+1,z,b,x,S,i+1) OR pending_selfdiag(t+1,x,z,b,add(b,S),i+1) OR excluded_doubt(t+1,x,b,z,b,add(b,S),i+1) excluded_doubt_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_doubt(t,x,xs,y,z,S,i) IMPLIES excluded_doubt(t+1,x,xs,y,z,S,i+1) OR excluded_doubt(t+1,x,xs,z,b,S,i+1) OR excluded_doubt(t+1,x,xs,z,b,add(b,S),i+1) OR stable(t+1,y,z) OR stable(t+1,z,b) pending_selfdiag_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN pending_selfdiag(t,x,y,z,S,i) IMPLIES pending_selfdiag(t+1,x,z,b,S,i+1) OR pending_selfdiag(t+1,x,z,b,add(b,S),i+1) OR pending_selfdiag(t+1,x,y,z,S,i+1) OR excluded_doubt(t+1,x,b,z,b,add(b,S),i+1) OR stable(t+1,y,z) missed_rcv_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv(t,x,y,z,S,i) IMPLIES missed_rcv(t+1,x,z,b,add(b,S),i+1) OR missed_rcv(t+1,x,y,z,S,i+1) OR excluded(t+1,y,z,x,S,1) OR excluded_z_doubt(t+1,y,z,x,S,1) OR excluded_z_not_ack(t+1,y,z,x,S,1) OR stable(t+1,y,z) excluded_z_not_ack_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_not_ack(t,y,z,x,S,i) IMPLIES excluded_z_not_ack(t+1,y,z,x,S,i+1) OR excluded(t+1,z,b,x,add(b,S),i+1) excluded_z_doubt_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN excluded_z_doubt(t,y,z,x,S,i) IMPLIES excluded_z_doubt(t+1,y,z,x,S,i+1) OR excluded(t+1,z,b,x,add(b,S),i+1) missed_rcv_x_not_ack_successors : LEMMA FORALL (i|i<=t): LET b = broadcaster(t) IN missed_rcv_x_not_ack(t,y,x,z,S,i) IMPLIES missed_rcv_x_not_ack(t+1,z,x,b,add(b,S),i+1) OR missed_rcv_x_not_ack(t+1,y,x,z,S,i+1) OR stable(t+1,y,z) % ---------------------------------------------------------------------- total(t) : bool = (EXISTS y,z: stable(t,y,z)) OR (t>0 AND EXISTS x,y,z: latent(t,x,y,z)) OR (EXISTS y,z,x,S,(i|i<=t): excluded(t,y,z,x,S,i)) OR (EXISTS y,z,x,S,(i|i<=t): excluded_z_not_ack(t,y,z,x,S,i)) OR (EXISTS y,z,x,S,(i|i<=t): excluded_z_doubt(t,y,z,x,S,i)) OR (EXISTS x,y,z,S,(i|i<=t): pending_selfdiag(t,x,y,z,S,i)) OR (EXISTS x,xs,y,z,S,(i|i<=t): excluded_doubt(t,x,xs,y,z,S,i)) OR (EXISTS x,y,z,S,(i|i<=t): missed_rcv(t,x,y,z,S,i)) OR (EXISTS y,x,z,S,(i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i)) total_invariant : LEMMA total(t) IMPLIES total(t+1) totality : LEMMA total(t) % ---------------------------------------------------------------------- validity : THEOREM IF faulty(t,p) THEN NOT membership(t,p)(p) OR subset?(membership(t,p), add(p,the_mem(t))) ELSE membership(t,p) = the_mem(t) OR EXISTS x: faulty(t,x) AND membership(t,p) = add(x,the_mem(t)) ENDIF agreement : THEOREM NOT faulty(t,p) AND NOT faulty(t,q) IMPLIES membership(t,p) = membership(t,q) % ---------------------------------------------------------------------- excluded_loop_or_exit : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) IMPLIES (FORALL s: EXISTS y,z: excluded(t+s,y,z,x,S,i+s)) OR (EXISTS s,z,b,S: pending_selfdiag(t+s,x,z,b,S,i+s)) OR (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) excluded_doubt_loop_or_exit : LEMMA FORALL (i|i<=t): excluded_doubt(t,x,xs,y,z,S,i) IMPLIES (FORALL s: EXISTS y,z,S: s < n AND excluded_doubt(t+s,x,xs,y,z,S,i+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) pending_selfdiag_loop_or_exit : LEMMA FORALL (i|i<=t): pending_selfdiag(t,x,y,z,S,i) IMPLIES (FORALL s: EXISTS y,z,S: pending_selfdiag(t+s,x,y,z,S,i+s)) OR (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) missed_rcv_loop_or_exit : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) IMPLIES (FORALL s: EXISTS y,z,S: missed_rcv(t+s,x,y,z,S,i+s)) OR (EXISTS s,y,z,S: s <= n-i AND excluded(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_doubt(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_not_ack(t+s,y,z,x,S,1)) OR (EXISTS s,y,z: s <= n-i AND stable(t+s,y,z)) excluded_z_not_ack_loop_or_exit : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) IMPLIES (FORALL s: excluded_z_not_ack(t+s,y,z,x,S,i+s)) OR (EXISTS s,z,b,S: excluded(t+s,z,b,x,S,i+s)) excluded_z_doubt_loop_or_exit : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) IMPLIES (FORALL s: excluded_z_doubt(t+s,y,z,x,S,i+s)) OR (EXISTS s,z,b,S: excluded(t+s,z,b,x,S,i+s)) missed_rcv_x_not_ack_loop_or_exit : LEMMA FORALL (i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i) IMPLIES (FORALL s: EXISTS y,z,S: s <= n+1-i AND missed_rcv_x_not_ack(t+s,y,x,z,S,i+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) % ---------------------------------------------------------------------- excluded_faulty_only_or_exit : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) IMPLIES (FORALL s: faulty(t,broadcaster(t+s))) OR (EXISTS s,z,b,S: pending_selfdiag(t+s,x,z,b,S,i+s)) OR (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) excluded_doubt_faulty_only_or_exit : LEMMA FORALL (i|i<=t): excluded_doubt(t,x,xs,y,z,S,i) IMPLIES (FORALL s: x /= broadcaster(t+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) pending_selfdiag_faulty_only_or_exit : LEMMA FORALL (i|i<=t): pending_selfdiag(t,x,y,z,S,i) IMPLIES (FORALL s: x /= broadcaster(t+s)) OR (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) missed_rcv_faulty_only_or_exit : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) IMPLIES (FORALL s: x /= broadcaster(t+s)) OR (EXISTS s,y,z,S: s <= n-i AND excluded(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_doubt(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_not_ack(t+s,y,z,x,S,1)) OR (EXISTS s,y,z: s <= n-i AND stable(t+s,y,z)) excluded_z_not_ack_faulty_only_or_exit : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) IMPLIES (FORALL s: faulty(t,broadcaster(t+s))) OR (EXISTS s,y,z,S: excluded(t+s,y,z,x,S,i+s)) excluded_z_doubt_faulty_only_or_exit : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) IMPLIES (FORALL s: faulty(t,broadcaster(t+s))) OR (EXISTS s,y,z,S: excluded(t+s,y,z,x,S,i+s)) missed_rcv_x_not_ack_faulty_only_or_exit : LEMMA FORALL (i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i) IMPLIES (FORALL s: x /= broadcaster(t+s)) OR (EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z)) % ---------------------------------------------------------------------- excluded_exit : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) IMPLIES (EXISTS s,z,b,S: pending_selfdiag(t+s,x,z,b,S,i+s)) OR (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) excluded_doubt_exit : LEMMA FORALL (i|i<=t): excluded_doubt(t,x,xs,y,z,S,i) IMPLIES EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) pending_selfdiag_exit : LEMMA FORALL (i|i<=t): pending_selfdiag(t,x,y,z,S,i) IMPLIES (EXISTS s,xs,y,z,S: excluded_doubt(t+s,x,xs,y,z,S,i+s)) OR EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) missed_rcv_exit : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) IMPLIES (EXISTS s,y,z,S: s <= n-i AND excluded(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_doubt(t+s,y,z,x,S,1)) OR (EXISTS s,y,z,S: s <= n-i AND excluded_z_not_ack(t+s,y,z,x,S,1)) OR (EXISTS s,y,z: s <= n-i AND stable(t+s,y,z)) excluded_z_not_ack_exit : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) IMPLIES EXISTS s,z,b,S: excluded(t+s,z,b,x,S,i+s) excluded_z_doubt_exit : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) IMPLIES EXISTS s,z,b,S: excluded(t+s,z,b,x,S,i+s) missed_rcv_x_not_ack_exit : LEMMA FORALL (i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i) IMPLIES EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) % ---------------------------------------------------------------------- excluded_doubt_eventually_stable : LEMMA FORALL (i|i<=t): excluded_doubt(t,x,xs,y,z,S,i) => EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) pending_selfdiag_eventually_stable : LEMMA FORALL (i|i<=t): pending_selfdiag(t,x,y,z,S,i) => EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) excluded_eventually_stable : LEMMA FORALL (i|i<=t): excluded(t,y,z,x,S,i) => EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) excluded_z_not_ack_eventually_stable : LEMMA FORALL (i|i<=t): excluded_z_not_ack(t,y,z,x,S,i) => EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) excluded_z_doubt_eventually_stable : LEMMA FORALL (i|i<=t): excluded_z_doubt(t,y,z,x,S,i) => EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) missed_rcv_eventually_stable : LEMMA FORALL (i|i<=t): missed_rcv(t,x,y,z,S,i) => EXISTS s,y,z: s <= 2*n-i AND stable(t+s,y,z) missed_rcv_x_not_ack_eventually_stable : LEMMA FORALL (i|i<=t): missed_rcv_x_not_ack(t,y,x,z,S,i) IMPLIES EXISTS s,y,z: s <= n+1-i AND stable(t+s,y,z) latent_eventually_stable : LEMMA FORALL (t|t>0): latent(t,x,y,z) => EXISTS s,y,z: s <= 2*n AND stable(t+s,y,z) % ---------------------------------------------------------------------- liveness : THEOREM stable(t,y,z) => (EXISTS s,y,z: 0 < s AND s <= 2*n+1 AND stable(t+s,y,z)) self_diagnosis : COROLLARY NOT faulty(t,x) AND faulty(t+1,x) IMPLIES EXISTS s: 0 < s AND s <= 2*n+1 AND NOT membership(t+s,x)(x) END ttp $$$ttp.prf (|ttp| (|proc_TCC1| "" (INST + 0) (("" (ASSERT) NIL NIL)) NIL) (|all_or_none| "" (SKOSIMP*) (("" (USE "arrival") (("" (USE "arrival" :SUBST ("p" "q!1")) (("" (ASSERT) (("" (CASE "sends(t!1, broadcaster(t!1))") (("1" (ASSERT) NIL NIL) ("2" (USE "nonarrival") (("2" (USE "nonarrival" :SUBST ("p" "p!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|faults_latch_always| "" (INDUCT "i") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "p!1" "t!1") (("2" (ASSERT) (("2" (USE "faults_latch") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|faults_latch_rev| "" (SKOSIMP*) (("" (USE "faults_latch" :POLARITY? T) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|at_least_four_nodes| "" (INST + 0 1 2 3) (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL) ("4" (GROUND) NIL NIL) ("5" (GROUND) NIL NIL)) NIL) (|at_least_three_nodes| "" (USE "at_least_four_nodes") (("" (SKOSIMP*) (("" (INST + "p!1" "x!1" "y!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|another_node_exists| "" (SKOSIMP*) (("" (CASE "x!1=0") (("1" (INST + 1) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (INST + 0) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|two_non_faulty_exist| "" (SKOSIMP*) (("" (USE "three_non_faulty_exist") (("" (SKOSIMP*) (("" (INST + "x!1" "y!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|non_faulty_exists| "" (SKOSIMP*) (("" (USE "two_non_faulty_exist") (("" (SKOSIMP*) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|two_other_nonfaulty_exist| "" (SKOSIMP*) (("" (USE "three_non_faulty_exist") (("" (SKOSIMP*) (("" (CASE "x!1 = x!2") (("1" (INST + "y!1" "z!1") (("1" (GROUND) NIL NIL)) NIL) ("2" (CASE "x!1 = y!1") (("1" (INST + "x!2" "z!1") (("1" (GROUND) NIL NIL)) NIL) ("2" (INST + "y!1" "x!2") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|another_nonfaulty_exists| "" (SKOSIMP*) (("" (USE "two_other_nonfaulty_exist") (("" (SKOSIMP*) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|mono| "" (SKOSIMP*) (("" (DECOMPOSE-EQUALITY) (("" (INST - "p!1") (("" (EXPAND "the_mem") (("" (IFF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|mono2| "" (SKOSIMP*) (("" (LEMMA "mono") (("" (INST? :WHERE +) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|faulty_mem| "" (SKOSIMP*) (("" (USE "mono2") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|faulty_x| "" (SKOSIMP*) (("" (DECOMPOSE-EQUALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|not_faulty_y| "" (SKOSIMP*) (("" (DECOMPOSE-EQUALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|useful| "" (GRIND) NIL NIL) (|set_prop1| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|set_prop1a| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|set_prop2| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|set_prop_3| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|none_before_current| "" (SKOSIMP*) (("" (EXPAND "before") (("" (INST - 0) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|round_prop| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cycle| "" (SKOSIMP*) (("" (EXPAND "broadcaster") (("" (GROUND) (("1" (LEMMA "mod_Ada") (("1" (INST-CP - "t!1" "n") (("1" (SKOSIMP) (("1" (INST - "j!1+t!1" "n") (("1" (SKOSIMP) (("1" (INST + "k!2-k!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE -3 :HIDE? T) (("2" (CASE "n*(k!2 - k!1) >= 0") (("1" (LEMMA "pos_times_ge") (("1" (INST - "n" "k!2-k!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (REPLACE -1 :HIDE? T) (("2" (LEMMA "mod_sum") (("2" (INST - "t!1" "n" "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|next_broadcast_slot| "" (SKOSIMP*) (("" (USE "cycle") (("" (GROUND) (("" (INST + 1) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|bcast_prop| "" (SKOSIMP) (("" (EXPAND "broadcaster") (("" (CASE "t!1=3") (("1" (INST?) (("1" (PROP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (INDUCT-AND-SIMPLIFY "i") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_prop_TCC1| "" (SKOSIMP) (("" (LEMMA "bcast_prop") (("" (INST - "s!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|before_prop| "" (SKOSIMP) (("" (EXPAND "broadcaster") (("" (LEMMA "mod_of_mod_diff") (("" (INST - "mod(x!1,n) + s!1" "s!1" "n") (("" (GROUND) (("" (REPLACE -1 :HIDE? T) (("" (LEMMA "mod_of_mod") (("" (INST - "0" "x!1" "n") (("" (REPLACE -1 :HIDE? T) (("" (LEMMA "mod_lt_nat") (("" (INST - "n" "x!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_prop1_TCC1| "" (SKOSIMP) (("" (LEMMA "bcast_prop") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|before_prop1| "" (SKOSIMP) (("" (LEMMA "before_prop") (("" (INST - "t!1" "x!1") (("" (EXPAND "broadcaster") (("" (LEMMA "mod_of_mod") (("" (INST - "t!1-mod(t!1,n)" "x!1" "n") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_prop1n_TCC1| "" (SKOSIMP*) (("" (LIFT-IF) (("" (ASSERT) (("" (PROP) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|before_prop1n| "" (SKOSIMP*) (("" (BETA) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (CASE "x!1 = broadcaster(t!1 + (x!1 - broadcaster(t!1)))") (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (REPLACE -4 -3) (("1" (EXPAND "broadcaster") (("1" (USE "mod_minus") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (USE "mod_of_mod_diff" :SUBST ("i" "i!1+t!1")) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (USE "mod_lt_nat" :SUBST ("n" "i!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "before_prop1") (("2" (ASSERT) NIL NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (CASE "x!1 = broadcaster(t!1 + (n + x!1 - broadcaster(t!1)))") (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (HIDE -1) (("1" (USE "mod_plus" :SUBST ("i" "t!1" "a" "i!1" "m" "n")) (("1" (EXPAND "broadcaster") (("1" (ASSERT) (("1" (CASE "mod(t!1, n) + i!1 < 2*n") (("1" (LEMMA "mod_it_is" :SUBST ("a" "i!1+t!1" "m" "n")) (("1" (INST - "mod(t!1,n)+i!1-n" _) (("1" (ASSERT) (("1" (USE "mod_Ada" :SUBST ("i" "t!1" "j" "n")) (("1" (SKOSIMP*) (("1" (INST - "k!1+1") (("1" (ASSERT) NIL NIL) ("2" (USE "neg_times_lt") (("2" (ASSERT) (("2" (CASE "k!1*n <= -n") (("1" (ASSERT) NIL NIL) ("2" (BOTH-SIDES "+" "n") (("2" (USE "neg_times_le" :SUBST ("x" "k!1+1" "y" "n")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "before_prop1") (("2" (EXPAND "broadcaster") (("2" (USE "mod_sum_pos" :SUBST ("k" 1)) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|next_b_prop| "" (SKOSIMP*) (("" (LEMMA "before_prop1n") (("" (INST - "t!1" "x!1") (("" (BETA) (("" (FLATTEN) (("" (INST? :FNUMS +) (("1" (LIFT-IF) (("1" (PROP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL) ("3" (FLATTEN) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonfaulty_broadcaster_exists| "" (SKOSIMP*) (("" (USE "non_faulty_exists") (("" (SKOSIMP*) (("" (USE "next_b_prop") (("" (SKOSIMP*) (("" (INST + "s!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_prop2| "" (SKOSIMP) (("" (LEMMA "cycle") (("" (INST - "1+i!1" "t!1") (("" (ASSERT) (("" (SKOSIMP) (("" (ASSERT) (("" (CASE "i!2=0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (LEMMA "both_sides_times_pos_le1") (("2" (INST - "n" "1" "i!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before0| "" (SKOSIMP) (("" (EXPAND "broadcaster") (("" (LEMMA "mod_plus") (("" (INST - "n-1" "1+t!1" "n") (("" (GROUND) (("" (CASE "mod(x!1,n)=mod(n+t!1,n)") (("1" (LEMMA "mod_sum_pos") (("1" (INST - "t!1" "1" "n") (("1" (ASSERT) (("1" (LEMMA "mod_lt_nat") (("1" (INST - "n" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before0a| "" (SKOSIMP) (("" (EXPAND "broadcaster") (("" (LEMMA "mod_minus") (("" (INST - "1" "1+t!1" "n") (("" (GROUND) (("" (CASE "mod(x!1,n)=mod(t!1,n)") (("1" (LEMMA "mod_lt_nat") (("1" (INST - "n" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before1| "" (SKOSIMP) (("" (EXPAND "before") (("" (SKOSIMP) (("" (CASE "broadcaster(x!1)>=broadcaster(1+t!1)") (("1" (INST + "broadcaster(x!1)-broadcaster(1+t!1)") (("1" (SPLIT) (("1" (TYPEPRED "broadcaster(1+t!1)") (("1" (TYPEPRED "broadcaster(x!1)") (("1" (FORWARD-CHAIN "before_prop2") (("1" (USE "before0") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "before_prop") (("2" (INST - "1+t!1" "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (INST + "n+broadcaster(x!1)-broadcaster(1+t!1)") (("1" (GROUND) (("1" (TYPEPRED "broadcaster(1+t!1)") (("1" (TYPEPRED "broadcaster(x!1)") (("1" (FORWARD-CHAIN "before_prop2") (("1" (USE "before0a") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "before_prop") (("2" (INST - "1+t!1" "x!1") (("2" (LEMMA "cycle") (("2" (INST - "n" "1 + t!1 + broadcaster(x!1) - broadcaster(1 + t!1)") (("1" (GROUND) (("1" (INST + 1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "bcast_prop") (("2" (INST - "1+t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before2| "" (SKOSIMP) (("" (EXPAND "before") (("" (SKOSIMP) (("" (INST - "i!1+1") (("" (ASSERT) (("" (SKOSIMP) (("" (INST + "s!1-1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_previous| "" (SKOSIMP*) (("" (EXPAND "before") (("" (SKOSIMP*) (("" (INST - "i!1-1") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (INST + "s!1+1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|before3| "" (SKOSIMP) (("" (EXPAND "before") (("" (INST - 0) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|before3_rev| "" (SKOSIMP*) (("" (INST + "broadcaster(t!1)") (("" (EXPAND "before") (("" (SKOSIMP*) (("" (INST + 0) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_irreflexive| "" (SKOSIMP*) (("" (EXPAND "before") (("" (LEMMA "next_b_prop") (("" (INST - "t!1" "x!1") (("" (SKOSIMP*) (("" (INST? :FNUMS -4) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST - "s!2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_asymmetric| "" (SKOSIMP*) (("" (EXPAND "before") (("" (USE "next_b_prop" :SUBST ("x" "y!1" "t" "t!1")) (("" (SKOSIMP*) (("" (INST -4 "s!1") (("" (ASSERT) (("" (SKOSIMP*) (("" (INST -6 "s!2") (("" (ASSERT) (("" (SKOSIMP*) (("" (INST - "s!3") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_transitive| "" (SKOSIMP*) (("" (EXPAND "before") (("" (SKOSIMP*) (("" (INST -2 "i!1") (("" (GROUND) (("" (SKOSIMP*) (("" (INST - "s!1") (("" (GROUND) (("" (SKOSIMP*) (("" (INST + "s!2") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|before_total| "" (SKOSIMP*) (("" (EXPAND "before") (("" (SKOSIMP*) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|not_prev_broadcaster_before| "" (SKOSIMP*) (("" (CASE-REPLACE "p!1=broadcaster(t!1)") (("1" (REWRITE "before_irreflexive") NIL NIL) ("2" (USE "before1" :SUBST ("x" "p!1")) (("2" (FORWARD-CHAIN "before_asymmetric") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|two_nonfaulty_before_broadcaster_exist| "" (SKOSIMP) (("" (LEMMA "three_non_faulty_exist") (("" (INST - "t!1+1") (("" (SKOSIMP) (("" (CASE "x!1=broadcaster(t!1)") (("1" (INST + "y!1" "z!1") (("1" (GROUND) (("1" (USE "before1") (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "before1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE "y!1=broadcaster(t!1)") (("1" (INST + "x!1" "z!1") (("1" (GROUND) (("1" (USE "before1") (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "before1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "y!1" "x!1") (("2" (GROUND) (("1" (USE "before1") (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "before1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonfaulty_before_broadcaster_exists| "" (SKOSIMP*) (("" (USE "two_nonfaulty_before_broadcaster_exist") (("" (SKOSIMP*) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|another_nonfaulty_before_broadcaster_exists| "" (SKOSIMP*) (("" (USE "two_nonfaulty_before_broadcaster_exist") (("" (SKOSIMP*) (("" (CASE "p!1=z!1") (("1" (INST + "q!1") (("1" (GROUND) NIL NIL)) NIL) ("2" (INST + "p!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|three_nonfaulty_before_faulty_broadbaster| "" (SKOSIMP*) (("" (USE "three_non_faulty_exist" :SUBST ("t" "t!1+1")) (("" (SKOSIMP*) (("" (INST + "x!1" "y!1" "z!1") (("" (GROUND) (("1" (REWRITE "before1") (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (REWRITE "before1") (("2" (USE "faults_latch" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL) ("3" (REWRITE "before1") (("3" (USE "faults_latch" :POLARITY? T) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|two_other_nonfaulty_before_faulty_broadcaster| "" (SKOSIMP*) (("" (USE "three_nonfaulty_before_faulty_broadbaster" :POLARITY? T) (("" (ASSERT) (("" (SKOSIMP*) (("" (CASE "x!1 = z!1") (("1" (INST + "y!1" "z!2") (("1" (GROUND) NIL NIL)) NIL) ("2" (CASE "y!1=z!1") (("1" (INST + "x!1" "z!2") (("1" (GROUND) NIL NIL)) NIL) ("2" (INST + "x!1" "y!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonfaulty_before_broadcaster_not_prev_exists| "" (SKOSIMP*) (("" (INST + "y!1") (("" (PROP) (("1" (REPLACE*) (("1" (REWRITE "before_irreflexive") NIL NIL)) NIL) ("2" (USE "faulty_mem" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL) ("3" (USE "before3" :SUBST ("y" "y!1")) (("3" (REWRITE "before1") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|nonfaulty_before_prev_exists_invariant| "" (SKOSIMP*) (("" (INST + "y!1") (("" (PROP) (("1" (USE "faulty_mem" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "before2" :POLARITY? T) (("2" (GROUND) (("2" (USE "before3" :SUBST ("y" "y!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|all_faulty_after_prev_invariant| "" (SKOSIMP*) (("" (USE "before_previous" :POLARITY? T) (("" (GROUND) (("1" (INST - "p!1") (("1" (GROUND) (("1" (USE "faults_latch") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "before_irreflexive") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|nonfaulty_before_prev_not_prevprev_exists_invariant| "" (SKOSIMP*) (("" (USE "before2" :POLARITY? T :SUBST ("x" "p!1")) (("" (GROUND) (("" (INST? :POLARITY? T) (("" (GROUND) (("" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|all_faulty_after_prev_faulty_broadcaster_invariant| "" (SKOSIMP*) (("" (USE "before_previous" :POLARITY? T) (("" (GROUND) (("1" (INST - "p!1") (("1" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "faults_latch" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|non_faulty_before_exists_invariant| "" (SKOSIMP*) (("" (USE "before2") (("" (GROUND) (("" (INST?) (("" (GROUND) (("" (USE "faulty_mem" :POLARITY? T) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|all_faulty_between_prev_and_prevprev_invariant| "" (SKOSIMP*) (("" (USE "before_previous" :POLARITY? T) (("" (USE "before_previous" :POLARITY? T :SUBST ("x" "p!1" "y" "z!1")) (("" (GROUND) (("1" (INST - "p!1") (("1" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "faults_latch" :POLARITY? T) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|CRC1a_char| "" (SKOSIMP*) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) (|CRC1a_char2| "" (GRIND) NIL NIL) (|CRC1b_char| "" (SKOSIMP*) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) (|CRC1b_char2| "" (SKOSIMP*) (("" (USE "CRC1b_char") (("" (GRIND) NIL NIL)) NIL)) NIL) (|CRC2a_char| "" (SKOSIMP*) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) (|CRC2a_char2| "" (SKOSIMP*) (("" (USE "CRC2a_char") (("" (GRIND) NIL NIL)) NIL)) NIL) (|CRC2b_char| "" (SKOSIMP*) (("" (PROP) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) (|CRC2b_char2| "" (SKOSIMP*) (("" (USE "CRC2b_char") (("" (GRIND) NIL NIL)) NIL)) NIL) (|newmem| "" (SKOSIMP*) (("" (BETA) (("" (USE "algorithm") (("" (LIFT-IF) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|newprev| "" (SKOSIMP*) (("" (BETA) (("" (USE "algorithm") (("" (LIFT-IF) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|newdoubt| "" (SKOSIMP*) (("" (BETA) (("" (USE "algorithm") (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL) (|newaccepted| "" (SKOSIMP*) (("" (BETA) (("" (LIFT-IF) (("" (USE "algorithm") (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|newrejected| "" (SKOSIMP*) (("" (BETA) (("" (LIFT-IF) (("" (USE "algorithm") (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|newmy_succ| "" (SKOSIMP*) (("" (BETA) (("" (LIFT-IF) (("" (USE "algorithm" :SUBST ("p" "p!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|stable_to_stable_non_faulty| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (REWRITE "before1") NIL NIL) ("4" (REWRITE "none_before_current" :SUBST ("y" "z!1")) (("4" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("4" (GROUND) NIL NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (USE "not_prev_broadcaster_before" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL)) NIL) ("6" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_after_prev_invariant") (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -3 -5) (("8" (GROUND) (("1" (MEM "p!1") NIL NIL) ("2" (MEM "p!1") NIL NIL) ("3" (ACC-REJ "p!1") NIL NIL) ("4" (ACC-REJ "p!1") NIL NIL) ("5" (ACC-REJ "p!1") NIL NIL) ("6" (PREV "p!1") NIL NIL) ("7" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|stable_to_stable_faulty| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -3 -5) (("8" (GROUND) (("1" (MEM "p!1") NIL NIL) ("2" (MEM "p!1") NIL NIL) ("3" (ACC-REJ- "p!1") NIL NIL) ("4" (ACC-REJ- "p!1") NIL NIL) ("5" (ACC-REJ- "p!1") NIL NIL) ("6" (PREV "p!1") NIL NIL) ("7" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|latent_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_x_is_faulty| "" (SKOSIMP*) (("" (EXPAND "latent") (("" (FLATTEN) (("" (FORWARD-CHAIN "faulty_x") NIL NIL)) NIL)) NIL)) NIL) (|stable_to_latent_non_faulty| "" (SKOSIMP*) (("" (EXPAND "stable") (("" (EXPAND "latent") (("" (REW) (("" (GROUND) (("1" (USE "not_faulty_y") (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "not_faulty_y") (("2" (GROUND) NIL NIL)) NIL) ("3" (FORWARD-CHAIN "before3") (("3" (USE "before1") (("3" (GROUND) NIL NIL)) NIL)) NIL) ("4" (USE "another_nonfaulty_before_broadcaster_exists" :SUBST ("t" "t!1")) (("4" (SKOSIMP*) (("4" (INST + "p!1") (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (USE "not_prev_broadcaster_before" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL)) NIL) ("6" (USE "another_nonfaulty_before_broadcaster_exists" :SUBST ("z" "z!1" "t" "t!1")) (("6" (SKOSIMP*) (("6" (INST + "p!1") (("6" (GROUND) (("6" (USE "before2" :SUBST ("t" "t!1")) (("6" (CASE-REPLACE "p!1=broadcaster(t!1)") (("1" (REWRITE "before_irreflexive") NIL NIL) ("2" (ASSERT) (("2" (USE "before_total") (("2" (ASSERT) (("2" (INST - "p!1") (("2" (ASSERT) (("2" (USE "faults_latch_rev") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (USE "all_faulty_after_prev_invariant") (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -3 -5) (("8" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (ACC-REJ "x!1") NIL NIL) ("4" (PREV "x!1") NIL NIL) ("5" (DOUBT "x!1") NIL NIL) ("6" (CASE "the_mem(t!1+1)(p!1)") (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL) ("2" (MEM "p!1" :SPLIT +) NIL NIL)) NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|stable_to_latent_faulty| "" (SKOSIMP*) (("" (EXPAND "stable") (("" (EXPAND "latent") (("" (REW) (("" (GROUND) (("1" (USE "not_faulty_y") (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "not_faulty_y") (("2" (GROUND) NIL NIL)) NIL) ("3" (USE "before2" :SUBST ("t" "t!1")) (("3" (GROUND) NIL NIL)) NIL) ("4" (USE "two_other_nonfaulty_before_faulty_broadcaster" :POLARITY? T :SUBST ("z" "y!1" "t" "t!1")) (("4" (ASSERT) (("4" (SKOSIMP*) (("4" (CASE "x!2 = z!1") (("1" (INST + "y!2") (("1" (GROUND) (("1" (USE "before_total" :SUBST ("x" "y!2" "y" "z!1" "t" "t!1+1")) (("1" (GROUND) (("1" (USE "before_previous" :SUBST ("x" "z!1" "y" "y!2" "t" "t!1")) (("1" (GROUND) (("1" (INST - "y!2") (("1" (ASSERT) (("1" (USE "faults_latch" :SUBST ("t" "t!1" "p" "y!2")) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (GROUND) (("2" (USE "before_total" :SUBST ("x" "x!2" "y" "z!1" "t" "t!1+1")) (("2" (GROUND) (("2" (USE "before_previous" :SUBST ("x" "z!1" "y" "x!2" "t" "t!1")) (("2" (GROUND) (("2" (INST - "x!2") (("2" (ASSERT) (("2" (USE "faults_latch" :SUBST ("t" "t!1" "p" "x!2")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "two_other_nonfaulty_before_faulty_broadcaster" :POLARITY? T :SUBST ("z" "z!1" "t" "t!1")) (("6" (ASSERT) (("6" (SKOSIMP*) (("6" (CASE "x!2 = y!1") (("1" (INST + "y!2") (("1" (GROUND) (("1" (USE "before_total" :SUBST ("t" "t!1+1" "x" "y!2" "y" "y!1")) (("1" (GROUND) (("1" (USE "before_previous" :SUBST ("x" "y!1" "y" "y!2" "t" "t!1")) (("1" (GROUND) (("1" (INST -10 "y!2") (("1" (GROUND) (("1" (USE "before_total" :SUBST ("t" "t!1" "x" "y!2" "y" "z!1")) (("1" (GROUND) (("1" (INST - "y!2") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (GROUND) (("2" (USE "before_total" :SUBST ("t" "t!1+1" "x" "x!2" "y" "y!1")) (("2" (GROUND) (("2" (USE "before_previous" :SUBST ("x" "y!1" "y" "x!2" "t" "t!1")) (("2" (GROUND) (("2" (INST -9 "x!2") (("2" (GROUND) (("2" (USE "before_total" :SUBST ("t" "t!1" "x" "x!2" "y" "z!1")) (("2" (ASSERT) (("2" (INST - "x!2") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (HIDE -3 -5) (("8" (SKOSIMP*) (("8" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ- "x!1") NIL NIL) ("3" (ACC-REJ- "x!1") NIL NIL) ("4" (PREV- "x!1") NIL NIL) ("5" (DOUBT- "x!1") NIL NIL) ("6" (CASE "the_mem(t!1+1)(p!1)") (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL) ("2" (MEM "p!1") NIL NIL)) NIL) ("7" (MEM- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (ACC-REJ- "p!1") NIL NIL) ("10" (PREV- "p!1") NIL NIL) ("11" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|latent_to_excluded_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_to_excluded| "" (SKOSIMP*) (("" (FORWARD-CHAIN "latent_x_is_faulty") (("" (EXPAND "latent") (("" (EXPAND "excluded") (("" (REW) (("" (ASSERT) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (GROUND) NIL NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (CASE "NOT faulty(1 + t!1,z!1)") (("1" (INST + "z!1") (("1" (GROUND) (("1" (REPLACE*) (("1" (REWRITE "before1" :SUBST ("x" "z!1")) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "y!1") (("2" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (REPLACE*) (("2" (REWRITE "before1" :SUBST ("x" "y!1")) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("9" (SKOSIMP*) (("9" (HIDE -5 -7) (("9" (GROUND) (("1" (REWRITE "difference_emptyset1") (("1" (MEM "x!1") NIL NIL)) NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("6" (MEM- "p!1") NIL NIL)) NIL) ("7" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("7" (ACC-REJ- "p!1") NIL NIL)) NIL) ("8" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("8" (ACC-REJ- "p!1") NIL NIL)) NIL) ("9" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("9" (ACC-REJ- "p!1") NIL NIL)) NIL) ("10" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("10" (PREV- "p!1") NIL NIL)) NIL) ("11" (USE "faulty_broadcaster" :SUBST ("t" "t!1-1")) (("11" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|x_not_broadcaster_in_excluded| "" (EXPAND "excluded") (("" (SKOSIMP*) (("" (REWRITE "none_before_current" :SUBST ("y" "x!1")) NIL NIL)) NIL)) NIL) (|excluded_loop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_loop| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "x_not_broadcaster_in_excluded") (("" (EXPAND "excluded") (("" (REW) (("" (ASSERT) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot") (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "before2" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (INST + "p!3") (("10" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (USE "before2" :SUBST ("t" "t!1" "x" "p!3" "y" "x!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("11" (SKOSIMP*) (("11" (HIDE -7 -9) (("11" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (ACC-REJ- "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_to_excluded_doubt_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_to_excluded_doubt| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded") (("" (EXPAND "excluded_doubt") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("5" (USE "next_broadcast_slot") (("5" (GROUND) NIL NIL)) NIL) ("6" (GROUND) NIL NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (REWRITE "before1") NIL NIL) ("9" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (USE "not_prev_broadcaster_before" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL)) NIL) ("11" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("11" (GROUND) NIL NIL)) NIL) ("12" (USE "all_faulty_after_prev_invariant") (("12" (GROUND) NIL NIL)) NIL) ("13" (SKOSIMP*) (("13" (HIDE -7 -9) (("13" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (INST + "x!3") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "x!3") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (MYSUCC "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("6" (MEM "p!1") NIL NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_loop_on_missed_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_doubt_loop_on_missed| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("5" (USE "next_broadcast_slot") (("5" (GROUND) NIL NIL)) NIL) ("6" (ASSERT) NIL NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "before2" :POLARITY? T :SUBST ("x" "x!1")) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (USE "not_prev_broadcaster_before" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL)) NIL) ("11" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("11" (GROUND) NIL NIL)) NIL) ("12" (USE "all_faulty_after_prev_invariant") (("12" (GROUND) NIL NIL)) NIL) ("13" (SKOSIMP*) (("13" (HIDE -8 -10) (("13" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MYSUCC "x!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_loop_on_disagree_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_doubt_loop_on_disagree| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("5" (USE "next_broadcast_slot" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (GROUND) NIL NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "before2" :POLARITY? T :SUBST ("x" "x!1")) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (USE "not_prev_broadcaster_before" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL)) NIL) ("11" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("11" (GROUND) NIL NIL)) NIL) ("12" (USE "all_faulty_after_prev_invariant") (("12" (GROUND) NIL NIL)) NIL) ("13" (SKOSIMP*) (("13" (HIDE -8 -10) (("13" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!2,remove(xs!1, add(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1),add(x!3, remove(x!2, difference(add(x!2, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL) ("3" (LEMMA "congruence[proc,bool]") (("3" (INST - "add(x!3,add(xs!1, remove(x!2, difference(add(x!2, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("3" (GROUND) NIL NIL)) NIL)) NIL) ("4" (LEMMA "congruence[proc,bool]") (("4" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!3, difference(add(x!3, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("4" (GROUND) NIL NIL)) NIL)) NIL) ("5" (LEMMA "congruence[proc,bool]") (("5" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("5" (GROUND) NIL NIL)) NIL)) NIL) ("6" (LEMMA "congruence[proc,bool]") (("6" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("6" (GROUND) NIL NIL)) NIL)) NIL) ("7" (LEMMA "congruence[proc,bool]") (("7" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!3, difference(add(x!3, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("7" (GROUND) NIL NIL)) NIL)) NIL) ("8" (LEMMA "congruence[proc,bool]") (("8" (INST - "add(broadcaster(t!1),add(x!3, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("8" (GROUND) NIL NIL)) NIL)) NIL) ("9" (LEMMA "congruence[proc,bool]") (("9" (INST - "add(x!3,add(xs!1, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (LEMMA "congruence[proc,bool]") (("10" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!3, difference(add(x!3, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("10" (GROUND) NIL NIL)) NIL)) NIL) ("11" (APPLY-EXTENSIONALITY 9 :HIDE? T) (("11" (LAZY-REDUCE) NIL NIL)) NIL) ("12" (APPLY-EXTENSIONALITY 9 :HIDE? T) (("12" (LAZY-REDUCE) NIL NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1),remove(xs!1, add(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1),remove(xs!1, add(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1),add(xs!1, remove(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (MYSUCC "x!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_doubt_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("5" (USE "next_broadcast_slot" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "before2" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "before2" :POLARITY? T :SUBST ("x" "x!1")) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -8 -10) (("12" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MYSUCC "x!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (ACC-REJ- "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_to_stable_on_x| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -8 -10) (("8" (GROUND) (("1" (MEM "p!1") NIL NIL) ("2" (MEM "p!1") NIL NIL) ("3" (USE "shutdown") (("3" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("4" (USE "shutdown") (("4" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("5" (USE "shutdown") (("5" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("6" (USE "shutdown") (("6" (GROUND) (("1" (PREV- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("7" (USE "shutdown") (("7" (GROUND) (("1" (DOUBT- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_to_stable| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (REWRITE "before1") NIL NIL) ("4" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("4" (GROUND) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (USE "not_prev_broadcaster_before" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL)) NIL) ("6" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_after_prev_invariant") (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -8 -10) (("8" (GROUND) (("1" (MEM "p!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - " add(broadcaster(t!1),remove(xs!1, add(x!1, difference(add(x!1, the_mem(t!1)), S!1))))" " the_mem(t!1)" "xs!1" "xs!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (MEM "p!1") NIL NIL) ("3" (ACC-REJ "p!1") NIL NIL) ("4" (ACC-REJ "p!1") NIL NIL) ("5" (ACC-REJ "p!1") NIL NIL) ("6" (PREV "p!1") NIL NIL) ("7" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_to_pending_selfdiag_on_disagree_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_to_pending_selfdiag_on_disagree| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded") (("" (EXPAND "pending_selfdiag") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (GROUND) NIL NIL) ("6" (INST + "broadcaster(t!1)") (("6" (GROUND) (("6" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -7 -9) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(x!2, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1),remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1),remove(x!2, difference(add(x!2, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1),remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ) NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_to_pending_selfdiag_on_missed_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_to_pending_selfdiag_on_missed| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded") (("" (EXPAND "pending_selfdiag") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (GROUND) NIL NIL) ("6" (INST + "broadcaster(t!1)") (("6" (GROUND) (("6" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -7 -9) (("12" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_loop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_loop| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (ASSERT) NIL NIL) ("6" (SKOSIMP*) (("6" (INST + "q!1") (("6" (GROUND) (("6" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -8 -10) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(x!2, difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" " the_mem(t!1)" "x!1" "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" " the_mem(t!1)" "q!1" "q!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1,difference(add(x!1, the_mem(t!1)), S!1)))" " the_mem(t!1)" "q!1" "q!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1), remove(x!2,difference(add(x!1, the_mem(t!1)), S!1)))" " the_mem(t!1)" "q!1" "q!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1,difference(add(x!1, the_mem(t!1)), S!1)))" " the_mem(t!1)" "q!1" "q!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_loop_on_missed_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_loop_on_missed| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (ASSERT) NIL NIL) ("6" (SKOSIMP*) (("6" (INST + "q!1") (("6" (GROUND) (("6" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -8 -10) (("12" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (INST + "q!1") (("5" (GROUND) (("5" (FORWARD-CHAIN "faulty_mem") NIL NIL)) NIL)) NIL)) NIL) ("6" (USE "before2" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (SKOSIMP*) (("11" (HIDE -8 -10) (("11" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ- "z!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_to_excluded_doubt_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_to_excluded_doubt| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (EXPAND "excluded_doubt") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("5" (USE "next_broadcast_slot" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "before2" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (REWRITE "before1") NIL NIL) ("9" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (USE "not_prev_broadcaster_before" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL)) NIL) ("11" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("11" (GROUND) NIL NIL)) NIL) ("12" (USE "all_faulty_after_prev_invariant") (("12" (GROUND) NIL NIL)) NIL) ("13" (SKOSIMP*) (("13" (HIDE -8 -10) (("13" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (INST + "x!3") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "x!3") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (MYSUCC "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1))) " " the_mem(t!1)" "x!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("6" (MEM "p!1") NIL NIL) ("7" (MEM "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_to_stable| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -8 -10) (("8" (GROUND) (("1" (MEM- "p!1") NIL NIL) ("2" (MEM- "p!1") NIL NIL) ("3" (USE "shutdown") (("3" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (USE "shutdown") (("4" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("5" (USE "shutdown") (("5" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("6" (USE "shutdown") (("6" (GROUND) (("1" (PREV- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("7" (USE "shutdown") (("7" (GROUND) (("1" (DOUBT- "p!1") NIL NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_broadcaster_since_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_broadcaster_since| "" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (FLATTEN) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|latent_to_missed_rcv_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_to_missed_rcv| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "latent_x_is_faulty") (("" (EXPAND "latent") (("" (EXPAND "missed_rcv") (("" (REW) (("" (USE "faulty_receiver" :SUBST ("t" "t!1-1" "p" "x!1")) (("" (FLATTEN) (("" (HIDE -4) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL) ("5" (REWRITE "before1") NIL NIL) ("6" (USE "another_nonfaulty_before_broadcaster_exists" :SUBST ("t" "t!1" "z" "z!1")) (("6" (SKOSIMP*) (("6" (INST?) (("6" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("7" (SKOSIMP*) (("7" (REWRITE "not_prev_broadcaster_before") NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (USE "another_nonfaulty_before_broadcaster_exists" :SUBST ("t" "t!1" "z" "z!1")) (("8" (SKOSIMP*) (("8" (INST + "p!3") (("8" (GROUND) (("8" (USE "before2" :SUBST ("t" "t!1" "x" "p!3" "y" "z!1")) (("8" (GROUND) (("1" (REPLACE*) (("1" (REWRITE "before_irreflexive") NIL NIL)) NIL) ("2" (USE "before_total" :POLARITY? T) (("2" (GROUND) (("2" (INST - "p!3") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("9" (USE "all_faulty_after_prev_invariant") (("9" (GROUND) NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (HIDE -5 -7) (("10" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (PREV "x!1") NIL NIL) ("3" (DOUBT "x!1") NIL NIL) ("4" (MEM "p!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (ACC-REJ "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (PREV "p!1") NIL NIL) ("9" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_loop_on_other_broadcaster_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_loop_on_other_broadcaster| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (GROUND) NIL NIL) ("5" (HIDE-ALL-BUT (-1 -3 -4 -5 1 5)) (("5" (CASE "i!1=n-1") (("1" (USE "next_b_prop" :SUBST ("t" "t!1-i!1")) (("1" (SKOSIMP*) (("1" (HIDE -3) (("1" (INST - "i!1-s!1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("6" (SKOSIMP*) (("6" (CASE "s!1=1") (("1" (GROUND) NIL NIL) ("2" (INST - "s!1-1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -5 -8 -10) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "difference(add(x!1, the_mem(t!1)), S!1)" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "difference(add(x!1, the_mem(t!1)), S!1)" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (LEMMA "congruence[proc,bool]") (("3" (INST - "difference(add(x!1, the_mem(t!1)), S!1)" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (LEMMA "congruence[proc,bool]") (("4" (INST - "difference(add(x!1, the_mem(t!1)), S!1)" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (PREV "x!1") NIL NIL) ("3" (DOUBT "x!1") NIL NIL) ("4" (MEM "p!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (ACC-REJ "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (PREV "p!1") NIL NIL) ("9" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (CASE "i!1=n-1") (("1" (USE "next_b_prop" :SUBST ("t" "t!1-i!1")) (("1" (SKOSIMP*) (("1" (HIDE -3) (("1" (INST - "i!1-s!1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (CASE "s!1=1") (("1" (GROUND) NIL NIL) ("2" (INST - "s!1-1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("6" (USE "before2" :POLARITY? T) (("6" (SKOSIMP*) (("6" (ASSERT) NIL NIL)) NIL)) NIL) ("7" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (GROUND) (("11" (SKOSIMP*) (("11" (HIDE -5 -8 -10) (("11" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") (("2" (PREV "x!1") NIL NIL)) NIL) ("3" (DOUBT "x!1") NIL NIL) ("4" (MEM "p!1") NIL NIL) ("5" (MEM- "p!1") NIL NIL) ("6" (ACC-REJ- "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (PREV- "p!1") NIL NIL) ("9" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_to_excluded_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_to_excluded| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (EXPAND "excluded") (("" (REW) (("" (GROUND) (("1" (GROUND) NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "before2" :POLARITY? T) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (REPLACE -12 :DIR RL) (("9" (INST + "y!1") (("9" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (REWRITE "before1") NIL NIL)) NIL)) NIL)) NIL) ("10" (SKOSIMP*) (("10" (HIDE -5 -8 -10) (("10" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM- "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (ACC-REJ- "p!1") NIL NIL) ("10" (PREV- "p!1") NIL NIL) ("11" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_to_stable| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -5 -8 -10) (("8" (GROUND) (("1" (MEM "p!1") NIL NIL) ("2" (USE "shutdown") (("2" (MEM- "p!1") NIL NIL)) NIL) ("3" (USE "shutdown") (("3" (ASSERT) (("3" (ACC-REJ- "p!1") NIL NIL)) NIL)) NIL) ("4" (USE "shutdown") (("4" (ASSERT) (("4" (ACC-REJ- "p!1") NIL NIL)) NIL)) NIL) ("5" (USE "shutdown") (("5" (ASSERT) (("5" (ACC-REJ- "p!1") NIL NIL)) NIL)) NIL) ("6" (USE "shutdown") (("6" (ASSERT) (("6" (PREV- "p!1") NIL NIL)) NIL)) NIL) ("7" (USE "shutdown") (("7" (ASSERT) (("7" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_to_excluded_z_not_ack_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_to_excluded_z_not_ack| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (EXPAND "excluded_z_not_ack") (("" (REW) (("" (GROUND) (("1" (GROUND) NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "before2" :POLARITY? T) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (REPLACE -12 :DIR RL) (("9" (REWRITE "before1") NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (HIDE -5 -8 -10) (("10" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (FORWARD-CHAIN "faults_latch_rev") (("6" (INST-CP - "broadcaster(t!1)") (("6" (INST - "p!1") (("6" (REWRITE "newmem") (("6" (ASSERT) (("6" (USE "sending" :SUBST ("t" "t!1")) (("6" (USE "arrival" :SUBST ("p" "p!1" "t" "t!1")) (("6" (ASSERT) (("6" (LIFT-IF) (("6" (REPLACE*) (("6" (ASSERT) (("6" (BDDSIMP +) (("1" (LAZY-REDUCE) (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(z!1, add(x!2, add(x!2, the_mem(t!1))))" "difference(add(x!2, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (LAZY-REDUCE) NIL NIL) ("3" (LAZY-REDUCE) NIL NIL) ("4" (LAZY-REDUCE) NIL NIL) ("5" (LAZY-REDUCE) NIL NIL) ("6" (FLATTEN) (("6" (ASSERT) (("6" (SPLIT -11) (("1" (PROPAX) NIL NIL) ("2" (FLATTEN) (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, the_mem(t!1))" "difference(add(x!1, the_mem(t!1)), S!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (LAZY-REDUCE) NIL NIL) ("8" (ASSERT) (("8" (BDDSIMP) (("1" (REPLACE*) (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, the_mem(t!1))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, the_mem(t!1))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (ACC-REJ "p!1") (("7" (LEMMA "congruence[proc,bool]") (("7" (INST - "add(z!1, add(x!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("7" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(z!1, add(x!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, remove(z!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "q!1" "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("10" (DOUBT "p!1") (("10" (LEMMA "congruence[proc,bool]") (("10" (INST - "add(x!1, remove(z!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "q!1" "q!1") (("10" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|x_not_broadcaster_in_excluded_z_not_ack| "" (SKOSIMP*) (("" (EXPAND "excluded_z_not_ack") (("" (REW) (("" (GROUND) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_not_ack_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "x_not_broadcaster_in_excluded_z_not_ack") (("" (EXPAND "excluded_z_not_ack") (("" (REW) (("" (ASSERT) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (INST? :POLARITY? T) (("5" (GROUND) (("5" (USE "before2" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("6" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "before2" :SUBST ("t" "t!1" "x" "z!1" "y" "x!1")) (("10" (GROUND) NIL NIL)) NIL) ("11" (SKOSIMP*) (("11" (HIDE -8 -10) (("11" (GROUND) (("1" (MEM- "x!1") NIL NIL) ("2" (ACC-REJ- "x!1") NIL NIL) ("3" (PREV- "x!1") NIL NIL) ("4" (DOUBT- "x!1") NIL NIL) ("5" (MEM- "p!1") NIL NIL) ("6" (MEM- "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (PREV- "p!1") NIL NIL) ("10" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_to_excluded_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_not_ack_to_excluded| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "x_not_broadcaster_in_excluded_z_not_ack") (("" (EXPAND "excluded_z_not_ack") (("" (EXPAND "excluded") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (GROUND) NIL NIL) ("6" (REWRITE "before1") NIL NIL) ("7" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (USE "not_prev_broadcaster_before" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL)) NIL) ("9" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "all_faulty_after_prev_invariant") (("10" (GROUND) NIL NIL)) NIL) ("11" (INST + "z!1") (("11" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (USE "before2" :SUBST ("t" "t!1" "x" "z!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -8 -10) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(x!2, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1), remove(x!2, difference(add(x!2, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_to_excluded_z_doubt_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_to_excluded_z_doubt| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (EXPAND "excluded_z_doubt") (("" (REW) (("" (GROUND) (("1" (GROUND) NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "before2" :SUBST ("t" "t!1" "y" "z!1")) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (REPLACE -12 :DIR RL) (("9" (REWRITE "before1") NIL NIL)) NIL) ("10" (SKOSIMP*) (("10" (HIDE -5 -8 -10) (("10" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (FORWARD-CHAIN "faults_latch_rev") (("6" (INST-CP - "broadcaster(t!1)") (("6" (INST - "p!1") (("6" (REWRITE "newmem") (("6" (ASSERT) (("6" (USE "sending" :SUBST ("t" "t!1")) (("6" (USE "arrival" :SUBST ("p" "p!1" "t" "t!1")) (("6" (ASSERT) (("6" (LIFT-IF) (("6" (REPLACE*) (("6" (ASSERT) (("6" (BDDSIMP +) (("1" (LAZY-REDUCE) (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(z!1, add(x!2, add(x!2, the_mem(t!1))))" "difference(add(x!2, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (LAZY-REDUCE) NIL NIL) ("3" (LAZY-REDUCE) NIL NIL) ("4" (LAZY-REDUCE) NIL NIL) ("5" (LAZY-REDUCE) NIL NIL) ("6" (ASSERT) (("6" (REPLACE*) (("6" (BDDSIMP) (("6" (REPLACE*) (("6" (LEMMA "congruence[proc,bool]") (("6" (INST - "add(x!1, the_mem(t!1))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("6" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (LAZY-REDUCE) NIL NIL) ("8" (LAZY-REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (ACC-REJ "p!1") (("7" (LEMMA "congruence[proc,bool]") (("7" (INST - "add(z!1, add(x!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("7" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") (("9" (INST + "x!3") (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (DOUBT "p!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(z!1, add(x!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (GROUND) NIL NIL)) NIL)) NIL) ("11" (MYSUCC "z!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(z!1, add(x!1, add(x!1, the_mem(t!1))))" "difference(add(x!1, the_mem(t!1)), S!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (INST + "x!2") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|x_not_broadcaster_in_excluded_z_doubt| "" (SKOSIMP*) (("" (EXPAND "excluded_z_doubt") (("" (REW) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_doubt_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "excluded_z_doubt") (("" (REW) (("" (ASSERT) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "before2" :SUBST ("t" "t!1" "y" "z!1")) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "before2" :SUBST ("t" "t!1" "y" "x!1")) (("10" (GROUND) NIL NIL)) NIL) ("11" (SKOSIMP*) (("11" (HIDE -8 -10) (("11" (GROUND) (("1" (MEM "x!1") NIL NIL) ("2" (ACC-REJ- "x!1") NIL NIL) ("3" (PREV "x!1") NIL NIL) ("4" (DOUBT "x!1") NIL NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL) ("11" (MYSUCC "z!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_to_excluded_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_doubt_to_excluded| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "x_not_broadcaster_in_excluded_z_doubt") (("" (EXPAND "excluded_z_doubt") (("" (EXPAND "excluded") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faults_latch") (("1" (ASSERT) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (USE "next_broadcast_slot" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (GROUND) NIL NIL) ("6" (REWRITE "before1") NIL NIL) ("7" (USE "nonfaulty_before_broadcaster_not_prev_exists") (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (USE "not_prev_broadcaster_before" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL)) NIL) ("9" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "all_faulty_after_prev_invariant") (("10" (GROUND) NIL NIL)) NIL) ("11" (INST + "z!1") (("11" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (USE "before2" :SUBST ("t" "t!1" "x" "z!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -8 -10) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(x!2, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(broadcaster(t!1), remove(x!2, difference(add(x!2, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "the_mem(t!1)" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (ACC-REJ "p!1") NIL NIL) ("10" (PREV "p!1") NIL NIL) ("11" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_to_missed_rcv_x_not_ack_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_to_missed_rcv_x_not_ack| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "latent_x_is_faulty") (("" (EXPAND "latent") (("" (EXPAND "missed_rcv_x_not_ack") (("" (REW) (("" (USE "faulty_receiver" :SUBST ("t" "t!1-1" "p" "x!1")) (("" (FLATTEN) (("" (CASE-REPLACE "x!1=y!1") (("1" (USE "before_irreflexive" :SUBST ("x" "x!1" "t" "t!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL) ("4" (REWRITE "before1") NIL NIL) ("5" (USE "another_nonfaulty_before_broadcaster_exists" :SUBST ("t" "t!1" "z" "y!1")) (("5" (SKOSIMP*) (("5" (INST?) (("5" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("6" (SKOSIMP*) (("6" (REWRITE "not_prev_broadcaster_before") NIL NIL)) NIL) ("7" (SKOSIMP*) (("7" (INST + "p!2") (("7" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (USE "before2" :SUBST ("x" "p!2" "y" "y!1" "t" "t!1")) (("2" (GROUND) (("2" (USE "two_nonfaulty_before_broadcaster_exist" :SUBST ("t" "t!1")) (("2" (SKOSIMP*) (("2" (REVEAL 1) (("2" (INST + "p!3") (("2" (GROUND) (("2" (USE "before2" :SUBST ("x" "p!3" "y" "y!1" "t" "t!1")) (("2" (GROUND) (("1" (REPLACE*) (("1" (REWRITE "before_irreflexive") NIL NIL)) NIL) ("2" (USE "before_total" :POLARITY? T) (("2" (GROUND) (("1" (INST -11 "p!3") (("1" (GROUND) (("1" (USE "before_total" :POLARITY? T) (("1" (GROUND) (("1" (INST -10 "p!3") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REVEAL 1) (("2" (INST + "q!1") (("2" (GROUND) (("2" (USE "before2" :SUBST ("x" "q!1" "y" "y!1" "t" "t!1")) (("2" (GROUND) (("1" (REPLACE*) (("1" (USE "before_irreflexive" :POLARITY? T) NIL NIL)) NIL) ("2" (USE "before_total" :POLARITY? T) (("2" (GROUND) (("2" (INST -12 "q!1") (("2" (GROUND) (("2" (USE "before_total" :POLARITY? T) (("2" (INST -11 "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (USE "all_faulty_after_prev_invariant" :SUBST ("z" "y!1" "t" "t!1")) (("8" (GROUND) (("8" (HIDE 2) (("8" (SKOSIMP*) (("8" (INST -8 "p!1") (("8" (GROUND) (("8" (USE "before_total" :POLARITY? T) (("8" (GROUND) (("8" (INST?) (("8" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("9" (SKOSIMP*) (("9" (HIDE -5 -7) (("9" (GROUND) (("1" (USE "faulty_receiver" :SUBST ("t" "t!1-1")) (("1" (MEM "x!1") NIL NIL)) NIL) ("2" (USE "faulty_receiver" :SUBST ("t" "t!1-1")) (("2" (ACC-REJ "x!1") NIL NIL)) NIL) ("3" (USE "faulty_receiver" :SUBST ("t" "t!1-1")) (("3" (PREV "x!1") NIL NIL)) NIL) ("4" (USE "faulty_receiver" :SUBST ("t" "t!1-1")) (("4" (DOUBT "x!1") NIL NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_loop_on_ignore_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_ack_loop_on_ignore| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv_x_not_ack") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "i!1=n") (("1" (INST-CP - "n") (("1" (ASSERT) (("1" (USE "next_b_prop" :SUBST ("t" "t!1-n")) (("1" (SKOSIMP*) (("1" (INST -9 "n-s!1") (("1" (GROUND) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("6" (SKOSIMP*) (("6" (INST - "s!1-1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("7" (REWRITE "before1") NIL NIL) ("8" (USE "nonfaulty_before_broadcaster_not_prev_exists" :SUBST ("z" "z!1")) (("8" (GROUND) NIL NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "not_prev_broadcaster_before" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL)) NIL) ("10" (USE "nonfaulty_before_prev_exists_invariant" :POLARITY? T :SUBST ("z" "z!1")) (("10" (GROUND) NIL NIL)) NIL) ("11" (USE "all_faulty_after_prev_invariant") (("11" (GROUND) NIL NIL)) NIL) ("12" (SKOSIMP*) (("12" (HIDE -5 -8 -10) (("12" (GROUND) (("1" (MEM "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1, add(x!2, difference(add(x!1, the_mem(t!1)), S!1)))" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (ACC-REJ "x!1") (("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (PREV "x!1") (("1" (LEMMA "congruence[proc,bool]") (("1" (INST - "add(x!1,add(broadcaster(t!1), difference(add(x!1, the_mem(t!1)), S!1)))" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "congruence[proc,bool]") (("2" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (DOUBT "x!1") (("4" (LEMMA "congruence[proc,bool]") (("4" (INST - "add(broadcaster(t!1), remove(x!1, difference(add(x!1, the_mem(t!1)), S!1)))" "add(x!1, the_mem(t!1))" "z!1" "z!1") (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (MEM "p!1") NIL NIL) ("6" (MEM "p!1") NIL NIL) ("7" (ACC-REJ "p!1") NIL NIL) ("8" (ACC-REJ "p!1") NIL NIL) ("9" (PREV "p!1") NIL NIL) ("10" (DOUBT "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_loop_on_dead_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_ack_loop_on_dead| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv_x_not_ack") (("" (REW) (("" (GROUND) (("1" (USE "faults_latch" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("4" (CASE "i!1=n") (("1" (INST-CP - "n") (("1" (ASSERT) (("1" (USE "next_b_prop" :SUBST ("t" "t!1-n")) (("1" (SKOSIMP*) (("1" (INST -9 "n-s!1") (("1" (GROUND) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("5" (SKOSIMP*) (("5" (INST - "s!1-1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("6" (USE "before2" :POLARITY? T) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("8" (GROUND) NIL NIL)) NIL) ("9" (USE "non_faulty_before_exists_invariant" :POLARITY? T) (("9" (GROUND) NIL NIL)) NIL) ("10" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("10" (GROUND) NIL NIL)) NIL) ("11" (SKOSIMP*) (("11" (HIDE -5 -8 -10) (("11" (GROUND) (("1" (MEM- "x!1") NIL NIL) ("2" (ACC-REJ- "x!1") NIL NIL) ("3" (PREV- "x!1") NIL NIL) ("4" (DOUBT- "x!1") NIL NIL) ("5" (MEM- "p!1") NIL NIL) ("6" (MEM- "p!1") NIL NIL) ("7" (ACC-REJ- "p!1") NIL NIL) ("8" (ACC-REJ- "p!1") NIL NIL) ("9" (PREV- "p!1") NIL NIL) ("10" (DOUBT- "p!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_to_stable| "" (BETA) (("" (SKOSIMP*) (("" (EXPAND "missed_rcv_x_not_ack") (("" (EXPAND "stable") (("" (REW) (("" (GROUND) (("1" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("2" (FORWARD-CHAIN "faulty_mem") NIL NIL) ("3" (USE "before2" :POLARITY? T) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (USE "nonfaulty_before_prev_not_prevprev_exists_invariant" :POLARITY? T) (("4" (GROUND) NIL NIL)) NIL) ("5" (USE "all_faulty_after_prev_faulty_broadcaster_invariant" :POLARITY? T) (("5" (GROUND) NIL NIL)) NIL) ("6" (USE "non_faulty_before_exists_invariant" :SUBST ("t" "t!1")) (("6" (GROUND) NIL NIL)) NIL) ("7" (USE "all_faulty_between_prev_and_prevprev_invariant" :POLARITY? T) (("7" (GROUND) NIL NIL)) NIL) ("8" (SKOSIMP*) (("8" (HIDE -5 -8 -10) (("8" (GROUND) (("1" (MEM- "p!1") NIL NIL) ("2" (USE "shutdown") (("2" (MEM- "p!1") NIL NIL)) NIL) ("3" (USE "shutdown") (("3" (ASSERT) (("3" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (USE "shutdown") (("4" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("5" (USE "shutdown") (("5" (GROUND) (("1" (ACC-REJ- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("6" (USE "shutdown") (("6" (GROUND) (("1" (PREV- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("7" (USE "shutdown") (("7" (GROUND) (("1" (DOUBT- "p!1") NIL NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|latent_is_nonstable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "latent_x_is_faulty") (("" (EXPAND "latent") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -7 -9 -13 -15) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "excluded") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -7 -9 -14 -16) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "excluded_doubt") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -7 -9 -14 -16) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "pending_selfdiag") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -4 -6 -10 -12) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "missed_rcv") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -7 -9 -14 -16) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "excluded_z_not_ack") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -8 -10 -15 -17) (("" (INST - "x!1") (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "excluded_z_doubt") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -8 -10 -15 -17) (("" (INST - "x!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_is_nonstable| "" (SKOSIMP*) (("" (EXPAND "missed_rcv_x_not_ack") (("" (EXPAND "stable") (("" (REW) (("" (FLATTEN) (("" (HIDE -5 -8 -10 -116 -14) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|always_non_stable_is_no_more_faults| "" (SKOLEM 1 ("t!1" "y!1" "z!1")) (("" (FLATTEN) (("" (INDUCT "s") (("1" (GROUND) NIL NIL) ("2" (SKOSIMP*) (("2" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1+j!1" "y" "y!1" "z" "z!1")) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|stable_successors| "" (BETA) (("" (SKOSIMP*) (("" (FORWARD-CHAIN "fault_may_occur_when_stable") (("1" (USE "stable_to_stable_non_faulty" :POLARITY? T) (("1" (GROUND) (("1" (USE "stable_to_stable_faulty" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST + "x!1") (("2" (INST + "x!1") (("2" (USE "stable_to_latent_non_faulty" :POLARITY? T) (("2" (GROUND) (("2" (USE "stable_to_latent_faulty" :POLARITY? T :SUBST ("y" "y!1" "z" "z!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|latent_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|latent_successors| "" (BETA) (("" (SKOSIMP*) (("" (USE "no_faults_when_not_stable") (("" (GROUND) (("1" (USE "latent_to_excluded" :POLARITY? T) (("1" (GROUND) (("1" (USE "latent_to_missed_rcv" :POLARITY? T) (("1" (GROUND) (("1" (USE "latent_to_missed_rcv_x_not_ack" :POLARITY? T) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "latent_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable") (("" (PROP) (("1" (USE "excluded_loop" :POLARITY? T) (("1" (ASSERT) (("1" (USE "x_not_broadcaster_in_excluded") (("1" (ASSERT) (("1" (USE "excluded_to_excluded_doubt") (("1" (ASSERT) (("1" (USE "excluded_to_pending_selfdiag_on_missed") (("1" (ASSERT) (("1" (USE "excluded_to_pending_selfdiag_on_disagree") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "excluded_is_nonstable") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_doubt_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1")) (("" (PROP) (("1" (USE "excluded_doubt_loop_on_dead") (("1" (ASSERT) (("1" (USE "excluded_doubt_loop_on_missed") (("1" (ASSERT) (("1" (USE "excluded_doubt_loop_on_disagree") (("1" (ASSERT) (("1" (USE "excluded_doubt_to_stable_on_x") (("1" (ASSERT) (("1" (USE "excluded_doubt_to_stable") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "excluded_doubt_is_nonstable") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1")) (("" (GROUND) (("1" (USE "pending_selfdiag_loop_on_dead") (("1" (USE "pending_selfdiag_loop") (("1" (USE "pending_selfdiag_loop_on_missed") (("1" (USE "pending_selfdiag_to_stable") (("1" (USE "pending_selfdiag_to_excluded_doubt") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "pending_selfdiag_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_successors_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1")) (("" (PROP) (("1" (USE "missed_rcv_loop_on_other_broadcaster" :POLARITY? T) (("1" (ASSERT) (("1" (USE "missed_rcv_loop_on_dead") (("1" (ASSERT) (("1" (USE "missed_rcv_to_stable") (("1" (ASSERT) (("1" (USE "missed_rcv_to_excluded") (("1" (ASSERT) (("1" (USE "missed_rcv_to_excluded_z_doubt") (("1" (ASSERT) (("1" (USE "missed_rcv_to_excluded_z_not_ack") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "missed_rcv_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_not_ack_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable") (("" (PROP) (("1" (USE "x_not_broadcaster_in_excluded_z_not_ack") (("1" (GROUND) (("1" (USE "excluded_z_not_ack_loop_on_dead") (("1" (USE "excluded_z_not_ack_to_excluded") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "excluded_z_not_ack_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_doubt_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable") (("" (PROP) (("1" (USE "x_not_broadcaster_in_excluded_z_doubt") (("1" (GROUND) (("1" (USE "excluded_z_doubt_loop_on_dead") (("1" (GROUND) (("1" (USE "excluded_z_doubt_to_excluded") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "excluded_z_doubt_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_successors_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_ack_successors| "" (BETA) (("" (SKOSIMP*) (("" (REW) (("" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1")) (("" (PROP) (("1" (USE "missed_rcv_x_not_ack_loop_on_ignore") (("1" (GROUND) (("1" (USE "missed_rcv_x_not_ack_loop_on_dead") (("1" (GROUND) (("1" (USE "missed_rcv_x_not_ack_to_stable") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "missed_rcv_x_not_ack_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|total_invariant| "" (SKOSIMP*) (("" (EXPAND "total") (("" (REW) (("" (PROP) (("1" (SKOSIMP*) (("1" (USE "stable_successors") (("1" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (SKOSIMP*) (("3" (INST? :FNUMS 2) NIL NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST? :FNUMS 2) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (USE "latent_successors") (("2" (PROP) (("1" (INST? :FNUMS 3) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 8) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 9) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (USE "excluded_successors") (("3" (PROP) (("1" (INST? :FNUMS 3) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 3) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 6) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST? :FNUMS 7) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (USE "excluded_z_not_ack_successors" :POLARITY? T) (("4" (PROP) (("1" (INST? :FNUMS 4) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 3) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (USE "excluded_z_doubt_successors" :POLARITY? T) (("5" (PROP) (("1" (INST? :FNUMS 5) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 3) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("6" (SKOSIMP*) (("6" (USE "pending_selfdiag_successors" :POLARITY? T) (("6" (PROP) (("1" (INST? :FNUMS 6) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 6) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 6) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST? :FNUMS 7) (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST? :FNUMS 1) (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("7" (SKOSIMP*) (("7" (USE "excluded_doubt_successors" :POLARITY? T) (("7" (PROP) (("1" (INST? :FNUMS 7) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 7) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 7) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST? :FNUMS 1) (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST? :FNUMS 1) (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("8" (SKOSIMP*) (("8" (USE "missed_rcv_successors" :POLARITY? T) (("8" (PROP) (("1" (INST? :FNUMS 8) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 8) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 3) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST? :FNUMS 5) (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST? :FNUMS 4) (("5" (ASSERT) NIL NIL)) NIL) ("6" (INST? :FNUMS 1) (("6" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("9" (SKOSIMP*) (("9" (USE "missed_rcv_x_not_ack_successors" :POLARITY? T) (("9" (PROP) (("1" (INST? :FNUMS 9) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? :FNUMS 9) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST? :FNUMS 1) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|totality| "" (INDUCT "t") (("1" (USE "initial") (("1" (EXPAND "total") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (USE "total_invariant") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|validity| "" (SKOSIMP*) (("" (USE "totality") (("" (EXPAND "total") (("" (REW) (("" (GROUND) (("1" (SKOSIMP*) (("1" (EXPAND "stable") (("1" (GROUND) (("1" (HIDE -7 -9) (("1" (INST - "p!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "stable") (("2" (GROUND) (("2" (HIDE -3 -5) (("2" (INST - "p!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (FORWARD-CHAIN "latent_x_is_faulty") (("3" (EXPAND "latent") (("3" (FLATTEN) (("3" (HIDE -12 -14) (("3" (INST - "p!1") (("3" (ASSERT) (("3" (SPLIT -13) (("1" (FLATTEN) (("1" (REPLACE -1) (("1" (REPLACE -2) (("1" (EXPAND "add") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (FORWARD-CHAIN "latent_x_is_faulty") (("4" (EXPAND "latent") (("4" (FLATTEN) (("4" (HIDE -8 -10) (("4" (INST - "p!1") (("4" (ASSERT) (("4" (FLATTEN) (("4" (INST + "x!1") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (EXPAND "excluded") (("5" (GROUND) (("5" (HIDE -11 -13) (("5" (INST - "p!1") (("5" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (SKOSIMP*) (("6" (EXPAND "excluded") (("6" (GROUND) (("6" (HIDE -7 -9) (("6" (INST - "p!1") (("6" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (SKOSIMP*) (("7" (EXPAND "excluded_z_not_ack") (("7" (GROUND) (("7" (HIDE -12 -14) (("7" (INST - "p!1") (("7" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (SKOSIMP*) (("8" (EXPAND "excluded_z_not_ack") (("8" (GROUND) (("8" (HIDE -8 -10) (("8" (INST - "p!1") (("8" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("9" (SKOSIMP*) (("9" (EXPAND "excluded_z_doubt") (("9" (GROUND) (("9" (HIDE -12 -14) (("9" (INST - "p!1") (("9" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("10" (SKOSIMP*) (("10" (EXPAND "excluded_z_doubt") (("10" (GROUND) (("10" (HIDE -8 -10) (("10" (INST - "p!1") (("10" (INST + "x!1") (("10" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("11" (SKOSIMP*) (("11" (EXPAND "pending_selfdiag") (("11" (GROUND) (("11" (HIDE -12 -14) (("11" (INST - "p!1") (("11" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("12" (SKOSIMP*) (("12" (EXPAND "pending_selfdiag") (("12" (GROUND) (("12" (HIDE -8 -10) (("12" (INST - "p!1") (("12" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("13" (SKOSIMP*) (("13" (EXPAND "excluded_doubt") (("13" (GROUND) (("13" (HIDE -12 -14) (("13" (INST - "p!1") (("13" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("14" (SKOSIMP*) (("14" (EXPAND "excluded_doubt") (("14" (GROUND) (("14" (HIDE -8 -10) (("14" (INST - "p!1") (("14" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("15" (SKOSIMP*) (("15" (EXPAND "missed_rcv") (("15" (GROUND) (("15" (HIDE -12 -14) (("15" (INST - "p!1") (("15" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("16" (SKOSIMP*) (("16" (EXPAND "missed_rcv") (("16" (GROUND) (("16" (HIDE -8 -10) (("16" (INST - "p!1") (("16" (INST + "x!1") (("16" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("17" (SKOSIMP*) (("17" (EXPAND "missed_rcv_x_not_ack") (("17" (GROUND) (("17" (HIDE -12 -14) (("17" (INST - "p!1") (("17" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("18" (SKOSIMP*) (("18" (EXPAND "missed_rcv_x_not_ack") (("18" (GROUND) (("18" (HIDE -8 -10) (("18" (INST - "p!1") (("18" (INST + "x!1") (("18" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|agreement| "" (SKOSIMP*) (("" (USE "totality") (("" (EXPAND "total") (("" (REW) (("" (GROUND) (("1" (SKOSIMP*) (("1" (EXPAND "stable") (("1" (GROUND) (("1" (HIDE -3 -5) (("1" (INST-CP - "p!1") (("1" (INST - "q!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "latent") (("2" (FLATTEN) (("2" (HIDE -7 -9) (("2" (INST-CP - "p!1") (("2" (INST - "q!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (EXPAND "excluded") (("3" (FLATTEN) (("3" (HIDE -7 -9) (("3" (INST-CP - "p!1") (("3" (INST - "q!1") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (EXPAND "excluded_z_not_ack") (("4" (FLATTEN) (("4" (HIDE -8 -10) (("4" (INST-CP - "p!1") (("4" (INST - "q!1") (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (EXPAND "excluded_z_doubt") (("5" (FLATTEN) (("5" (HIDE -8 -10) (("5" (INST-CP - "p!1") (("5" (INST - "q!1") (("5" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("6" (SKOSIMP*) (("6" (EXPAND "pending_selfdiag") (("6" (FLATTEN) (("6" (HIDE -8 -10) (("6" (INST-CP - "p!1") (("6" (INST - "q!1") (("6" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("7" (SKOSIMP*) (("7" (EXPAND "excluded_doubt") (("7" (FLATTEN) (("7" (HIDE -8 -10) (("7" (INST-CP - "p!1") (("7" (INST - "q!1") (("7" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("8" (SKOSIMP*) (("8" (EXPAND "missed_rcv") (("8" (FLATTEN) (("8" (HIDE -5 -8 -10) (("8" (INST-CP - "p!1") (("8" (INST - "q!1") (("8" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("9" (SKOSIMP*) (("9" (EXPAND "missed_rcv_x_not_ack") (("9" (FLATTEN) (("9" (HIDE -5 -8 -10) (("9" (INST-CP - "p!1") (("9" (INST - "q!1") (("9" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (USE "excluded_successors" :POLARITY? T) (("2" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (HIDE 1) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 1 2) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_doubt_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (USE "excluded_doubt_successors" :POLARITY? T) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (REVEAL -2) (("1" (EXPAND "excluded_doubt") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) (("2" (REVEAL -2) (("2" (EXPAND "excluded_doubt") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST?) (("3" (ASSERT) (("3" (REVEAL -2) (("3" (EXPAND "excluded_doubt") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (HIDE 1) (("4" (INST?) (("4" (REVEAL -2) (("4" (EXPAND "excluded_doubt") (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("5" (HIDE 1) (("5" (INST?) (("5" (REVEAL -2) (("5" (EXPAND "excluded_doubt") (("5" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pending_selfdiag_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (USE "pending_selfdiag_successors" :POLARITY? T) (("2" (REVEAL -2) (("2" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL) ("4" (HIDE 1) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (HIDE 1 2) (("5" (INST?) (("5" (ASSERT) (("5" (EXPAND "pending_selfdiag") (("5" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_loop_or_exit_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (USE "missed_rcv_successors" :POLARITY? T) (("2" (REVEAL -2) (("2" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (HIDE 1) (("3" (INST?) (("3" (ASSERT) (("3" (EXPAND "missed_rcv") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (HIDE 1 2) (("4" (INST?) (("4" (EXPAND "missed_rcv") (("4" (FLATTEN) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (HIDE 1 2 3) (("5" (INST?) (("5" (EXPAND "missed_rcv") (("5" (FLATTEN) (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("6" (HIDE 1 2 3 4) (("6" (INST?) (("6" (EXPAND "missed_rcv") (("6" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_not_ack_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (USE "excluded_z_not_ack_successors" :POLARITY? T) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|excluded_z_doubt_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP*) (("2" (HIDE -2) (("2" (USE "excluded_z_doubt_successors" :POLARITY? T) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_loop_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_x_not_ack_loop_or_exit| "" (SKOSIMP) (("" (INDUCT "s") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "missed_rcv_x_not_ack") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (USE "missed_rcv_x_not_ack_successors" :POLARITY? T) (("2" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "missed_rcv_x_not_ack") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (EXPAND "missed_rcv_x_not_ack") (("2" (GROUND) NIL NIL)) NIL)) NIL) ("3" (HIDE 1) (("3" (INST?) (("3" (GROUND) (("3" (EXPAND "missed_rcv_x_not_ack") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "excluded_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (CASE "NOT faulty(s!1+t!1,broadcaster(s!1+t!1))") (("1" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("1" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (SKOSIMP*) (("1" (HIDE -3) (("1" (ASSERT) (("1" (USE "excluded_to_excluded_doubt" :POLARITY? T) (("1" (GROUND) (("1" (HIDE 3) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "excluded_to_pending_selfdiag_on_missed" :POLARITY? T) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "excluded_to_pending_selfdiag_on_disagree" :POLARITY? T) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (USE "excluded_to_pending_selfdiag_on_disagree" :POLARITY? T) (("3" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "excluded_to_pending_selfdiag_on_missed" :POLARITY? T) (("2" (GROUND) (("2" (HIDE 1) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (USE "excluded_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1")) (("2" (PROP) (("1" (INST - "s!1") (("1" (DECOMPOSE-EQUALITY) (("1" (INST - "broadcaster(s!1+t!1)") (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!2") (("2" (SKOSIMP*) (("2" (HIDE -4) (("2" (USE "excluded_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "excluded_doubt_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (SKOSIMP*) (("1" (HIDE -4) (("1" (USE "excluded_doubt_to_stable" :POLARITY? T) (("1" (REVEAL -2) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "excluded_doubt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "excluded_doubt_to_stable_on_x" :POLARITY? T :SUBST ("t" "t!1+s!1")) (("2" (GROUND) (("2" (INST?) (("2" (EXPAND "excluded_doubt") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (USE "excluded_doubt_to_stable_on_x" :POLARITY? T :SUBST ("t" "t!1+s!1")) (("3" (GROUND) (("3" (INST?) (("3" (ASSERT) (("3" (EXPAND "excluded_doubt") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (USE "excluded_doubt_to_stable_on_x" :POLARITY? T :SUBST ("t" "t!1+s!1")) (("4" (GROUND) (("4" (INST?) (("4" (ASSERT) (("4" (EXPAND "excluded_doubt") (("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (SKOSIMP*) (("2" (HIDE -4) (("2" (USE "excluded_doubt_is_nonstable" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "pending_selfdiag_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (SKOSIMP*) (("1" (USE "pending_selfdiag_to_stable" :POLARITY? T :SUBST ("t" "t!1+s!1")) (("1" (GROUND) (("1" (HIDE 1) (("1" (INST?) (("1" (EXPAND "pending_selfdiag") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (USE "pending_selfdiag_is_nonstable" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_faulty_only_or_exit_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|missed_rcv_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "missed_rcv_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (SKOSIMP*) (("1" (USE "missed_rcv_to_excluded" :POLARITY? T :SUBST ("t" "t!1+s!1")) (("1" (ASSERT) (("1" (PROP) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "missed_rcv") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "missed_rcv_to_stable" :SUBST ("t" "t!1+s!1")) (("2" (GROUND) (("2" (HIDE 1 2 3 4) (("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "missed_rcv") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (USE "missed_rcv_to_stable" :SUBST ("t" "t!1+s!1")) (("3" (ASSERT) (("3" (GROUND) (("1" (HIDE 1 2 3) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "missed_rcv") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "missed_rcv_to_excluded_z_doubt" :SUBST ("t" "t!1+s!1")) (("2" (GROUND) (("1" (HIDE 2) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "missed_rcv") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "missed_rcv_to_excluded_z_not_ack" :SUBST ("t" "t!1+s!1")) (("2" (GROUND) (("2" (HIDE 2 3) (("2" (INST?) (("2" (GROUND) (("2" (EXPAND "missed_rcv") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (SKOSIMP*) (("2" (HIDE -3) (("2" (USE "missed_rcv_is_nonstable" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "excluded_z_not_ack_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (CASE "NOT faulty(s!1+t!1,broadcaster(s!1+t!1))") (("1" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("1" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (HIDE -3) (("1" (USE "excluded_z_not_ack_to_excluded" :POLARITY? T) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (HIDE -3) (("2" (USE "excluded_z_not_ack_is_nonstable" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1")) (("2" (PROP) (("1" (INST - "s!1") (("1" (DECOMPOSE-EQUALITY) (("1" (INST - "broadcaster(s!1+t!1)") (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!2") (("2" (HIDE -4) (("2" (USE "excluded_z_not_ack_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "excluded_z_doubt_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (CASE "NOT faulty(s!1+t!1,broadcaster(s!1+t!1))") (("1" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("1" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (HIDE -3) (("1" (USE "excluded_z_doubt_to_excluded" :POLARITY? T) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (HIDE -3) (("2" (USE "excluded_z_doubt_is_nonstable" :POLARITY? T) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1")) (("2" (PROP) (("1" (INST - "s!1") (("1" (DECOMPOSE-EQUALITY) (("1" (INST - "broadcaster(s!1+t!1)") (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!2") (("2" (HIDE -4) (("2" (USE "excluded_z_doubt_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_faulty_only_or_exit| "" (SKOSIMP*) (("" (USE "missed_rcv_x_not_ack_loop_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "always_non_stable_is_no_more_faults" :SUBST ("t" "t!1+s!1")) (("" (PROP) (("1" (INST - 1) (("1" (INST - "s!1") (("1" (SKOSIMP*) (("1" (HIDE -4) (("1" (USE "missed_rcv_x_not_ack_to_stable") (("1" (GROUND) (("1" (INST?) (("1" (EXPAND "missed_rcv_x_not_ack") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST - "s!1+s!2") (("2" (SKOSIMP*) (("2" (HIDE -4) (("2" (USE "missed_rcv_x_not_ack_is_nonstable") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_exit| "" (SKOSIMP*) (("" (USE "excluded_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "nonfaulty_broadcaster_exists") (("" (SKOSIMP*) (("" (INST - "s!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_exit| "" (SKOSIMP*) (("" (USE "excluded_doubt_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "next_b_prop" :SUBST ("x" "x!1" "t" "t!1")) (("" (SKOSIMP*) (("" (HIDE -3) (("" (INST - "s!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pending_selfdiag_exit| "" (SKOSIMP*) (("" (USE "pending_selfdiag_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "next_b_prop" :SUBST ("x" "x!1" "t" "t!1")) (("" (SKOSIMP*) (("" (HIDE -3) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_exit_TCC1| "" (TCC) NIL NIL) (|missed_rcv_exit| "" (SKOSIMP*) (("" (USE "missed_rcv_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "next_b_prop" :SUBST ("t" "t!1")) (("" (SKOSIMP*) (("" (HIDE -3) (("" (INST? :FNUMS -) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_exit| "" (SKOSIMP*) (("" (USE "excluded_z_not_ack_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "nonfaulty_broadcaster_exists") (("" (SKOSIMP*) (("" (INST - "s!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_exit| "" (SKOSIMP*) (("" (USE "excluded_z_doubt_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "nonfaulty_broadcaster_exists") (("" (SKOSIMP*) (("" (INST - "s!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_exit| "" (SKOSIMP*) (("" (USE "missed_rcv_x_not_ack_faulty_only_or_exit" :POLARITY? T) (("" (GROUND) (("" (USE "next_b_prop" :SUBST ("t" "t!1")) (("" (SKOSIMP*) (("" (HIDE -3) (("" (INST? :FNUMS -) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_doubt_eventually_stable| "" (USE "excluded_doubt_exit") NIL NIL) (|pending_selfdiag_eventually_stable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "pending_selfdiag_exit") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_doubt_eventually_stable") (("" (SKOSIMP*) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_eventually_stable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_exit") (("1" (SKOSIMP*) (("1" (FORWARD-CHAIN "pending_selfdiag_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "excluded_doubt_exit") (("2" (SKOSIMP*) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_not_ack_eventually_stable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_z_not_ack_exit") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_eventually_stable") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|excluded_z_doubt_eventually_stable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_z_doubt_exit") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "excluded_eventually_stable") (("" (SKOSIMP*) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_eventually_stable| "" (SKOSIMP*) (("" (FORWARD-CHAIN "missed_rcv_exit") (("1" (SKOSIMP*) (("1" (FORWARD-CHAIN "excluded_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "missed_rcv") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "excluded_z_doubt_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "missed_rcv") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (FORWARD-CHAIN "excluded_z_not_ack_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "missed_rcv") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP*) (("4" (INST?) (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|missed_rcv_x_not_ack_eventually_stable| "" (USE "missed_rcv_x_not_ack_exit") NIL NIL) (|latent_eventually_stable| "" (SKOSIMP*) (("" (USE "no_faults_when_not_stable" :SUBST ("t" "t!1")) (("" (GROUND) (("1" (USE "latent_to_excluded" :POLARITY? T) (("1" (GROUND) (("1" (FORWARD-CHAIN "excluded_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "latent_to_missed_rcv") (("2" (GROUND) (("1" (FORWARD-CHAIN "missed_rcv_eventually_stable") (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "latent_to_missed_rcv_x_not_ack") (("2" (GROUND) (("2" (FORWARD-CHAIN "missed_rcv_x_not_ack_exit") (("2" (SKOSIMP*) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|liveness| "" (SKOSIMP*) (("" (USE "fault_may_occur_when_stable") (("" (GROUND) (("1" (USE "stable_to_stable_non_faulty") (("1" (GROUND) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL) ("2" (USE "stable_to_stable_faulty") (("2" (GROUND) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (USE "stable_to_latent_non_faulty" :SUBST ("x" "x!1") :POLARITY? T) (("2" (GROUND) (("1" (USE "latent_eventually_stable" :POLARITY? T) (("1" (GROUND) (("1" (SKOSIMP*) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "stable_to_latent_faulty" :SUBST ("x" "x!1") :POLARITY? T) (("2" (GROUND) (("2" (USE "latent_eventually_stable" :POLARITY? T) (("2" (GROUND) (("2" (SKOSIMP*) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|self_diagnosis| "" (SKOSIMP*) (("" (USE "liveness") (("" (GROUND) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "stable") (("1" (FLATTEN) (("1" (HIDE -3 -4 -5 -6 -7) (("1" (INST - "x!1") (("1" (ASSERT) (("1" (USE "faults_latch_always" :SUBST ("p" "x!1" "t" "t!1+1" "i" "s!1-1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "no_faults_when_not_stable") (("2" (GROUND) (("2" (CASE "the_mem(t!1)(x!1)") (("1" (REPLACE -2 :DIR RL) (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (EXPAND "the_mem") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$../../../lib/NASA-mod/floor_div_props.pvs floor_div_props: THEORY BEGIN i,k: VAR int j: VAR nonzero_integer x: VAR real sgn(x): int = IF x >= 0 THEN 1 ELSE -1 ENDIF floor_val: LEMMA i >= k*j AND i < (k+1)*j IMPLIES floor(i/j) = k floor_small: LEMMA abs(i) < abs(j) IMPLIES floor(i/j) = IF i/j >= 0 THEN 0 ELSE -1 ENDIF floor_eq_0: LEMMA floor(x) = 0 IMPLIES x >= 0 AND x < 1 is_multiple: LEMMA integer?(i/j) = (EXISTS k: i = k*j) END floor_div_props $$$../../../lib/NASA-mod/floor_div_props.prf (|floor_div_props| (|floor_val| "" (SKOSIMP*) (("" (CASE "j!1 >= 0") (("1" (LEMMA "both_sides_div_pos_lt1") (("1" (INST -1 "j!1" "i!1" "(k!1 + 1) * j!1") (("1" (LEMMA "both_sides_div_pos_ge1") (("1" (INST -1 "j!1" "i!1" "k!1 * j!1") (("1" (FLATTEN) (("1" (HIDE -1 -3) (("1" (ASSERT) (("1" (CASE "floor(i!1 / j!1) > k!1 - 1 AND floor(i!1 / j!1) < k!1 + 1") (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -3 -4 -5 -6 -7) (("1" (CASE "integer_pred(floor(i!1 / j!1))") (("1" (ASSERT) (("1" (NAME "II" "floor(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))) ("2" (LEMMA "both_sides_div_neg_lt1") (("2" (INST -1 "j!1" "(k!1 + 1) * j!1" "i!1") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (LEMMA "both_sides_div_neg_ge1") (("1" (INST -1 "j!1" "k!1 * j!1" "i!1") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))) (|floor_small| "" (SKOSIMP*) (("" (LEMMA "pos_div_ge") (("" (INST?) (("" (LIFT-IF) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (LEMMA "floor_val") (("1" (INST -1 "-i!1" "-j!1" "0") (("1" (ASSERT) NIL))))) ("2" (LEMMA "floor_val") (("2" (INST?) (("2" (ASSERT) NIL))))) ("3" (LEMMA "floor_val") (("3" (INST -1 "-i!1" "-j!1" "-1") (("3" (ASSERT) NIL))))) ("4" (LEMMA "floor_val") (("4" (INST -1 "i!1" "j!1" "-1") (("4" (ASSERT) NIL))))))))))))))))))) (|floor_eq_0| "" (TCC) NIL) (|is_multiple| "" (SKOSIMP*) (("" (IFF 1) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (INST 1 "i!1/j!1") (("1" (ASSERT) NIL) ("2" (EXPAND "integer?") (("2" (PROPAX) NIL))))))) ("2" (FLATTEN) (("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "integer?") (("2" (PROPAX) NIL)))))))))))))))) $$$../../../lib/NASA-mod/mod.pvs mod: THEORY %------------------------------------------------------------------------ % % mod function as defined on page 82 of: % % Concrete Mathematics: A Foundation for Computer Science % by R. L. Graham, D. E. Knuth, and O. Patashnik % Addison-Wesley, 1989. % % (restricted to the integers, the definition cited above % allows real arguments as well) % % Author: % Paul S. Miner | email: p.s.miner@larc.nasa.gov % 1 South Wright St. / MS 130 | fax: (804) 864-4234 % NASA Langley Research Center | phone: (804) 864-6201 % Hampton, Virginia 23681 | %------------------------------------------------------------------------ BEGIN IMPORTING floor_div_props i,k,cc: VAR int m: VAR posnat n,a,b,c: VAR nat j: VAR nonzero_integer ml3: LEMMA abs(i - m * floor(i/m)) < m ml4: LEMMA abs(i + m * floor(-i/m)) < m mod(i,j): {k| abs(k) < abs(j)} = i-j*floor(i/j) mod_even: LEMMA integer?(i/j) IMPLIES mod(i,j) = 0 mod_neg: LEMMA mod(-i,j) = IF integer?(i/j) THEN 0 ELSE j - mod(i,j) ENDIF mod_neg_d: LEMMA mod(i,-j) = IF integer?(i/j) THEN 0 ELSE mod(i,j) - j ENDIF mod_eq_arg: LEMMA mod(j,j) = 0 mod_lt: LEMMA abs(i) < abs(j) IMPLIES mod(i,j) = IF sgn(i) = sgn(j) OR i = 0 THEN i ELSE i + j ENDIF mod_lt_nat: LEMMA n < m IMPLIES mod(n,m) = n mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m) mod_sum: LEMMA mod(i+k*j,j) = mod(i,j) mod_it_is: LEMMA a = b + m*c AND b < m IMPLIES b = mod(a,m) mod_Ada: LEMMA (EXISTS k: i = k*j + mod(i,j)) mod_zero: LEMMA mod(0,j) = 0 mod_one: LEMMA mod(1,j) = IF abs(j) = 1 THEN 0 ELSIF j > 0 THEN 1 ELSE j + 1 ENDIF mod_of_mod: LEMMA mod(i + mod(k,m), m) = mod(i+k, m) mod_pos: LEMMA mod(i,m) >= 0 AND mod(i,m) < m mod_below_m : JUDGEMENT mod(i,m) HAS_TYPE below(m) END mod $$$../../../lib/NASA-mod/mod.prf (|mod| (|ml3| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1") (("1" (FLATTEN) (("1" (ASSERT) NIL))))))) ("2" (TYPEPRED "floor(i!1 / m!1)") (("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))))) (|ml4| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (TYPEPRED "floor(-i!1 / m!1)") (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL))))))))))) ("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))) (|mod_TCC1| "" (SKOSIMP*) (("" (CASE "j!1 >= 0") (("1" (LEMMA "ml3") (("1" (INST?) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))) ("2" (LEMMA "ml4") (("2" (INST -1 "i!1" "-j!1") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))))))) (|mod_even| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (REWRITE "floor_int") (("1" (ASSERT) NIL) ("2" (EXPAND "integer?") (("2" (PROPAX) NIL))))))))) (|mod_neg| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "-i!1/j!1 = -(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (REWRITE "floor_neg") (("2" (LIFT-IF) (("2" (GROUND) (("2" (ASSERT) (("2" (CASE "integer?(--(i!1/j!1))") (("1" (EXPAND "integer?") (("1" (PROPAX) NIL))) ("2" (LEMMA "integers.closed_neg") (("2" (INST -1 "-(i!1/j!1)") (("2" (NAME "q" "i!1/j!1") (("2" (REPLACE -1) (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_neg_d| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "i!1/-j!1=-(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "floor_neg") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (CASE "integer_pred(--(i!1/j!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_eq_arg| "" (TCC) NIL) (|mod_lt| "" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (GRIND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (REWRITE "floor_small") (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL))))))) ("3" (REWRITE "floor_small") (("3" (LIFT-IF) (("3" (GROUND) (("3" (REWRITE "pos_div_ge") NIL))))))) ("4" (REWRITE "floor_small") (("4" (LIFT-IF) (("4" (GROUND) (("4" (REWRITE "pos_div_ge") NIL))))))))))))))))))) (|mod_lt_nat| "" (SKOSIMP*) (("" (REWRITE "mod_lt") (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))) (|mod_sum_pos| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*m!1/m!1" "i!1/m!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_sum| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*j!1/j!1" "i!1/j!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_it_is| "" (SKOSIMP*) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "mod_sum") (("" (INST - "b!1" "m!1" "c!1") (("" (REPLACE -1) (("" (HIDE -1) (("" (REWRITE "mod_lt") (("1" (LIFT-IF) (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))))))))))))) (|mod_Ada| "" (SKOLEM!) (("" (EXPAND "mod") (("" (INST + "floor(i!1/j!1)") (("" (ASSERT) NIL))))))) (|mod_zero| "" (TCC) NIL) (|mod_one| "" (GRIND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (REWRITE "floor_small") (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL))))))))) (|mod_of_mod| "" (SKOSIMP*) (("" (REWRITE "mod") (("" (LEMMA "mod_sum") (("" (INST - "i!1+k!1" "m!1" "-floor(k!1/m!1)") (("" (ASSERT) NIL))))))))) (|mod_pos| "" (SKOSIMP*) (("" (TYPEPRED "mod(i!1,m!1)") (("" (TCC) (("" (LEMMA "both_sides_times_pos_le1") (("" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1") (("" (ASSERT) NIL))))))))))) (|mod_below_m| "" (SKOSIMP*) (("" (ASSERT) (("" (REWRITE "mod_pos") NIL NIL)) NIL)) NIL)) $$$mod_props.pvs mod_props : THEORY BEGIN mod : LIBRARY = "../../../lib/NASA-mod/" IMPORTING mod@mod i, k : VAR int m : VAR posnat a : VAR nat mod_mod: lemma mod(mod(a, m),m) = mod(a,m) mod_of_mod_diff: LEMMA i>= k => mod(i - mod(k,m), m) = mod(i-k, m) mod_plus: lemma mod(i,m)+a mod(i,m)+a=mod(i+a,m) mod_minus: lemma mod(i,m)-a>=0 => mod(i,m)-a=mod(i-a,m) END mod_props $$$mod_props.prf (|mod_props| (|ml3| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1") (("1" (FLATTEN) (("1" (ASSERT) NIL))))))) ("2" (TYPEPRED "floor(i!1 / m!1)") (("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))))) (|ml4| "" (SKOSIMP*) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (GROUND) (("1" (TYPEPRED "floor(-i!1 / m!1)") (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)") (("1" (FLATTEN) (("1" (HIDE -1) (("1" (ASSERT) NIL))))))))))) ("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1") (("2" (FLATTEN) (("2" (HIDE -1) (("2" (ASSERT) NIL))))))))))))))))) (|mod_TCC1| "" (SKOSIMP*) (("" (CASE "j!1 >= 0") (("1" (LEMMA "ml3") (("1" (INST?) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))) ("2" (LEMMA "ml4") (("2" (INST -1 "i!1" "-j!1") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (ASSERT) NIL))))))))) (|mod_even| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (REWRITE "floor_int") (("1" (ASSERT) NIL) ("2" (EXPAND "integer?") (("2" (PROPAX) NIL))))))))) (|mod_neg| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "-i!1/j!1 = -(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (REWRITE "floor_neg") (("2" (LIFT-IF) (("2" (GROUND) (("2" (ASSERT) (("2" (CASE "integer?(--(i!1/j!1))") (("1" (EXPAND "integer?") (("1" (PROPAX) NIL))) ("2" (LEMMA "integers.closed_neg") (("2" (INST -1 "-(i!1/j!1)") (("2" (NAME "q" "i!1/j!1") (("2" (REPLACE -1) (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_neg_d| "" (AUTO-REWRITE-THEORY "integers") (("" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (CASE "i!1/-j!1=-(i!1/j!1)") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "floor_neg") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "floor_int") (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (CASE "integer_pred(--(i!1/j!1))") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))) ("2" (ASSERT) NIL))))))))))) (|mod_eq_arg| "" (TCC) NIL) (|mod_lt| "" (SKOSIMP*) (("" (LIFT-IF) (("" (EXPAND "mod") (("" (EXPAND "abs") (("" (EXPAND "sgn") (("" (GRIND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (REWRITE "floor_small") (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL))))))) ("3" (REWRITE "floor_small") (("3" (LIFT-IF) (("3" (GROUND) (("3" (REWRITE "pos_div_ge") NIL))))))) ("4" (REWRITE "floor_small") (("4" (LIFT-IF) (("4" (GROUND) (("4" (REWRITE "pos_div_ge") NIL))))))))))))))))))) (|mod_lt_nat| "" (SKOSIMP*) (("" (REWRITE "mod_lt") (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))) (|mod_sum_pos| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*m!1/m!1" "i!1/m!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_sum| "" (SKOSIMP*) (("" (EXPAND "mod") (("" (LEMMA "floor_plus_int") (("" (INST - "k!1*j!1/j!1" "i!1/j!1") (("" (REPLACE -1) (("" (ASSERT) NIL))))))))))) (|mod_it_is| "" (SKOSIMP*) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "mod_sum") (("" (INST - "b!1" "m!1" "c!1") (("" (REPLACE -1) (("" (HIDE -1) (("" (REWRITE "mod_lt") (("1" (LIFT-IF) (("1" (EXPAND "sgn") (("1" (PROPAX) NIL))))) ("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))))))))))))) (|mod_Ada| "" (SKOLEM!) (("" (EXPAND "mod") (("" (INST + "floor(i!1/j!1)") (("" (ASSERT) NIL))))))) (|mod_zero| "" (TCC) NIL) (|mod_one| "" (GRIND) (("1" (REWRITE "floor_small") (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "pos_div_ge") NIL))))))) ("2" (REWRITE "floor_small") (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "pos_div_ge") NIL))))))))) (|mod_of_mod| "" (SKOSIMP*) (("" (REWRITE "mod") (("" (LEMMA "mod_sum") (("" (INST - "i!1+k!1" "m!1" "-floor(k!1/m!1)") (("" (ASSERT) NIL))))))))) (|mod_mod| "" (SKOSIMP) (("" (LEMMA "mod_of_mod") (("" (INST - "0" "a!1" "m!1") (("" (GROUND) NIL))))))) (|mod_of_mod_diff| "" (SKOSIMP*) (("" (REWRITE "mod") (("" (LEMMA "mod_sum") (("" (INST - "i!1-k!1" "m!1" "floor(k!1/m!1)") (("" (ASSERT) NIL))))))))) (|mod_pos| "" (SKOSIMP*) (("" (TYPEPRED "mod(i!1,m!1)") (("" (GRIND) (("" (LEMMA "both_sides_times_pos_le1") (("" (INST -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1") (("" (ASSERT) NIL))))))))))) (|mod_plus| "" (SKOSIMP) (("" (LEMMA "mod_lt_nat") (("" (INST - "m!1" "mod(i!1,m!1)+a!1") (("1" (ASSERT) (("1" (LEMMA "mod_of_mod") (("1" (INST - "a!1" "i!1" "m!1") (("1" (ASSERT) NIL))))))) ("2" (LEMMA "mod_pos") (("2" (INST - "i!1" "m!1") (("2" (ASSERT) NIL))))))))))) (|mod_minus| "" (SKOSIMP) (("" (LEMMA "mod_lt_nat") (("" (INST - "m!1" "mod(i!1,m!1)-a!1") (("" (ASSERT) (("" (GROUND) (("1" (LEMMA "mod_of_mod") (("1" (INST - "-a!1" "i!1" "m!1") (("1" (ASSERT) NIL))))) ("2" (LEMMA "mod_pos") (("2" (INST - "i!1" "m!1") (("2" (ASSERT) NIL))))))))))))))) (|mod_TCC2| "" (SKOSIMP*) (("" (ASSERT) (("" (REWRITE "mod_pos") NIL))))))