Nuprl Lemma : consensus-state2-cases
∀[V:Type]
∀x:consensus-state2(V)
((x = AMBIVALENT ∈ consensus-state2(V))
∨ (∃v:V. ((x = PREDECIDED[v] ∈ consensus-state2(V)) ∨ (x = Decided[v] ∈ consensus-state2(V)))))
Proof
Definitions occuring in Statement :
cs-predecided: PREDECIDED[v],
cs-ambivalent: AMBIVALENT,
consensus-state2: consensus-state2(T),
cs-decided: Decided[v],
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
union_subtype_base,
top_wf,
subtype_base_sq,
consensus-state2_wf,
equal-wf-T-base,
equal-wf-base-T,
equal-wf-base,
equal_wf,
or_wf,
cs-decided_wf2,
cs-predecided_wf,
isect_subtype_base,
exists_wf,
cs-ambivalent_wf
\mforall{}[V:Type]
\mforall{}x:consensus-state2(V). ((x = AMBIVALENT) \mvee{} (\mexists{}v:V. ((x = PREDECIDED[v]) \mvee{} (x = Decided[v]))))
Date html generated:
2015_07_17-AM-11_21_48
Last ObjectModification:
2015_01_28-AM-07_32_34
Home
Index