:: deftheorem Def1 defines idiv1_prg PRGCOR_1:def 1 :
for n, m being Integer st n >= 0 & m > 0 holds
for b₃ being Integer holds
( b₃ = idiv1_prg (n,m) iff ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b₃ = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b₃ = pn . 1 ) ) ) ) );