Nuprl - Some Definitions

	Some definitions of interest.

adjm-graph	`Def adjm-graph(A) == < vertices = A.size, edges = {p:(A.sizeA.size)\| (A.adj(1of(p),2of(p))) }, incidence = e.e >`

adjmatrix	`Def AdjMatrix == size:sizesize`

	`Thm* AdjMatrix Type`

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

	`Thm* b:. b Prop`

eq_adjm	`Def x =M= y == x=y`

	`Thm* M:AdjMatrix, x,y:Vertices(adjm-graph(M)). x =M= 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: