Nuprl - Some Definitions

	Some definitions of interest.

adjl-graph	`Def adjl-graph(G) == < vertices = G.size, edges = x:G.size\|\|G.out(x)\|\|, incidence = e. < 1of(e),(G.out(1of(e)))[2of(e)] > >`

adjlist	`Def AdjList == size:size(size List)`

	`Thm* AdjList Type`

assert	`Def b == if b True else False fi`

	`Thm* b:. b Prop`

eq_adjl	`Def x =A= y == x=y`

	`Thm* A:AdjList, x,y:Vertices(adjl-graph(A)). x =A= y`

gr_v	`Def Vertices(t) == 1of(t)`

	`Thm* t:Graph. Vertices(t) Type`

iff	`Def P Q == (P Q) & (P Q)`

	`Thm* A,B:Prop. (A B) Prop`

About: