Nuprl Lemma : pairs-fpf_property
[A,B:Type].
eq1:EqDecider(A). eq2:EqDecider(B). L:(A 
B) List.
(no_repeats(A;fpf-domain(fpf(L)))
(a:A. ((a 
fpf-domain(fpf(L))) 
b:B. (<a, b> L)))
adom(fpf(L)). l=fpf(L)(a) no_repeats(B;l) (b:B. ((b l) (<a, b> L))))
Proof not projected
Definitions occuring in Statement :
pairs-fpf: fpf(L),
fpf-all: xdom(f). v=f(x) P[x; v],
fpf-domain: fpf-domain(f),
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
pair: <a, b>,
product: x:A B[x],
list: type List,
universe: Type,
no_repeats: no_repeats(T;l),
l_member: (x l),
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
and: P Q,
cand: A c B,
member: t T,
subtype: S 
T,
top: Top,
pi1: fst(t),
pairs-fpf: fpf(L),
fpf-domain: fpf-domain(f),
fpf-all: xdom(f). v=f(x) P[x; v],
implies: P Q,
so_lambda: 
x.t[x],
fpf-ap: f(x),
pi2: snd(t),
guard: {T},
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
eqof: eqof(d),
reduce: reduce(f;k;as),
rev_implies: P Q,
iff: P Q,
or: P 
Q,
so_apply: x[s],
uiff: uiff(P;Q),
unit: Unit,
bool: 
,
uimplies: b supposing a,
deq: EqDecider(T),
ycomb: Y,
select: l[i],
length: ||as||,
nat: 
,
exists: x:A. B[x],
false: False,
l_member: (x l),
prop: 
,
not: 
A,
it: 
Lemmas :
deq_wf,
pi1_wf_top,
map_wf,
remove-repeats_property,
assert_wf,
fpf-dom_wf,
pairs-fpf_wf,
fpf-trivial-subtype-top,
fpf_wf,
top_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
assert-deq,
eqtt_to_assert,
uiff_transitivity,
not_wf,
bnot_wf,
insert_wf,
ifthenelse_wf,
reduce_wf,
pi2_wf,
no_repeats-insert,
equal_wf,
bool_wf,
no_repeats_nil,
and_wf,
member-insert,
cons_member,
or_functionality_wrt_iff,
iff_functionality_wrt_iff,
or_wf,
l_member_wf
\mforall{}[A,B:Type].
\mforall{}eq1:EqDecider(A). \mforall{}eq2:EqDecider(B). \mforall{}L:(A \mtimes{} B) List.
(no\_repeats(A;fpf-domain(fpf(L)))
\mwedge{} (\mforall{}a:A. ((a \mmember{} fpf-domain(fpf(L))) \mLeftarrow{}{}\mRightarrow{} \mexists{}b:B. (<a, b> \mmember{} L)))
\mwedge{} \mforall{}a\mmember{}dom(fpf(L)). l=fpf(L)(a) {}\mRightarrow{} no\_repeats(B;l) \mwedge{} (\mforall{}b:B. ((b \mmember{} l) \mLeftarrow{}{}\mRightarrow{} (<a, b> \mmember{} L))))
Date html generated:
2012_01_23-AM-11_56_10
Last ObjectModification:
2011_12_10-PM-12_56_43
Home
Index