Nuprl Lemma : consensus-ts6-reachability1

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀L:consensus-event(V;A) List.
  ∀x,y:{a:Id| (a ∈ A)}  ⟶ (consensus-event(V;A) List). ∀a:{a:Id| (a ∈ A)} .
    ((∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
        ((consensus-message(b;i;z) ∈ L)
        ⇒ let i',est,knw = consensus-accum-state(A;x b) in
           (i ≤ i')
           ∧ case z
              of inl(p) =>
              let j,v = p

              in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (¬↑k ∈ dom(est)) supposing (k < i and j < k)) ∧ (v = est(j) ∈ V)

              | inr(a) =>
              ∀j:ℤ. ¬↑j ∈ dom(est) supposing j < i))
       ⇒ (∀v:V. ∀j:ℕ||L||.
             let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;L)) in

             (¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw)

             supposing L[j] = Archive(v) ∈ consensus-event(V;A))
       ⇒ (x (ts-rel(consensus-ts6(V;A;W))^*) y)) supposing
       (((y a) = ((x a) @ L) ∈ (consensus-event(V;A) List)) and

       (∀b:{a:Id| (a ∈ A)} . (y b) = (x b) ∈ (consensus-event(V;A) List) supposing ¬(b = a ∈ Id)))

Proof

Definitions occuring in Statement : consensus-ts6: consensus-ts6(V;A;W), consensus-accum-state: consensus-accum-state(A;L), consensus-message: consensus-message(b;i;z), archive-event: Archive(v), consensus-event: consensus-event(V;A), cs-knowledge-precondition: may consider v in inning i based on knowledge (s), fpf-ap: f(x), fpf-domain: fpf-domain(f), fpf-dom: x ∈ dom(f), Id: Id, firstn: firstn(n;as), l_member: (x ∈ l), select: L[n], length: ||as||, append: as @ bs, list: T List, int-deq: IntDeq, rel_star: R^*, int_seg: {i..j^-}, nat: ℕ, assert: ↑b, less_than: a < b, spreadn: spread3, uimplies: b supposing a, uall: ∀[x:A]. B[x], infix_ap: x f y, le: A ≤ B, all: ∀x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, unit: Unit, set: {x:A| B[x]} , apply: f a, function: x:A ⟶ B[x], spread: spread def, product: x:A × B[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], union: left + right, natural_number: $n, int: ℤ, universe: Type, equal: s = t ∈ T, ts-rel: ts-rel(ts), ts-type: ts-type(ts)
Definitions unfolded in proof : uall: ∀[x:A]. B[x], all: ∀x:A. B[x], member: t ∈ T, so_lambda: λ₂x.t[x], so_apply: x[s], implies: P ⇒ Q, guard: {T}, prop: ℙ, uimplies: b supposing a, nat: ℕ, spreadn: spread3, int_seg: {i..j^-}, lelt: i ≤ j < k, and: P ∧ Q, subtype_rel: A ⊆r B, top: Top, decidable: Dec(P), or: P ∨ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, not: ¬A, less_than: a < b, squash: ↓T, ts-type: ts-type(ts), pi1: fst(t), consensus-ts6: consensus-ts6(V;A;W), consensus-state6: consensus-state6(V;A), select: L[n], nil: [], it: ⋅, so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], firstn: firstn(n;as), so_lambda: so_lambda(x,y,z.t[x; y; z]), so_apply: x[s1;s2;s3], iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, bool: 𝔹, unit: Unit, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , bfalse: ff, sq_type: SQType(T), bnot: ¬_bb, assert: ↑b, le: A ≤ B, ts-rel: ts-rel(ts), pi2: snd(t), infix_ap: x f y, consensus-event-constraint: e@a allowed in state x, ge: i ≥ j , consensus-accum-state: consensus-accum-state(A;L), Id: Id, list_accum: list_accum, cand: A c∧ B, consensus-accum: consensus-accum(s;e), consensus-event: consensus-event(V;A), one-consensus-event: y = x after e@a

Latex:
\mforall{}[V:Type] \mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. \mforall{}L:consensus-event(V;A) List. \mforall{}x,y:\{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-event(V;A) List). \mforall{}a:\{a:Id| (a \mmember{} A)\} . ((\mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbN{}. \mforall{}z:\mBbbN{}i \mtimes{} V?. ((consensus-message(b;i;z) \mmember{} L) {}\mRightarrow{} let i',est,knw = consensus-accum-state(A;x b) in (i \mleq{} i') \mwedge{} case z of inl(p) => let j,v = p in (\muparrow{}j \mmember{} dom(est)) \mwedge{} (\mforall{}k:\mBbbZ{}. (\mneg{}\muparrow{}k \mmember{} dom(est)) supposing (k < i and j < k)) \mwedge{} (v = est(j\000C)) | inr(a) => \mforall{}j:\mBbbZ{}. \mneg{}\muparrow{}j \mmember{} dom(est) supposing j < i)) {}\mRightarrow{} (\mforall{}v:V. \mforall{}j:\mBbbN{}||L||. let i,est,knw = consensus-accum-state(A;(x a) @ firstn(j;L)) in (\mneg{}(i \mmember{} fpf-domain(est))) \mwedge{} may consider v in inning i based on knowledge (knw) supposing L[j] = Archive(v)) {}\mRightarrow{} (x rel\_star(ts-type(consensus-ts6(V;A;W)); ts-rel(consensus-ts6(V;A;W))) y)) supposing (((y a) = ((x a) @ L)) and (\mforall{}b:\{a:Id| (a \mmember{} A)\} . (y b) = (x b) supposing \mneg{}(b = a))) Date html generated: 2016_05_16-PM-00_32_12 Last ObjectModification: 2016_01_17-PM-03_59_24 Theory : event-ordering Home Index