Nuprl Lemma : consensus-refinement1
∀[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)
Lemmas :
infix_ap_wf,
ts-reachable_wf,
consensus-ts2_wf,
subtype_rel_set,
subtype_rel_wf,
ts-type_wf,
ts-rel_wf,
subtype_rel_dep_function,
subtype_rel_self,
ts-final_wf,
consensus-ts1_wf,
rel_star_weakening,
ts-init_wf,
bfalse_wf,
bool_wf,
eqtt_to_assert,
it_wf,
subtype_rel_sum,
top_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
cs-undecided_wf,
isect_subtype_rel_trivial,
consensus-state1_wf,
consensus-state2_wf,
rel_star_wf,
or_wf,
equal-wf-T-base,
exists_wf,
cs-predecided_wf,
cs-decided_wf2,
cs-is-decided_wf,
cs-decided_wf,
rel_rel_star,
cs-ambivalent_wf,
equal-wf-base-T,
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:
2015_07_17-AM-11_22_02
Last ObjectModification:
2015_01_28-AM-07_37_32
Home
Index