Nuprl - Definition Cascade for atomic

WhoCites Definitions MarkB generic Sections NuprlLIB Doc

	Who Cites atomic?

atomic	`Def atomic(a) == a = 0 & (a ~ 1) & reducible(a)`

	`Thm* a:. atomic(a) Prop`

reducible	`Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc`

	`Thm* a:. reducible(a) Prop`

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

	`Thm* Type`

nequal	`Def a b T == a = b T`

	`Thm* A:Type, x,y:A. (x y) Prop`

not	`Def A == A False`

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

assoced	`Def a ~ b == (a \| b) & (b \| a)`

	`Thm* a,b:. (a ~ b) Prop`

divides	`Def b \| a == c:. a = bc`

	`Thm* a,b:. (a \| b) Prop`

About:

WhoCites Definitions MarkB generic Sections NuprlLIB Doc