% This is a PVS dump file: save and do M-x undump-pvs-files
% from within PVS.

%Patch files loaded: patch2 version 1.2.2.115

$$$pvs-strategies

(defstep repl-assrt ()
  (then (repeat (replace*)) (assert))
  "Does REPEAT* (repeatedly) followed by ASSERT"
  "Replacing all LHS by RHS and using decision procedures"
)

(defstep grnd-repl-assrt ()
  (then (ground) (repeat (replace*)) (assert))
  "Does GROUND, then REPEAT* (repeatedly) followed by ASSERT"
  "Replacing all LHS by RHS and using propositional calculus and
decision procedures"
)

(defstep use-grnd-repl-assrt (lemma)
  (then (use lemma :polarity? t) (ground) (repeat (replace*))
(assert))
  "Uses named LEMMA, then does GROUND, then REPEAT* (repeatedly)
followed by ASSERT"
  "Using lemma ~a, Replacing all LHS by RHS and using propositional
calculus and decision procedures"
)

(defstep mem (&optional (term))
 (then
  (inst-cp - "broadcaster(t!1)")
  (if term (inst - term) (inst?))
  (rewrite "newmem")
  (lift-if)
  (grnd-repl-assrt)
  (USE-GRND-REPL-ASSRT "arrival"))
  "mem strategy"
 "Strategy for next mem"
)

(defstep ack (&optional (term))
 (then
  (inst-cp - "broadcaster(t!1)")
  (if term (inst - term) (inst?))
  (rewrite "newack")
  (lift-if)
  (grnd-repl-assrt)
  (USE-GRND-REPL-ASSRT "arrival"))
"ack strategy"
"ack strategy"
)


;;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")


$$$cav00.pvs
CAV00[n: posnat]: THEORY
 BEGIN

  proc: TYPE = {m: nat | m < n}

  procset: TYPE = setof[proc]

  x, y, p, q, b: VAR proc

  time: TYPE = nat

  postime: TYPE = posnat

  j, r, s, t, tt, tf: VAR time

  t1: VAR postime

  IMPORTING mod

  modn(t): proc = mod(t, n)

  broadcaster(t): proc = modn(t)

  cycle: LEMMA
    broadcaster(t) = broadcaster(t + j) IFF (EXISTS (i: nat): j = i * n)

  bcast_prop: LEMMA broadcaster(t) <= t

  bcast_arith: LEMMA x = broadcaster(s + broadcaster(x) - broadcaster(s))

  bcast_arith2: LEMMA broadcaster(t) = broadcaster(1 + r + t) => r >= n - 1

  bcast_arith3: LEMMA
    broadcaster(x) - broadcaster(1 + t) = n - 1 => x = broadcaster(t)

  bcast_arith4: LEMMA
    broadcaster(x) - broadcaster(1 + t) = -1 => x = broadcaster(t)

  membership(t, p): procset

  ack(t, p): bool

  faulty(t, p): bool

  max_faults: AXIOM EXISTS p: NOT faulty(t, p)

  set_prop1: LEMMA FORALL (a: procset): a(x) OR remove(x, add(x, a)) = a

  set_prop2: LEMMA FORALL (a: procset): a(x) => add(x, remove(x, a)) = a

  the_mem(t)(p): bool = NOT faulty(t, p)

  the_mem_faulty: LEMMA
    the_mem(j + t) = the_mem(t) AND faulty(t, x) => faulty(j + t, x)

  the_mem_nonfaulty: LEMMA
    the_mem(j + t) = the_mem(t) AND NOT faulty(t, x) => NOT faulty(j + t, x)

  the_mem_remove: LEMMA 
    FORALL (a: procset): the_mem(t) = remove(x, a) => faulty(t, x)

  faults_latch: AXIOM FORALL (j: nat): faulty(t, p) => faulty(t + j, p)

  faults_latch1: LEMMA faulty(t, p) => faulty(t + 1, p)

  faults_latch1_back: LEMMA NOT faulty(1 + t, p) => NOT faulty(t, p)

  arrives(t, p): bool

  arrival: AXIOM
    LET b = broadcaster(t) IN
      NOT faulty(t, b) AND NOT faulty(t, p) AND membership(t, b)(b) IMPLIES
       arrives(t, p)

  nonarrival: AXIOM
    NOT membership(t, broadcaster(t))(broadcaster(t)) IMPLIES
     NOT arrives(t, p)

  faulty_broadcaster: AXIOM
    NOT faulty(t, b) AND faulty(t + 1, b) AND b = broadcaster(t + 1)
     IMPLIES NOT arrives(t + 1, p)

  faulty_receiver: AXIOM
    NOT faulty(t, p) AND faulty(t + 1, p) AND p /= broadcaster(t + 1)
     IMPLIES NOT faulty(t + 1, broadcaster(t + 1)) AND NOT arrives(t + 1, p)

  all_or_none: AXIOM
    NOT faulty(t, p) AND NOT faulty(t, q) IMPLIES
     arrives(t, p) = arrives(t, q)

  nonfaulty_soon: LEMMA
    EXISTS j: j < n AND NOT faulty(t, broadcaster(t + j))

  next_nf(t): proc =
      broadcaster(t +
                   choose! j: j < n AND NOT faulty(t, broadcaster(t + j)))

  next_nf_prop: LEMMA NOT faulty(t, next_nf(t))

  next_nf_prop2: LEMMA EXISTS j: j < n AND next_nf(t) = broadcaster(t + j)

  staterec: TYPE = [# mem: setof[proc], ack: bool #]

  state: TYPE = [proc -> staterec]

  initstate(p: proc): staterec = (# mem := fullset, ack := TRUE #)

  exec(pre: state, b: proc, f: upto(n))(p: proc): staterec =
      IF p = b
        THEN pre(p) WITH [ack := TRUE]
      ELSIF NOT pre(p)`mem(b) OR NOT pre(p)`mem(p)
            THEN pre(p)
            ELSE IF pre(p)`ack
                   THEN IF p = f OR b = f OR NOT pre(b)`mem(b)
                          THEN pre(p)
                                 WITH [mem := remove(b, pre(p)`mem),
                                       ack := FALSE]
                        ELSIF pre(b)`ack
                              THEN pre(p) WITH [ack := TRUE]
                              ELSE pre(p)
                                     WITH [mem := remove(b, pre(p)`mem),
                                           ack := TRUE]
                        ENDIF
                 ELSE IF p = f OR b = f OR NOT pre(b)`mem(b)
                        THEN pre(p) WITH [mem := remove(p, pre(p)`mem)]
                      ELSIF pre(b)`ack
                            THEN pre(p)
                                   WITH [mem := remove(p, pre(p)`mem),
                                         ack := TRUE]
                            ELSE pre(p) WITH [ack := TRUE]
                      ENDIF
                 ENDIF
      ENDIF

  algdef(pre: state, b: proc, arr: procset)(p: proc): staterec =
      IF p = b
        THEN pre(p) WITH [ack := TRUE]
      ELSIF NOT pre(p)`mem(b) OR NOT pre(p)`mem(p)
            THEN pre(p)
            ELSE TABLE
	    %-------------------------------------------------------||
	    | pre(p)`ack AND NOT arr(p) | 
		pre(p) WITH [mem:=remove(b,pre(p)`mem), ack:=FALSE] ||
	    %-------------------------------------------------------||
	    | pre(p)`ack AND arr(p) AND pre(b)`ack |
					    pre(p) WITH [ack:=TRUE] ||
	    %-------------------------------------------------------||
	    | pre(p)`ack AND arr(p) AND NOT pre(b)`ack |
		 pre(p) WITH [mem:=remove(b,pre(p)`mem), ack:=TRUE] ||
	    %-------------------------------------------------------||
	    | NOT pre(p)`ack AND NOT arr(p) | 
			    pre(p) WITH [mem:=remove(p,pre(p)`mem)] ||
	    %-------------------------------------------------------||
	    | NOT pre(p)`ack AND arr(p) AND NOT pre(b)`ack |
					    pre(p) WITH [ack:=TRUE] ||
	    %-------------------------------------------------------||
	    | NOT pre(p)`ack AND arr(p) AND pre(b)`ack |
		 pre(p) WITH [mem:=remove(p,pre(p)`mem), ack:=TRUE] ||
	    %-------------------------------------------------------||
            ENDTABLE
      ENDIF

  algspec: AXIOM
    LET b = broadcaster(t),
        st(j: proc) = (# mem := membership(t, j), ack := ack(t, j) #),
        arr(j: proc) = arrives(t, j),
        tt = t + 1
     IN
        membership(tt, p) = algdef(st, b, arr)(p)`mem AND
        ack(tt, p) = algdef(st, b, arr)(p)`ack

  newmem: LEMMA
    membership(t + 1, p) =
     LET b = broadcaster(t) IN
       IF p = b
         THEN membership(t, p)
       ELSIF NOT membership(t, p)(p) OR
              NOT membership(t, p)(b) OR
               (arrives(t, p) AND ack(t, p) = ack(t, b))
             THEN membership(t, p)
             ELSE IF ack(t, p)
                    THEN remove(b, membership(t, p))
                  ELSE remove(p, membership(t, p))
                  ENDIF
       ENDIF

  newack: LEMMA
    ack(t + 1, p) =
     LET b = broadcaster(t) IN
       IF p = b
         THEN TRUE
       ELSIF NOT membership(t, p)(p) OR NOT membership(t, p)(b)
             THEN ack(t, p)
             ELSE IF arrives(t, p) THEN TRUE ELSE FALSE ENDIF
       ENDIF

  stable(t): bool =
      FORALL p:
        NOT faulty(t, p) IMPLIES membership(t, p) = the_mem(t) AND ack(t, p)

  initial: AXIOM stable(0)

  fault_nonarrival: AXIOM NOT stable(t) => the_mem(t + 1) = the_mem(t)

  fault_arrival: AXIOM
    stable(t) =>
     (the_mem(t + 1) = the_mem(t) OR
       (EXISTS x:
          NOT faulty(t, x) AND the_mem(t + 1) = remove(x, the_mem(t))))

  fault_nonarrival_lemma: LEMMA
    NOT stable(t) => faulty(t + 1, p) = faulty(t, p)

  none_since(tf, t): bool =
      NOT faulty(t, broadcaster(tf)) AND
       tf < t AND
        (FORALL (j: below(t - tf)):
           j /= 0 => broadcaster(tf + j) /= broadcaster(tf))

  none_since_weak(tf, t): bool =
      tf < t AND
       (FORALL (j: below(t - tf)):
          j /= 0 => broadcaster(tf + j) /= broadcaster(tf))

  none_yet(tf, t, y): bool =
      NOT faulty(t, y) AND
       tf < t AND (FORALL (j: below(t - tf)): broadcaster(tf + j) /= y)

  one_yet(tf, t, y): bool =
      NOT faulty(t, y) AND
       tf < t AND
        (FORALL (j: below(t - tf)):
           j /= t - tf - 1 => broadcaster(tf + j) /= y)

  stable_timed(t: postime, tf): bool = stable(t) AND none_since_weak(tf, t)

  one_since(tf, t): bool =
      tf < t AND
       (FORALL (j: below(t - tf)):
          j /= 0 AND j /= t - tf - 1 =>
           broadcaster(tf + j) /= broadcaster(tf))

  stable_timed2(t: postime, tf): bool = stable(t) AND one_since(tf, t)

  stable_timed22(t: postime, tf, y): bool = stable(t) AND one_yet(tf, t, y)

  stable_to_stable: LEMMA
    stable(t) AND the_mem(t + 1) = the_mem(t) IMPLIES stable(t + 1)

  latent(t: postime, x): bool =
      NOT faulty(t - 1, x) AND
       the_mem(t) = remove(x, the_mem(t - 1)) AND
        membership(t, x) = add(x, the_mem(t)) AND
         ack(t, x) AND
          (FORALL p:
             NOT faulty(t, p) IMPLIES
              membership(t, p) = add(x, the_mem(t)) AND ack(t, p))

  latent_is_nonstable: LEMMA latent(t1, x) => NOT stable(t1)

  stable_to_latent: LEMMA
    stable(t) AND
     NOT faulty(t, x) AND the_mem(t + 1) = remove(x, the_mem(t))
     IMPLIES latent(t + 1, x)

  excluded(t, x): bool =
      FORALL p:
        NOT faulty(t, p) IMPLIES
         membership(t, p) = the_mem(t) AND NOT ack(t, p)

  excluded_timed1(t, x, tf): bool = excluded(t, x) AND none_since(tf, t)

  excluded_timed2(t, x, tf, y): bool = excluded(t, x) AND none_yet(tf, t, y)

  excluded_is_nonstable: LEMMA excluded(t, x) => NOT stable(t)

  latent_means_faulty: LEMMA
    FORALL (t: postime): latent(t, x) => faulty(t, x)

  latent_to_excluded: LEMMA
    t > 0 AND latent(t, x) AND x = broadcaster(t) => excluded(t + 1, x)

  latent_to_excluded2_timed: LEMMA
    t > 0 AND latent(t, x) AND x = broadcaster(t) =>
     excluded_timed2(t + 1, x, t, next_nf(t))

  before(t, x, y): bool =
      FORALL (r: nat):
        y = broadcaster(t + r) =>
         (EXISTS s: s < r AND x = broadcaster(t + s))

  before_prop1: LEMMA
    x /= broadcaster(t) => before(t + 1, x, broadcaster(t))

  before_prop2: LEMMA
    before(t, x, y) => x = broadcaster(t) OR before(t + 1, x, y)

  missed_rcv(t, tf, x): bool =
      LET y = broadcaster(tf) IN
        faulty(t, x) AND
         membership(t, x) = remove(y, add(x, the_mem(t))) AND
          NOT ack(t, x) AND
           (FORALL p:
              NOT faulty(t, p) IMPLIES
               membership(t, p) = add(x, the_mem(t)) AND ack(t, p))

  missed_rcv_ext(t, tf, x): bool =
      missed_rcv(t, tf, x) AND
       LET y = broadcaster(tf) IN x /= y AND before(t, x, y)

  missed_rcv_timed(t, tf, x): bool =
      missed_rcv_ext(t, tf, x) AND none_since(tf, t)

  missed_basic_is_nonstable: LEMMA
    missed_rcv(t, tf, x) => NOT stable(t)

  missed_is_nonstable: LEMMA missed_rcv_ext(t, tf, x) => NOT stable(t)

  latent_to_missed_basic: LEMMA
    t > 0 AND latent(t, x) AND x /= broadcaster(t) =>
     missed_rcv(t + 1, t, x)

  latent_to_missed: LEMMA
    t > 0 AND latent(t, x) AND x /= broadcaster(t) =>
     missed_rcv_ext(t + 1, t, x)

  latent_to_missed_timed: LEMMA
    t > 0 AND latent(t, x) AND x /= broadcaster(t) =>
     missed_rcv_timed(t + 1, t, x)

  missed_basic_to_excluded: LEMMA
    (EXISTS tf: missed_rcv(t, tf, x)) AND
     x = broadcaster(t) AND
      (FORALL p: NOT faulty(t, p) => NOT arrives(t, p))
     IMPLIES excluded(t + 1, x)

  missed_to_excluded: LEMMA
    (EXISTS tf: missed_rcv_ext(t, tf, x)) AND
     x = broadcaster(t) AND
      (FORALL p: NOT faulty(t, p) => NOT arrives(t, p))
     IMPLIES excluded(t + 1, x)

  missed_to_excluded_timed: LEMMA
    missed_rcv_timed(t, tf, x) AND
     x = broadcaster(t) AND
      (FORALL p: NOT faulty(t, p) => NOT arrives(t, p))
     IMPLIES excluded_timed1(t + 1, x, tf)

  missed_basic_to_stable: LEMMA
    (EXISTS tf: missed_rcv(t, tf, x)) AND
     x = broadcaster(t) AND (EXISTS p: NOT faulty(t, p) AND arrives(t, p))
     IMPLIES stable(t + 1)

  missed_to_stable: LEMMA
    (EXISTS tf: missed_rcv_ext(t, tf, x)) AND
     x = broadcaster(t) AND (EXISTS p: NOT faulty(t, p) AND arrives(t, p))
     IMPLIES stable(t + 1)

  missed_to_stable_timed: LEMMA
    missed_rcv_timed(t, tf, x) AND
     x = broadcaster(t) AND (EXISTS p: NOT faulty(t, p) AND arrives(t, p))
     IMPLIES stable_timed(t + 1, tf)

  excluded_to_stable: LEMMA
    (EXISTS x: excluded(t, x)) AND NOT faulty(t, broadcaster(t)) IMPLIES
     stable(t + 1)

  excluded1_to_stable_timed: LEMMA
    (EXISTS x: excluded_timed1(t, x, tf)) AND NOT faulty(t, broadcaster(t))
     IMPLIES stable_timed2(t + 1, tf)

  excluded2_to_stable_timed: LEMMA
    (EXISTS x: excluded_timed2(t, x, tf, y)) AND
     NOT faulty(t, broadcaster(t))
     IMPLIES stable_timed22(t + 1, tf, y)

  excluded_to_excluded: LEMMA
    excluded(t, x) AND faulty(t, broadcaster(t)) IMPLIES excluded(t + 1, x)

  excluded1_to_excluded_timed: LEMMA
    excluded_timed1(t, x, tf) AND faulty(t, broadcaster(t)) IMPLIES
     excluded_timed1(t + 1, x, tf)

  excluded2_to_excluded_timed: LEMMA
    excluded_timed2(t, x, tf, y) AND faulty(t, broadcaster(t)) IMPLIES
     excluded_timed2(t + 1, x, tf, y)

  missed_basic_to_missed_basic: LEMMA
    missed_rcv(t, tf, x) AND
     faulty(t, broadcaster(t)) AND x /= broadcaster(t)
     IMPLIES missed_rcv(t + 1, tf, x)

  missed_to_missed: LEMMA
    missed_rcv_ext(t, tf, x) AND
     faulty(t, broadcaster(t)) AND x /= broadcaster(t)
     IMPLIES missed_rcv_ext(t + 1, tf, x)

  missed_to_missed_timed: LEMMA
    missed_rcv_timed(t, tf, x) AND
     faulty(t, broadcaster(t)) AND x /= broadcaster(t)
     IMPLIES missed_rcv_timed(t + 1, tf, x)

  self_diag(t, tf, x): bool =
      faulty(t, x) AND
       NOT member(x, membership(t, x)) AND
        (FORALL p:
           NOT faulty(t, p) IMPLIES
            membership(t, p) = add(x, the_mem(t)) AND ack(t, p))

  self_diag_timed(t, tf, x): bool =
      self_diag(t, tf, x) AND
       none_since(tf, t) AND
        LET y = broadcaster(tf) IN x /= y AND before(t, x, y)

  selfdiag_is_nonstable: LEMMA self_diag(t, tf, x) => NOT stable(t)

  missed_basic_to_selfdiag: LEMMA
    missed_rcv(t, tf, x) AND
     NOT faulty(t, broadcaster(t)) AND
      x /= broadcaster(t) AND broadcaster(t) /= broadcaster(tf)
     IMPLIES self_diag(t + 1, tf, x)

  missed_to_selfdiag: LEMMA
    missed_rcv_ext(t, tf, x) AND
     NOT faulty(t, broadcaster(t)) AND
      x /= broadcaster(t) AND broadcaster(t) /= broadcaster(tf)
     IMPLIES self_diag(t + 1, tf, x)

  missed_to_selfdiag_timed: LEMMA
    missed_rcv_timed(t, tf, x) AND
     NOT faulty(t, broadcaster(t)) AND
      x /= broadcaster(t) AND broadcaster(t) /= broadcaster(tf)
     IMPLIES self_diag_timed(t + 1, tf, x)

  selfdiag_to_selfdiag: LEMMA
    self_diag(t, tf, x) AND x /= broadcaster(t) IMPLIES
     self_diag(t + 1, tf, x)

  selfdiag_to_selfdiag_timed: LEMMA
    self_diag_timed(t, tf, x) AND x /= broadcaster(t) IMPLIES
     self_diag_timed(t + 1, tf, x)

  selfdiag_to_excluded: LEMMA
    (EXISTS tf: self_diag(t, tf, x)) AND x = broadcaster(t) IMPLIES
     excluded(t + 1, x)

  selfdiag_to_excluded_timed: LEMMA
    self_diag_timed(t, tf, x) AND x = broadcaster(t) IMPLIES
     excluded_timed1(t + 1, x, tf)

  total(t): bool =
      stable(t) OR
       (t > 0 AND (EXISTS x: latent(t, x))) OR
        (EXISTS x: excluded(t, x)) OR
         (EXISTS x, tf: missed_rcv_ext(t, tf, x)) OR
          (EXISTS x, tf: self_diag(t, tf, x))

  excluded_exit: LEMMA
    excluded(t, x) IMPLIES
     (FORALL j: faulty(t, broadcaster(t + j))) OR (EXISTS j: stable(t + j))

  excluded_exit2: LEMMA excluded(t, x) IMPLIES (EXISTS j: stable(t + j))

  stable_faults: LEMMA
    the_mem(j + t) = the_mem(t) AND NOT stable(t + j) AND NOT faulty(t, x)
     IMPLIES NOT faulty(t + j + 1, x)

  excluded_exit2_timed: LEMMA
    excluded_timed1(t, x, tf) IMPLIES (EXISTS j: stable_timed2(t + j, tf))

  excluded2_exit1_timed: LEMMA
    excluded_timed2(t, x, tf, y) IMPLIES
     (EXISTS j: stable_timed22(t + j, tf, y))

  self_diag_exit: LEMMA
    self_diag(t, tf, x) IMPLIES
     (FORALL j: x /= broadcaster(t + j)) OR (EXISTS j: excluded(t + j, x))

  self_diag_exit2: LEMMA
    self_diag(t, tf, x) IMPLIES (EXISTS j: excluded(t + j, x))

  self_diag_exit0_timed: LEMMA
    self_diag_timed(t, tf, x) IMPLIES
     (self_diag_timed(t + 1, tf, x) AND x /= broadcaster(t)) OR
      excluded_timed1(t + 1, x, tf)

  self_diag_exit1_timed: LEMMA
    self_diag_timed(t, tf, x) IMPLIES
     (EXISTS j: excluded_timed1(t + j, x, tf))

  missed_rcv_exit: LEMMA
    missed_rcv_ext(t, tf, x) IMPLIES
     (FORALL j: faulty(t, broadcaster(t + j))) OR
      (EXISTS j: excluded(t + j, x)) OR
       (EXISTS j: stable(t + j)) OR (EXISTS j: self_diag(t + j, tf, x))

  missed_rcv_exit2: LEMMA
    missed_rcv_ext(t, tf, x) IMPLIES
     (EXISTS j: excluded(t + j, x)) OR
      (EXISTS j: stable(t + j)) OR (EXISTS j: self_diag(t + j, tf, x))

  missed_rcv_exit0_timed: LEMMA
    missed_rcv_timed(t, tf, x) IMPLIES
     (missed_rcv_timed(t + 1, tf, x) AND faulty(t, broadcaster(t))) OR
      excluded_timed1(t + 1, x, tf) OR
       stable_timed(t + 1, tf) OR self_diag_timed(t + 1, tf, x)

  missed_rcv_exit1_timed: LEMMA
    missed_rcv_timed(t, tf, x) IMPLIES
     (EXISTS j: excluded_timed1(t + j, x, tf)) OR
      (EXISTS j: stable_timed(t + j, tf)) OR
       (EXISTS j: self_diag_timed(t + j, tf, x))

  final: LEMMA total(t) => total(t + 1)

  final_final: LEMMA total(t)

  liveness1: LEMMA latent(t1, x) IMPLIES (EXISTS j: stable(t1 + j))

  liveness1_timed: LEMMA
    missed_rcv_timed(tf + 1, tf, x) IMPLIES
     (EXISTS j:
        j > 0 AND (stable_timed(tf + j, tf) OR stable_timed2(tf + j, tf)))

  liveness1_timed1: LEMMA
    missed_rcv_timed(tf + 1, tf, x) IMPLIES
     (EXISTS j: j <= n + 1 AND stable(tf + j))

  liveness2_timed: LEMMA
    t > 0 AND latent(t, x) AND x = broadcaster(t) IMPLIES
     (EXISTS j: stable_timed22(t + j, t, next_nf(t)))

  liveness2_timed1: LEMMA
    t > 0 AND latent(t, x) AND x = broadcaster(t) IMPLIES
     (EXISTS j: j <= n + 1 AND stable(t + j))

  liveness: THEOREM stable(t) IMPLIES (EXISTS j: j > 0 AND stable(t + j))

  recovery: THEOREM
    stable(t) IMPLIES (EXISTS j: j > 0 AND j <= n + 2 AND stable(t + j))

  validity: THEOREM
    NOT faulty(t, p) IMPLIES
     (membership(t, p) = the_mem(t) OR
       (EXISTS x: faulty(t, x) AND membership(t, p) = add(x, the_mem(t))))

  agreement: THEOREM
    NOT faulty(t, p) AND NOT faulty(t, q) IMPLIES
     membership(t, p) = membership(t, q)

 END CAV00

$$$cav00.prf
(CAV00
 (|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" (EXPAND "modn")
                  (("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))
        NIL)
       ("2" (SKOSIMP)
        (("2" (REPLACE -1 :HIDE? T)
          (("2" (EXPAND "modn")
            (("2" (LEMMA "mod_sum")
              (("2" (INST - "t!1" "n" "i!1") (("2" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bcast_prop| "" (SKOSIMP)
  (("" (EXPAND "broadcaster")
    (("" (EXPAND "modn")
      (("" (CASE "t!1=t then p!1-t else n+p!1-t endif")
          (("1" (BETA *)
            (("1" (LIFT-IF)
              (("1" (LEMMA "bcast_arith")
                (("1" (INST - "t!1" "p!1")
                  (("1" (ASSERT)
                    (("1" (CASE-REPLACE "broadcaster(p!1)=p!1")
                      (("1" (GROUND)
                        (("1" (LEMMA "cycle")
                          (("1"
                            (INST - "n" "p!1 - broadcaster(t!1) + t!1")
                            (("1" (GROUND)
                              (("1"
                                (INST + "1")
                                (("1" (ASSERT) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (LEMMA "bcast_prop")
                              (("2"
                                (INST - "t!1")
                                (("2" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (HIDE -1 -2)
                        (("2" (EXPAND "broadcaster")
                          (("2" (EXPAND "modn")
                            (("2" (USE "mod_lt_nat")
                              (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (REDUCE) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|next_nf_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE "broadcaster")
  (("" (REWRITE "forall_not")
    (("" (USE "nonfaulty_soon" :POLARITY? T) (("" (ASSERT) NIL NIL))
      NIL))
    NIL))
  NIL)
 (|next_nf_prop| "" (SKOSIMP)
  (("" (EXPAND "next_nf")
    ((""
      (TYPEPRED "choose! j:
                           j < n AND NOT faulty(t!1, broadcaster(j + t!1))")
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE -1)
        (("2" (EXPAND "nonempty?")
          (("2" (EXPAND "empty?")
            (("2" (EXPAND "member")
              (("2" (USE "nonfaulty_soon" :POLARITY? T)
                (("2" (ASSERT)
                  (("2" (INST -1 "t!1")
                    (("2" (SKOSIMP)
                      (("2" (INST - "j!1") (("2" (GROUND) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|next_nf_prop2| "" (SKOSIMP)
  (("" (EXPAND "next_nf")
    ((""
      (TYPEPRED
       "choose! j: j < n AND NOT faulty(t!1, broadcaster(j + t!1))")
      (("1"
        (NAME-REPLACE "P"
         "choose! j: j < n AND NOT faulty(t!1, broadcaster(j + t!1))")
        (("1" (INST + "P") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
       ("2" (EXPAND "nonempty?")
        (("2" (EXPAND "empty?")
          (("2" (EXPAND "member")
            (("2" (USE "nonfaulty_soon" :POLARITY? T)
              (("2" (ASSERT)
                (("2" (INST -1 "t!1")
                  (("2" (SKOSIMP)
                    (("2" (INST - "j!1") (("2" (GROUND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|algdef_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|algdef_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|newmem| "" (SKOSIMP)
  (("" (BETA *)
    (("" (USE "algspec")
      (("" (FLATTEN)
        (("" (HIDE -2)
          (("" (REPLACE -1 :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|newack| "" (SKOSIMP)
  (("" (BETA *)
    (("" (USE "algspec")
      (("" (FLATTEN)
        (("" (HIDE -1)
          (("" (REPLACE -1 :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|fault_nonarrival_lemma| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "fault_nonarrival")
    (("" (IFF)
      (("" (GROUND)
        (("1" (CASE "the_mem(t!1+1)(p!1)")
          (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL)
           ("2" (REPLACE -2 :HIDE? T)
            (("2" (EXPAND "the_mem") (("2" (PROPAX) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (CASE "the_mem(t!1+1)(p!1)")
          (("1" (REPLACE -3 :HIDE? T)
            (("1" (EXPAND "the_mem") (("1" (PROPAX) NIL NIL)) NIL))
            NIL)
           ("2" (EXPAND "the_mem") (("2" (PROPAX) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|stable_to_stable| "" (SKOSIMP)
  (("" (EXPAND "stable")
    (("" (SKOSIMP)
      ((""
        (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
         ("the_mem" "faults_latch1"))
        (("" (GROUND)
          (("1" (REWRITE "newmem")
            (("1" (INST-CP -1 "broadcaster(t!1)")
              (("1" (INST - "p!1")
                (("1" (LIFT-IF)
                  (("1" (GROUND)
                    (("1" (USE-GRND-REPL-ASSRT "arrival") NIL NIL)
                     ("2" (USE-GRND-REPL-ASSRT "arrival") NIL NIL)
                     ("3" (GRND-REPL-ASSRT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (REWRITE "newack")
            (("2" (INST-CP -1 "broadcaster(t!1)")
              (("2" (INST - "p!1")
                (("2" (GRND-REPL-ASSRT)
                  (("2" (USE-GRND-REPL-ASSRT "arrival") NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|latent_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|latent_is_nonstable| "" (SKOSIMP*)
  (("" (EXPAND "stable")
    (("" (EXPAND "latent")
      (("" (GROUND)
        (("" (USE "max_faults")
          (("" (SKOSIMP)
            (("" (FORWARD-CHAIN -)
              (("" (FORWARD-CHAIN -)
                (("" (REPLACE -1 :HIDE? T)
                  (("" (REPLACE -4 :HIDE? T)
                    (("" (CASE "the_mem(t1!1-1)(x!1)")
                      (("1"
                        (CASE "not remove(x!1, the_mem(t1!1 - 1))(x!1)")
                        (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)
                         ("2" (GRIND) NIL NIL))
                        NIL)
                       ("2" (GRIND) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|stable_to_latent| "" (SKOSIMP)
  (("" (EXPAND "latent")
    (("" (EXPAND "stable")
      ((""
        (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
         ("the_mem" "set_prop2" "faults_latch1"))
        (("" (GROUND)
          (("1" (MEM "x!1") NIL NIL) ("2" (ACK "x!1") NIL NIL)
           ("3" (SKOSIMP)
            (("3" (GROUND)
              (("1" (MEM "p!1") NIL NIL) ("2" (ACK "p!1") NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_is_nonstable| "" (SKOSIMP*)
  (("" (EXPAND "excluded")
    (("" (EXPAND "stable")
      (("" (USE "max_faults")
        (("" (SKOSIMP)
          (("" (FORWARD-CHAIN -) (("" (FORWARD-CHAIN -) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|latent_means_faulty| "" (SKOSIMP)
  (("" (EXPAND "latent")
    (("" (FLATTEN)
      (("" (DECOMPOSE-EQUALITY) (("" (GRIND) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|latent_to_excluded| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "latent_means_faulty")
    (("" (FORWARD-CHAIN "latent_is_nonstable")
      (("" (FORWARD-CHAIN "fault_nonarrival")
        (("" (EXPAND "excluded")
          (("" (EXPAND "latent")
            ((""
              (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
               ("the_mem" "faults_latch1" "set_prop2"))
              (("" (ASSERT)
                (("" (GROUND)
                  (("" (SKOSIMP)
                    (("" (ASSERT)
                      (("" (LEMMA "faulty_broadcaster")
                        (("" (INST - "x!1" "p!1" "t!1-1")
                          (("" (GROUND)
                            (("1" (MEM "p!1") NIL NIL)
                             ("2" (ACK "p!1") NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|latent_to_excluded2_timed| "" (SKOSIMP)
  (("" (USE "latent_to_excluded" :POLARITY? T)
    (("" (EXPAND "excluded_timed2")
      (("" (GROUND)
        (("" (EXPAND "none_yet")
          (("" (GROUND)
            (("1" (USE "next_nf_prop")
              (("1" (FORWARD-CHAIN "latent_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (ASSERT)
                    (("1" (FORWARD-CHAIN "the_mem_nonfaulty") NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP)
              (("2" (CASE-REPLACE "j!1=0")
                (("1" (ASSERT)
                  (("1" (USE "next_nf_prop")
                    (("1" (EXPAND "latent")
                      (("1" (FLATTEN)
                        (("1" (FORWARD-CHAIN "the_mem_remove")
                          (("1" (ASSERT) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|before_prop1| "" (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 "bcast_arith2")
                  (("1" (USE "bcast_arith3") (("1" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (LEMMA "bcast_arith")
              (("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 "bcast_arith2")
                  (("1" (USE "bcast_arith4") (("1" (GROUND) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (LEMMA "bcast_arith")
              (("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)
 (|before_prop2| "" (SKOSIMP)
  (("" (EXPAND "before")
    (("" (SKOSIMP)
      (("" (INST - "r!1+1")
        (("" (ASSERT)
          (("" (SKOSIMP)
            (("" (INST + "s!1-1")
              (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_basic_is_nonstable| "" (SKOSIMP)
  (("" (EXPAND "stable")
    (("" (EXPAND "missed_rcv")
      (("" (SKOSIMP*)
        (("" (USE "max_faults")
          (("" (SKOSIMP)
            (("" (FORWARD-CHAIN -)
              (("" (FORWARD-CHAIN -)
                (("" (CASE "the_mem(t!1)(x!1)")
                  (("1" (GRIND) NIL NIL)
                   ("2" (CASE "add(x!1, the_mem(t!1))(x!1)")
                    (("1" (GROUND) NIL NIL) ("2" (GRIND) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_is_nonstable| "" (SKOSIMP*)
  (("" (EXPAND "missed_rcv_ext")
    (("" (FLATTEN)
      (("" (FORWARD-CHAIN "missed_basic_is_nonstable") NIL NIL)) NIL))
    NIL))
  NIL)
 (|latent_to_missed_basic| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "latent_means_faulty")
    (("" (FORWARD-CHAIN "latent_is_nonstable")
      (("" (FORWARD-CHAIN "fault_nonarrival")
        (("" (EXPAND "missed_rcv")
          (("" (EXPAND "latent")
            ((""
              (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
               ("the_mem" "faults_latch1" "set_prop2"))
              (("" (GROUND)
                (("1" (ASSERT) NIL NIL)
                 ("2" (USE "faulty_receiver" :POLARITY? T)
                  (("2" (GROUND) (("2" (MEM "x!1") NIL NIL)) NIL)) NIL)
                 ("3" (USE "faulty_receiver" :POLARITY? T)
                  (("3" (GROUND) (("3" (ACK "x!1") NIL NIL)) NIL)) NIL)
                 ("4" (USE "faulty_receiver" :POLARITY? T)
                  (("4" (SKOSIMP)
                    (("4" (GROUND)
                      (("1" (MEM "p!1") NIL NIL)
                       ("2" (ACK "p!1") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|latent_to_missed| "" (SKOSIMP*)
  (("" (USE "latent_to_missed_basic")
    (("" (EXPAND "missed_rcv_ext")
      (("" (GROUND)
        (("" (USE "before_prop1") (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|latent_to_missed_timed| "" (SKOSIMP*)
  (("" (USE "latent_to_missed")
    (("" (EXPAND "missed_rcv_timed")
      (("" (GROUND)
        (("" (EXPAND "none_since")
          (("" (FORWARD-CHAIN "latent_is_nonstable")
            (("" (FORWARD-CHAIN "fault_nonarrival")
              (("" (LEMMA "faulty_receiver")
                (("" (INST - "x!1" "t!1-1")
                  (("" (EXPAND "latent")
                    (("" (GROUND)
                      (("1" (FORWARD-CHAIN "the_mem_nonfaulty") NIL
                        NIL)
                       ("2" (FORWARD-CHAIN "the_mem_remove") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_basic_to_excluded| "" (SKOSIMP*)
  (("" (FORWARD-CHAIN "missed_basic_is_nonstable")
    (("" (EXPAND "excluded")
      (("" (SKOSIMP)
        (("" (FORWARD-CHAIN "fault_nonarrival")
          (("" (FORWARD-CHAIN "faults_latch1_back")
            (("" (FORWARD-CHAIN -)
              (("" (EXPAND "missed_rcv")
                (("" (FLATTEN)
                  (("" (FORWARD-CHAIN -)
                    ((""
                      (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets")
                       :REWRITES
                       ("the_mem" "faults_latch1" "set_prop2"))
                      (("" (GROUND)
                        (("1" (MEM "p!1")
                          (("1" (USE "set_prop1" :POLARITY? T)
                            (("1" (ASSERT) NIL NIL)) NIL)
                           ("2" (USE "set_prop1" :POLARITY? T)
                            (("2" (ASSERT) NIL NIL)) NIL))
                          NIL)
                         ("2" (ACK "p!1") NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_excluded| "" (SKOSIMP*)
  (("" (USE "missed_basic_to_excluded")
    (("" (GROUND)
      (("" (EXPAND "missed_rcv_ext")
        (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_excluded_timed| "" (SKOSIMP*)
  (("" (EXPAND "excluded_timed1")
    (("" (EXPAND "missed_rcv_timed")
      (("" (USE "missed_to_excluded")
        (("" (GROUND)
          (("1" (EXPAND "none_since")
            (("1" (GROUND)
              (("1" (FORWARD-CHAIN "missed_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (ASSERT)
                    (("1" (FORWARD-CHAIN "the_mem_nonfaulty") NIL NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (SKOSIMP)
                (("2" (INST - "j!1")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (EXPAND "missed_rcv_ext")
                    (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_basic_to_stable| "" (SKOSIMP*)
  (("" (FORWARD-CHAIN "missed_basic_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (HIDE 1)
        (("" (EXPAND "stable")
          (("" (SKOSIMP)
            (("" (EXPAND "missed_rcv")
              (("" (FLATTEN)
                (("" (FORWARD-CHAIN "faults_latch1_back")
                  ((""
                    (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets")
                     :REWRITES ("the_mem" "faults_latch1" "set_prop2"))
                    (("" (GROUND)
                      (("1" (INST - "p!2")
                        (("1" (GROUND)
                          (("1" (LEMMA "set_prop1")
                            (("1" (MEM "p!2")
                              (("1"
                                (INST? :WHERE 1)
                                (("1" (GRND-REPL-ASSRT) NIL NIL))
                                NIL)
                               ("2"
                                (INST? :WHERE 1)
                                (("2" (GROUND) NIL NIL))
                                NIL)
                               ("3"
                                (INST? :WHERE 2)
                                (("3" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (ACK "p!2")
                        (("1" (LEMMA "all_or_none")
                          (("1" (INST - "p!1" "p!2" "t!1")
                            (("1" (ASSERT) NIL NIL)) NIL))
                          NIL)
                         ("2" (LEMMA "all_or_none")
                          (("2" (INST - "p!1" "p!2" "t!1")
                            (("2" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_stable| "" (SKOSIMP*)
  (("" (EXPAND "missed_rcv_ext")
    (("" (GROUND)
      (("" (USE "missed_basic_to_stable" :POLARITY? T)
        (("" (GROUND)
          (("1" (INST?) NIL NIL)
           ("2" (INST?) (("2" (GROUND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_stable_timed| "" (SKOSIMP*)
  (("" (EXPAND "missed_rcv_timed")
    (("" (EXPAND "stable_timed")
      (("" (USE "missed_to_stable")
        (("" (GROUND)
          (("1" (EXPAND "none_since")
            (("1" (EXPAND "none_since_weak")
              (("1" (GROUND)
                (("1" (SKOSIMP*)
                  (("1" (INST - "j!1")
                    (("1" (ASSERT) NIL NIL)
                     ("2" (EXPAND "missed_rcv_ext")
                      (("2" (GROUND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL)
           ("4" (REDUCE) NIL NIL) ("5" (REDUCE) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_to_stable| "" (SKOSIMP*)
  (("" (FORWARD-CHAIN "excluded_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "stable")
        (("" (SKOSIMP*)
          (("" (HIDE 2)
            (("" (EXPAND "excluded")
              ((""
                (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets")
                 :REWRITES ("the_mem" "faults_latch1" "set_prop2"))
                (("" (GROUND)
                  (("1" (MEM "p!2") NIL NIL) ("2" (ACK "p!2") NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded1_to_stable_timed| "" (SKOSIMP*)
  (("" (EXPAND "stable_timed2")
    (("" (EXPAND "excluded_timed1")
      (("" (USE "excluded_to_stable")
        (("" (GROUND)
          (("1" (EXPAND "one_since")
            (("1" (EXPAND "none_since")
              (("1" (GROUND)
                (("1" (SKOSIMP)
                  (("1" (CASE-REPLACE "j!1=t!1-tf!1")
                    (("1" (INST - "j!1")
                      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded2_to_stable_timed| "" (SKOSIMP*)
  (("" (EXPAND "stable_timed22")
    (("" (EXPAND "excluded_timed2")
      (("" (USE "excluded_to_stable")
        (("" (GROUND)
          (("1" (EXPAND "one_yet")
            (("1" (EXPAND "none_yet")
              (("1" (GROUND)
                (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                  (("1" (FORWARD-CHAIN "fault_nonarrival")
                    (("1" (ASSERT)
                      (("1" (FORWARD-CHAIN "the_mem_nonfaulty") NIL
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (SKOSIMP)
                  (("2" (INST - "j!1") (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_to_excluded| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "excluded_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "excluded")
        (("" (SKOSIMP)
          (("" (FORWARD-CHAIN "faults_latch1_back")
            (("" (FORWARD-CHAIN -)
              ((""
                (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets")
                 :REWRITES ("the_mem" "faults_latch1" "set_prop2"))
                (("" (GROUND)
                  (("1" (MEM "p!1") NIL NIL) ("2" (ACK "p!1") NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded1_to_excluded_timed| "" (SKOSIMP)
  (("" (EXPAND "excluded_timed1")
    (("" (USE "excluded_to_excluded" :POLARITY? T)
      (("" (GROUND)
        (("" (EXPAND "none_since")
          (("" (GROUND)
            (("1" (HIDE -2 -4 -5)
              (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (USE "the_mem_nonfaulty")
                    (("1" (GROUND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP)
              (("2" (INST - "j!1")
                (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded2_to_excluded_timed| "" (SKOSIMP)
  (("" (EXPAND "excluded_timed2")
    (("" (GROUND)
      (("1" (USE "excluded_to_excluded" :POLARITY? T)
        (("1" (GROUND) NIL NIL)) NIL)
       ("2" (EXPAND "none_yet")
        (("2" (GROUND)
          (("1" (FORWARD-CHAIN "excluded_is_nonstable")
            (("1" (FORWARD-CHAIN "fault_nonarrival")
              (("1" (ASSERT)
                (("1" (FORWARD-CHAIN "the_mem_nonfaulty") NIL NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP)
            (("2" (INST - "j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_basic_to_missed_basic| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "missed_basic_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "missed_rcv")
        ((""
          (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
           ("the_mem" "faults_latch1" "set_prop2"))
          (("" (GROUND)
            (("1" (ASSERT) NIL NIL) ("2" (MEM "x!1") NIL NIL)
             ("3" (ACK "x!1") NIL NIL)
             ("4" (SKOSIMP)
              (("4" (ASSERT)
                (("4" (FORWARD-CHAIN "faults_latch1_back")
                  (("4" (FORWARD-CHAIN -)
                    (("4" (GROUND)
                      (("1" (MEM "p!1") NIL NIL)
                       ("2" (ACK "p!1") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_missed| "" (SKOSIMP)
  (("" (EXPAND "missed_rcv_ext")
    (("" (GROUND)
      (("1" (USE "missed_basic_to_missed_basic" :POLARITY? T)
        (("1" (GROUND) NIL NIL)) NIL)
       ("2" (FORWARD-CHAIN "before_prop2") (("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_missed_timed| "" (SKOSIMP)
  (("" (EXPAND "missed_rcv_timed")
    (("" (USE "missed_to_missed")
      (("" (GROUND)
        (("" (EXPAND "none_since")
          (("" (GROUND)
            (("1" (HIDE -2)
              (("1" (FORWARD-CHAIN "missed_is_nonstable")
                (("1" (REWRITE "fault_nonarrival_lemma") NIL NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP)
              (("2" (INST - "j!1")
                (("1" (ASSERT) NIL NIL)
                 ("2" (EXPAND "missed_rcv_ext")
                  (("2" (FLATTEN)
                    (("2" (EXPAND "before")
                      (("2" (INST -5 0) (("2" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|selfdiag_is_nonstable| "" (SKOSIMP*)
  (("" (EXPAND "self_diag")
    (("" (EXPAND "stable")
      (("" (GROUND)
        (("" (USE "max_faults")
          (("" (SKOSIMP)
            (("" (FORWARD-CHAIN -)
              (("" (FORWARD-CHAIN -)
                (("" (CASE "not the_mem(t!1)(x!1)")
                  (("1" (CASE "add(x!1, the_mem(t!1))(x!1)")
                    (("1" (GROUND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
                   ("2" (GRIND) NIL NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_basic_to_selfdiag| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "missed_basic_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "missed_rcv")
        (("" (FLATTEN)
          (("" (EXPAND "self_diag")
            ((""
              (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
               ("the_mem" "faults_latch1" "set_prop2"))
              (("" (GROUND)
                (("1" (ASSERT) NIL NIL)
                 ("2" (FORWARD-CHAIN -) (("2" (MEM "x!1") NIL NIL))
                  NIL)
                 ("3" (SKOSIMP)
                  (("3" (GROUND)
                    (("1" (MEM "p!1") NIL NIL)
                     ("2" (ACK "p!1") NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_selfdiag| "" (SKOSIMP*)
  (("" (EXPAND "missed_rcv_ext")
    (("" (FLATTEN)
      (("" (USE "missed_basic_to_selfdiag" :POLARITY? T)
        (("" (GROUND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|missed_to_selfdiag_timed| "" (SKOSIMP)
  (("" (EXPAND "missed_rcv_timed")
    (("" (EXPAND "self_diag_timed")
      (("" (USE "missed_to_selfdiag")
        (("" (GROUND)
          (("1" (EXPAND "none_since")
            (("1" (GROUND)
              (("1" (FORWARD-CHAIN "missed_is_nonstable")
                (("1" (REWRITE "fault_nonarrival_lemma") NIL NIL)) NIL)
               ("2" (SKOSIMP)
                (("2" (INST - "j!1")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (EXPAND "missed_rcv_ext")
                    (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (EXPAND "missed_rcv_ext") (("2" (PROPAX) NIL NIL)) NIL)
           ("3" (EXPAND "missed_rcv_ext")
            (("3" (FLATTEN)
              (("3" (FORWARD-CHAIN "before_prop2")
                (("3" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|selfdiag_to_selfdiag| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "selfdiag_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "self_diag")
        (("" (FLATTEN)
          ((""
            (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets") :REWRITES
             ("the_mem" "faults_latch1" "set_prop2"))
            (("" (GROUND)
              (("1" (ASSERT) NIL NIL) ("2" (MEM "x!1") NIL NIL)
               ("3" (SKOSIMP)
                (("3" (FORWARD-CHAIN "faults_latch1_back")
                  (("3" (COPY -3)
                    (("3" (FORWARD-CHAIN -)
                      (("3" (GROUND)
                        (("1" (MEM "p!1") NIL NIL)
                         ("2" (ACK "p!1") NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|selfdiag_to_selfdiag_timed| "" (SKOSIMP)
  (("" (EXPAND "self_diag_timed")
    (("" (USE "selfdiag_to_selfdiag")
      (("" (GROUND)
        (("1" (EXPAND "none_since")
          (("1" (GROUND)
            (("1" (HIDE -2)
              (("1" (FORWARD-CHAIN "selfdiag_is_nonstable")
                (("1" (REWRITE "fault_nonarrival_lemma") NIL NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP)
              (("2" (INST - "j!1")
                (("1" (ASSERT) NIL NIL)
                 ("2" (EXPAND "before")
                  (("2" (INST -5 0) (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (FORWARD-CHAIN "before_prop2") (("2" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|selfdiag_to_excluded| "" (SKOSIMP*)
  (("" (FORWARD-CHAIN "selfdiag_is_nonstable")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (EXPAND "excluded")
        (("" (SKOSIMP)
          (("" (EXPAND "self_diag")
            (("" (FLATTEN)
              ((""
                (INSTALL-REWRITES :DEFS NIL :THEORIES ("sets")
                 :REWRITES ("the_mem" "faults_latch1" "set_prop2"))
                (("" (FORWARD-CHAIN "faults_latch1_back")
                  (("" (FORWARD-CHAIN -)
                    (("" (GROUND)
                      (("1" (REWRITE "newmem")
                        (("1" (LIFT-IF)
                          (("1" (GRND-REPL-ASSRT)
                            (("1" (USE-GRND-REPL-ASSRT "nonarrival")
                              NIL NIL)
                             ("2" (LEMMA "set_prop1")
                              (("2"
                                (INST
                                 -
                                 "broadcaster(t!1)"
                                 "the_mem(t!1)")
                                (("2" (GROUND) NIL NIL))
                                NIL))
                              NIL)
                             ("3" (LEMMA "set_prop1")
                              (("3"
                                (INST
                                 -
                                 "broadcaster(t!1)"
                                 "the_mem(t!1)")
                                (("3" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (REWRITE "newack")
                        (("2" (GRND-REPL-ASSRT)
                          (("2" (USE-GRND-REPL-ASSRT "nonarrival") NIL
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|selfdiag_to_excluded_timed| "" (SKOSIMP)
  (("" (EXPAND "excluded_timed1")
    (("" (USE "selfdiag_to_excluded" :POLARITY? T)
      (("" (GROUND)
        (("1" (EXPAND "self_diag_timed")
          (("1" (FLATTEN)
            (("1" (EXPAND "none_since")
              (("1" (GROUND)
                (("1" (FORWARD-CHAIN "selfdiag_is_nonstable")
                  (("1" (REWRITE "fault_nonarrival_lemma") NIL NIL))
                  NIL)
                 ("2" (SKOSIMP)
                  (("2" (INST - "j!1")
                    (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (EXPAND "self_diag_timed")
          (("2" (FLATTEN) (("2" (INST?) NIL NIL)) NIL)) NIL)
         ("3" (EXPAND "self_diag_timed")
          (("3" (FLATTEN) (("3" (INST?) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_exit| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and excluded(t!1+j,x!1)")
    (("1" (INST + "j!1+1")
      (("1" (INST - "j!1")
        (("1" (FLATTEN)
          (("1" (LEMMA "excluded_to_stable")
            (("1" (INST - "t!1+j!1")
              (("1" (ASSERT)
                (("1" (GROUND)
                  (("1" (INST?) NIL NIL)
                   ("2" (CASE "the_mem(t!1)(broadcaster(j!1+t!1))")
                    (("1" (REPLACE -3 :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))
        NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)
       ("3" (SKOSIMP*)
        (("3" (GROUND)
          (("1" (LEMMA "fault_nonarrival")
            (("1" (INST - "j!2+t!1")
              (("1" (ASSERT)
                (("1" (USE "excluded_is_nonstable")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (LEMMA "excluded_to_excluded")
            (("2" (INST? - :POLARITY? T)
              (("2" (ASSERT)
                (("2" (GROUND)
                  (("2" (USE "excluded_to_stable")
                    (("2" (INST + "j!2+1")
                      (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_exit2| "" (SKOSIMP)
  (("" (USE "excluded_exit")
    (("" (ASSERT)
      (("" (GROUND)
        (("" (USE "nonfaulty_soon")
          (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|stable_faults| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "the_mem_nonfaulty")
    (("" (FORWARD-CHAIN "fault_nonarrival")
      (("" (REPLACE -2 :HIDE? T)
        (("" (CASE "the_mem(t!1+j!1+1)(x!1)")
          (("1" (EXPAND "the_mem") (("1" (GROUND) NIL NIL)) NIL)
           ("2" (REPLACE -1)
            (("2" (EXPAND "the_mem") (("2" (PROPAX) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded_exit2_timed_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|excluded_exit2_timed| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and faulty(t!1,broadcaster(t!1+j)) and excluded_timed1(t!1+j,x!1,tf!1)")
    (("1" (USE "nonfaulty_soon")
      (("1" (SKOSIMP)
        (("1" (INST - "j!1") (("1" (FLATTEN) NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL)
       ("2" (ASSERT)
        (("2" (INST + 1)
          (("2" (USE "excluded1_to_stable_timed")
            (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL)
       ("3" (ASSERT) NIL NIL)
       ("4" (SKOSIMP*)
        (("4" (GROUND)
          (("1" (EXPAND "excluded_timed1")
            (("1" (FLATTEN)
              (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (USE "excluded1_to_excluded_timed" :POLARITY? T)
            (("2" (GROUND)
              (("1" (INST + "j!1+2")
                (("1" (USE "excluded1_to_stable_timed" :POLARITY? T)
                  (("1" (REDUCE)
                    (("1" (HIDE -2 -6)
                      (("1" (EXPAND "excluded_timed1")
                        (("1" (FLATTEN)
                          (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                            (("1" (FORWARD-CHAIN "stable_faults")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (ASSERT) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (FORWARD-CHAIN "the_mem_faulty") NIL NIL))
              NIL))
            NIL)
           ("3" (USE "excluded1_to_excluded_timed" :POLARITY? T)
            (("3" (GROUND)
              (("3" (USE "excluded1_to_stable_timed" :POLARITY? T)
                (("3" (GROUND)
                  (("3" (INST + "j!1+1")
                    (("3" (INST - "tf!1")
                      (("3" (GROUND) (("3" (INST?) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|excluded2_exit1_timed_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|excluded2_exit1_timed| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and faulty(t!1,broadcaster(t!1+j)) and excluded_timed2(t!1+j,x!1,tf!1,y!1)")
    (("1" (USE "nonfaulty_soon")
      (("1" (SKOSIMP)
        (("1" (INST - "j!1") (("1" (FLATTEN) NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL)
       ("2" (ASSERT)
        (("2" (INST + 1)
          (("2" (USE "excluded2_to_stable_timed")
            (("2" (REDUCE) NIL NIL)) NIL))
          NIL))
        NIL)
       ("3" (ASSERT) NIL NIL)
       ("4" (SKOSIMP*)
        (("4" (GROUND)
          (("1" (EXPAND "excluded_timed2")
            (("1" (FLATTEN)
              (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (USE "excluded2_to_excluded_timed" :POLARITY? T)
            (("2" (GROUND)
              (("1" (INST + "j!1+2")
                (("1" (USE "excluded2_to_stable_timed")
                  (("1" (REDUCE)
                    (("1" (HIDE -2 -6)
                      (("1" (EXPAND "excluded_timed2")
                        (("1" (FLATTEN)
                          (("1" (FORWARD-CHAIN "excluded_is_nonstable")
                            (("1" (FORWARD-CHAIN "stable_faults")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (ASSERT) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (TYPEPRED "j!1")
                (("2" (FORWARD-CHAIN "the_mem_faulty") NIL NIL)) NIL))
              NIL))
            NIL)
           ("3" (FORWARD-CHAIN "the_mem_faulty")
            (("3" (USE "excluded2_to_excluded_timed" :POLARITY? T)
              (("3" (GROUND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|self_diag_exit| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and self_diag(t!1+j,tf!1,x!1)")
    (("1" (INST + "j!1+1")
      (("1" (INST - "j!1")
        (("1" (FLATTEN)
          (("1" (LEMMA "selfdiag_to_excluded")
            (("1" (INST? - :POLARITY? T)
              (("1" (ASSERT)
                (("1" (FORWARD-CHAIN "selfdiag_is_nonstable")
                  (("1" (GROUND) (("1" (INST?) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)
       ("3" (SKOSIMP*)
        (("3" (FORWARD-CHAIN "selfdiag_is_nonstable")
          (("3" (GROUND)
            (("1" (LEMMA "fault_nonarrival")
              (("1" (INST - "j!2+t!1") (("1" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("2" (USE "selfdiag_to_selfdiag" :POLARITY? T)
              (("2" (ASSERT)
                (("2" (GROUND)
                  (("2" (USE "selfdiag_to_excluded")
                    (("2" (INST + "j!2+1")
                      (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|self_diag_exit2| "" (SKOSIMP)
  (("" (USE "self_diag_exit")
    (("" (GROUND)
      ((""
        (INST -
         "let t=broadcaster(t!1) in if x!1>=t then x!1-t else n+x!1-t endif")
        (("1" (BETA *)
          (("1" (LIFT-IF)
            (("1" (LEMMA "bcast_arith")
              (("1" (INST - "t!1" "x!1")
                (("1" (ASSERT)
                  (("1" (CASE-REPLACE "broadcaster(x!1)=x!1")
                    (("1" (GROUND)
                      (("1" (LEMMA "cycle")
                        (("1"
                          (INST - "n" "x!1 - broadcaster(t!1) + t!1")
                          (("1" (GROUND)
                            (("1" (INST + "1") (("1" (ASSERT) NIL NIL))
                              NIL))
                            NIL)
                           ("2" (LEMMA "bcast_prop")
                            (("2" (INST - "t!1")
                              (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (HIDE -1 -2 2 3)
                      (("2" (EXPAND "broadcaster")
                        (("2" (EXPAND "modn")
                          (("2" (USE "mod_lt_nat")
                            (("2" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (REDUCE) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|self_diag_exit0_timed| "" (SKOSIMP)
  (("" (USE "selfdiag_to_excluded_timed" :POLARITY? T)
    (("" (REDUCE)
      (("" (USE "selfdiag_to_selfdiag_timed" :POLARITY? T)
        (("" (GROUND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|self_diag_exit1_timed| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and x!1/=broadcaster(t!1+j) and self_diag_timed(t!1+j,tf!1,x!1)")
    (("1"
      (INST -
       "let t=broadcaster(t!1) in if x!1>=t then x!1-t else n+x!1-t endif")
      (("1" (BETA *)
        (("1" (LIFT-IF)
          (("1" (EXPAND "self_diag_timed")
            (("1" (FLATTEN)
              (("1" (LEMMA "bcast_arith")
                (("1" (INST - "t!1" "x!1")
                  (("1" (ASSERT)
                    (("1" (CASE-REPLACE "broadcaster(x!1)=x!1")
                      (("1" (GROUND)
                        (("1" (LEMMA "cycle")
                          (("1"
                            (INST - "n" "x!1 - broadcaster(t!1) + t!1")
                            (("1" (GROUND)
                              (("1"
                                (INST + "1")
                                (("1" (ASSERT) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (LEMMA "bcast_prop")
                              (("2"
                                (INST - "t!1")
                                (("2" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (HIDE -1 -2 -3 -4 2 3)
                        (("2" (EXPAND "broadcaster")
                          (("2" (EXPAND "modn")
                            (("2" (USE "mod_lt_nat")
                              (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (REDUCE) NIL NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL)
       ("2" (USE "self_diag_exit0_timed" :POLARITY? T)
        (("2" (REDUCE) NIL NIL)) NIL)
       ("3" (ASSERT) NIL NIL)
       ("4" (SKOSIMP*)
        (("4" (GROUND)
          (("1" (EXPAND "self_diag_timed")
            (("1" (FLATTEN)
              (("1" (FORWARD-CHAIN "selfdiag_is_nonstable")
                (("1" (FORWARD-CHAIN "fault_nonarrival")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (USE "selfdiag_to_selfdiag_timed" :POLARITY? T)
            (("2" (ASSERT)
              (("2" (INST + "2+j!1")
                (("2" (USE "selfdiag_to_excluded_timed" :POLARITY? T)
                  (("2" (REDUCE) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("3" (USE "selfdiag_to_selfdiag_timed" :POLARITY? T)
            (("3" (GROUND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_rcv_exit| "" (SKOSIMP*)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and missed_rcv_ext(t!1+j,tf!1,x!1)")
    (("1" (INST - "j!1")
      (("1" (FLATTEN)
        (("1" (INST + "j!1+1")
          (("1" (INST + "j!1+1")
            (("1" (INST + "j!1+1")
              (("1" (LEMMA "fault_nonarrival")
                (("1" (INST - "j!1+t!1")
                  (("1" (GROUND)
                    (("1" (CASE "the_mem(t!1)(broadcaster(j!1+t!1))")
                      (("1" (REPLACE -3 :DIR RL)
                        (("1" (EXPAND "the_mem" -1)
                          (("1" (HIDE -2 -4 2)
                            (("1" (CASE "x!1=broadcaster(j!1+t!1)")
                              (("1"
                                (USE "missed_to_excluded")
                                (("1"
                                  (GROUND)
                                  (("1" (INST?) NIL NIL)
                                   ("2"
                                    (USE "missed_to_stable")
                                    (("2"
                                      (GROUND)
                                      (("1" (INST? 1) NIL NIL)
                                       ("2"
                                        (SKOSIMP)
                                        (("2"
                                          (INST? 1)
                                          (("2" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2"
                                (USE "missed_to_selfdiag")
                                (("2"
                                  (GROUND)
                                  (("2"
                                    (EXPAND "missed_rcv_ext")
                                    (("2"
                                      (GROUND)
                                      (("2"
                                        (EXPAND "before")
                                        (("2"
                                          (INST - 0)
                                          (("2" (GROUND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (EXPAND "the_mem") (("2" (PROPAX) NIL NIL))
                        NIL))
                      NIL)
                     ("2" (USE "missed_is_nonstable")
                      (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)
       ("3" (SKOSIMP)
        (("3" (GROUND)
          (("1" (LEMMA "fault_nonarrival")
            (("1" (INST - "j!2+t!1")
              (("1" (GROUND)
                (("1" (USE "missed_is_nonstable")
                  (("1" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (INST + "j!2+1")
            (("2" (INST + "j!2+1")
              (("2" (INST + "j!2+1")
                (("2" (LEMMA "fault_nonarrival")
                  (("2" (INST - "j!2+t!1")
                    (("2" (GROUND)
                      (("1" (HIDE -4 2)
                        (("1" (CASE "x!1=broadcaster(j!2+t!1)")
                          (("1" (USE "missed_to_excluded")
                            (("1" (GROUND)
                              (("1" (INST?) NIL NIL)
                               ("2"
                                (USE "missed_to_stable")
                                (("2"
                                  (GROUND)
                                  (("1" (INST? 1) NIL NIL)
                                   ("2"
                                    (SKOSIMP)
                                    (("2"
                                      (INST? 1)
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (USE "missed_to_selfdiag" :POLARITY? T)
                            (("2" (GROUND)
                              (("1"
                                (USE "missed_to_missed" :POLARITY? T)
                                (("1" (GROUND) NIL NIL))
                                NIL)
                               ("2"
                                (EXPAND "missed_rcv_ext" -)
                                (("2"
                                  (GROUND)
                                  (("2"
                                    (EXPAND "before")
                                    (("2"
                                      (INST - 0)
                                      (("2" (GROUND) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (USE "missed_is_nonstable" :POLARITY? T)
                        (("2" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_rcv_exit2| "" (SKOSIMP)
  (("" (USE "missed_rcv_exit")
    (("" (GROUND)
      (("" (USE "nonfaulty_soon")
        (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_rcv_exit0_timed| "" (SKOSIMP)
  (("" (USE "missed_to_selfdiag_timed" :POLARITY? T)
    (("" (GROUND)
      (("1" (USE "missed_to_missed_timed" :POLARITY? T)
        (("1" (GROUND)
          (("1" (USE "missed_to_excluded_timed" :POLARITY? T)
            (("1" (GROUND)
              (("1" (SKOSIMP)
                (("1" (USE "missed_to_stable_timed" :POLARITY? T)
                  (("1" (GROUND)
                    (("1" (INST + "p!1") (("1" (GROUND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (USE "missed_to_excluded_timed" :POLARITY? T)
        (("2" (GROUND)
          (("2" (SKOSIMP)
            (("2" (USE "missed_to_stable_timed" :POLARITY? T)
              (("2" (GROUND)
                (("2" (INST + "p!1") (("2" (GROUND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("3" (USE "missed_to_excluded_timed" :POLARITY? T)
        (("3" (GROUND)
          (("3" (SKOSIMP)
            (("3" (USE "missed_to_stable_timed" :POLARITY? T)
              (("3" (GROUND)
                (("3" (INST + "p!1") (("3" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("4" (EXPAND "missed_rcv_timed")
        (("4" (FLATTEN)
          (("4" (EXPAND "missed_rcv_ext")
            (("4" (FLATTEN)
              (("4" (EXPAND "before")
                (("4" (INST - 0) (("4" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("5" (EXPAND "missed_rcv_timed")
        (("5" (EXPAND "missed_rcv_ext")
          (("5" (FLATTEN)
            (("5" (EXPAND "before")
              (("5" (INST - 0) (("5" (ASSERT) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|missed_rcv_exit1_timed_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|missed_rcv_exit1_timed| "" (SKOSIMP)
  ((""
    (CASE "forall j: the_mem(t!1+j)=the_mem(t!1) and faulty(t!1,broadcaster(t!1+j)) and missed_rcv_timed(t!1+j,tf!1,x!1)")
    (("1" (USE "nonfaulty_soon")
      (("1" (SKOSIMP)
        (("1" (INST - "j!1") (("1" (GROUND) NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (INDUCT "j" 1)
      (("1" (ASSERT) NIL NIL)
       ("2" (USE "missed_rcv_exit0_timed") (("2" (REDUCE) NIL NIL))
        NIL)
       ("3" (ASSERT) NIL NIL)
       ("4" (SKOSIMP)
        (("4" (HIDE -4)
          (("4" (GROUND)
            (("1" (EXPAND "missed_rcv_timed")
              (("1" (FLATTEN)
                (("1" (FORWARD-CHAIN "missed_is_nonstable")
                  (("1" (FORWARD-CHAIN "fault_nonarrival")
                    (("1" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (USE "missed_rcv_exit0_timed")
              (("2" (GROUND)
                (("1" (USE "missed_rcv_exit0_timed")
                  (("1" (REDUCE)
                    (("1" (HIDE -1 -3)
                      (("1" (EXPAND "missed_rcv_timed")
                        (("1" (FLATTEN)
                          (("1" (FORWARD-CHAIN "missed_is_nonstable")
                            (("1" (FORWARD-CHAIN "stable_faults")
                              (("1" (ASSERT) NIL NIL)
                               ("2" (ASSERT) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (REDUCE) NIL NIL) ("3" (REDUCE) NIL NIL)
                 ("4" (REDUCE) NIL NIL))
                NIL))
              NIL)
             ("3" (LEMMA "missed_rcv_exit0_timed")
              (("3" (INST? :WHERE -) (("3" (REDUCE) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|final| "" (SKOSIMP)
  (("" (EXPAND "total")
    (("" (GROUND)
      (("1" (USE "stable_to_stable")
        (("1" (GROUND)
          (("1" (LEMMA "fault_arrival")
            (("1" (INST? :POLARITY? T)
              (("1" (GROUND)
                (("1" (SKOSIMP)
                  (("1" (USE "stable_to_latent")
                    (("1" (GROUND) (("1" (INST?) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (SKOSIMP)
        (("2" (LEMMA "latent_is_nonstable")
          (("2" (INST - "t!1" _)
            (("2" (INST?)
              (("2" (GROUND)
                (("2" (USE "fault_nonarrival")
                  (("2" (USE "latent_to_excluded")
                    (("2" (GROUND)
                      (("1" (INST? 4) NIL NIL)
                       ("2" (USE "latent_to_missed")
                        (("2" (GROUND) (("2" (INST? 6) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("3" (SKOSIMP)
        (("3" (LEMMA "excluded_is_nonstable")
          (("3" (INST? :WHERE -)
            (("3" (GROUND)
              (("3" (USE "fault_nonarrival")
                (("3" (USE "excluded_to_excluded")
                  (("3" (GROUND)
                    (("1" (INST? 4) NIL NIL)
                     ("2" (LEMMA "excluded_to_stable")
                      (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("4" (SKOSIMP)
        (("4" (LEMMA "missed_is_nonstable")
          (("4" (INST? :WHERE -)
            (("4" (GROUND)
              (("4" (USE "fault_nonarrival")
                (("4" (ASSERT)
                  (("4" (CASE "x!1=broadcaster(t!1)")
                    (("1" (USE "missed_to_excluded")
                      (("1" (GROUND)
                        (("1" (INST? 4) NIL NIL)
                         ("2" (INST? 1) NIL NIL)
                         ("3" (USE "missed_to_stable")
                          (("3" (GROUND)
                            (("1" (INST? 1) NIL NIL)
                             ("2" (SKOSIMP)
                              (("2"
                                (INST? 1)
                                (("2" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (USE "missed_to_selfdiag")
                      (("2" (GROUND)
                        (("1" (INST? 7) NIL NIL)
                         ("2" (USE "missed_to_missed")
                          (("2" (GROUND) (("2" (INST? 6) NIL NIL))
                            NIL))
                          NIL)
                         ("3" (EXPAND "missed_rcv_ext" -)
                          (("3" (FLATTEN)
                            (("3" (EXPAND "before")
                              (("3"
                                (INST - 0)
                                (("3" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("5" (SKOSIMP)
        (("5" (LEMMA "selfdiag_is_nonstable")
          (("5" (INST? :WHERE -)
            (("5" (GROUND)
              (("5" (USE "fault_nonarrival")
                (("5" (USE "selfdiag_to_selfdiag")
                  (("5" (GROUND)
                    (("1" (INST? 6) NIL NIL)
                     ("2" (USE "selfdiag_to_excluded")
                      (("2" (GROUND)
                        (("1" (INST? 4) NIL NIL)
                         ("2" (INST? 1) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|final_final| "" (INDUCT "t")
  (("1" (USE "initial")
    (("1" (ASSERT)
      (("1" (EXPAND "total") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
    NIL)
   ("2" (USE "final") NIL NIL))
  NIL)
 (|liveness1| "" (SKOSIMP)
  (("" (USE "latent_to_excluded")
    (("" (GROUND)
      (("1" (USE "excluded_exit2")
        (("1" (APPLY (THEN (GROUND) (SKOSIMP) (INST?))) NIL NIL)) NIL)
       ("2" (USE "latent_to_missed")
        (("2" (GROUND)
          (("2" (USE "missed_rcv_exit2")
            (("2" (APPLY (THEN (GROUND) (SKOSIMP)))
              (("1" (USE "excluded_exit2")
                (("1" (APPLY (THEN (GROUND) (SKOSIMP) (INST?))) NIL
                  NIL))
                NIL)
               ("2" (INST?) NIL NIL)
               ("3" (USE "self_diag_exit2")
                (("3" (APPLY (THEN (GROUND) (SKOSIMP)))
                  (("3" (USE "excluded_exit2")
                    (("3" (APPLY (THEN (GROUND) (SKOSIMP) (INST?))) NIL
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|liveness1_timed_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|liveness1_timed_TCC2| "" (SUBTYPE-TCC))
 (|liveness1_timed| "" (SKOSIMP)
  (("" (USE "missed_rcv_exit1_timed")
    (("" (GROUND)
      (("1" (SKOSIMP)
        (("1" (USE "excluded_exit2_timed" :POLARITY? T)
          (("1" (GROUND)
            (("1" (SKOSIMP)
              (("1" (INST? :POLARITY? T) (("1" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)
       ("3" (SKOSIMP)
        (("3" (USE "self_diag_exit1_timed")
          (("3" (GROUND)
            (("3" (SKOSIMP)
              (("3" (USE "excluded_exit2_timed" :POLARITY? T)
                (("3" (GROUND)
                  (("3" (SKOSIMP)
                    (("3" (INST? :POLARITY? T) (("3" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|liveness1_timed1| "" (SKOSIMP)
  (("" (USE "liveness1_timed")
    (("" (GROUND)
      (("" (SKOSIMP)
        (("" (GROUND)
          (("1" (EXPAND "stable_timed")
            (("1" (GROUND)
              (("1" (INST?)
                (("1" (ASSERT)
                  (("1" (EXPAND "none_since_weak")
                    (("1" (INST - "n")
                      (("1" (ASSERT)
                        (("1" (LEMMA "cycle")
                          (("1" (INST - "n" "tf!1")
                            (("1" (GROUND)
                              (("1"
                                (INST + 1)
                                (("1" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (EXPAND "stable_timed2")
            (("2" (GROUND)
              (("2" (INST?)
                (("2" (ASSERT)
                  (("2" (EXPAND "one_since")
                    (("2" (INST - "n")
                      (("2" (GROUND)
                        (("2" (LEMMA "cycle")
                          (("2" (INST - "n" "tf!1")
                            (("2" (GROUND)
                              (("2"
                                (INST + 1)
                                (("2" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|liveness2_timed_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|liveness2_timed| "" (SKOSIMP)
  (("" (USE "latent_to_excluded2_timed" :POLARITY? T)
    (("" (GROUND)
      (("" (USE "excluded2_exit1_timed")
        (("" (GROUND) (("" (SKOSIMP) (("" (INST?) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|liveness2_timed1| "" (SKOSIMP)
  (("" (USE "liveness2_timed")
    (("" (GROUND)
      (("" (SKOSIMP)
        (("" (EXPAND "stable_timed22")
          (("" (GROUND)
            (("" (INST?)
              (("" (ASSERT)
                (("" (EXPAND "one_yet")
                  (("" (FLATTEN)
                    (("" (USE "next_nf_prop2")
                      (("" (SKOSIMP)
                        (("" (INST - "j!2")
                          (("1" (ASSERT) NIL NIL)
                           ("2" (ASSERT) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|liveness| "" (SKOSIMP)
  (("" (USE "fault_arrival" :POLARITY? T)
    (("" (APPLY (THEN (GROUND) (SKOSIMP)))
      (("1" (USE "stable_to_stable")
        (("1" (APPLY (THEN (GROUND) (SKOSIMP) (INST?) (ASSERT))) NIL
          NIL))
        NIL)
       ("2" (USE "stable_to_latent")
        (("2" (GROUND)
          (("2" (USE "liveness1")
            (("2" (APPLY (THEN (GROUND) (SKOSIMP) (INST?) (ASSERT)))
              NIL NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|recovery| "" (SKOSIMP)
  (("" (USE "fault_arrival" :POLARITY? T)
    (("" (APPLY (THEN (GROUND) (SKOSIMP)))
      (("1" (USE "stable_to_stable" :POLARITY? T)
        (("1" (GROUND)
          (("1" (INST + 1)
            (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL)
       ("2" (USE "stable_to_latent")
        (("2" (GROUND)
          (("2" (USE "liveness2_timed1" :POLARITY? T)
            (("2" (GROUND)
              (("1" (SKOSIMP)
                (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)
               ("2" (USE "latent_to_missed_timed" :POLARITY? T)
                (("2" (GROUND)
                  (("2" (USE "liveness1_timed1" :POLARITY? T)
                    (("2" (GROUND)
                      (("2" (SKOSIMP)
                        (("2" (INST + "1+j!1") (("2" (GROUND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|validity| "" (SKOSIMP)
  (("" (USE "final_final")
    (("" (EXPAND "total")
      (("" (GROUND)
        (("1" (EXPAND "stable") (("1" (FORWARD-CHAIN -) NIL NIL)) NIL)
         ("2" (SKOSIMP)
          (("2" (FORWARD-CHAIN "latent_means_faulty")
            (("2" (EXPAND "latent")
              (("2" (GROUND)
                (("2" (INST? +)
                  (("2" (GROUND)
                    (("2" (INST - "p!1") (("2" (GROUND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("3" (SKOSIMP)
          (("3" (EXPAND "excluded")
            (("3" (GROUND) (("3" (GRIND) NIL NIL)) NIL)) NIL))
          NIL)
         ("4" (SKOSIMP)
          (("4" (EXPAND "missed_rcv_ext")
            (("4" (EXPAND "missed_rcv")
              (("4" (GROUND)
                (("4" (INST? +)
                  (("4" (GROUND)
                    (("4" (INST - "p!1") (("4" (GROUND) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("5" (SKOSIMP)
          (("5" (EXPAND "self_diag")
            (("5" (GROUND)
              (("5" (INST? +)
                (("5" (GROUND)
                  (("5" (INST - "p!1") (("5" (GROUND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|agreement| "" (SKOSIMP)
  (("" (USE "final_final")
    (("" (EXPAND "total")
      (("" (GROUND)
        (("1" (EXPAND "stable")
          (("1" (COPY -1)
            (("1" (FORWARD-CHAIN -)
              (("1" (FORWARD-CHAIN -) (("1" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (SKOSIMP)
          (("2" (FORWARD-CHAIN "latent_means_faulty")
            (("2" (EXPAND "latent")
              (("2" (GROUND)
                (("2" (COPY -6)
                  (("2" (FORWARD-CHAIN -)
                    (("2" (FORWARD-CHAIN -) (("2" (GROUND) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("3" (SKOSIMP)
          (("3" (EXPAND "excluded")
            (("3" (COPY -1)
              (("3" (FORWARD-CHAIN -)
                (("3" (FORWARD-CHAIN -) (("3" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("4" (SKOSIMP)
          (("4" (EXPAND "missed_rcv_ext")
            (("4" (EXPAND "missed_rcv")
              (("4" (GROUND)
                (("4" (COPY -3)
                  (("4" (FORWARD-CHAIN -)
                    (("4" (FORWARD-CHAIN -) (("4" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("5" (SKOSIMP)
          (("5" (EXPAND "self_diag")
            (("5" (GROUND)
              (("5" (COPY -2)
                (("5" (FORWARD-CHAIN -)
                  (("5" (FORWARD-CHAIN -) (("5" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$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




$$$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))))))))))))))))
$$$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_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_pos:        LEMMA mod(i,m) >= 0 AND mod(i,m) < 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)

  JUDGEMENT mod(i,m) HAS_TYPE below(m)

END 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_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)")
    (("" (TCC)
      (("" (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))))))