Nuprl Lemma : consensus-refinement2
∀[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)
Lemmas :
infix_ap_wf,
ts-reachable_wf,
consensus-ts3_wf,
subtype_rel_set,
subtype_rel_wf,
ts-type_wf,
ts-rel_wf,
subtype_rel_dep_function,
subtype_rel_self,
ts-final_wf,
consensus-ts2_wf,
cs-ambivalent_wf,
null_nil_lemma,
filter_nil_lemma,
ts-init_wf,
rel_star_weakening,
consensus-state2-cases,
cs-ref-map3_wf,
consensus-state2_wf,
rel_star_wf,
top_wf,
cs-decided_wf2,
cs-predecided_wf,
equal_wf,
exists_wf,
equal-wf-T-base,
or_wf,
equal-wf-base-T,
rel_rel_star,
rel_star_transitivity,
cs-ref-map3-predecided,
l_member_wf,
consensus-state3_wf,
cs-commited_wf,
all_wf,
not_wf,
cs-considering_wf,
cs-ref-map3-decided,
consensus-ts3-invariant1,
member_singleton,
nil_wf,
cs-initial_wf,
cons_wf,
member_append,
btrue_neq_bfalse,
bfalse_wf,
bool_wf,
isl_wf,
and_wf,
btrue_wf,
sq_stable__le,
select_wf,
less_than_wf,
le-add-cancel,
add-commutes,
add-swap,
add-associates,
add_functionality_wrt_le,
less-iff-le,
le_antisymmetry_iff,
false_wf,
decidable__lt,
lelt_wf,
le_weakening,
less_than_transitivity1,
list_wf,
length_wf,
le_wf,
squash_wf,
consensus-state3-unequal,
int_seg_subtype-nat,
assert_wf,
cs-is-considering_wf,
int_seg_wf,
decidable__exists_int_seg,
decidable__cand,
decidable__not,
decidable__equal_int,
decidable__assert,
assert-cs-is-considering,
iff_weakening_equal,
cs-ref-map3-ambivalent,
equal-wf-base,
colength_wf,
int-value-type,
set-value-type,
nat_wf,
has-value_wf-partial,
colist_wf,
lt_int_wf,
cons_wf_listp,
length_of_cons_lemma,
base_wf,
stuck-spread,
length_of_nil_lemma,
list_ind_nil_lemma,
list_ind_cons_lemma,
cs-withdrawn_wf,
less_than_irreflexivity,
le-add-cancel2,
minus-zero,
minus-add,
condition-implies-le,
zero-add,
add-zero,
not-equal-2,
length_wf_nat,
length_cons,
length_wf_nil,
non_neg_length,
length_nil,
length-singleton,
reduce_hd_cons_lemma,
null_cons_lemma,
filter_cons_lemma
\mforall{}[V:Type]. ts-refinement(consensus-ts2(V);consensus-ts3(V);\mlambda{}L.cs-ref-map3(L))
Date html generated:
2015_07_17-AM-11_25_21
Last ObjectModification:
2015_07_16-AM-09_49_01
Home
Index