WhoCites
Definitions
Graphs
Sections
NuprlLIB
Doc
Who Cites eq
adjl?
eq_adjl
Def x =A= y == x=
y
Thm*
A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y
eq_int
Def
i=
j == if i=j
true
; false
fi
Thm*
i,j:
. (i=
j)
Syntax:
x =A= y
has structure:
eq_adjl(A; x; y)
About:
WhoCites
Definitions
Graphs
Sections
NuprlLIB
Doc