PART A  (Section 4: metamonovalued reloids; all relations F from A to B, |A|,|B| <= 3)
  relations F checked: 689  (Theorem 1.1 pair, second pair of Remark 4.5, F o F^-1, top o F): no mismatch
  Proposition 4.2, key step: 91042 triples (single valued F, G1, G2) with |A| <= 2, |B| <= 3, |C| <= 2: no mismatch
  Remark 4.5: {(a,y)} o F_k is empty exactly for k > a (window 0..30); no F_k is single valued
PART B  (Section 5: the example of Theorem 1.2 on the window 0..40, c_1..c_40)
  closed form of (F_m)^m, Step 2 ((0,c_n) not in K) and Step 3 ((0,c_j) in F_j o P^j): OK
  Remark 5.3: closed form of S(F_j) and S(F_j) inside (id + F_j) o Q: OK
PART B' (Proposition 5.2(a) and the facts on S(F) used in its proof; all relations on <= 3 points)
  n=0: 1 relations: S(F)oS(F) = S(F) = S(S(F));  S(F & F') inside S(F) & S(F') on 1 pairs: OK
  n=1: 2 relations: S(F)oS(F) = S(F) = S(S(F));  S(F & F') inside S(F) & S(F') on 4 pairs: OK
  n=2: 16 relations: S(F)oS(F) = S(F) = S(S(F));  S(F & F') inside S(F) & S(F') on 256 pairs: OK
  n=3: 512 relations: S(F)oS(F) = S(F) = S(S(F));  S(F & F') inside S(F) & S(F') on 40000 pairs: OK
PART B''(Remark 5.4: the two further examples, exact rational arithmetic)
  (a) n-fold composition of F_eps: 20000 random exact cases OK;  (b) band argument for the shifted uniformity: OK
PART C  (Section 6: the sets F_j[X] used in the proof of Theorem 1.3, window 0..40)
  F_{k+1}[{k}] = {k+1};  c_j in F_j[N];  F_max(j,j')[X & X'] inside F_j[X] & F_j'[X']: OK
ALL CHECKS PASSED
(elapsed: 1.3 s)
