Def  A == A  False

is mentioned by

Thm*  a,b:, f:({a..b}), x:. Thm*  a  x < b  complete_intseg_mset(a; b; f)(x) = 0	[complete_intseg_mset_ismin]
Thm*  k:{2...}, g:({2..k}), z:{2..k}. Thm*  prime(z) Thm*   Thm*  (g':({2..k}).  Thm*  ({2..k}(g) = {2..k}(g') Thm*  (& g'(z) = 0 Thm*  (& (u:{2..k}. z<u  g'(u) = g(u)))	[can_reduce_composite_factor2]
Thm*  a:{2...}, b:, f:({a..b}). Thm*  {a..b}(f) = 1  (i:{a..b}. f(i) = 0)	[eval_factorization_not_one]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i))	[eval_factorization_one_b]
Thm*  f:(Prime), x:. prime(x)  prime_mset_complete(f)(x) = 0	[prime_mset_complete_ismin]

In prior sections: core bool 1 rel 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html