Nuprl Lemma : id-graph-edge

{

[S:Id List].

[G:Graph(S)].

[i:{i:Id| (i

S)} ].

[j:Id]. ((i

j)

G

) }

{ Proof }

Definitions occuring in Statement : id-graph-edge: (i

j)

G, id-graph: Graph(S), Id: Id, uall:

[x:A]. B[x], prop:

, member: t

T, set: {x:A| B[x]} , list: type List, l_member: (x

l)
Definitions : uall:

[x:A]. B[x], id-graph: Graph(S), member: t

T, id-graph-edge: (i

j)

G, all:

x:A. B[x], subtype: S

T, prop:

Lemmas : l_member_wf, Id_wf, id-graph_wf

\mforall{}[S:Id List]. \mforall{}[G:Graph(S)]. \mforall{}[i:\{i:Id| (i \mmember{} S)\} ]. \mforall{}[j:Id]. ((i{}\mrightarrow{}j)\mmember{}G \mmember{} \mBbbP{}) Date html generated: 2011_08_10-AM-07_50_25 Last ObjectModification: 2011_06_18-AM-08_13_39 Home Index