Mathematical models of N-finite (N  2) (especially for N= 216 typical for IBM-compatible personal computers) real, integer or boolean valued computations are proposed in the frameworks of a finite-discrete mathematics. Such a mathematical model more precisely characterizes the contemporary practice of the computer use. Notions of an N-finite RAM (Random Access Machine), an N-finite RASP (Random Access Machine with Stored Program) and an N-finite Pascal program using integer operations modulo N with the reminders from the segment [–N/2, N/2 – 1 + (N mod 2)] are introduced. A formal N-finite quantifier logic language of modulo N arithmetic operations is defined. It allows to formulate mathematical properties of such a non-recursive total Pascal function or predicate. It is proved that the problem of a formula identical truth in such a language containing arithmetic operations modulo N is a P-SPACE-complete one. So, the proof of a correctness of a non-recursive total Pascal program may be simplified with t