Nuprl Lemma : cs-ref-map-step
[V:Type]
({
v1,v2:V. (
(v1 = v2))}
(A:Id List. W:{a:Id| (a 
A)} List List.
f:ConsensusState 
(consensus-state3(V) List)
(cs-ref-map-constraints(V;A;W;f)
(x,y:ts-reachable(consensus-ts4(V;A;W)).
((x ts-rel(consensus-ts4(V;A;W)) y)
{(||f x|| 
||f y||)
(i:
((j:
||f x||. f y[j] = f x[j] supposing (j = i))
(||f y|| = (||f x|| + 1)) (f y[||f x||] = INITIAL) supposing ||f x|| < ||f y||))})))
supposing ||W|| 
1 ))
Proof not projected
Definitions occuring in Statement :
cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),
consensus-ts4: consensus-ts4(V;A;W),
consensus-state4: ConsensusState,
cs-initial: INITIAL,
consensus-state3: consensus-state3(T),
Id: Id,
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
guard: {T},
infix_ap: x f y,
ge: i j ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
add: n + m,
natural_number: $n,
int: ,
universe: Type,
equal: s = t,
l_member: (x l),
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts)
Definitions :
so_lambda: 
x.t[x],
cand: A c B,
prop: 
,
false: False,
member: t T,
le: A B,
and: P Q,
infix_ap: x f y,
ge: i j ,
uimplies: b supposing a,
all: x:A. B[x],
not: A,
exists: x:A. B[x],
guard: {T},
implies: P Q,
uall: [x:A]. B[x],
pi2: snd(t),
pi1: fst(t),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts),
consensus-ts4: consensus-ts4(V;A;W),
subtype: S 
T,
top: Top,
squash: 
T,
true: True,
rev_implies: P 
Q,
iff: P Q,
Id: Id,
or: P 
Q,
so_apply: x[s],
consensus-state4: ConsensusState,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
cs-not-completed: in state s, a has not completed inning i,
cs-archived: by state s, a archived v in inning i,
lelt: i j < k,
cs-inning-committed: in state s, inning i has committed v,
cs-inning-committable: in state s, inning i could commit v ,
int_seg: {i..j},
nat: ,
null: null(as),
assert: 
b,
ts-init: ts-init(ts),
ts-reachable: ts-reachable(ts),
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y]),
decidable: Dec(P),
cs-ref-map-constraints: cs-ref-map-constraints(V;A;W;f),
consensus-rel: CR[x,y],
uiff: uiff(P;Q),
sq_type: SQType(T),
fpf-single: x : v,
fpf-domain: fpf-domain(f),
unit: Unit,
bool: 
,
ycomb: Y,
length: ||as||,
it: 
Lemmas :
equal_wf,
not_wf,
exists_wf,
guard_wf,
ge_wf,
consensus-state3_wf,
consensus-state4_wf,
cs-ref-map-constraints_wf,
ts-type_wf,
ts-reachable_wf,
consensus-ts4_wf,
ts-rel_wf,
l_member_wf,
Id_wf,
length_wf,
rel_rel_star,
le_wf,
cs-inning_wf,
consensus-ts4-inning-rel,
top_wf,
length_wf_nat,
decidable__le,
cs-initial_wf,
non_neg_length,
select_wf,
isect_wf,
int_seg_wf,
all_wf,
decidable__equal_Id,
true_wf,
squash_wf,
fpf_wf,
member_wf,
fpf-trivial-subtype-top,
iff_wf,
subtype-top,
subtype-fpf2,
cs-estimate_wf,
fpf-domain_wf,
atom2_subtype_base,
subtype_base_sq,
fpf-domain-join,
iff_functionality_wrt_iff,
member_singleton,
or_functionality_wrt_iff,
int-deq_wf,
fpf-single_wf,
subtype_rel_simple_product,
subtype_rel_self,
subtype_rel_function,
member-fpf-dom,
deq_wf,
fpf-dom_wf,
assert_wf,
fpf-ap_wf,
int_seg_properties,
fpf-join-ap-sq,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
iff_weakening_uiff,
bnot_wf,
bool_wf,
member-fpf-domain,
int_subtype_base,
cs-inning-committed_wf,
cs-inning-committable_wf,
or_wf,
cs-archived_wf,
cs-not-completed_wf,
lelt_wf,
cs-ref-map-equal,
less_than_wf,
nat_wf,
and_wf,
decidable__cs-not-completed,
hd_member,
hd_wf,
false_wf,
consensus-ts4-estimate-domain,
fpf-empty_wf,
consensus-rel_wf,
rel_star_wf
\mforall{}[V:Type]
(\{\mexists{}v1,v2:V. (\mneg{}(v1 = v2))\}
{}\mRightarrow{} (\mforall{}A:Id List. \mforall{}W:\{a:Id| (a \mmember{} A)\} List List.
\mforall{}f:ConsensusState {}\mrightarrow{} (consensus-state3(V) List)
(cs-ref-map-constraints(V;A;W;f)
{}\mRightarrow{} (\mforall{}x,y:ts-reachable(consensus-ts4(V;A;W)).
((x ts-rel(consensus-ts4(V;A;W)) y)
{}\mRightarrow{} \{(||f x|| \mleq{} ||f y||)
\mwedge{} (\mexists{}i:\mBbbZ{}
((\mforall{}j:\mBbbN{}||f x||. f y[j] = f x[j] supposing \mneg{}(j = i))
\mwedge{} (||f y|| = (||f x|| + 1)) \mwedge{} (f y[||f x||] = INITIAL)
supposing ||f x|| < ||f y||))\})))
supposing ||W|| \mgeq{} 1 ))
Date html generated:
2012_01_23-PM-12_05_01
Last ObjectModification:
2011_12_14-PM-04_14_56
Home
Index