corrected static scope: multi-argument composition does not apply partially

less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic

tuned;

added postorder

tuned

int version slicker

tuned

tuned

clarified theory name; tuned;

New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof