Def A == A  False

is mentioned by

Thm* m,n:. m+n+1m	[not_suc_add_less_eq]
Thm* m,n:. nm  m+1n	[not_greater_eq]
Thm* m,n:. n<m  mn	[not_greater]
Thm* m,n:. m = n  m+1n  n+1m	[not_num_eq]
Thm* m,n:. mn  n+1m	[not_leq]
Thm* n:. n+10	[not_suc_less_eq_0]
Thm* m,n:. odd(m+n)  (odd(m)  odd(n))	[odd_add]
Thm* n:. (even(n) & odd(n))	[even_and_odd]
Thm* n:. odd(n)  even(n)	[odd_even]
Thm* n:. even(n)  odd(n)	[even_odd]
Thm* m,n:. mn  n<m	[not_less_equal]
Thm* m,n:. exp(n+1;m) = 0	[not_exp_0]

In prior sections: core bool 1 hol hol bool hol num hol prim rec int 2 hol arithmetic 3 hol arithmetic 4

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