:: PRGCOR_1 semantic presentation begin theorem Th1: :: PRGCOR_1:1 for n, m, k being Element of NAT holds (n + k) -' (m + k) = n -' m proof let n, m, k be Element of NAT ; ::_thesis: (n + k) -' (m + k) = n -' m A1: (n + k) - (m + k) = n - m ; percases ( n - m >= 0 or n - m < 0 ) ; suppose n - m >= 0 ; ::_thesis: (n + k) -' (m + k) = n -' m then n -' m = n - m by XREAL_0:def_2; hence (n + k) -' (m + k) = n -' m by A1, XREAL_0:def_2; ::_thesis: verum end; supposeA2: n - m < 0 ; ::_thesis: (n + k) -' (m + k) = n -' m then n -' m = 0 by XREAL_0:def_2; hence (n + k) -' (m + k) = n -' m by A1, A2, XREAL_0:def_2; ::_thesis: verum end; end; end; theorem Th2: :: PRGCOR_1:2 for n, k being Element of NAT st k > 0 & n mod (2 * k) >= k holds ( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) ) proof let n, k be Element of NAT ; ::_thesis: ( k > 0 & n mod (2 * k) >= k implies ( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) ) ) assume that A1: k > 0 and A2: n mod (2 * k) >= k ; ::_thesis: ( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) ) ( ex t being Nat st ( n = ((2 * k) * t) + (n mod (2 * k)) & n mod (2 * k) < 2 * k ) or ( n mod (2 * k) = 0 & 2 * k = 0 ) ) by NAT_D:def_2; then consider t being Nat such that A3: n = ((2 * k) * t) + (n mod (2 * k)) by A1; 2 * k > 2 * 0 by A1, XREAL_1:68; then n mod (2 * k) < 2 * k by NAT_D:1; then A4: (n mod (2 * k)) - k < (2 * k) - k by XREAL_1:9; reconsider t = t as Element of NAT by ORDINAL1:def_12; (n mod (2 * k)) - k >= 0 by A2, XREAL_1:48; then A5: (n mod (2 * k)) -' k = (n mod (2 * k)) - k by XREAL_0:def_2; then n = (k * ((2 * t) + 1)) + ((n mod (2 * k)) -' k) by A3; hence (n mod (2 * k)) - k = n mod k by A5, A4, NAT_D:def_2; ::_thesis: (n mod k) + k = n mod (2 * k) hence (n mod k) + k = n mod (2 * k) ; ::_thesis: verum end; theorem Th3: :: PRGCOR_1:3 for n, k being Element of NAT st k > 0 & n mod (2 * k) >= k holds n div k = ((n div (2 * k)) * 2) + 1 proof let n, k be Element of NAT ; ::_thesis: ( k > 0 & n mod (2 * k) >= k implies n div k = ((n div (2 * k)) * 2) + 1 ) assume that A1: k > 0 and A2: n mod (2 * k) >= k ; ::_thesis: n div k = ((n div (2 * k)) * 2) + 1 2 * k > 2 * 0 by A1, XREAL_1:68; then A3: n = ((2 * k) * (n div (2 * k))) + (n mod (2 * k)) by NAT_D:2 .= ((2 * k) * (n div (2 * k))) + ((n mod k) + k) by A1, A2, Th2 .= (k * ((2 * (n div (2 * k))) + 1)) + (n mod k) ; n mod k < k by A1, NAT_D:1; hence n div k = ((n div (2 * k)) * 2) + 1 by A3, NAT_D:def_1; ::_thesis: verum end; theorem Th4: :: PRGCOR_1:4 for n, k being Element of NAT st k > 0 & n mod (2 * k) < k holds n mod (2 * k) = n mod k proof let n, k be Element of NAT ; ::_thesis: ( k > 0 & n mod (2 * k) < k implies n mod (2 * k) = n mod k ) assume that A1: k > 0 and A2: n mod (2 * k) < k ; ::_thesis: n mod (2 * k) = n mod k ( ex t being Nat st ( n = ((2 * k) * t) + (n mod (2 * k)) & n mod (2 * k) < 2 * k ) or ( n mod (2 * k) = 0 & 2 * k = 0 ) ) by NAT_D:def_2; then consider t being Nat such that A3: n = ((2 * k) * t) + (n mod (2 * k)) by A1; reconsider t = t as Element of NAT by ORDINAL1:def_12; n = (k * (2 * t)) + (n mod (2 * k)) by A3; hence n mod (2 * k) = n mod k by A2, NAT_D:def_2; ::_thesis: verum end; theorem Th5: :: PRGCOR_1:5 for n, k being Element of NAT st k > 0 & n mod (2 * k) < k holds n div k = (n div (2 * k)) * 2 proof let n, k be Element of NAT ; ::_thesis: ( k > 0 & n mod (2 * k) < k implies n div k = (n div (2 * k)) * 2 ) assume that A1: k > 0 and A2: n mod (2 * k) < k ; ::_thesis: n div k = (n div (2 * k)) * 2 2 * k > 2 * 0 by A1, XREAL_1:68; then A3: n = ((2 * k) * (n div (2 * k))) + (n mod (2 * k)) by NAT_D:2 .= (k * (2 * (n div (2 * k)))) + (n mod k) by A2, Th4 ; n mod k < k by A1, NAT_D:1; hence n div k = (n div (2 * k)) * 2 by A3, NAT_D:def_1; ::_thesis: verum end; theorem Th6: :: PRGCOR_1:6 for m, n being Element of NAT st m > 0 holds ex i being Element of NAT st ( ( for k2 being Element of NAT st k2 < i holds m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) proof let m, n be Element of NAT ; ::_thesis: ( m > 0 implies ex i being Element of NAT st ( ( for k2 being Element of NAT st k2 < i holds m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) ) defpred S1[ Nat] means m * (2 |^ $1) > n; (n + 1) - 1 = n ; then A1: (n + 1) -' 1 = n by XREAL_0:def_2; assume A2: m > 0 ; ::_thesis: ex i being Element of NAT st ( ( for k2 being Element of NAT st k2 < i holds m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) then m >= 0 + 1 by NAT_1:13; then A3: m * n >= 1 * n by XREAL_1:64; m * (2 |^ ((n + 1) -' 1)) > m * ((n + 1) -' 1) by A2, NEWTON:86, XREAL_1:68; then m * (2 |^ ((n + 1) -' 1)) > n by A1, A3, XXREAL_0:2; then A4: ex k being Nat st S1[k] ; ex k being Nat st ( S1[k] & ( for j being Nat st S1[j] holds k <= j ) ) from NAT_1:sch_5(A4); then consider k being Nat such that A5: S1[k] and A6: for j being Nat st S1[j] holds k <= j ; ( k in NAT & ( for k2 being Element of NAT st k2 < k holds m * (2 |^ k2) <= n ) ) by A6, ORDINAL1:def_12; hence ex i being Element of NAT st ( ( for k2 being Element of NAT st k2 < i holds m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) by A5; ::_thesis: verum end; theorem Th7: :: PRGCOR_1:7 for i being Integer for f being FinSequence st 1 <= i & i <= len f holds i in dom f proof let i be Integer; ::_thesis: for f being FinSequence st 1 <= i & i <= len f holds i in dom f let f be FinSequence; ::_thesis: ( 1 <= i & i <= len f implies i in dom f ) assume that A1: 1 <= i and A2: i <= len f ; ::_thesis: i in dom f i is Element of NAT by A1, INT_1:3; hence i in dom f by A1, A2, FINSEQ_3:25; ::_thesis: verum end; definition let n, m be Integer; assume that A1: n >= 0 and A2: m > 0 ; func idiv1_prg (n,m) -> Integer means :Def1: :: PRGCOR_1:def 1 ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies it = 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 ) ) ) ) & it = pn . 1 ) ) ) ); existence ex b1 being Integer ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) proof reconsider n2 = n, m2 = m as Element of NAT by A1, A2, INT_1:3; percases ( n < m or n >= m ) ; supposeA3: n < m ; ::_thesis: ex b1 being Integer ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) set ssm = (Seg (n2 + 1)) --> 1; A4: dom ((Seg (n2 + 1)) --> 1) = Seg (n2 + 1) by FUNCOP_1:13; then reconsider ssm = (Seg (n2 + 1)) --> 1 as FinSequence by FINSEQ_1:def_2; A5: rng ssm c= {1} by FUNCOP_1:13; rng ssm c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssm or y in INT ) assume y in rng ssm ; ::_thesis: y in INT then y = 1 by A5, TARSKI:def_1; hence y in INT by INT_1:def_2; ::_thesis: verum end; then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def_4; len ssm = n + 1 by A4, FINSEQ_1:def_3; hence ex b1 being Integer ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) by A3; ::_thesis: verum end; supposeA6: n >= m ; ::_thesis: ex b1 being Integer ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) deffunc H1( Nat) -> Element of NAT = n2 div (m2 * (2 |^ ($1 -' 1))); A7: m2 * (2 |^ 0) = m2 * 1 by NEWTON:4 .= m2 ; ex ppn being FinSequence st ( len ppn = n2 + 1 & ( for k2 being Nat st k2 in dom ppn holds ppn . k2 = H1(k2) ) ) from FINSEQ_1:sch_2(); then consider ppn being FinSequence such that A8: len ppn = n + 1 and A9: for k2 being Nat st k2 in dom ppn holds ppn . k2 = n2 div (m2 * (2 |^ (k2 -' 1))) ; A10: dom ppn = Seg (n2 + 1) by A8, FINSEQ_1:def_3; rng ppn c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ppn or y in INT ) assume y in rng ppn ; ::_thesis: y in INT then consider x being set such that A11: x in dom ppn and A12: y = ppn . x by FUNCT_1:def_3; reconsider n3 = x as Element of NAT by A11; ppn . n3 = n2 div (m2 * (2 |^ (n3 -' 1))) by A9, A11; hence y in INT by A12, INT_1:def_2; ::_thesis: verum end; then reconsider ppn = ppn as FinSequence of INT by FINSEQ_1:def_4; n2 >= 0 + 1 by A2, A6, NAT_1:13; then 1 < n2 + 1 by NAT_1:13; then A13: 1 in Seg (n2 + 1) by FINSEQ_1:1; then A14: ppn . 1 = n2 div (m2 * (2 |^ (1 -' 1))) by A9, A10 .= n2 div m2 by A7, XREAL_1:232 ; deffunc H2( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1))); deffunc H3( Nat) -> Element of NAT = m2 * (2 |^ ($1 -' 1)); ex ssm being FinSequence st ( len ssm = n2 + 1 & ( for k2 being Nat st k2 in dom ssm holds ssm . k2 = H3(k2) ) ) from FINSEQ_1:sch_2(); then consider ssm being FinSequence such that A15: len ssm = n2 + 1 and A16: for k2 being Nat st k2 in dom ssm holds ssm . k2 = m * (2 |^ (k2 -' 1)) ; A17: dom ssm = Seg (n2 + 1) by A15, FINSEQ_1:def_3; A18: rng ssm c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssm or y in INT ) assume y in rng ssm ; ::_thesis: y in INT then consider x being set such that A19: x in dom ssm and A20: y = ssm . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A19; ssm . n = m * (2 |^ (n -' 1)) by A16, A19; hence y in INT by A20, INT_1:def_2; ::_thesis: verum end; ex ssn being FinSequence st ( len ssn = n2 + 1 & ( for k2 being Nat st k2 in dom ssn holds ssn . k2 = H2(k2) ) ) from FINSEQ_1:sch_2(); then consider ssn being FinSequence such that A21: len ssn = n2 + 1 and A22: for k2 being Nat st k2 in dom ssn holds ssn . k2 = n2 mod (m2 * (2 |^ (k2 -' 1))) ; A23: dom ssn = Seg (n2 + 1) by A21, FINSEQ_1:def_3; rng ssn c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssn or y in INT ) assume y in rng ssn ; ::_thesis: y in INT then consider x being set such that A24: x in dom ssn and A25: y = ssn . x by FUNCT_1:def_3; reconsider n3 = x as Element of NAT by A24; ssn . n3 = n2 mod (m2 * (2 |^ (n3 -' 1))) by A22, A24; hence y in INT by A25, INT_1:def_2; ::_thesis: verum end; then reconsider ssn = ssn as FinSequence of INT by FINSEQ_1:def_4; consider ii0 being Element of NAT such that A26: for k2 being Element of NAT st k2 < ii0 holds m * (2 |^ k2) <= n2 and A27: m2 * (2 |^ ii0) > n2 by A2, Th6; reconsider i0 = ii0 as Integer ; A28: 0 + 1 <= i0 + 1 by XREAL_1:7; now__::_thesis:_not_i0_=_0 assume i0 = 0 ; ::_thesis: contradiction then m2 * 1 > n2 by A27, NEWTON:4; hence contradiction by A6; ::_thesis: verum end; then A29: ii0 >= 0 + 1 by NAT_1:13; then A30: i0 - 1 >= 0 by XREAL_1:48; A31: now__::_thesis:_not_i0_>_n2 1 + 0 <= m2 by A2, NAT_1:13; then A32: 1 * (2 |^ n2) <= m2 * (2 |^ n2) by XREAL_1:64; A33: n2 + 1 <= 2 |^ n2 by NEWTON:85; assume i0 > n2 ; ::_thesis: contradiction then m * (2 |^ n2) <= n2 by A26; then 2 |^ n2 <= n2 by A32, XXREAL_0:2; hence contradiction by A33, NAT_1:13; ::_thesis: verum end; then ( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 ) by NAT_1:11, XREAL_1:7; then A34: ii0 + 1 in Seg (n2 + 1) by FINSEQ_1:1; reconsider k5 = m2 * (2 |^ ((ii0 + 1) -' 1)) as Element of NAT ; A35: k5 > n2 by A27, NAT_D:34; i0 < n2 + 1 by A31, NAT_1:13; then ii0 + 1 <= n2 + 1 by NAT_1:13; then ii0 + 1 in Seg (n2 + 1) by A28, FINSEQ_1:1; then ssn . (i0 + 1) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' 1))) by A22, A23; then A36: ssn . (i0 + 1) = n by A35, NAT_D:24; (ii0 + 1) -' 1 = (i0 - 1) + 1 by NAT_D:34 .= (ii0 -' 1) + 1 by A30, XREAL_0:def_2 ; then A37: 2 |^ ((ii0 + 1) -' 1) = (2 |^ (ii0 -' 1)) * 2 by NEWTON:6; A38: 1 <= i0 + 1 by A29, NAT_1:13; reconsider ssm = ssm as FinSequence of INT by A18, FINSEQ_1:def_4; A39: ssm . 1 = m * (2 |^ (1 -' 1)) by A13, A16, A17 .= m * (2 |^ 0) by XREAL_1:232 .= m * 1 by NEWTON:4 .= m ; A40: (ii0 + 1) -' 1 = ii0 by NAT_D:34; then n2 div (m2 * (2 |^ ((ii0 + 1) -' 1))) = 0 by A27, NAT_D:27; then A41: ppn . (i0 + 1) = 0 by A9, A10, A34; A42: for j being Integer st 1 <= j & j <= i0 holds ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) proof let j be Integer; ::_thesis: ( 1 <= j & j <= i0 implies ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) ) assume that A43: 1 <= j and A44: j <= i0 ; ::_thesis: ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) reconsider jj = j as Element of NAT by A43, INT_1:3; A45: j - 1 >= 0 by A43, XREAL_1:48; A46: i0 - j >= 0 by A44, XREAL_1:48; then A47: ii0 -' jj = i0 - j by XREAL_0:def_2; thus ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) ::_thesis: ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) proof ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A44, XXREAL_0:2; then (i0 + 1) - j >= 0 by XREAL_1:48; then A48: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; i0 + 1 <= n2 + j by A31, A43, XREAL_1:7; then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9; then A49: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A48, XREAL_1:7; assume A50: ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; ::_thesis: ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ( j + 1 <= i0 + 1 & j < j + 1 ) by A44, XREAL_1:7, XREAL_1:29; then A51: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= j by NAT_D:35; then jj -' 1 < i0 + 1 by A51, XXREAL_0:2; then A52: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7; then A53: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= jj by NAT_D:35; then jj -' 1 < i0 + 1 by A53, XXREAL_0:2; then A54: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; 2 |^ (ii0 -' jj) <> 0 by CARD_4:3; then A55: m2 * (2 |^ (ii0 -' jj)) > m2 * 0 by A2, XREAL_1:68; ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A44, XXREAL_0:2; then A56: (i0 + 1) - j > 0 by XREAL_1:50; then A57: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; then A58: (ii0 + 1) -' jj >= 0 + 1 by A56, NAT_1:13; then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48; then A59: ((ii0 + 1) -' jj) -' 1 = i0 - j by A57, XREAL_0:def_2; ( (ii0 + 1) -' jj <= i0 + 1 & i0 + 1 <= n2 + 1 ) by A31, NAT_D:35, XREAL_1:7; then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2; then A60: (ii0 + 1) -' jj in Seg (n2 + 1) by A58, FINSEQ_1:1; then A61: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A22, A23; (ii0 + 1) -' jj = (i0 - j) + 1 by A56, XREAL_0:def_2; then ((ii0 + 1) -' jj) - 1 >= 0 by A44, XREAL_1:48; then A62: ((ii0 + 1) -' jj) -' 1 = i0 - j by A57, XREAL_0:def_2 .= ii0 -' jj by A46, XREAL_0:def_2 ; then A63: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A16, A17, A60; A64: jj -' 1 = j - 1 by A45, XREAL_0:def_2; then A65: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A52, XREAL_0:def_2; then A66: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A57, NAT_D:34; 1 <= (ii0 + 1) -' (jj -' 1) by A57, A65, NAT_1:11; then A67: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A57, A65, A49, FINSEQ_1:1; then A68: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1))) by A22, A23; jj -' 1 = j - 1 by A45, XREAL_0:def_2; then (ii0 + 1) -' (jj -' 1) = ((ii0 + 1) -' jj) + 1 by A57, A54, XREAL_0:def_2; then A69: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by A68, NAT_D:34; A70: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A64, A52, XREAL_0:def_2; A71: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A47, A56, XREAL_0:def_2 .= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6 .= 2 * (m2 * (2 |^ (ii0 -' jj))) ; (ii0 + 1) -' jj = (i0 + 1) - j by A56, XREAL_0:def_2; then A72: (ssn . ((ii0 + 1) -' (jj -' 1))) - (ssm . ((ii0 + 1) -' jj)) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A50, A65, A69, A71, A63, A55, Th2; ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A9, A10, A60 .= ((n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2) + 1 by A50, A57, A66, A70, A68, A62, A71, A63, A55, Th3 .= ((ppn . ((ii0 + 1) -' (jj -' 1))) * 2) + 1 by A9, A10, A67 ; hence ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) by A57, A65, A59, A61, A72, XREAL_0:def_2; ::_thesis: verum end; thus ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ::_thesis: verum proof ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7; then A73: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= j by NAT_D:35; then jj -' 1 < i0 + 1 by A73, XXREAL_0:2; then A74: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7; then A75: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= jj by NAT_D:35; then jj -' 1 < i0 + 1 by A75, XXREAL_0:2; then A76: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A44, XXREAL_0:2; then (i0 + 1) - j >= 0 by XREAL_1:48; then A77: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; i0 + 1 <= n2 + j by A31, A43, XREAL_1:7; then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9; then A78: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A77, XREAL_1:7; assume A79: not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; ::_thesis: ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A44, XXREAL_0:2; then A80: (i0 + 1) - j > 0 by XREAL_1:50; then A81: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; then A82: (ii0 + 1) -' jj >= 0 + 1 by A80, NAT_1:13; then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48; then A83: ((ii0 + 1) -' jj) -' 1 = i0 - j by A81, XREAL_0:def_2; ( (ii0 + 1) -' jj <= ii0 + 1 & i0 + 1 <= n2 + 1 ) by A31, NAT_D:35, XREAL_1:7; then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2; then A84: (ii0 + 1) -' jj in Seg (n2 + 1) by A82, FINSEQ_1:1; then ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A22, A23; then A85: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A83, XREAL_0:def_2; (ii0 + 1) -' jj = (i0 - j) + 1 by A80, XREAL_0:def_2; then ((ii0 + 1) -' jj) - 1 >= 0 by A44, XREAL_1:48; then A86: ((ii0 + 1) -' jj) -' 1 = i0 - j by A81, XREAL_0:def_2 .= ii0 -' jj by A46, XREAL_0:def_2 ; then A87: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A16, A17, A84; A88: jj -' 1 = j - 1 by A45, XREAL_0:def_2; then A89: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A76, XREAL_0:def_2; then A90: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A81, NAT_D:34; 1 <= (ii0 + 1) -' (jj -' 1) by A81, A89, NAT_1:11; then A91: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A81, A89, A78, FINSEQ_1:1; then A92: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1))) by A22, A23; jj -' 1 = j - 1 by A45, XREAL_0:def_2; then (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A74, XREAL_0:def_2 .= ((ii0 + 1) -' jj) + 1 by A80, XREAL_0:def_2 ; then A93: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by A92, NAT_D:34; A94: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A88, A76, XREAL_0:def_2; A95: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A47, A80, XREAL_0:def_2 .= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6 .= 2 * (m2 * (2 |^ (ii0 -' jj))) ; ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A9, A10, A84 .= (n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2 by A79, A81, A90, A92, A94, A86, A95, A87, Th5 .= (ppn . ((ii0 + 1) -' (jj -' 1))) * 2 by A9, A10, A91 ; hence ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) by A79, A81, A89, A85, A93, A95, A87, Th4; ::_thesis: verum end; end; A96: for k being Element of NAT st 1 <= k & k < i0 holds ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) ) assume that A97: 1 <= k and A98: k < i0 ; ::_thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) A99: k <= n2 by A31, A98, XXREAL_0:2; then A100: k + 1 <= n2 + 1 by XREAL_1:7; k <= n2 + 1 by A99, NAT_1:12; then k in Seg (n2 + 1) by A97, FINSEQ_1:1; then A101: ssm . k = m * (2 |^ (k -' 1)) by A16, A17; 1 < k + 1 by A97, NAT_1:13; then k + 1 in Seg (n2 + 1) by A100, FINSEQ_1:1; then A102: ( (k + 1) -' 1 = k & ssm . (k + 1) = m * (2 |^ ((k + 1) -' 1)) ) by A16, A17, NAT_D:34; A103: k - 1 >= 0 by A97, XREAL_1:48; (k + 1) -' 1 = (k - 1) + 1 by NAT_D:34 .= (k -' 1) + 1 by A103, XREAL_0:def_2 ; then 2 |^ ((k + 1) -' 1) = (2 |^ (k -' 1)) * 2 by NEWTON:6; hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A26, A98, A102, A101; ::_thesis: verum end; A104: for k being Integer st 1 <= k & k < i0 holds ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) proof let k be Integer; ::_thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) ) assume that A105: 1 <= k and A106: k < i0 ; ::_thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) reconsider kk = k as Element of NAT by A105, INT_1:3; ssm . (kk + 1) = (ssm . kk) * 2 by A96, A105, A106; hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A96, A105, A106; ::_thesis: verum end; i0 < n2 + 1 by A31, NAT_1:13; then A107: ii0 in Seg (n2 + 1) by A29, FINSEQ_1:1; i0 + 1 <= n2 + 1 by A31, XREAL_1:7; then ii0 + 1 in Seg (n2 + 1) by A38, FINSEQ_1:1; then ssm . (i0 + 1) = m * (2 |^ ((ii0 + 1) -' 1)) by A16, A17; then A108: ssm . (i0 + 1) = (m * (2 |^ (ii0 -' 1))) * 2 by A37 .= (ssm . i0) * 2 by A16, A17, A107 ; ssm . (i0 + 1) > n by A16, A17, A27, A40, A34; hence ex b1 being Integer ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) by A6, A15, A21, A8, A14, A39, A29, A31, A108, A104, A41, A36, A42; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Integer st ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 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 ) ) ) ) & b1 = pn . 1 ) ) ) ) & ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b2 = 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 ) ) ) ) & b2 = pn . 1 ) ) ) ) holds b1 = b2 proof let t1, t2 be Integer; ::_thesis: ( ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t1 = 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 ) ) ) ) & t1 = pn . 1 ) ) ) ) & ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t2 = 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 ) ) ) ) & t2 = pn . 1 ) ) ) ) implies t1 = t2 ) assume that A109: ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t1 = 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 ) ) ) ) & t1 = pn . 1 ) ) ) ) and A110: ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies t2 = 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 ) ) ) ) & t2 = pn . 1 ) ) ) ) ; ::_thesis: t1 = t2 consider sm1, sn1, pn1 being FinSequence of INT such that len sm1 = n + 1 and len sn1 = n + 1 and len pn1 = n + 1 and A111: ( n < m implies t1 = 0 ) and A112: ( not n < m implies ( sm1 . 1 = m & ex i being Integer st ( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( sm1 . (k + 1) = (sm1 . k) * 2 & not sm1 . (k + 1) > n ) ) & sm1 . (i + 1) = (sm1 . i) * 2 & sm1 . (i + 1) > n & pn1 . (i + 1) = 0 & sn1 . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( ( sn1 . ((i + 1) - (j - 1)) >= sm1 . ((i + 1) - j) implies ( sn1 . ((i + 1) - j) = (sn1 . ((i + 1) - (j - 1))) - (sm1 . ((i + 1) - j)) & pn1 . ((i + 1) - j) = ((pn1 . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn1 . ((i + 1) - (j - 1)) >= sm1 . ((i + 1) - j) implies ( sn1 . ((i + 1) - j) = sn1 . ((i + 1) - (j - 1)) & pn1 . ((i + 1) - j) = (pn1 . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t1 = pn1 . 1 ) ) ) by A109; consider sm2, sn2, pn2 being FinSequence of INT such that len sm2 = n + 1 and len sn2 = n + 1 and len pn2 = n + 1 and A113: ( n < m implies t2 = 0 ) and A114: ( not n < m implies ( sm2 . 1 = m & ex i being Integer st ( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( sm2 . (k + 1) = (sm2 . k) * 2 & not sm2 . (k + 1) > n ) ) & sm2 . (i + 1) = (sm2 . i) * 2 & sm2 . (i + 1) > n & pn2 . (i + 1) = 0 & sn2 . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( ( sn2 . ((i + 1) - (j - 1)) >= sm2 . ((i + 1) - j) implies ( sn2 . ((i + 1) - j) = (sn2 . ((i + 1) - (j - 1))) - (sm2 . ((i + 1) - j)) & pn2 . ((i + 1) - j) = ((pn2 . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn2 . ((i + 1) - (j - 1)) >= sm2 . ((i + 1) - j) implies ( sn2 . ((i + 1) - j) = sn2 . ((i + 1) - (j - 1)) & pn2 . ((i + 1) - j) = (pn2 . ((i + 1) - (j - 1))) * 2 ) ) ) ) & t2 = pn2 . 1 ) ) ) by A110; now__::_thesis:_t1_=_t2 percases ( n < m or n >= m ) ; suppose n < m ; ::_thesis: t1 = t2 hence t1 = t2 by A111, A113; ::_thesis: verum end; supposeA115: n >= m ; ::_thesis: t1 = t2 then consider i1 being Integer such that A116: 1 <= i1 and i1 <= n and A117: for k being Integer st 1 <= k & k < i1 holds ( sm1 . (k + 1) = (sm1 . k) * 2 & not sm1 . (k + 1) > n ) and A118: sm1 . (i1 + 1) = (sm1 . i1) * 2 and A119: sm1 . (i1 + 1) > n and A120: pn1 . (i1 + 1) = 0 and A121: sn1 . (i1 + 1) = n and A122: for j being Integer st 1 <= j & j <= i1 holds ( ( sn1 . ((i1 + 1) - (j - 1)) >= sm1 . ((i1 + 1) - j) implies ( sn1 . ((i1 + 1) - j) = (sn1 . ((i1 + 1) - (j - 1))) - (sm1 . ((i1 + 1) - j)) & pn1 . ((i1 + 1) - j) = ((pn1 . ((i1 + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn1 . ((i1 + 1) - (j - 1)) >= sm1 . ((i1 + 1) - j) implies ( sn1 . ((i1 + 1) - j) = sn1 . ((i1 + 1) - (j - 1)) & pn1 . ((i1 + 1) - j) = (pn1 . ((i1 + 1) - (j - 1))) * 2 ) ) ) and A123: t1 = pn1 . 1 by A112; reconsider ii1 = i1 as Element of NAT by A116, INT_1:3; defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= i1 + 1 implies sm1 . $1 = sm2 . $1 ); defpred S2[ Element of NAT ] means ( 1 <= $1 & $1 <= i1 + 1 implies pn1 . (((ii1 + 1) + 1) -' $1) = pn2 . (((ii1 + 1) + 1) -' $1) ); defpred S3[ Element of NAT ] means ( 1 <= $1 & $1 <= i1 + 1 implies sn1 . (((ii1 + 1) + 1) -' $1) = sn2 . (((ii1 + 1) + 1) -' $1) ); consider i2 being Integer such that A124: 1 <= i2 and i2 <= n and A125: for k being Integer st 1 <= k & k < i2 holds ( sm2 . (k + 1) = (sm2 . k) * 2 & not sm2 . (k + 1) > n ) and A126: sm2 . (i2 + 1) = (sm2 . i2) * 2 and A127: sm2 . (i2 + 1) > n and A128: pn2 . (i2 + 1) = 0 and A129: sn2 . (i2 + 1) = n and A130: for j being Integer st 1 <= j & j <= i2 holds ( ( sn2 . ((i2 + 1) - (j - 1)) >= sm2 . ((i2 + 1) - j) implies ( sn2 . ((i2 + 1) - j) = (sn2 . ((i2 + 1) - (j - 1))) - (sm2 . ((i2 + 1) - j)) & pn2 . ((i2 + 1) - j) = ((pn2 . ((i2 + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn2 . ((i2 + 1) - (j - 1)) >= sm2 . ((i2 + 1) - j) implies ( sn2 . ((i2 + 1) - j) = sn2 . ((i2 + 1) - (j - 1)) & pn2 . ((i2 + 1) - j) = (pn2 . ((i2 + 1) - (j - 1))) * 2 ) ) ) and A131: t2 = pn2 . 1 by A114, A115; reconsider ii2 = i2 as Element of NAT by A124, INT_1:3; A132: now__::_thesis:_not_i2_<_i1 assume A133: i2 < i1 ; ::_thesis: contradiction A134: for k being Integer st 1 <= k & k <= i2 + 1 holds sm2 . k = sm1 . k proof defpred S4[ Element of NAT ] means ( $1 < i2 + 1 implies sm2 . ($1 + 1) = sm1 . ($1 + 1) ); let k be Integer; ::_thesis: ( 1 <= k & k <= i2 + 1 implies sm2 . k = sm1 . k ) assume that A135: 1 <= k and A136: k <= i2 + 1 ; ::_thesis: sm2 . k = sm1 . k reconsider kh = k as Element of NAT by A135, INT_1:3; k - 1 >= 0 by A135, XREAL_1:48; then A137: kh -' 1 = k - 1 by XREAL_0:def_2; then A138: (kh -' 1) + 1 = k ; A139: for e being Element of NAT st S4[e] holds S4[e + 1] proof let e be Element of NAT ; ::_thesis: ( S4[e] implies S4[e + 1] ) assume A140: S4[e] ; ::_thesis: S4[e + 1] percases ( e + 1 < i2 + 1 or e + 1 >= i2 + 1 ) ; suppose e + 1 < i2 + 1 ; ::_thesis: S4[e + 1] then (e + 1) + 1 <= ii2 + 1 by NAT_1:13; then A141: ((e + 1) + 1) - 1 <= (i2 + 1) - 1 by XREAL_1:9; A142: 0 + 1 <= e + 1 by XREAL_1:7; A143: now__::_thesis:_(_(_e_+_1_<_i2_&_sm2_._((e_+_1)_+_1)_=_(sm2_._(e_+_1))_*_2_)_or_(_e_+_1_>=_i2_&_sm2_._((e_+_1)_+_1)_=_(sm2_._(e_+_1))_*_2_)_) percases ( e + 1 < i2 or e + 1 >= i2 ) ; case e + 1 < i2 ; ::_thesis: sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 hence sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 by A125, A142; ::_thesis: verum end; case e + 1 >= i2 ; ::_thesis: sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 then e + 1 = i2 by A141, XXREAL_0:1; hence sm2 . ((e + 1) + 1) = (sm2 . (e + 1)) * 2 by A126; ::_thesis: verum end; end; end; A144: e < e + 1 by NAT_1:13; e + 1 < i1 by A133, A141, XXREAL_0:2; hence S4[e + 1] by A117, A140, A142, A144, A143, XXREAL_0:2; ::_thesis: verum end; suppose e + 1 >= i2 + 1 ; ::_thesis: S4[e + 1] hence S4[e + 1] ; ::_thesis: verum end; end; end; A145: S4[ 0 ] by A112, A114, A115; A146: for e being Element of NAT holds S4[e] from NAT_1:sch_1(A145, A139); A147: ii2 < ii2 + 1 by NAT_1:13; k - 1 <= (i2 + 1) - 1 by A136, XREAL_1:9; then kh -' 1 < i2 + 1 by A137, A147, XXREAL_0:2; hence sm2 . k = sm1 . k by A138, A146; ::_thesis: verum end; 0 <= ii2 ; then 0 + 1 <= i2 + 1 by XREAL_1:7; then sm2 . (i2 + 1) = sm1 . (i2 + 1) by A134; hence contradiction by A117, A124, A127, A133; ::_thesis: verum end; A148: now__::_thesis:_not_i1_<_i2 assume A149: i1 < i2 ; ::_thesis: contradiction A150: for k being Integer st 1 <= k & k <= i1 + 1 holds sm1 . k = sm2 . k proof defpred S4[ Element of NAT ] means ( $1 < i1 + 1 implies sm1 . ($1 + 1) = sm2 . ($1 + 1) ); let k be Integer; ::_thesis: ( 1 <= k & k <= i1 + 1 implies sm1 . k = sm2 . k ) assume that A151: 1 <= k and A152: k <= i1 + 1 ; ::_thesis: sm1 . k = sm2 . k reconsider kh = k as Element of NAT by A151, INT_1:3; k - 1 >= 0 by A151, XREAL_1:48; then A153: kh -' 1 = k - 1 by XREAL_0:def_2; then A154: (kh -' 1) + 1 = k ; A155: for e being Element of NAT st S4[e] holds S4[e + 1] proof let e be Element of NAT ; ::_thesis: ( S4[e] implies S4[e + 1] ) assume A156: S4[e] ; ::_thesis: S4[e + 1] percases ( e + 1 < i1 + 1 or e + 1 >= i1 + 1 ) ; suppose e + 1 < i1 + 1 ; ::_thesis: S4[e + 1] then (e + 1) + 1 <= ii1 + 1 by NAT_1:13; then A157: ((e + 1) + 1) - 1 <= (i1 + 1) - 1 by XREAL_1:9; A158: 0 + 1 <= e + 1 by XREAL_1:7; A159: now__::_thesis:_(_(_e_+_1_<_i1_&_sm1_._((e_+_1)_+_1)_=_(sm1_._(e_+_1))_*_2_)_or_(_e_+_1_>=_i1_&_sm1_._((e_+_1)_+_1)_=_(sm1_._(e_+_1))_*_2_)_) percases ( e + 1 < i1 or e + 1 >= i1 ) ; case e + 1 < i1 ; ::_thesis: sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 hence sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 by A117, A158; ::_thesis: verum end; case e + 1 >= i1 ; ::_thesis: sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 then e + 1 = i1 by A157, XXREAL_0:1; hence sm1 . ((e + 1) + 1) = (sm1 . (e + 1)) * 2 by A118; ::_thesis: verum end; end; end; A160: e < e + 1 by NAT_1:13; e + 1 < i2 by A149, A157, XXREAL_0:2; hence S4[e + 1] by A125, A156, A158, A160, A159, XXREAL_0:2; ::_thesis: verum end; suppose e + 1 >= i1 + 1 ; ::_thesis: S4[e + 1] hence S4[e + 1] ; ::_thesis: verum end; end; end; A161: S4[ 0 ] by A112, A114, A115; A162: for e being Element of NAT holds S4[e] from NAT_1:sch_1(A161, A155); A163: ii1 < ii1 + 1 by NAT_1:13; k - 1 <= (i1 + 1) - 1 by A152, XREAL_1:9; then kh -' 1 < i1 + 1 by A153, A163, XXREAL_0:2; hence sm1 . k = sm2 . k by A154, A162; ::_thesis: verum end; 0 <= ii1 ; then 0 + 1 <= i1 + 1 by XREAL_1:7; then sm1 . (i1 + 1) = sm2 . (i1 + 1) by A150; hence contradiction by A116, A119, A125, A149; ::_thesis: verum end; then A164: i1 = i2 by A132, XXREAL_0:1; A165: ii1 < ii1 + 1 by NAT_1:13; A166: for kk being Element of NAT st S1[kk] holds S1[kk + 1] proof let kk be Element of NAT ; ::_thesis: ( S1[kk] implies S1[kk + 1] ) assume A167: S1[kk] ; ::_thesis: S1[kk + 1] ( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies sm1 . (kk + 1) = sm2 . (kk + 1) ) proof assume that 1 <= kk + 1 and A168: kk + 1 <= i1 + 1 ; ::_thesis: sm1 . (kk + 1) = sm2 . (kk + 1) percases ( kk + 1 < i1 + 1 or kk + 1 = i1 + 1 ) by A168, XXREAL_0:1; supposeA169: kk + 1 < i1 + 1 ; ::_thesis: sm1 . (kk + 1) = sm2 . (kk + 1) then A170: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, XREAL_1:9; now__::_thesis:_(_(_0_<_kk_&_sm1_._(kk_+_1)_=_sm2_._(kk_+_1)_)_or_(_0_>=_kk_&_sm1_._(kk_+_1)_=_sm2_._(kk_+_1)_)_) percases ( 0 < kk or 0 >= kk ) ; case 0 < kk ; ::_thesis: sm1 . (kk + 1) = sm2 . (kk + 1) then A171: 0 + 1 <= kk by NAT_1:13; A172: now__::_thesis:_(_(_kk_<_i2_&_sm2_._(kk_+_1)_=_(sm2_._kk)_*_2_)_or_(_kk_>=_i2_&_sm2_._(kk_+_1)_=_(sm2_._kk)_*_2_)_) percases ( kk < i2 or kk >= i2 ) ; case kk < i2 ; ::_thesis: sm2 . (kk + 1) = (sm2 . kk) * 2 hence sm2 . (kk + 1) = (sm2 . kk) * 2 by A125, A171; ::_thesis: verum end; case kk >= i2 ; ::_thesis: sm2 . (kk + 1) = (sm2 . kk) * 2 then kk = i2 by A170, XXREAL_0:1; hence sm2 . (kk + 1) = (sm2 . kk) * 2 by A126; ::_thesis: verum end; end; end; kk < i1 by A169, XREAL_1:7; hence sm1 . (kk + 1) = sm2 . (kk + 1) by A117, A165, A167, A171, A172, XXREAL_0:2; ::_thesis: verum end; case 0 >= kk ; ::_thesis: sm1 . (kk + 1) = sm2 . (kk + 1) then kk = 0 ; hence sm1 . (kk + 1) = sm2 . (kk + 1) by A112, A114, A115; ::_thesis: verum end; end; end; hence sm1 . (kk + 1) = sm2 . (kk + 1) ; ::_thesis: verum end; suppose kk + 1 = i1 + 1 ; ::_thesis: sm1 . (kk + 1) = sm2 . (kk + 1) hence sm1 . (kk + 1) = sm2 . (kk + 1) by A116, A118, A126, A164, A167, NAT_1:13; ::_thesis: verum end; end; end; hence S1[kk + 1] ; ::_thesis: verum end; A173: S1[ 0 ] ; A174: for jj being Element of NAT holds S1[jj] from NAT_1:sch_1(A173, A166); A175: for jj being Integer st 1 <= jj & jj <= i1 + 1 holds sm1 . jj = sm2 . jj proof let jj be Integer; ::_thesis: ( 1 <= jj & jj <= i1 + 1 implies sm1 . jj = sm2 . jj ) assume that A176: 1 <= jj and A177: jj <= i1 + 1 ; ::_thesis: sm1 . jj = sm2 . jj reconsider jj2 = jj as Element of NAT by A176, INT_1:3; sm1 . jj2 = sm2 . jj2 by A174, A176, A177; hence sm1 . jj = sm2 . jj ; ::_thesis: verum end; A178: for kk being Element of NAT st S3[kk] holds S3[kk + 1] proof let kk be Element of NAT ; ::_thesis: ( S3[kk] implies S3[kk + 1] ) assume A179: S3[kk] ; ::_thesis: S3[kk + 1] ( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) ) proof assume that 1 <= kk + 1 and A180: kk + 1 <= i1 + 1 ; ::_thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) A181: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, A180, XREAL_1:9; percases ( 0 < kk or 0 >= kk ) ; supposeA182: 0 < kk ; ::_thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) A183: kk < i1 + 1 by A164, A165, A181, XXREAL_0:2; then (i1 + 1) - kk > 0 by XREAL_1:50; then A184: (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def_2; A185: 0 + 1 <= kk by A182, NAT_1:13; then A186: kk - 1 >= 0 by XREAL_1:48; kk -' 1 <= kk by NAT_D:35; then kk -' 1 < i1 + 1 by A183, XXREAL_0:2; then (i1 + 1) - (kk -' 1) >= 0 by XREAL_1:48; then A187: (ii1 + 1) -' (kk -' 1) = (i1 + 1) - (kk -' 1) by XREAL_0:def_2 .= (i1 + 1) - (kk - 1) by A186, XREAL_0:def_2 ; now__::_thesis:_(_(_kk_<=_i2_&_sn1_._(((ii1_+_1)_+_1)_-'_(kk_+_1))_=_sn2_._(((ii1_+_1)_+_1)_-'_(kk_+_1))_)_or_(_kk_>_i2_&_contradiction_)_) percases ( kk <= i2 or kk > i2 ) ; caseA188: kk <= i2 ; ::_thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) ii1 < ii1 + 1 by NAT_1:13; then kk < i1 + 1 by A164, A188, XXREAL_0:2; then A189: (i1 + 1) - kk > 0 by XREAL_1:50; then (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def_2; then A190: (ii1 + 1) -' kk >= 0 + 1 by A189, NAT_1:13; A191: ( (ii1 + 1) -' kk <= i1 + 1 & ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk ) by Th1, NAT_D:35; A192: ( not sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = sn2 . ((ii1 + 1) -' (kk -' 1)) & pn2 . ((ii1 + 1) -' kk) = (pn2 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A130, A164, A185, A187, A184, A188; kk - 1 >= 0 by A185, XREAL_1:48; then kk -' 1 = kk - 1 by XREAL_0:def_2; then kk = (kk -' 1) + 1 ; then A193: ((ii1 + 1) + 1) -' kk = (ii1 + 1) -' (kk -' 1) by Th1; A194: ( sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = (sn2 . ((ii1 + 1) -' (kk -' 1))) - (sm2 . ((ii1 + 1) -' kk)) & pn2 . ((ii1 + 1) -' kk) = ((pn2 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A130, A164, A185, A187, A184, A188; A195: ( not sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = sn1 . ((ii1 + 1) -' (kk -' 1)) & pn1 . ((ii1 + 1) -' kk) = (pn1 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A122, A164, A185, A187, A184, A188; ( sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = (sn1 . ((ii1 + 1) -' (kk -' 1))) - (sm1 . ((ii1 + 1) -' kk)) & pn1 . ((ii1 + 1) -' kk) = ((pn1 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A122, A164, A185, A187, A184, A188; hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A164, A175, A179, A182, A188, A195, A194, A192, A190, A193, A191, NAT_1:13; ::_thesis: verum end; case kk > i2 ; ::_thesis: contradiction hence contradiction by A181; ::_thesis: verum end; end; end; hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) ; ::_thesis: verum end; suppose 0 >= kk ; ::_thesis: sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) then A196: kk = 0 ; ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1 .= ii1 + 1 by A196, NAT_D:40 ; hence sn1 . (((ii1 + 1) + 1) -' (kk + 1)) = sn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A121, A129, A148, A132, XXREAL_0:1; ::_thesis: verum end; end; end; hence S3[kk + 1] ; ::_thesis: verum end; A197: S3[ 0 ] ; A198: for jj being Element of NAT holds S3[jj] from NAT_1:sch_1(A197, A178); A199: for kk being Element of NAT st S2[kk] holds S2[kk + 1] proof let kk be Element of NAT ; ::_thesis: ( S2[kk] implies S2[kk + 1] ) assume A200: S2[kk] ; ::_thesis: S2[kk + 1] ( 1 <= kk + 1 & kk + 1 <= i1 + 1 implies pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) ) proof assume that 1 <= kk + 1 and A201: kk + 1 <= i1 + 1 ; ::_thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) A202: (kk + 1) - 1 <= (i2 + 1) - 1 by A164, A201, XREAL_1:9; percases ( 0 < kk or 0 >= kk ) ; supposeA203: 0 < kk ; ::_thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) A204: kk -' 1 < (kk -' 1) + 1 by NAT_1:13; kk < ii1 + 1 by A201, NAT_1:13; then (i1 + 1) - kk > 0 by XREAL_1:50; then A205: (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def_2; A206: 0 + 1 <= kk by A203, NAT_1:13; then A207: kk - 1 >= 0 by XREAL_1:48; then kk - 1 = kk -' 1 by XREAL_0:def_2; then kk -' 1 < i2 by A202, A204, XXREAL_0:2; then kk -' 1 < i2 + 1 by A164, A165, XXREAL_0:2; then (i1 + 1) - (kk -' 1) >= 0 by A164, XREAL_1:48; then A208: (ii1 + 1) -' (kk -' 1) = (i1 + 1) - (kk -' 1) by XREAL_0:def_2 .= (i1 + 1) - (kk - 1) by A207, XREAL_0:def_2 ; now__::_thesis:_(_(_kk_<=_i2_&_pn1_._(((ii1_+_1)_+_1)_-'_(kk_+_1))_=_pn2_._(((ii1_+_1)_+_1)_-'_(kk_+_1))_)_or_(_kk_>_i2_&_contradiction_)_) percases ( kk <= i2 or kk > i2 ) ; caseA209: kk <= i2 ; ::_thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) ii1 < ii1 + 1 by NAT_1:13; then A210: kk < i1 + 1 by A164, A209, XXREAL_0:2; then A211: (i1 + 1) - kk > 0 by XREAL_1:50; then (ii1 + 1) -' kk = (i1 + 1) - kk by XREAL_0:def_2; then (ii1 + 1) -' kk >= 0 + 1 by A211, NAT_1:13; then A212: sm1 . ((ii1 + 1) -' kk) = sm2 . ((ii1 + 1) -' kk) by A175, NAT_D:35; kk - 1 >= 0 by A206, XREAL_1:48; then kk -' 1 = kk - 1 by XREAL_0:def_2; then kk = (kk -' 1) + 1 ; then A213: ((ii1 + 1) + 1) -' kk = (ii1 + 1) -' (kk -' 1) by Th1; A214: ( not sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = sn1 . ((ii1 + 1) -' (kk -' 1)) & pn1 . ((ii1 + 1) -' kk) = (pn1 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A122, A164, A206, A208, A205, A209; A215: ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1; A216: ( not sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = sn2 . ((ii1 + 1) -' (kk -' 1)) & pn2 . ((ii1 + 1) -' kk) = (pn2 . ((ii1 + 1) -' (kk -' 1))) * 2 ) ) by A130, A164, A206, A208, A205, A209; A217: ( sn2 . ((ii1 + 1) -' (kk -' 1)) >= sm2 . ((ii1 + 1) -' kk) implies ( sn2 . ((ii1 + 1) -' kk) = (sn2 . ((ii1 + 1) -' (kk -' 1))) - (sm2 . ((ii1 + 1) -' kk)) & pn2 . ((ii1 + 1) -' kk) = ((pn2 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A130, A164, A206, A208, A205, A209; ( sn1 . ((ii1 + 1) -' (kk -' 1)) >= sm1 . ((ii1 + 1) -' kk) implies ( sn1 . ((ii1 + 1) -' kk) = (sn1 . ((ii1 + 1) -' (kk -' 1))) - (sm1 . ((ii1 + 1) -' kk)) & pn1 . ((ii1 + 1) -' kk) = ((pn1 . ((ii1 + 1) -' (kk -' 1))) * 2) + 1 ) ) by A122, A164, A206, A208, A205, A209; hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A198, A200, A206, A214, A217, A216, A210, A213, A212, A215; ::_thesis: verum end; case kk > i2 ; ::_thesis: contradiction hence contradiction by A202; ::_thesis: verum end; end; end; hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) ; ::_thesis: verum end; suppose 0 >= kk ; ::_thesis: pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) then A218: kk = 0 ; ((ii1 + 1) + 1) -' (kk + 1) = (ii1 + 1) -' kk by Th1 .= i1 + 1 by A218, NAT_D:40 ; hence pn1 . (((ii1 + 1) + 1) -' (kk + 1)) = pn2 . (((ii1 + 1) + 1) -' (kk + 1)) by A120, A128, A148, A132, XXREAL_0:1; ::_thesis: verum end; end; end; hence S2[kk + 1] ; ::_thesis: verum end; A219: S2[ 0 ] ; A220: for jj being Element of NAT holds S2[jj] from NAT_1:sch_1(A219, A199); A221: for jj being Integer st 1 <= jj & jj <= i1 + 1 holds pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) proof let jj be Integer; ::_thesis: ( 1 <= jj & jj <= i1 + 1 implies pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) ) assume that A222: 1 <= jj and A223: jj <= i1 + 1 ; ::_thesis: pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) reconsider j2 = jj as Element of NAT by A222, INT_1:3; ii1 + 1 < (ii1 + 1) + 1 by NAT_1:13; then jj < (ii1 + 1) + 1 by A223, XXREAL_0:2; then ((ii1 + 1) + 1) - j2 >= 0 by XREAL_1:48; then ((ii1 + 1) + 1) -' j2 = ((ii1 + 1) + 1) - jj by XREAL_0:def_2; hence pn1 . (((i1 + 1) + 1) - jj) = pn2 . (((i1 + 1) + 1) - jj) by A220, A222, A223; ::_thesis: verum end; ( 1 <= 1 + ii1 & ((i1 + 1) + 1) - (i1 + 1) = 1 ) by NAT_1:11; hence t1 = t2 by A123, A131, A221; ::_thesis: verum end; end; end; hence t1 = t2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines idiv1_prg PRGCOR_1:def_1_:_ for n, m being Integer st n >= 0 & m > 0 holds for b3 being Integer holds ( b3 = 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 b3 = 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 ) ) ) ) & b3 = pn . 1 ) ) ) ) ); theorem :: PRGCOR_1:8 for n, m being Integer st n >= 0 holds for sm, sn, pn being FinSequence of INT for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) proof let n, m be Integer; ::_thesis: ( n >= 0 implies for sm, sn, pn being FinSequence of INT for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) ) assume A1: n >= 0 ; ::_thesis: for sm, sn, pn being FinSequence of INT for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) then reconsider n2 = n as Element of NAT by INT_1:3; let sm, sn, pn be FinSequence of INT ; ::_thesis: for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) let i be Integer; ::_thesis: ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) implies ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) ) assume that A2: len sm = n + 1 and A3: ( len sn = n + 1 & len pn = n + 1 ) and A4: ( not n < m implies ( sm . 1 = m & 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 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) ; ::_thesis: ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) proof 1 <= n2 + 1 by NAT_1:12; then A5: 1 in Seg (len sm) by A2, FINSEQ_1:1; assume A6: not n < m ; ::_thesis: ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) then reconsider i2 = i as Element of NAT by A4, INT_1:3; A7: 1 <= i2 + 1 by NAT_1:12; A8: i2 <= n2 + 1 by A4, A6, NAT_1:13; A9: for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) proof let k be Integer; ::_thesis: ( 1 <= k & k < i implies ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) assume that A10: 1 <= k and A11: k < i ; ::_thesis: ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) reconsider k2 = k as Element of NAT by A10, INT_1:3; A12: 1 <= k2 + 1 by NAT_1:12; A13: k2 < n2 + 1 by A8, A11, XXREAL_0:2; then k2 + 1 <= n2 + 1 by NAT_1:13; then A14: k2 + 1 in Seg (n2 + 1) by A12, FINSEQ_1:1; k in Seg (n2 + 1) by A10, A13, FINSEQ_1:1; hence ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) by A2, A4, A6, A10, A11, A14, FINSEQ_1:def_3; ::_thesis: verum end; A15: for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) proof let j be Integer; ::_thesis: ( 1 <= j & j <= i implies ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) assume that A16: 1 <= j and A17: j <= i ; ::_thesis: ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) j - 1 >= 0 by A16, XREAL_1:48; then (i + 1) + 0 <= (i + 1) + (j - 1) by XREAL_1:7; then A18: (i + 1) - (j - 1) <= ((i + 1) + (j - 1)) - (j - 1) by XREAL_1:9; i - j < (i - j) + 1 by XREAL_1:29; then 0 < (i - j) + 1 by A17, XREAL_1:48; then reconsider ij = (i - j) + 1 as Element of NAT by INT_1:3; 0 <= i - j by A17, XREAL_1:48; then A19: ( 0 + 1 <= ((i - j) + 1) + 1 & 0 + 1 <= ij ) by XREAL_1:7; A20: i + 1 <= n2 + 1 by A4, A6, XREAL_1:7; (i + 1) + 0 <= (i + 1) + j by A16, XREAL_1:7; then (i + 1) - j <= ((i + 1) + j) - j by XREAL_1:9; then A21: (i + 1) - j <= n2 + 1 by A20, XXREAL_0:2; i + 1 <= n2 + 1 by A4, A6, XREAL_1:7; then (i + 1) - (j - 1) <= n2 + 1 by A18, XXREAL_0:2; hence ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) by A2, A3, A4, A6, A16, A17, A19, A21, Th7; ::_thesis: verum end; i2 + 1 <= n2 + 1 by A4, A6, XREAL_1:7; then A22: i2 + 1 in Seg (n2 + 1) by A7, FINSEQ_1:1; i2 in Seg (n2 + 1) by A4, A6, A8, FINSEQ_1:1; hence ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) by A2, A3, A4, A6, A5, A15, A22, A9, FINSEQ_1:def_3; ::_thesis: verum end; hence ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds ( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds ( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) ) by A1, A2, A3, Def1; ::_thesis: verum end; theorem Th9: :: PRGCOR_1:9 for n, m being Element of NAT st m > 0 holds idiv1_prg (n,m) = n div m proof let n2, m2 be Element of NAT ; ::_thesis: ( m2 > 0 implies idiv1_prg (n2,m2) = n2 div m2 ) reconsider n = n2, m = m2 as Integer ; assume A1: m2 > 0 ; ::_thesis: idiv1_prg (n2,m2) = n2 div m2 now__::_thesis:_ex_sm,_sn,_pn_being_FinSequence_of_INT_st_ (_len_sm_=_n_+_1_&_len_sn_=_n_+_1_&_len_pn_=_n_+_1_&_(_n_<_m_implies_n2_div_m2_=_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_)_)_)_)_&_n2_div_m2_=_pn_._1_)_)_)_) percases ( n < m or n >= m ) ; supposeA2: n < m ; ::_thesis: ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) set ssm = (Seg (n2 + 1)) --> 1; A3: dom ((Seg (n2 + 1)) --> 1) = Seg (n2 + 1) by FUNCOP_1:13; then reconsider ssm = (Seg (n2 + 1)) --> 1 as FinSequence by FINSEQ_1:def_2; A4: rng ssm c= {1} by FUNCOP_1:13; rng ssm c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssm or y in INT ) assume y in rng ssm ; ::_thesis: y in INT then y = 1 by A4, TARSKI:def_1; hence y in INT by INT_1:def_2; ::_thesis: verum end; then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def_4; A5: ( n < m implies n2 div m2 = 0 ) by PRE_FF:4; len ssm = n + 1 by A3, FINSEQ_1:def_3; hence ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A2, A5; ::_thesis: verum end; supposeA6: n >= m ; ::_thesis: ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) deffunc H1( Nat) -> Element of NAT = n2 div (m2 * (2 |^ ($1 -' 1))); ex ppn being FinSequence st ( len ppn = n2 + 1 & ( for k2 being Nat st k2 in dom ppn holds ppn . k2 = H1(k2) ) ) from FINSEQ_1:sch_2(); then consider ppn being FinSequence such that A7: len ppn = n2 + 1 and A8: for k2 being Nat st k2 in dom ppn holds ppn . k2 = n2 div (m2 * (2 |^ (k2 -' 1))) ; A9: dom ppn = Seg (n2 + 1) by A7, FINSEQ_1:def_3; rng ppn c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ppn or y in INT ) assume y in rng ppn ; ::_thesis: y in INT then consider x being set such that A10: x in dom ppn and A11: y = ppn . x by FUNCT_1:def_3; reconsider n3 = x as Element of NAT by A10; ppn . n3 = n2 div (m2 * (2 |^ (n3 -' 1))) by A8, A10; hence y in INT by A11, INT_1:def_2; ::_thesis: verum end; then reconsider ppn = ppn as FinSequence of INT by FINSEQ_1:def_4; consider ii0 being Element of NAT such that A12: for k2 being Element of NAT st k2 < ii0 holds m * (2 |^ k2) <= n2 and A13: m2 * (2 |^ ii0) > n2 by A1, Th6; reconsider i0 = ii0 as Integer ; deffunc H2( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1))); deffunc H3( Nat) -> Element of NAT = m2 * (2 |^ ($1 -' 1)); A14: 0 + 1 <= i0 + 1 by XREAL_1:7; A15: now__::_thesis:_not_i0_>_n2 1 + 0 <= m2 by A1, NAT_1:13; then A16: 1 * (2 |^ n2) <= m2 * (2 |^ n2) by XREAL_1:64; A17: n2 + 1 <= 2 |^ n2 by NEWTON:85; assume i0 > n2 ; ::_thesis: contradiction then m * (2 |^ n2) <= n2 by A12; then 2 |^ n2 <= n2 by A16, XXREAL_0:2; hence contradiction by A17, NAT_1:13; ::_thesis: verum end; then ( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 ) by NAT_1:11, XREAL_1:7; then A18: ii0 + 1 in Seg (n2 + 1) by FINSEQ_1:1; A19: (ii0 + 1) -' 1 = ii0 by NAT_D:34; then n2 div (m2 * (2 |^ ((ii0 + 1) -' 1))) = 0 by A13, NAT_D:27; then A20: ppn . (i0 + 1) = 0 by A8, A9, A18; n2 >= 0 + 1 by A1, A6, NAT_1:13; then 1 < n2 + 1 by NAT_1:13; then A21: 1 in Seg (n2 + 1) by FINSEQ_1:1; then A22: ppn . 1 = n2 div (m2 * (2 |^ (1 -' 1))) by A8, A9 .= n2 div (m2 * (2 |^ 0)) by XREAL_1:232 .= n2 div (m2 * 1) by NEWTON:4 .= n2 div m2 ; now__::_thesis:_not_i0_=_0 assume i0 = 0 ; ::_thesis: contradiction then m2 * 1 > n2 by A13, NEWTON:4; hence contradiction by A6; ::_thesis: verum end; then A23: ii0 >= 0 + 1 by NAT_1:13; then A24: i0 - 1 >= 0 by XREAL_1:48; reconsider k5 = m2 * (2 |^ ((ii0 + 1) -' 1)) as Element of NAT ; A25: k5 > n2 by A13, NAT_D:34; (ii0 + 1) -' 1 = (i0 - 1) + 1 by NAT_D:34 .= (ii0 -' 1) + 1 by A24, XREAL_0:def_2 ; then A26: 2 |^ ((ii0 + 1) -' 1) = (2 |^ (ii0 -' 1)) * 2 by NEWTON:6; ex ssn being FinSequence st ( len ssn = n2 + 1 & ( for k2 being Nat st k2 in dom ssn holds ssn . k2 = H2(k2) ) ) from FINSEQ_1:sch_2(); then consider ssn being FinSequence such that A27: len ssn = n2 + 1 and A28: for k2 being Nat st k2 in dom ssn holds ssn . k2 = n2 mod (m2 * (2 |^ (k2 -' 1))) ; A29: dom ssn = Seg (n2 + 1) by A27, FINSEQ_1:def_3; rng ssn c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssn or y in INT ) assume y in rng ssn ; ::_thesis: y in INT then consider x being set such that A30: x in dom ssn and A31: y = ssn . x by FUNCT_1:def_3; reconsider n3 = x as Element of NAT by A30; ssn . n3 = n2 mod (m2 * (2 |^ (n3 -' 1))) by A28, A30; hence y in INT by A31, INT_1:def_2; ::_thesis: verum end; then reconsider ssn = ssn as FinSequence of INT by FINSEQ_1:def_4; A32: 1 <= i0 + 1 by A23, NAT_1:13; ex ssm being FinSequence st ( len ssm = n2 + 1 & ( for k2 being Nat st k2 in dom ssm holds ssm . k2 = H3(k2) ) ) from FINSEQ_1:sch_2(); then consider ssm being FinSequence such that A33: len ssm = n2 + 1 and A34: for k2 being Nat st k2 in dom ssm holds ssm . k2 = m * (2 |^ (k2 -' 1)) ; A35: dom ssm = Seg (n2 + 1) by A33, FINSEQ_1:def_3; rng ssm c= INT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ssm or y in INT ) assume y in rng ssm ; ::_thesis: y in INT then consider x being set such that A36: x in dom ssm and A37: y = ssm . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A36; ssm . n = m * (2 |^ (n -' 1)) by A34, A36; hence y in INT by A37, INT_1:def_2; ::_thesis: verum end; then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def_4; A38: ssm . 1 = m * (2 |^ (1 -' 1)) by A21, A34, A35 .= m * (2 |^ 0) by XREAL_1:232 .= m * 1 by NEWTON:4 .= m ; A39: for j being Integer st 1 <= j & j <= i0 holds ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) proof let j be Integer; ::_thesis: ( 1 <= j & j <= i0 implies ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) ) assume that A40: 1 <= j and A41: j <= i0 ; ::_thesis: ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) reconsider jj = j as Element of NAT by A40, INT_1:3; A42: j - 1 >= 0 by A40, XREAL_1:48; A43: i0 - j >= 0 by A41, XREAL_1:48; then A44: ii0 -' jj = i0 - j by XREAL_0:def_2; hereby ::_thesis: ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A41, XXREAL_0:2; then (i0 + 1) - j >= 0 by XREAL_1:48; then A45: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; i0 + 1 <= n2 + j by A15, A40, XREAL_1:7; then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9; then A46: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A45, XREAL_1:7; assume A47: ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; ::_thesis: ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7; then A48: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= jj by NAT_D:35; then jj -' 1 < i0 + 1 by A48, XXREAL_0:2; then A49: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; 2 |^ (ii0 -' jj) <> 0 by CARD_4:3; then A50: m2 * (2 |^ (ii0 -' jj)) > m2 * 0 by A1, XREAL_1:68; ( j + 1 <= i0 + 1 & j < j + 1 ) by A41, XREAL_1:7, XREAL_1:29; then A51: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= j by NAT_D:35; then jj -' 1 < i0 + 1 by A51, XXREAL_0:2; then A52: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A41, XXREAL_0:2; then A53: (i0 + 1) - j > 0 by XREAL_1:50; then A54: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; then A55: (ii0 + 1) -' jj >= 0 + 1 by A53, NAT_1:13; then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48; then A56: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def_2; A57: jj -' 1 = j - 1 by A42, XREAL_0:def_2; then A58: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A52, XREAL_0:def_2; then A59: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A54, NAT_D:34; A60: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A57, A52, XREAL_0:def_2; A61: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A53, XREAL_0:def_2 .= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6 .= 2 * (m2 * (2 |^ (ii0 -' jj))) ; ( (ii0 + 1) -' jj <= i0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7; then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2; then A62: (ii0 + 1) -' jj in Seg (n2 + 1) by A55, FINSEQ_1:1; then A63: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29; (ii0 + 1) -' jj = (i0 - j) + 1 by A53, XREAL_0:def_2; then ((ii0 + 1) -' jj) - 1 >= 0 by A41, XREAL_1:48; then A64: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def_2 .= ii0 -' jj by A43, XREAL_0:def_2 ; then A65: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A62; 1 <= (ii0 + 1) -' (jj -' 1) by A54, A58, NAT_1:11; then A66: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A54, A58, A46, FINSEQ_1:1; jj -' 1 = j - 1 by A42, XREAL_0:def_2; then (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A49, XREAL_0:def_2 .= ((ii0 + 1) -' jj) + 1 by A53, XREAL_0:def_2 ; then A67: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A66 .= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ; (ii0 + 1) -' jj = (i0 + 1) - j by A53, XREAL_0:def_2; then A68: (ssn . ((ii0 + 1) -' (jj -' 1))) - (ssm . ((ii0 + 1) -' jj)) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A47, A58, A67, A61, A65, A50, Th2; ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A62 .= ((n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2) + 1 by A47, A54, A59, A60, A67, A64, A61, A65, A50, Th3 .= ((ppn . ((ii0 + 1) -' (jj -' 1))) * 2) + 1 by A8, A9, A66 ; hence ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) by A54, A58, A56, A63, A68, XREAL_0:def_2; ::_thesis: verum end; thus ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ::_thesis: verum proof ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7; then A69: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= j by NAT_D:35; then jj -' 1 < i0 + 1 by A69, XXREAL_0:2; then A70: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ( j + 1 <= i0 + 1 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7; then A71: j < i0 + 1 by XXREAL_0:2; jj -' 1 <= jj by NAT_D:35; then jj -' 1 < i0 + 1 by A71, XXREAL_0:2; then A72: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48; ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A41, XXREAL_0:2; then (i0 + 1) - j >= 0 by XREAL_1:48; then A73: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; i0 + 1 <= n2 + j by A15, A40, XREAL_1:7; then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9; then A74: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A73, XREAL_1:7; assume A75: not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; ::_thesis: ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ii0 < ii0 + 1 by NAT_1:13; then j < i0 + 1 by A41, XXREAL_0:2; then A76: (i0 + 1) - j > 0 by XREAL_1:50; then A77: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def_2; then A78: (ii0 + 1) -' jj >= 0 + 1 by A76, NAT_1:13; then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48; then A79: ((ii0 + 1) -' jj) -' 1 = i0 - j by A77, XREAL_0:def_2; A80: jj -' 1 = j - 1 by A42, XREAL_0:def_2; then A81: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A72, XREAL_0:def_2; then A82: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A77, NAT_D:34; A83: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A80, A72, XREAL_0:def_2; A84: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A76, XREAL_0:def_2 .= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6 .= 2 * (m2 * (2 |^ (ii0 -' jj))) ; ( (ii0 + 1) -' jj <= ii0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7; then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2; then A85: (ii0 + 1) -' jj in Seg (n2 + 1) by A78, FINSEQ_1:1; then ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29; then A86: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A79, XREAL_0:def_2; (ii0 + 1) -' jj = (i0 - j) + 1 by A76, XREAL_0:def_2; then A87: ((ii0 + 1) -' jj) -' 1 = ((i0 - j) + 1) - 1 by A43, XREAL_0:def_2 .= ii0 -' jj by A43, XREAL_0:def_2 ; then A88: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A85; 1 <= (ii0 + 1) -' (jj -' 1) by A77, A81, NAT_1:11; then A89: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A77, A81, A74, FINSEQ_1:1; jj -' 1 = j - 1 by A42, XREAL_0:def_2; then (ii0 + 1) -' (jj -' 1) = ((ii0 + 1) -' jj) + 1 by A77, A70, XREAL_0:def_2; then A90: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A89 .= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ; ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A85 .= (n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2 by A75, A77, A82, A83, A90, A87, A84, A88, Th5 .= (ppn . ((ii0 + 1) -' (jj -' 1))) * 2 by A8, A9, A89 ; hence ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) by A75, A77, A81, A86, A90, A84, A88, Th4; ::_thesis: verum end; end; i0 < n2 + 1 by A15, NAT_1:13; then ii0 + 1 <= n2 + 1 by NAT_1:13; then ii0 + 1 in Seg (n2 + 1) by A14, FINSEQ_1:1; then ssn . (i0 + 1) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' 1))) by A28, A29; then A91: ssn . (i0 + 1) = n by A25, NAT_D:24; i0 < n2 + 1 by A15, NAT_1:13; then A92: ii0 in Seg (n2 + 1) by A23, FINSEQ_1:1; A93: for k being Element of NAT st 1 <= k & k < i0 holds ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) ) assume that A94: 1 <= k and A95: k < i0 ; ::_thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) A96: k <= n2 by A15, A95, XXREAL_0:2; then A97: k + 1 <= n2 + 1 by XREAL_1:7; k <= n2 + 1 by A96, NAT_1:12; then k in Seg (n2 + 1) by A94, FINSEQ_1:1; then A98: ssm . k = m * (2 |^ (k -' 1)) by A34, A35; 1 < k + 1 by A94, NAT_1:13; then k + 1 in Seg (n2 + 1) by A97, FINSEQ_1:1; then A99: ( (k + 1) -' 1 = k & ssm . (k + 1) = m * (2 |^ ((k + 1) -' 1)) ) by A34, A35, NAT_D:34; A100: k - 1 >= 0 by A94, XREAL_1:48; (k + 1) -' 1 = (k - 1) + 1 by NAT_D:34 .= (k -' 1) + 1 by A100, XREAL_0:def_2 ; then 2 |^ ((k + 1) -' 1) = (2 |^ (k -' 1)) * 2 by NEWTON:6; hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A12, A95, A99, A98; ::_thesis: verum end; A101: for k being Integer st 1 <= k & k < i0 holds ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) proof let k be Integer; ::_thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) ) assume that A102: 1 <= k and A103: k < i0 ; ::_thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) reconsider kk = k as Element of NAT by A102, INT_1:3; ssm . (kk + 1) = (ssm . kk) * 2 by A93, A102, A103; hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A93, A102, A103; ::_thesis: verum end; A104: ssm . (i0 + 1) > n by A34, A35, A13, A19, A18; i0 + 1 <= n2 + 1 by A15, XREAL_1:7; then ii0 + 1 in Seg (n2 + 1) by A32, FINSEQ_1:1; then ssm . (i0 + 1) = m * (2 |^ ((ii0 + 1) -' 1)) by A34, A35 .= (m * (2 |^ (ii0 -' 1))) * 2 by A26 .= (ssm . i0) * 2 by A34, A35, A92 ; hence ex sm, sn, pn being FinSequence of INT st ( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A6, A33, A27, A7, A22, A38, A23, A15, A101, A104, A20, A91, A39; ::_thesis: verum end; end; end; hence idiv1_prg (n2,m2) = n2 div m2 by A1, Def1; ::_thesis: verum end; theorem Th10: :: PRGCOR_1:10 for n, m being Integer st n >= 0 & m > 0 holds idiv1_prg (n,m) = n div m proof let n, m be Integer; ::_thesis: ( n >= 0 & m > 0 implies idiv1_prg (n,m) = n div m ) assume that A1: n >= 0 and A2: m > 0 ; ::_thesis: idiv1_prg (n,m) = n div m reconsider n2 = n, m2 = m as Element of NAT by A1, A2, INT_1:3; idiv1_prg (n,m) = n2 div m2 by A2, Th9; hence idiv1_prg (n,m) = n div m ; ::_thesis: verum end; theorem Th11: :: PRGCOR_1:11 for n, m being Integer for n2, m2 being Element of NAT holds ( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) proof let n, m be Integer; ::_thesis: for n2, m2 being Element of NAT holds ( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) let n2, m2 be Element of NAT ; ::_thesis: ( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) thus ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) by INT_1:48; ::_thesis: ( ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) thus ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) ; ::_thesis: ( ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) thus ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) ::_thesis: ( ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ) proof assume that n >= 0 and A1: m < 0 and A2: n2 = n and A3: m2 = - m ; ::_thesis: ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) thus ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) ::_thesis: ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) proof assume A4: m2 * (n2 div m2) = n2 ; ::_thesis: n div m = - (n2 div m2) A5: m2 > 0 by A1, A3, XREAL_1:58; then A6: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2; thus n div m = [\(n / m)/] by INT_1:def_9 .= [\((- n) / (- m))/] by XCMPLX_1:191 .= (- n2) div m2 by A2, A3, INT_1:def_9 .= - (n2 div m2) by A4, A5, A6, WSIERP_1:42 ; ::_thesis: verum end; thus ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ::_thesis: verum proof assume A7: m2 * (n2 div m2) <> n2 ; ::_thesis: n div m = (- (n2 div m2)) - 1 A8: m2 > 0 by A1, A3, XREAL_1:58; then n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2; then not n2 mod m2 = 0 by A7; then A9: ((- n2) div m2) + 1 = - (n2 div m2) by A8, WSIERP_1:41; n div m = [\(n / m)/] by INT_1:def_9 .= [\((- n) / (- m))/] by XCMPLX_1:191 .= (- n2) div m2 by A2, A3, INT_1:def_9 ; hence n div m = (- (n2 div m2)) - 1 by A9; ::_thesis: verum end; end; thus ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) ::_thesis: ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) proof assume that n < 0 and A10: m > 0 and A11: n2 = - n and A12: m2 = m ; ::_thesis: ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) thus ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) ::_thesis: ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) proof A13: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A10, A12, NAT_D:2; assume A14: m2 * (n2 div m2) = n2 ; ::_thesis: n div m = - (n2 div m2) n div m = (- n2) div m by A11 .= - (n2 div m2) by A10, A12, A14, A13, WSIERP_1:42 ; hence n div m = - (n2 div m2) ; ::_thesis: verum end; thus ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ::_thesis: verum proof assume A15: m2 * (n2 div m2) <> n2 ; ::_thesis: n div m = (- (n2 div m2)) - 1 n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A10, A12, NAT_D:2; then not n2 mod m2 = 0 by A15; then ((- n2) div m2) + 1 = - (n2 div m2) by A10, A12, WSIERP_1:41; hence n div m = (- (n2 div m2)) - 1 by A11, A12; ::_thesis: verum end; end; thus ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) ::_thesis: verum proof assume that n < 0 and m < 0 and A16: ( n2 = - n & m2 = - m ) ; ::_thesis: n div m = n2 div m2 thus n div m = [\(n / m)/] by INT_1:def_9 .= [\((- n) / (- m))/] by XCMPLX_1:191 .= n2 div m2 by A16, INT_1:def_9 ; ::_thesis: verum end; end; definition let n, m be Integer; func idiv_prg (n,m) -> Integer means :Def2: :: PRGCOR_1:def 2 ex i being Integer st ( ( m = 0 implies it = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies it = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies it = - i ) & ( (- m) * i <> n implies it = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies it = - i ) & ( m * i <> - n implies it = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies it = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ); existence ex b1, i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) proof defpred S1[ Integer] means ( ( m = 0 implies n div m = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies n div m = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( $1 = idiv1_prg (n,(- m)) & ( (- m) * $1 = n implies n div m = - $1 ) & ( (- m) * $1 <> n implies n div m = (- $1) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( $1 = idiv1_prg ((- n),m) & ( m * $1 = - n implies n div m = - $1 ) & ( m * $1 <> - n implies n div m = (- $1) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies n div m = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ); percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: ex b1, i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) hence ex b1, i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) ; ::_thesis: verum end; supposeA1: m <> 0 ; ::_thesis: ex b1, i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) now__::_thesis:_(_(_n_>=_0_&_ex_i_being_Integer_st_S1[i]_)_or_(_n_<_0_&_ex_i_being_Integer_st_S1[i]_)_) percases ( n >= 0 or n < 0 ) ; caseA2: n >= 0 ; ::_thesis: ex i being Integer st S1[i] now__::_thesis:_(_(_m_>_0_&_ex_i_being_Integer_st_S1[i]_)_or_(_m_<_0_&_ex_i_being_Integer_st_S1[i]_)_) percases ( m > 0 or m < 0 ) by A1; case m > 0 ; ::_thesis: ex i being Integer st S1[i] then S1[ idiv1_prg (n,m)] by A2, Th10; hence ex i being Integer st S1[i] ; ::_thesis: verum end; caseA3: m < 0 ; ::_thesis: ex i being Integer st S1[i] then reconsider n2 = n, m2 = - m as Element of NAT by A2, INT_1:3; A4: - m > 0 by A3, XREAL_1:58; now__::_thesis:_(_(_(-_m)_*_(idiv1_prg_(n,(-_m)))_=_n_&_ex_i_being_Integer_st_S1[i]_)_or_(_(-_m)_*_(idiv1_prg_(n,(-_m)))_<>_n_&_ex_i_being_Integer_st_S1[i]_)_) percases ( (- m) * (idiv1_prg (n,(- m))) = n or (- m) * (idiv1_prg (n,(- m))) <> n ) ; caseA5: (- m) * (idiv1_prg (n,(- m))) = n ; ::_thesis: ex i being Integer st S1[i] A6: idiv1_prg (n,(- m)) = n div (- m) by A2, A4, Th10; then n div m = - (n2 div m2) by A3, A5, Th11; hence ex i being Integer st S1[i] by A3, A5, A6; ::_thesis: verum end; caseA7: (- m) * (idiv1_prg (n,(- m))) <> n ; ::_thesis: ex i being Integer st S1[i] A8: idiv1_prg (n,(- m)) = n div (- m) by A2, A4, Th10; then n div m = (- (n2 div m2)) - 1 by A3, A7, Th11; hence ex i being Integer st S1[i] by A3, A7, A8; ::_thesis: verum end; end; end; hence ex i being Integer st S1[i] ; ::_thesis: verum end; end; end; hence ex i being Integer st S1[i] ; ::_thesis: verum end; caseA9: n < 0 ; ::_thesis: ex i being Integer st S1[i] now__::_thesis:_(_(_m_<_0_&_ex_i_being_Integer_st_S1[i]_)_or_(_m_>_0_&_ex_i_being_Integer_st_S1[i]_)_) percases ( m < 0 or m > 0 ) by A1; caseA10: m < 0 ; ::_thesis: ex i being Integer st S1[i] A11: n div m = [\(n / m)/] by INT_1:def_9 .= [\((- n) / (- m))/] by XCMPLX_1:191 .= (- n) div (- m) by INT_1:def_9 ; - m > 0 by A10, XREAL_1:58; then S1[ idiv1_prg ((- n),(- m))] by A9, A11, Th10; hence ex i being Integer st S1[i] ; ::_thesis: verum end; caseA12: m > 0 ; ::_thesis: ex i being Integer st S1[i] then reconsider n2 = - n, m2 = m as Element of NAT by A9, INT_1:3; now__::_thesis:_(_(_m_*_(idiv1_prg_((-_n),m))_=_-_n_&_ex_i_being_Integer_st_S1[i]_)_or_(_m_*_(idiv1_prg_((-_n),m))_<>_-_n_&_ex_i_being_Integer_st_S1[i]_)_) percases ( m * (idiv1_prg ((- n),m)) = - n or m * (idiv1_prg ((- n),m)) <> - n ) ; caseA13: m * (idiv1_prg ((- n),m)) = - n ; ::_thesis: ex i being Integer st S1[i] A14: idiv1_prg ((- n),m) = (- n) div m by A9, A12, Th10; then n div m = - (n2 div m2) by A9, A12, A13, Th11; hence ex i being Integer st S1[i] by A9, A12, A13, A14; ::_thesis: verum end; caseA15: m * (idiv1_prg ((- n),m)) <> - n ; ::_thesis: ex i being Integer st S1[i] A16: idiv1_prg ((- n),m) = (- n) div m by A9, A12, Th10; then n div m = (- (n2 div m2)) - 1 by A9, A12, A15, Th11; hence ex i being Integer st S1[i] by A9, A12, A15, A16; ::_thesis: verum end; end; end; hence ex i being Integer st S1[i] ; ::_thesis: verum end; end; end; hence ex i being Integer st S1[i] ; ::_thesis: verum end; end; end; hence ex b1, i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Integer st ex i being Integer st ( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) & ex i being Integer st ( ( m = 0 implies b2 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b2 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b2 = - i ) & ( (- m) * i <> n implies b2 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b2 = - i ) & ( m * i <> - n implies b2 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b2 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) holds b1 = b2 ; end; :: deftheorem Def2 defines idiv_prg PRGCOR_1:def_2_:_ for n, m, b3 being Integer holds ( b3 = idiv_prg (n,m) iff ex i being Integer st ( ( m = 0 implies b3 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b3 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b3 = - i ) & ( (- m) * i <> n implies b3 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b3 = - i ) & ( m * i <> - n implies b3 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b3 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) ); theorem :: PRGCOR_1:12 for n, m being Integer holds idiv_prg (n,m) = n div m proof let n, m be Integer; ::_thesis: idiv_prg (n,m) = n div m percases ( m = 0 or m <> 0 ) ; supposeA1: m = 0 ; ::_thesis: idiv_prg (n,m) = n div m then idiv_prg (n,m) = 0 by Def2; hence idiv_prg (n,m) = n div m by A1, INT_1:48; ::_thesis: verum end; supposeA2: m <> 0 ; ::_thesis: idiv_prg (n,m) = n div m now__::_thesis:_(_(_n_>=_0_&_idiv_prg_(n,m)_=_n_div_m_)_or_(_n_<_0_&_idiv_prg_(n,m)_=_n_div_m_)_) percases ( n >= 0 or n < 0 ) ; caseA3: n >= 0 ; ::_thesis: idiv_prg (n,m) = n div m now__::_thesis:_(_(_m_>_0_&_idiv_prg_(n,m)_=_n_div_m_)_or_(_m_<_0_&_idiv_prg_(n,m)_=_n_div_m_)_) percases ( m > 0 or m < 0 ) by A2; caseA4: m > 0 ; ::_thesis: idiv_prg (n,m) = n div m hence idiv_prg (n,m) = idiv1_prg (n,m) by A3, Def2 .= n div m by A3, A4, Th10 ; ::_thesis: verum end; caseA5: m < 0 ; ::_thesis: idiv_prg (n,m) = n div m now__::_thesis:_(_(_(-_m)_*_(idiv1_prg_(n,(-_m)))_=_n_&_idiv_prg_(n,m)_=_n_div_m_)_or_(_(-_m)_*_(idiv1_prg_(n,(-_m)))_<>_n_&_idiv_prg_(n,m)_=_n_div_m_)_) percases ( (- m) * (idiv1_prg (n,(- m))) = n or (- m) * (idiv1_prg (n,(- m))) <> n ) ; caseA6: (- m) * (idiv1_prg (n,(- m))) = n ; ::_thesis: idiv_prg (n,m) = n div m reconsider m2 = - m, n2 = n as Element of NAT by A3, A5, INT_1:3; - m > 0 by A5, XREAL_1:58; then A7: idiv1_prg (n,(- m)) = n2 div m2 by Th9; idiv_prg (n,m) = - (idiv1_prg (n,(- m))) by A3, A5, A6, Def2; hence idiv_prg (n,m) = n div m by A5, A6, A7, Th11; ::_thesis: verum end; caseA8: (- m) * (idiv1_prg (n,(- m))) <> n ; ::_thesis: idiv_prg (n,m) = n div m reconsider m2 = - m, n2 = n as Element of NAT by A3, A5, INT_1:3; - m > 0 by A5, XREAL_1:58; then A9: idiv1_prg (n,(- m)) = n2 div m2 by Th9; idiv_prg (n,m) = (- (idiv1_prg (n,(- m)))) - 1 by A3, A5, A8, Def2; hence idiv_prg (n,m) = n div m by A5, A8, A9, Th11; ::_thesis: verum end; end; end; hence idiv_prg (n,m) = n div m ; ::_thesis: verum end; end; end; hence idiv_prg (n,m) = n div m ; ::_thesis: verum end; caseA10: n < 0 ; ::_thesis: idiv_prg (n,m) = n div m now__::_thesis:_(_(_m_<_0_&_idiv_prg_(n,m)_=_n_div_m_)_or_(_m_>_0_&_idiv_prg_(n,m)_=_n_div_m_)_) percases ( m < 0 or m > 0 ) by A2; caseA11: m < 0 ; ::_thesis: idiv_prg (n,m) = n div m then A12: - m > 0 by XREAL_1:58; A13: n div m = [\(n / m)/] by INT_1:def_9 .= [\((- n) / (- m))/] by XCMPLX_1:191 .= (- n) div (- m) by INT_1:def_9 ; idiv_prg (n,m) = idiv1_prg ((- n),(- m)) by A10, A11, Def2 .= (- n) div (- m) by A10, A12, Th10 ; hence idiv_prg (n,m) = n div m by A13; ::_thesis: verum end; caseA14: m > 0 ; ::_thesis: idiv_prg (n,m) = n div m now__::_thesis:_(_(_m_*_(idiv1_prg_((-_n),m))_=_-_n_&_idiv_prg_(n,m)_=_n_div_m_)_or_(_m_*_(idiv1_prg_((-_n),m))_<>_-_n_&_idiv_prg_(n,m)_=_n_div_m_)_) percases ( m * (idiv1_prg ((- n),m)) = - n or m * (idiv1_prg ((- n),m)) <> - n ) ; caseA15: m * (idiv1_prg ((- n),m)) = - n ; ::_thesis: idiv_prg (n,m) = n div m reconsider m2 = m, n2 = - n as Element of NAT by A10, A14, INT_1:3; A16: idiv1_prg ((- n),m) = n2 div m2 by A14, Th9; idiv_prg (n,m) = - (idiv1_prg ((- n),m)) by A10, A14, A15, Def2; hence idiv_prg (n,m) = n div m by A10, A14, A15, A16, Th11; ::_thesis: verum end; caseA17: m * (idiv1_prg ((- n),m)) <> - n ; ::_thesis: idiv_prg (n,m) = n div m reconsider m2 = m, n2 = - n as Element of NAT by A10, A14, INT_1:3; A18: idiv1_prg ((- n),m) = n2 div m2 by A14, Th9; idiv_prg (n,m) = (- (idiv1_prg ((- n),m))) - 1 by A10, A14, A17, Def2; hence idiv_prg (n,m) = n div m by A10, A14, A17, A18, Th11; ::_thesis: verum end; end; end; hence idiv_prg (n,m) = n div m ; ::_thesis: verum end; end; end; hence idiv_prg (n,m) = n div m ; ::_thesis: verum end; end; end; hence idiv_prg (n,m) = n div m ; ::_thesis: verum end; end; end;