Nuprl Lemma : ohc_v1-ilf-part1
HIDDEN 
HIDDEN HIDDEN HIDDEN HIDDEN
Proof not projected
Definitions occuring in Statement :
ohc_v1_Initial: ohc_v1_Initial(Cmd),
ohc_v1_Halt: ohc_v1_Halt(),
ohc_v1_RoundInfo: ohc_v1_RoundInfo(Cmd),
ohc_v1_vote'base: ohc_v1_vote'base(Cmd),
ohc_v1_proposal'base: ohc_v1_proposal'base(Cmd),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
classrel: v 
X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
sq_or: a 
b,
it: 
,
uall: 
[x:A]. B[x],
guard: {T},
all: x:A. B[x],
exists: 
x:A. B[x],
iff: P 
Q,
and: P Q,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
union: left + right,
cons: [car / cdr],
nil: [],
int: 
,
token: "$token",
universe: Type,
equal: s = t,
hide: HIDDEN,
valueall-type: valueall-type(T)
Definitions :
and: P Q,
hide: HIDDEN,
uall: [x:A]. B[x],
all: x:A. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
member: t T,
prop: 
,
name: Name,
vatype: ValueAllType,
implies: P Q,
rev_implies: P Q,
bag-member: x bs,
squash: T,
true: True,
ohc_v1_vote'base: ohc_v1_vote'base(Cmd),
ohc_v1_proposal'base: ohc_v1_proposal'base(Cmd),
sq_or: a b,
exists: x:A. B[x],
or: P Q,
cand: A c B,
so_lambda: 
x.t[x],
ohc_v1_retry'base: ohc_v1_retry'base(Cmd),
ohc_v1_prop2retry: ohc_v1_prop2retry(Cmd),
ohc_v1_RoundInfo: ohc_v1_RoundInfo(Cmd),
ohc_v1_initial'base: ohc_v1_initial'base(Cmd),
ohc_v1_prop2init: ohc_v1_prop2init(Cmd),
ohc_v1_Initial: ohc_v1_Initial(Cmd),
nequal: a 
b T ,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
ohc_v1_decided'base: ohc_v1_decided'base(),
ohc_v1_Halt: ohc_v1_Halt(),
so_apply: x[s],
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
unit: Unit,
bool: 
,
subtype: S 
T,
it:
Lemmas :
classrel_wf,
Message_wf,
unit_wf2,
Id_wf,
base-headers-msg-val_wf,
ohc_v1_vote'base_wf,
false_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
valueall-type_wf,
ohc_v1_proposal'base_wf,
exists_wf,
bag-member_wf,
single-bag_wf,
or_wf,
squash_wf,
sq_or_wf,
parallel-class_wf,
ohc_v1_retry'base_wf,
simple-loc-comb-1_wf,
concat-lifting-loc-1_wf,
ohc_v1_prop2retry_wf,
ohc_v1_RoundInfo_wf,
exists-product1,
bag-member-single-weak,
sq_or_squash3,
parallel-classrel-weak,
simple-loc-comb-1-concat-classrel-weak,
es-loc_wf,
ohc_v1_initial'base_wf,
ohc_v1_prop2init_wf,
ohc_v1_Initial_wf,
true_wf,
ifthenelse_wf,
eq_int_wf,
it_wf,
bag_wf,
empty-bag_wf,
ohc_v1_decided'base_wf,
ohc_v1_Halt_wf,
and_true_r,
squash_and,
squash-classrel,
squash_equal,
exists-elim,
equal_wf,
or_false_r,
iff_transitivity,
assert_wf,
not_wf,
ifthenelse-prop,
or_functionality_wrt_iff,
nequal_wf,
and_functionality_wrt_uiff2,
assert_of_eq_int,
neg_assert_of_eq_int,
trivial-eq,
and_false_r,
bag-member-ifthenelse,
bool_wf,
uiff_transitivity,
eqtt_to_assert,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
bag-member-empty-weak
HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN
Date html generated:
2012_02_20-PM-05_29_22
Last ObjectModification:
2012_02_16-PM-03_49_44
Home
Index