WhoCites Definitions FTA Sections DiscrMathExt Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites prime factorization of?
prime_factorization_ofDef  f is a factorization of k
Def  == (x:Primek<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))
Thm*  f:(Prime), k:f is a factorization of k  Prop
prime_mset_completeDef  prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi
Thm*  f:(Prime). prime_mset_complete(f 
eval_factorizationDef  {a..b}(f) ==  i:{a..b}. if(i)
Thm*  a,b:f:({a..b}). {a..b}(f 
prime_natsDef  Prime == {x:| prime(x) }
prime_deciderDef  is_prime(x) == prime_decider_exists{1:l}(x)
Thm*  x:. is_prime(x 
iter_via_intsegDef  Iter(f;ui:{a..b}. e(i)
Def  == if a<b f((Iter(f;ui:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)
Thm*  f:(AAA), u:Aa,b:e:({a..b}A). (Iter(f;ui:{a..b}. e(i))  A
primeDef  prime(a) == a = 0 & (a ~ 1) & (b,c:a | bc  a | b  a | c)
Thm*  a:. prime(a Prop
natDef   == {i:| 0i }
Thm*    Type
lt_intDef  i<j == if i<j true ; false fi
Thm*  i,j:. (i<j 
assocedDef  a ~ b == a | b & b | a
Thm*  a,b:. (a ~ b Prop
dividesDef  b | a == c:a = bc
Thm*  a,b:. (a | b Prop
leDef  AB == B<A
Thm*  i,j:. (ij Prop
notDef  A == A  False
Thm*  A:Prop. (A Prop

Syntax:f is a factorization of k has structure: prime_factorization_of(fk)

About:
boolbfalsebtrueifthenelseintnatural_numberaddsubtractmultiplyless
less_thansetlambdaapplyfunctionrecursive_def_noticeuniverseequal
memberpropimpliesandorfalseallexists!abstraction
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions FTA Sections DiscrMathExt Search Doc