Nuprl - Some Definitions

	Some definitions of interest.

accumulate	`Def process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } == if P(j;u) F(j;u) else G(j;list_accum(s',i'.process s' i' where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } ;H(j;u);N(j;u))) fi (recursive)`

	`Thm* A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } {s:A\| M(s)M(u) })`

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

	`Thm* b:. b Prop`

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

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

nat	`Def == {i:\| 0i }`

	`Thm* Type`

le	`Def AB == B < A`

	`Thm* i,j:. (ij) Prop`

not	`Def A == A False`

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

About: