Nuprl Lemma : decidable__cs-inning-committable-some

{

[V:Type]
((

v,v':V. (

(v = v')))

(

v,v':V. Dec(v = v'))

(

A:Id List.

W:{a:Id| (a

A)}  List List.
          (one-intersection(A;W)

(

s:ConsensusState.

i:

.
Dec(

v:V. in state s, inning i could commit v ))))) }

{ Proof }

Definitions occuring in Statement : one-intersection: one-intersection(A;W), cs-inning-committable: in state s, inning i could commit v , consensus-state4: ConsensusState, Id: Id, decidable: Dec(P), uall:

[x:A]. B[x], all:

x:A. B[x], exists:

x:A. B[x], not:

A, implies: P

Q, set: {x:A| B[x]} , list: type List, int:

, universe: Type, equal: s = t, l_member: (x

l)
Definitions : limited-type: LimitedType, member: t

T, strong-subtype: strong-subtype(A;B), ge: i

j , uimplies: b supposing a, uiff: uiff(P;Q), subtype_rel: A

r B, false: False, iff: P

Q, less_than: a < b, le: A

B, assert:

b, int_seg: {i..j

}, divides: b | a, assoced: a ~ b, set_leq: a

b, set_lt: a <p b, grp_lt: a < b, cand: A c

B, l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, nat:

, l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), apply: f a, infix_ap: x f y, and: P

Q, fun-connected: y is f*(x), qle: r

s, qless: r < s, q-rel: q-rel(r;x), i-finite: i-finite(I), i-closed: i-closed(I), p-outcome: Outcome, fset-member: a

s, f-subset: xs

ys, fset-closed: (s closed under fs), l_disjoint: l_disjoint(T;l1;l2), cs-not-completed: in state s, a has not completed inning i, cs-archived: by state s, a archived v in inning i, cs-passed: by state s, a passed inning i without archiving a value, cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-precondition: state s may consider v in inning i, cs-inning-committed: in state s, inning i has committed v, cs-inning-committable: in state s, inning i could commit v , int:

, consensus-state4: ConsensusState, uall:

[x:A]. B[x], isect:

x:A. B[x], or: P

Q, union: left + right, universe: Type, exists:

x:A. B[x], product: x:A

B[x], not:

A, decidable: Dec(P), equal: s = t, list: type List, set: {x:A| B[x]} , l_member: (x

l), Id: Id, implies: P

Q, one-intersection: one-intersection(A;W), prop:

, all:

x:A. B[x], function: x:A

B[x], D: Error :D, Auto: Error :Auto, CollapseTHENA: Error :CollapseTHENA, CollapseTHEN: Error :CollapseTHEN, tactic: Error :tactic, void: Void, lambda:

x.A[x], rev_implies: P

Q, nat_plus:

, rationals:

, atom: Atom$n, dstype: dstype(TypeNames; d; a), fset: FSet{T}, string: Error :string, IdLnk: IdLnk, Knd: Knd, MaName: MaName, consensus-state3: consensus-state3(T), so_lambda:

x.t[x], fpf: a:A fp-> B[a], bool:

, MaAuto: Error :MaAuto
Lemmas : false_wf, l_exists_wf, cs-not-completed_wf, decidable__cs-not-completed, decidable__equal_Id, decidable__equal_set, decidable__l_member, decidable__implies_better, decidable__all-list, decidable__l_exists_better-extract, decidable__cs-inning-committable, decidable__or, member_wf, cs-inning-committable_wf, consensus-state4_wf, one-intersection_wf, l_member_wf, Id_wf, decidable_wf, not_wf, cs-inning-committable-some1

\mforall{}[V:Type] ((\mexists{}v,v':V. (\mneg{}(v = v'))) {}\mRightarrow{} (\mforall{}v,v':V. Dec(v = v')) {}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List. (one-intersection(A;W) {}\mRightarrow{} (\mforall{}s:ConsensusState. \mforall{}i:\mBbbZ{}. Dec(\mexists{}v:V. in state s, inning i could commit v ))))) Date html generated: 2011_08_16-AM-10_02_11 Last ObjectModification: 2011_06_18-AM-09_00_27 Home Index