{ 
S:Id List. G:Graph(S). a:Id 
Id Id. b:Id. j:{j:Id| (j 
S)} . k:Knd\000C
.
((k graph-rcvs(S;G;a;b;j))
i:Id. ((i S) 
(ij)G (k = rcv((link(a i j) from i to j),b)))) }
{ Proof }
Definitions occuring in Statement :
graph-rcvs: graph-rcvs(S;G;a;b;j),
id-graph-edge: (ij)G,
id-graph: Graph(S),
rcv: rcv(l,tg),
Knd: Knd,
mk_lnk: (link(n) from i to j),
Id: Id,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
equal: s = t,
l_member: (x l)
Definitions :
all: x:A. B[x],
id-graph: Graph(S),
l_member: (x l),
Knd: Knd,
iff: P Q,
exists: x:A. B[x],
and: P Q,
member: t T,
prop: 
,
implies: P Q,
l_all: (xL.P[x]),
so_lambda: 
x.t[x],
cand: A c B,
le: A 
B,
not: 
A,
false: False,
subtype: S 
T,
rev_implies: P Q,
graph-rcvs: graph-rcvs(S;G;a;b;j),
id-graph-edge: (ij)G,
so_apply: x[s],
nat: 
Lemmas :
list-set-type2,
l_member_wf,
IdLnk_wf,
Id_wf,
mapfilter_wf,
property-from-l_member,
sq_stable_from_decidable,
decidable__l_member,
decidable__equal_Id,
deq-member_wf,
id-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
assert_wf,
rcv_wf,
mk_lnk_wf,
nat_wf,
length_wf1,
select_wf,
l_member-settype,
l_member-set,
iff_functionality_wrt_iff,
member_map_filter,
assert-deq-member
\mforall{}S:Id List. \mforall{}G:Graph(S). \mforall{}a:Id {}\mrightarrow{} Id {}\mrightarrow{} Id. \mforall{}b:Id. \mforall{}j:\{j:Id| (j \mmember{} S)\} . \mforall{}k:Knd.
((k \mmember{} graph-rcvs(S;G;a;b;j))
\mLeftarrow{}{}\mRightarrow{} \mexists{}i:Id. ((i \mmember{} S) \mwedge{} (i{}\mrightarrow{}j)\mmember{}G \mwedge{} (k = rcv((link(a i j) from i to j),b))))
Date html generated:
2010_08_26-PM-11_41_22
Last ObjectModification:
2009_03_22-PM-01_24_22
Home
Index