{ 
a:Id 
Id Id. b:Id. S:Id List. G:Graph(S). k:Knd.
(
graph-rcvset(a;b;S;G;k)
i,j:Id
((i 
S)
(j S)
(ij)G
(k = rcv((link(a i j) from i to j),b)))) }
{ Proof }
Definitions occuring in Statement :
graph-rcvset: graph-rcvset(a;b;S;G;k),
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,
assert: b,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
list: type List,
equal: s = t,
l_member: (x l)
Definitions :
member: t T,
id-graph: Graph(S),
le: A 
B,
exists: x:A. B[x],
false: False,
not: 
A,
cand: A c B,
and: P Q,
subtype: S 
T,
prop: 
,
bfalse: ff,
ifthenelse: if b then t else f fi ,
btrue: tt,
band: p 
q,
implies: P Q,
all: x:A. B[x],
graph-rcvset: graph-rcvset(a;b;S;G;k),
l_member: (x l),
guard: {T},
sq_type: SQType(T),
id-graph-edge: (ij)G,
rev_implies: P Q,
nat: 
,
iff: P Q,
unit: Unit,
bool: 
,
it: 
Lemmas :
id-graph-edge-implies-member,
Knd_sq,
and_functionality_wrt_iff,
assert_of_band,
select_wf,
length_wf1,
nat_wf,
assert-deq-member,
bfalse_wf,
not_functionality_wrt_iff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
assert-eq-id,
eqtt_to_assert,
iff_transitivity,
bool_wf,
l_member_wf,
id-deq_wf,
deq-member_wf,
eq_id_wf,
band_wf,
assert_wf
\mforall{}a:Id {}\mrightarrow{} Id {}\mrightarrow{} Id. \mforall{}b:Id. \mforall{}S:Id List. \mforall{}G:Graph(S). \mforall{}k:Knd.
(\muparrow{}graph-rcvset(a;b;S;G;k)
\mLeftarrow{}{}\mRightarrow{} \mexists{}i,j:Id. ((i \mmember{} S) \mwedge{} (j \mmember{} S) \mwedge{} (i{}\mrightarrow{}j)\mmember{}G \mwedge{} (k = rcv((link(a i j) from i to j),b))))
Date html generated:
2011_08_10-AM-07_50_47
Last ObjectModification:
2010_09_24-PM-09_19_38
Home
Index