Nuprl Lemma : Q-R-glued-first
[Info:Type]
es:EO+(Info)
[Q,R:E 
E 
]. [A,B:Type].
Ias:EClass(A) List. Ibs:EClass(B) List. f:E(first-class(Ias)) B.
((i:
||Ias||. Ias[i]:Q f Ibs[i]:R)
first-class(Ias):Q f first-class(Ibs):R
supposing (Ia1,Ia2
Ias. e,e':E.
((
(Q e e')) 
((Q e' e))) supposing ((
e' 
Ia2) and (e Ia1)))) supposi\000Cng
((||Ias|| = ||Ibs||) and
(Ib1,Ib2Ibs. Ib1 
Ib2 = 0) and
(Ia1,Ia2Ias. Ia1 Ia2 = 0))
Proof not projected
Definitions occuring in Statement :
Q-R-glued: Ia:Qa f Ib:Rb,
es-interface-disjoint: X Y = 0,
es-E-interface: E(X),
first-class: first-class(L),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
select: l[i],
length: ||as||,
assert: b,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
list: type List,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
pairwise: (x,yL. P[x; y])
Definitions :
so_lambda: 
x y.t[x; y],
member: t T,
prop: ,
all: x:A. B[x],
uall: [x:A]. B[x],
subtype: S 
T,
le: A 
B,
top: Top,
cand: A c B,
false: False,
ycomb: Y,
not: A,
and: P Q,
implies: P Q,
length: ||as||,
es-interface-disjoint: X Y = 0,
pairwise: (x,yL. P[x; y]),
uimplies: b supposing a,
reduce: reduce(f;k;as),
first-class: first-class(L),
suptype: suptype(S; T),
so_lambda: x.t[x],
es-E-interface: E(X),
true: True,
ifthenelse: if b then t else f fi ,
guard: {T},
btrue: tt,
or: P 
Q,
assert: b,
rev_implies: P 
Q,
iff: P Q,
rel_equivalent: R1 R2,
infix_ap: x f y,
es-interface-predicate: {I},
rel-restriction: R|P,
rel_or: R1 R2,
exists: 
x:A. B[x],
Q-R-glued: Ia:Qa f Ib:Rb,
l_exists: (xL. P[x]),
so_apply: x[s1;s2],
lelt: i j < k,
int_seg: {i..j},
so_apply: x[s],
sq_type: SQType(T),
bfalse: ff,
lt_int: i <z j,
bnot: b,
le_int: i z j,
select: l[i],
l_all: (xL.P[x]),
decidable: Dec(P)
Lemmas :
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
eclass_wf,
first-class_wf,
es-E-interface_wf,
es-interface-disjoint_wf,
length_wf_nat,
non_neg_length,
length_cons,
length_wf,
es-interface-top,
not_wf,
int_seg_wf,
length_wf2,
int_seg_properties,
top_wf,
Error :eclass_wf,
select_wf,
in-eclass_wf,
assert_wf,
Q-R-glued-empty,
equal_wf,
Q-R-glued_wf,
isect_wf,
all_wf,
pairwise_wf,
subtype_rel_self,
subtype_rel_sets,
assert_elim,
bool_subtype_base,
bool_wf,
subtype_base_sq,
is-cond-class,
pairwise-cons,
select_cons_tl_sq,
Q-R-glued-conditional,
cond-class_wf,
subtype_rel_function,
is-first-class,
and_functionality_wrt_iff,
l_member_wf,
l_exists_wf,
es-interface-conditional-domain-iff,
decidable__assert,
assert_witness,
Q-R-glues_wf,
es-interface-predicate_wf,
rel-restriction_wf,
rel_or_wf,
Q-R-glues_functionality,
select_member
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[Q,R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]. \mforall{}[A,B:Type].
\mforall{}Ias:EClass(A) List. \mforall{}Ibs:EClass(B) List. \mforall{}f:E(first-class(Ias)) {}\mrightarrow{} B.
((\mforall{}i:\mBbbN{}||Ias||. Ias[i]:Q \mrightarrow{}{}f{}\mrightarrow{} Ibs[i]:R)
{}\mRightarrow{} first-class(Ias):Q \mrightarrow{}{}f{}\mrightarrow{} first-class(Ibs):R
supposing (\mforall{}Ia1,Ia2\mmember{}Ias. \mforall{}e,e':E.
((\mneg{}(Q e e')) \mwedge{} (\mneg{}(Q e' e))) supposing
((\muparrow{}e' \mmember{}\msubb{} Ia2) and
(\muparrow{}e \mmember{}\msubb{} Ia1)))) supposing
((||Ias|| = ||Ibs||) and
(\mforall{}Ib1,Ib2\mmember{}Ibs. Ib1 \mcap{} Ib2 = 0) and
(\mforall{}Ia1,Ia2\mmember{}Ias. Ia1 \mcap{} Ia2 = 0))
Date html generated:
2012_01_23-PM-12_29_26
Last ObjectModification:
2011_12_13-PM-02_41_37
Home
Index