{ 
[S:Id List]. [G:Graph(S)]. [a:Id 
Id Id]. [b:Id].
[j:{j:Id| (j 
S)} ].
(graph-rcvs(S;G;a;b;j) Knd List) }
{ Proof }
Definitions occuring in Statement :
graph-rcvs: graph-rcvs(S;G;a;b;j),
id-graph: Graph(S),
Knd: Knd,
Id: Id,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
list: type List,
l_member: (x l)
Definitions :
uall: [x:A]. B[x],
member: t T,
graph-rcvs: graph-rcvs(S;G;a;b;j),
prop: 
,
so_lambda: 
x.t[x],
id-graph: Graph(S),
uimplies: b supposing a,
so_apply: x[s]
Lemmas :
Id_wf,
l_member_wf,
id-graph_wf,
list-subtype,
mapfilter_wf,
deq-member_wf,
id-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
Knd_wf,
rcv_wf,
mk_lnk_wf,
assert_wf
\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)\} ].
(graph-rcvs(S;G;a;b;j) \mmember{} Knd List)
Date html generated:
2011_08_10-AM-07_50_50
Last ObjectModification:
2011_06_18-AM-08_13_45
Home
Index