{ 
[V:Type]
ts-refinement(consensus-ts1(V);consensus-ts2(V);
x.if cs-is-decided(x)
then x
else UNDECIDED
fi ) }
{ Proof }
Definitions occuring in Statement :
consensus-ts2: consensus-ts2(T),
cs-is-decided: cs-is-decided(x),
consensus-ts1: consensus-ts1(T),
cs-undecided: UNDECIDED,
ifthenelse: if b then t else f fi ,
uall: [x:A]. B[x],
lambda: x.A[x],
universe: Type,
ts-refinement: ts-refinement(ts1;ts2;f)
Definitions :
uall: [x:A]. B[x],
ts-refinement: ts-refinement(ts1;ts2;f),
and: P 
Q,
infix_ap: x f y,
all: x:A. B[x],
implies: P 
Q,
member: t 
T,
ts-type: ts-type(ts),
consensus-ts1: consensus-ts1(T),
ts-init: ts-init(ts),
ifthenelse: if b then t else f fi ,
cs-is-decided: cs-is-decided(x),
consensus-ts2: consensus-ts2(T),
pi1: fst(t),
isl: isl(x),
pi2: snd(t),
cs-ambivalent: AMBIVALENT,
bfalse: ff,
ts-rel: ts-rel(ts),
consensus-state2: consensus-state2(T),
or: P 
Q,
exists: 
x:A. B[x],
cs-predecided: PREDECIDED[v],
cs-decided: Decided[v],
prop: 
,
btrue: tt,
cand: A c B,
top: Top,
ts-reachable: ts-reachable(ts),
guard: {T},
ts-final: ts-final(ts),
uimplies: b supposing a,
sq_type: SQType(T),
bool: 
,
unit: Unit,
iff: P 
Q,
assert: 
b,
false: False,
it: 
Lemmas :
ts-rel_wf,
consensus-ts2_wf,
ts-reachable_wf,
ts-type_wf,
ts-final_wf,
consensus-ts1_wf,
rel_star_weakening,
ts-init_wf,
cs-undecided_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
rel_star_wf,
consensus-state2_wf,
cs-predecided_wf,
cs-decided_wf2,
bfalse_wf,
cs-is-decided_wf,
consensus-state1_wf,
cs-decided_wf,
rel_rel_star,
top_wf,
iff_weakening_uiff,
assert_wf,
eqtt_to_assert,
not_wf,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
cs-ambivalent_wf,
rel_star_transitivity
\mforall{}[V:Type]
ts-refinement(consensus-ts1(V);consensus-ts2(V);\mlambda{}x.if cs-is-decided(x) then x else UNDECIDED fi )
Date html generated:
2011_08_16-AM-09_54_55
Last ObjectModification:
2011_06_18-AM-08_54_44
Home
Index