Entry	Value
Package Name	natural-numeral-def
Count	3
Theorems	BIT0_SUC : !n. BIT0 (SUC n) = SUC (SUC (BIT0 n)) BIT0_ZERO : BIT0 0 = 0 BIT1_DEF : !n. BIT1 n = SUC (BIT0 n)

Back to main package page