---

{ [V:Type]. [A:Id List]. [W:{a:Id| (a  A)}  List List].
  [s,s2:ConsensusState].
    [i:]. [v,v2:V].
      (v = v2) supposing 
         (in state s, inning i has committed v2 and 
         in state s2, inning i could commit v  and 
         two-intersection(A;W)) 
    supposing s ts-rel(consensus-ts4(V;A;W)) s2 }

{ Proof }

---

Definitions occuring in Statement :  two-intersection: two-intersection(A;W),  cs-inning-committable: in state s, inning i could commit v ,  cs-inning-committed: in state s, inning i has committed v,  consensus-ts4: consensus-ts4(V;A;W),  consensus-state4: ConsensusState,  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  infix_ap: x f y,  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  equal: s = t,  l_member: (x  l),  ts-rel: ts-rel(ts)
Definitions :  assert: b,  pair: <a, b>,  axiom: Ax,  cs-not-completed: in state s, a has not completed inning i,  cs-archived: by state s, a archived v in inning i,  cs-inning-committed: in state s, inning i has committed v,  l_all: (xL.P[x]),  cs-inning-committable: in state s, inning i could commit v ,  two-intersection: two-intersection(A;W),  bool: ,  transition-system: transition-system{i:l},  tag-by: zT,  rev_implies: P  Q,  iff: P  Q,  record+: record+,  record: record(x.T[x]),  fset: FSet{T},  isect2: T1  T2,  b-union: A  B,  true: True,  intensional-universe: IType,  int-deq: IntDeq,  fpf-cap: f(x)?z,  fpf-single: x : v,  fpf-join: f  g,  cs-precondition: state s may consider v in inning i,  exists: x:A. B[x],  top: Top,  fpf-domain: fpf-domain(f),  natural_number: $n,  add: n + m,  union: left + right,  or: P  Q,  cs-estimate: Estimate(s;a),  lambda: x.A[x],  so_lambda: x.t[x],  cs-inning: Inning(s;a),  limited-type: LimitedType,  implies: P  Q,  strong-subtype: strong-subtype(A;B),  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  and: P  Q,  uiff: uiff(P;Q),  subtype_rel: A r B,  spread: spread def,  pi1: fst(t),  ts-type: ts-type(ts),  consensus-ts4: consensus-ts4(V;A;W),  ts-rel: ts-rel(ts),  apply: f a,  infix_ap: x f y,  uimplies: b supposing a,  fpf: a:A fp-> B[a],  int: ,  product: x:A  B[x],  consensus-state4: ConsensusState,  prop: ,  isect: x:A. B[x],  all: x:A. B[x],  function: x:A  B[x],  uall: [x:A]. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  list: type List,  universe: Type,  member: t  T,  equal: s = t,  tactic: Error :tactic,  ts-stable: ts-stable(ts;x.P[x])
Lemmas :  consensus-ts4-inning-committed-stable,  cs-inning-committed-single,  member_wf,  ts-type_wf,  consensus-ts4_wf,  ts-rel_wf,  subtype_rel_wf,  consensus-state4_wf,  Id_wf,  l_member_wf,  not_wf,  cs-inning_wf,  fpf_wf,  cs-estimate_wf,  fpf-domain_wf,  top_wf,  cs-precondition_wf,  fpf-join_wf,  fpf-single_wf,  int-deq_wf,  intensional-universe_wf,  two-intersection_wf,  cs-inning-committable_wf,  cs-inning-committed_wf

---

\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].  \mforall{}[s,s2:ConsensusState].
    \mforall{}[i:\mBbbZ{}].  \mforall{}[v,v2:V].
        (v  =  v2)  supposing 
              (in  state  s,  inning  i  has  committed  v2  and 
              in  state  s2,  inning  i  could  commit  v    and 
              two-intersection(A;W)) 
    supposing  s  ts-rel(consensus-ts4(V;A;W))  s2


Date html generated: 2011_08_16-AM-10_01_36
Last ObjectModification: 2011_06_18-AM-08_58_58

Home Index