{ 
[i:Id]. [k:Knd]. uiff(
has-src(i;k);(isrcv(k)) c
(source(lnk(k)) = i)) }
{ Proof }
Definitions occuring in Statement :
has-src: has-src(i;k),
lsrc: source(l),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
cand: A c B,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
cand: A c B,
member: t 
T,
and: P Q,
uimplies: b supposing a,
prop: 
,
so_lambda: 
x.t[x],
assert: b,
isrcv: isrcv(k),
isl: isl(x),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
lnk: lnk(k),
outl: outl(x),
top: Top,
all: x:A. B[x],
subtype: S 
T,
has-src: has-src(i;k),
band: p 
q,
so_apply: x[s],
implies: P 
Q,
Knd: Knd,
bfalse: ff,
false: False,
iff: P 
Q,
rev_implies: P Q
Lemmas :
pair_wf,
assert_wf,
isrcv_wf,
Id_wf,
assert_witness,
has-src_wf,
lsrc_wf,
lnk_wf,
Knd_wf,
iff_weakening_uiff,
eq_id_wf,
pi1_wf_top,
IdLnk_wf,
assert-eq-id
\mforall{}[i:Id]. \mforall{}[k:Knd]. uiff(\muparrow{}has-src(i;k);(\muparrow{}isrcv(k)) c\mwedge{} (source(lnk(k)) = i))
Date html generated:
2011_08_10-AM-07_51_26
Last ObjectModification:
2011_06_18-AM-08_14_03
Home
Index