{ 
[V:Type]
ts-refinement(consensus-ts2(V);consensus-ts3(V);
L.cs-ref-map3(L)) }
{ Proof }
Definitions occuring in Statement :
cs-ref-map3: cs-ref-map3(L),
consensus-ts3: consensus-ts3(T),
consensus-ts2: consensus-ts2(T),
uall: [x:A]. B[x],
lambda: x.A[x],
universe: Type,
ts-refinement: ts-refinement(ts1;ts2;f)
Definitions :
btrue: tt,
reduce: reduce(f;k;as),
pi2: snd(t),
hd: hd(l),
null: null(as),
ifthenelse: if b then t else f fi ,
filter: filter(P;l),
let: let,
pi1: fst(t),
member: t 
T,
consensus-ts3: consensus-ts3(T),
cs-ref-map3: cs-ref-map3(L),
ts-init: ts-init(ts),
consensus-ts2: consensus-ts2(T),
ts-type: ts-type(ts),
implies: P 
Q,
all: x:A. B[x],
ts-rel: ts-rel(ts),
prop: 
,
exists: 
x:A. B[x],
and: P 
Q,
or: P 
Q,
infix_ap: x f y,
cand: A c B,
guard: {T},
consensus-state2: consensus-state2(T),
iff: P 
Q,
rev_implies: P Q,
lelt: i 
j < k,
l_member: (x l),
not: 
A,
int_seg: {i..j
},
true: True,
squash: 
T,
ts-reachable: ts-reachable(ts),
top: Top,
false: False,
le: A B,
ycomb: Y,
length: ||as||,
append: as @ bs,
label: ...$L... t,
ge: i 
j ,
bfalse: ff,
lt_int: i <z j,
bnot: 
b,
le_int: i z j,
select: l[i],
ts-final: ts-final(ts),
isl: isl(x),
outl: outl(x),
cs-committed-val: cs-committed-val(x),
cs-is-committed: cs-is-committed(x),
cs-commited: COMMITED[v],
uimplies: b supposing a,
uall: [x:A]. B[x],
nat: 
,
decidable: Dec(P)
Lemmas :
ts-rel_wf,
cs-ambivalent_wf,
ts-init_wf,
consensus-ts2_wf,
ts-type_wf,
rel_star_weakening,
consensus-state2_wf,
cs-ref-map3_wf,
cs-decided_wf2,
cs-predecided_wf,
rel_star_wf,
consensus-state2-cases,
rel_rel_star,
rel_star_transitivity,
cs-ref-map3-decided,
cs-considering_wf,
consensus-state3_wf,
l_member_wf,
consensus-ts3-invariant1,
member_singleton,
or_functionality_wrt_iff,
member_append,
iff_transitivity,
cs-initial_wf,
cs-commited_wf,
select_wf,
le_wf,
length_wf1,
squash_wf,
consensus-state3-unequal,
consensus-ts3_wf,
ts-final_wf,
cs-withdrawn_wf,
length_wf2,
nat_wf,
top_wf,
length_wf_nat,
not_wf,
int_seg_wf,
non_neg_length,
length_cons,
length_nil,
int_seg_properties,
decidable__equal_cs-withdrawn
\mforall{}[V:Type]. ts-refinement(consensus-ts2(V);consensus-ts3(V);\mlambda{}L.cs-ref-map3(L))
Date html generated:
2011_08_16-AM-09_57_27
Last ObjectModification:
2011_06_18-AM-08_56_31
Home
Index