Nuprl Lemma : cs-ref-map3-ambivalent
∀[V:Type]. ∀[L:ts-reachable(consensus-ts3(V))].
  uiff((∀[v:V]. (¬(COMMITED[v] ∈ L))) ∧ (∀[v:V]. (¬(CONSIDERING[v] ∈ L)));cs-ref-map3(L)
  = AMBIVALENT
  ∈ consensus-state2(V))
Proof
Definitions occuring in Statement : 
cs-ref-map3: cs-ref-map3(L)
, 
consensus-ts3: consensus-ts3(T)
, 
cs-commited: COMMITED[v]
, 
cs-considering: CONSIDERING[v]
, 
consensus-state3: consensus-state3(T)
, 
cs-ambivalent: AMBIVALENT
, 
consensus-state2: consensus-state2(T)
, 
l_member: (x ∈ l)
, 
uiff: uiff(P;Q)
, 
uall: ∀[x:A]. B[x]
, 
not: ¬A
, 
and: P ∧ Q
, 
universe: Type
, 
equal: s = t ∈ T
, 
ts-reachable: ts-reachable(ts)
Lemmas : 
uall_wf, 
not_wf, 
l_member_wf, 
consensus-state3_wf, 
cs-considering_wf, 
cs-commited_wf, 
equal-wf-T-base, 
ts-reachable_wf, 
consensus-ts3_wf, 
subtype_rel_wf, 
ts-type_wf, 
consensus-ts3-invariant1, 
cs-ref-map3-decided, 
cs-ref-map3-predecided, 
consensus-state2_wf, 
cs-ref-map3_wf, 
filter_is_empty, 
cs-is-committed_wf, 
null_wf3, 
filter_wf5, 
subtype_rel_list, 
top_wf, 
bool_wf, 
assert_wf, 
list_wf, 
bnot_wf, 
uiff_transitivity, 
eqtt_to_assert, 
assert_of_null, 
iff_transitivity, 
iff_weakening_uiff, 
eqff_to_assert, 
assert_of_bnot, 
cs-is-considering_wf, 
cs-ambivalent_wf, 
uiff_wf, 
true_wf, 
int_seg_wf, 
select_wf, 
sq_stable__le, 
length_wf, 
false_wf, 
assert-cs-is-considering, 
int_seg_subtype-nat, 
less_than_wf, 
assert-cs-is-committed, 
btrue_wf, 
and_wf, 
equal_wf, 
isl_wf, 
bfalse_wf, 
btrue_neq_bfalse, 
ppcc-problem, 
unit_wf2, 
iff_weakening_equal
\mforall{}[V:Type].  \mforall{}[L:ts-reachable(consensus-ts3(V))].
    uiff((\mforall{}[v:V].  (\mneg{}(COMMITED[v]  \mmember{}  L)))  \mwedge{}  (\mforall{}[v:V].  (\mneg{}(CONSIDERING[v]  \mmember{}  L)));cs-ref-map3(L)
    =  AMBIVALENT)
Date html generated:
2015_07_17-AM-11_24_59
Last ObjectModification:
2015_02_04-PM-05_01_39
Home
Index