Nuprl Lemma : base-disjoint-classrel
A,B:Type. es:EO'. hdr1,hdr2:Name. ((
(hdr1 = hdr2)) 
disjoint-classrel(es;A;Base(hdr1;A);B;Base(hdr2;B)))
Proof not projected
Definitions occuring in Statement :
base-headers-msg-val: Base(hdr;typ),
Message: Message,
disjoint-classrel: disjoint-classrel(es;A;X;B;Y),
event-ordering+: EO+(Info),
name: Name,
all: x:A. B[x],
not: A,
implies: P Q,
universe: Type,
equal: s = t
Definitions :
all: x:A. B[x],
name: Name,
implies: P Q,
not: A,
disjoint-classrel: disjoint-classrel(es;A;X;B;Y),
or: P 
Q,
member: t 
T,
guard: {T},
false: False,
so_lambda: 
x.t[x],
decidable: Dec(P),
uall: [x:A]. B[x],
uimplies: b supposing a,
squash: 
T,
and: P 
Q,
uiff: uiff(P;Q),
sq_type: SQType(T),
so_apply: x[s],
prop: 
,
subtype: S 
T
Lemmas :
decidable__equal_name,
es-header_wf,
base-noloc-classrel,
subtype_base_sq,
name_wf,
list_subtype_base,
atom_subtype_base,
classrel_wf,
base-headers-msg-val_wf,
all_wf,
not_wf,
es-E_wf,
event-ordering+_inc,
equal_wf,
event-ordering+_wf,
Message_wf
\mforall{}A,B:Type. \mforall{}es:EO'. \mforall{}hdr1,hdr2:Name.
((\mneg{}(hdr1 = hdr2)) {}\mRightarrow{} disjoint-classrel(es;A;Base(hdr1;A);B;Base(hdr2;B)))
Date html generated:
2012_01_23-PM-01_24_26
Last ObjectModification:
2012_01_12-AM-01_26_19
Home
Index