  We construct here an iterative evaluation of all PR map codes: progress of
this iteration is measured by descending complexity within "Ordinal" O :=
N[\omega] of polynomials in one indeterminate, ordered lexicographically.
Non-infinit descent of such iterations is added as a mild additional axiom
schema (\pi_O) to Theory PR_A = PR+(abstr) of Primitive Recursion with
predicate abstraction, out of forgoing part RCF 1. This then gives (correct)
"on"-termination of iterative evaluation of argumented deduction trees as well,
for theories PR_A+(\pi_O). By means of this constructive evaluation the Main
Theorem is proved, on Termination-conditioned (Inner) Soundness for such
theories, Ordinal O extending N[\omega]. As a consequence we get
Self-Consistency for these theories, namely derivation of its own free-variable
Consistency formula.
  As to expect from classical setting, Self-Consistency gives (unconditioned)
Objective Soundness. Termination-Conditioned Soundness holds "already" for
PR_A, but it turns out that at least present derivation of Consistency from
this conditioned Soundness depends on schema (\pi_O) of non-infinit descent in
Ordinal O := \N[\omega].
