prgcor_1.miz

begin

 theorem :: PRGCOR_1:1



 Th1: for n,m,k be Nat holds ((n + k) -' (m + k)) = (n -' m)

 proof

 let n,m,k be Nat;



 A1: ((n + k) - (m + k)) = (n - m);

 per cases ;

 suppose (n - m) >= 0 ;

 then (n -' m) = (n - m) by XREAL_0:def 2;

 hence thesis by A1, XREAL_0:def 2;

 end;

 suppose

 A2: (n - m) < 0 ;

 then (n -' m) = 0 by XREAL_0:def 2;

 hence thesis by A1, A2, XREAL_0:def 2;

 end;

 end;

 theorem :: PRGCOR_1:2



 Th2: for n,k be 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 ;

 assume that

 A1: k > 0 and

 A2: (n mod (2 * k)) >= k;

 (ex t be 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 be 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 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;

 hence thesis;

 end;

 theorem :: PRGCOR_1:3



 Th3: for n,k be 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 ;

 assume that

 A1: k > 0 and

 A2: (n mod (2 * k)) >= k;

 (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 thesis by A3, NAT_D:def 1;

 end;

 theorem :: PRGCOR_1:4



 Th4: for n,k be 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 ;

 assume that

 A1: k > 0 and

 A2: (n mod (2 * k)) < k;

 (ex t be 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 be Nat such that

 A3: n = (((2 * k) * t) + (n mod (2 * k))) by A1;

 reconsider t as Element of NAT by ORDINAL1:def 12;

 n = ((k * (2 * t)) + (n mod (2 * k))) by A3;

 hence thesis by A2, NAT_D:def 2;

 end;

 theorem :: PRGCOR_1:5



 Th5: for n,k be 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 ;

 assume that

 A1: k > 0 and

 A2: (n mod (2 * k)) < k;

 (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 thesis by A3, NAT_D:def 1;

 end;

 theorem :: PRGCOR_1:6



 Th6: for m,n be Element of NAT st m > 0 holds ex i be Element of NAT st (for k2 be Element of NAT st k2 n

 proof

 let m,n be Element of NAT ;

 defpred P[ 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 ;

 then m >= ( 0 + 1) by NAT_1: 13;

 then

 A3: (m * n) >= (1 * n) by XREAL_1: 64;

 (2 |^ ((n + 1) -' 1)) > ((n + 1) -' 1) by NEWTON: 86;

 then (m * (2 |^ ((n + 1) -' 1))) > (m * ((n + 1) -' 1)) by A2, XREAL_1: 68;

 then (m * (2 |^ ((n + 1) -' 1))) > n by A1, A3, XXREAL_0: 2;

 then

 A4: ex k be Nat st P[k];

 ex k be Nat st P[k] & for j be Nat st P[j] holds k <= j from NAT_1:sch 5( A4);

 then

 consider k be Nat such that

 A5: P[k] and

 A6: for j be Nat st P[j] holds k <= j;

 k in NAT & for k2 be Element of NAT st k2 < k holds (m * (2 |^ k2)) <= n by A6, ORDINAL1:def 12;

 hence thesis by A5;

 end;

 theorem :: PRGCOR_1:7



 Th7: for i be Integer, f be FinSequence st 1 <= i & i <= ( len f) holds i in ( dom f)

 proof

 let i be Integer, f be FinSequence;

 assume that

 A1: 1 <= i and

 A2: i <= ( len f);

 i is Element of NAT by A1, INT_1: 3;

 hence thesis by A1, A2, FINSEQ_3: 25;

 end;

 definition

 let n,m be Integer;

 assume that

 A1: n >= 0 and

 A2: m > 0 ;

 :: PRGCOR_1:def1

 func idiv1_prg (n,m) -> Integer means

 : Def1: ex sm,sn,pn be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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

 proof

 reconsider n2 = n, m2 = m as Element of NAT by A1, A2, INT_1: 3;

 per cases ;

 suppose

 A3: n < m;

 set ssm = (( Seg (n2 + 1)) --> 1);



 A4: ( dom ssm) = ( Seg (n2 + 1)) by FUNCOP_1: 13;

 then

 reconsider ssm as FinSequence by FINSEQ_1:def 2;



 A5: ( rng ssm) c= {1} by FUNCOP_1: 13;

 ( rng ssm) c= INT

 proof

 let y be object;

 assume y in ( rng ssm);

 then y = 1 by A5, TARSKI:def 1;

 hence thesis by INT_1:def 2;

 end;

 then

 reconsider ssm as FinSequence of INT by FINSEQ_1:def 4;

 ( len ssm) = (n + 1) by A4, FINSEQ_1:def 3;

 hence thesis by A3;

 end;

 suppose

 A6: n >= m;

 deffunc F3( Nat) = (n2 div (m2 * (2 |^ ($1 -' 1))));



 A7: (m2 * (2 |^ 0 )) = (m2 * 1) by NEWTON: 4

 .= m2;

 ex ppn be FinSequence st ( len ppn) = (n2 + 1) & for k2 be Nat st k2 in ( dom ppn) holds (ppn . k2) = F3(k2) from FINSEQ_1:sch 2;

 then

 consider ppn be FinSequence such that

 A8: ( len ppn) = (n + 1) and

 A9: for k2 be 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 object;

 assume y in ( rng ppn);

 then

 consider x be object 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 thesis by A12, INT_1:def 2;

 end;

 then

 reconsider 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 F( Nat) = (n2 mod (m2 * (2 |^ ($1 -' 1))));

 deffunc F1( Nat) = (m2 * (2 |^ ($1 -' 1)));

 ex ssm be FinSequence st ( len ssm) = (n2 + 1) & for k2 be Nat st k2 in ( dom ssm) holds (ssm . k2) = F1(k2) from FINSEQ_1:sch 2;

 then

 consider ssm be FinSequence such that

 A15: ( len ssm) = (n2 + 1) and

 A16: for k2 be 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 object;

 assume y in ( rng ssm);

 then

 consider x be object 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 thesis by A20, INT_1:def 2;

 end;

 ex ssn be FinSequence st ( len ssn) = (n2 + 1) & for k2 be Nat st k2 in ( dom ssn) holds (ssn . k2) = F(k2) from FINSEQ_1:sch 2;

 then

 consider ssn be FinSequence such that

 A21: ( len ssn) = (n2 + 1) and

 A22: for k2 be 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 object;

 assume y in ( rng ssn);

 then

 consider x be object 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 thesis by A25, INT_1:def 2;

 end;

 then

 reconsider ssn as FinSequence of INT by FINSEQ_1:def 4;

 consider ii0 be Element of NAT such that

 A26: for k2 be 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

 assume i0 = 0 ;

 then (m2 * 1) > n2 by A27, NEWTON: 4;

 hence contradiction by A6;

 end;

 then

 A29: ii0 >= ( 0 + 1) by NAT_1: 13;

 then

 A30: (i0 - 1) >= 0 by XREAL_1: 48;

 A31:

 now

 (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;

 then (m * (2 |^ n2)) <= n2 by A26;

 then (2 |^ n2) <= n2 by A32, XXREAL_0: 2;

 hence contradiction by A33, NAT_1: 13;

 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 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 be 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;

 assume that

 A43: 1 <= j and

 A44: j <= i0;

 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)

 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));

 (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 thesis by A57, A65, A59, A61, A72, XREAL_0:def 2;

 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)

 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));

 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 thesis by A79, A81, A89, A85, A93, A95, A87, Th4;

 end;

 end;



 A96: for k be 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 ;

 assume that

 A97: 1 <= k and

 A98: k < i0;



 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 thesis by A26, A98, A102, A101;

 end;



 A104: for k be Integer st 1 <= k & k < i0 holds (ssm . (k + 1)) = ((ssm . k) * 2) & not (ssm . (k + 1)) > n

 proof

 let k be Integer;

 assume that

 A105: 1 <= k and

 A106: k < i0;

 reconsider kk = k as Element of NAT by A105, INT_1: 3;

 (ssm . (kk + 1)) = ((ssm . kk) * 2) by A96, A105, A106;

 hence thesis by A96, A105, A106;

 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 thesis by A6, A15, A21, A8, A14, A39, A29, A31, A108, A104, A41, A36, A42;

 end;

 end;

 uniqueness

 proof

 let t1,t2 be Integer;

 assume that

 A109: ex sm,sn,pn be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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 be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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));

 consider sm1,sn1,pn1 be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm1 . (i + 1)) = ((sm1 . i) * 2) & (sm1 . (i + 1)) > n & (pn1 . (i + 1)) = 0 & (sn1 . (i + 1)) = n & (for j be 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 be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm2 . (i + 1)) = ((sm2 . i) * 2) & (sm2 . (i + 1)) > n & (pn2 . (i + 1)) = 0 & (sn2 . (i + 1)) = n & (for j be 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

 per cases ;

 suppose n < m;

 hence thesis by A111, A113;

 end;

 suppose

 A115: n >= m;

 then

 consider i1 be Integer such that

 A116: 1 <= i1 and i1 <= n and

 A117: for k be 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 be 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 P2[ Nat] means 1 <= $1 & $1 <= (i1 + 1) implies (sm1 . $1) = (sm2 . $1);

 defpred P4[ Nat] means 1 <= $1 & $1 <= (i1 + 1) implies (pn1 . (((ii1 + 1) + 1) -' $1)) = (pn2 . (((ii1 + 1) + 1) -' $1));

 defpred P3[ Nat] means 1 <= $1 & $1 <= (i1 + 1) implies (sn1 . (((ii1 + 1) + 1) -' $1)) = (sn2 . (((ii1 + 1) + 1) -' $1));

 consider i2 be Integer such that

 A124: 1 <= i2 and i2 <= n and

 A125: for k be 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 be 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

 assume

 A133: i2 < i1;



 A134: for k be Integer st 1 <= k & k <= (i2 + 1) holds (sm2 . k) = (sm1 . k)

 proof

 defpred P[ Nat] means $1 < (i2 + 1) implies (sm2 . ($1 + 1)) = (sm1 . ($1 + 1));

 let k be Integer;

 assume that

 A135: 1 <= k and

 A136: k <= (i2 + 1);

 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 be Nat st P[e] holds P[(e + 1)]

 proof

 let e be Nat;

 assume

 A140: P[e];

 per cases ;

 suppose (e + 1) < (i2 + 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

 per cases ;

 case (e + 1) < i2;

 hence (sm2 . ((e + 1) + 1)) = ((sm2 . (e + 1)) * 2) by A125, A142;

 end;

 case (e + 1) >= i2;

 then (e + 1) = i2 by A141, XXREAL_0: 1;

 hence (sm2 . ((e + 1) + 1)) = ((sm2 . (e + 1)) * 2) by A126;

 end;

 end;



 A144: e < (e + 1) by NAT_1: 13;

 (e + 1) < i1 by A133, A141, XXREAL_0: 2;

 hence thesis by A117, A140, A142, A144, A143, XXREAL_0: 2;

 end;

 suppose (e + 1) >= (i2 + 1);

 hence thesis;

 end;

 end;



 A145: P[ 0 ] by A112, A114, A115;



 A146: for e be Nat holds P[e] from NAT_1:sch 2( 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 thesis by A138, A146;

 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;

 end;

 A148:

 now

 assume

 A149: i1 < i2;



 A150: for k be Integer st 1 <= k & k <= (i1 + 1) holds (sm1 . k) = (sm2 . k)

 proof

 defpred P[ Nat] means $1 < (i1 + 1) implies (sm1 . ($1 + 1)) = (sm2 . ($1 + 1));

 let k be Integer;

 assume that

 A151: 1 <= k and

 A152: k <= (i1 + 1);

 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 be Nat st P[e] holds P[(e + 1)]

 proof

 let e be Nat;

 assume

 A156: P[e];

 per cases ;

 suppose (e + 1) < (i1 + 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

 per cases ;

 case (e + 1) < i1;

 hence (sm1 . ((e + 1) + 1)) = ((sm1 . (e + 1)) * 2) by A117, A158;

 end;

 case (e + 1) >= i1;

 then (e + 1) = i1 by A157, XXREAL_0: 1;

 hence (sm1 . ((e + 1) + 1)) = ((sm1 . (e + 1)) * 2) by A118;

 end;

 end;



 A160: e < (e + 1) by NAT_1: 13;

 (e + 1) < i2 by A149, A157, XXREAL_0: 2;

 hence thesis by A125, A156, A158, A160, A159, XXREAL_0: 2;

 end;

 suppose (e + 1) >= (i1 + 1);

 hence thesis;

 end;

 end;



 A161: P[ 0 ] by A112, A114, A115;



 A162: for e be Nat holds P[e] from NAT_1:sch 2( 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 thesis by A154, A162;

 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;

 end;

 then

 A164: i1 = i2 by A132, XXREAL_0: 1;



 A165: ii1 < (ii1 + 1) by NAT_1: 13;



 A166: for kk be Nat st P2[kk] holds P2[(kk + 1)]

 proof

 let kk be Nat;

 assume

 A167: P2[kk];

 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);

 per cases by A168, XXREAL_0: 1;

 suppose

 A169: (kk + 1) < (i1 + 1);

 then

 A170: ((kk + 1) - 1) <= ((i2 + 1) - 1) by A164, XREAL_1: 9;

 now

 per cases ;

 case 0 < kk;

 then

 A171: ( 0 + 1) <= kk by NAT_1: 13;

 A172:

 now

 per cases ;

 case kk < i2;

 hence (sm2 . (kk + 1)) = ((sm2 . kk) * 2) by A125, A171;

 end;

 case kk >= i2;

 then kk = i2 by A170, XXREAL_0: 1;

 hence (sm2 . (kk + 1)) = ((sm2 . kk) * 2) by A126;

 end;

 end;

 kk < i1 by A169, XREAL_1: 7;

 hence thesis by A117, A165, A167, A171, A172, XXREAL_0: 2;

 end;

 case 0 >= kk;

 then kk = 0 ;

 hence thesis by A112, A114, A115;

 end;

 end;

 hence thesis;

 end;

 suppose (kk + 1) = (i1 + 1);

 hence thesis by A116, A118, A126, A164, A167, NAT_1: 13;

 end;

 end;

 hence thesis;

 end;



 A173: P2[ 0 ];



 A174: for jj be Nat holds P2[jj] from NAT_1:sch 2( A173, A166);



 A175: for jj be Integer st 1 <= jj & jj <= (i1 + 1) holds (sm1 . jj) = (sm2 . jj)

 proof

 let jj be Integer;

 assume that

 A176: 1 <= jj and

 A177: jj <= (i1 + 1);

 reconsider jj2 = jj as Element of NAT by A176, INT_1: 3;

 (sm1 . jj2) = (sm2 . jj2) by A174, A176, A177;

 hence thesis;

 end;



 A178: for kk be Nat st P3[kk] holds P3[(kk + 1)]

 proof

 let kk be Nat;

 assume

 A179: P3[kk];

 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);



 A181: ((kk + 1) - 1) <= ((i2 + 1) - 1) by A164, A180, XREAL_1: 9;

 per cases ;

 suppose

 A182: 0 < kk;



 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

 per cases ;

 case

 A188: kk <= i2;

 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 thesis by A164, A175, A179, A182, A188, A195, A194, A192, A190, A193, A191, NAT_1: 13;

 end;

 case kk > i2;

 hence contradiction by A181;

 end;

 end;

 hence thesis;

 end;

 suppose 0 >= kk;

 then

 A196: kk = 0 ;

 (((ii1 + 1) + 1) -' (kk + 1)) = ((ii1 + 1) -' kk) by Th1

 .= (ii1 + 1) by A196, NAT_D: 40;

 hence thesis by A121, A129, A148, A132, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;



 A197: P3[ 0 ];



 A198: for jj be Nat holds P3[jj] from NAT_1:sch 2( A197, A178);



 A199: for kk be Nat st P4[kk] holds P4[(kk + 1)]

 proof

 let kk be Nat;

 assume

 A200: P4[kk];

 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);



 A202: ((kk + 1) - 1) <= ((i2 + 1) - 1) by A164, A201, XREAL_1: 9;

 per cases ;

 suppose

 A203: 0 < kk;



 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

 per cases ;

 case

 A209: kk <= i2;

 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 thesis by A198, A200, A206, A214, A217, A216, A210, A213, A212, A215;

 end;

 case kk > i2;

 hence contradiction by A202;

 end;

 end;

 hence thesis;

 end;

 suppose 0 >= kk;

 then

 A218: kk = 0 ;

 (((ii1 + 1) + 1) -' (kk + 1)) = ((ii1 + 1) -' kk) by Th1

 .= (i1 + 1) by A218, NAT_D: 40;

 hence thesis by A120, A128, A148, A132, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;



 A219: P4[ 0 ];



 A220: for jj be Nat holds P4[jj] from NAT_1:sch 2( A219, A199);



 A221: for jj be Integer st 1 <= jj & jj <= (i1 + 1) holds (pn1 . (((i1 + 1) + 1) - jj)) = (pn2 . (((i1 + 1) + 1) - jj))

 proof

 let jj be Integer;

 assume that

 A222: 1 <= jj and

 A223: jj <= (i1 + 1);

 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 thesis by A220, A222, A223;

 end;

 1 <= (1 + ii1) & (((i1 + 1) + 1) - (i1 + 1)) = 1 by NAT_1: 11;

 hence thesis by A123, A131, A221;

 end;

 end;

 hence thesis;

 end;

 end

 theorem :: PRGCOR_1:8

 for n,m be Integer st n >= 0 holds for sm,sn,pn be FinSequence of INT , i be 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 be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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 be Integer st 1 <= k & k 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 be 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;

 assume

 A1: n >= 0 ;

 then

 reconsider n2 = n as Element of NAT by INT_1: 3;

 let sm,sn,pn be FinSequence of INT , i be Integer;

 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 be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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);

 not n < m implies 1 in ( dom sm) & (sm . 1) = m & 1 <= i & i <= n & (for k be Integer st 1 <= k & k 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 be 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;

 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 be Integer st 1 <= k & k n

 proof

 let k be Integer;

 assume that

 A10: 1 <= k and

 A11: k < i;

 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 thesis by A2, A4, A6, A10, A11, A14, FINSEQ_1:def 3;

 end;



 A15: for j be 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;

 assume that

 A16: 1 <= j and

 A17: j <= i;

 (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 thesis by A2, A3, A4, A6, A16, A17, A19, A21, Th7;

 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 thesis by A2, A3, A4, A6, A5, A15, A22, A9, FINSEQ_1:def 3;

 end;

 hence thesis by A1, A2, A3, Def1;

 end;

 theorem :: PRGCOR_1:9



 Th9: for n,m be Element of NAT st m > 0 holds ( idiv1_prg (n qua Integer,m qua Integer)) = (n div m)

 proof

 let n2,m2 be Element of NAT ;

 reconsider n = n2, m = m2 as Integer;

 assume

 A1: m2 > 0 ;

 now

 per cases ;

 suppose

 A2: n < m;

 set ssm = (( Seg (n2 + 1)) --> 1);



 A3: ( dom ssm) = ( Seg (n2 + 1)) by FUNCOP_1: 13;

 then

 reconsider ssm as FinSequence by FINSEQ_1:def 2;



 A4: ( rng ssm) c= {1} by FUNCOP_1: 13;

 ( rng ssm) c= INT

 proof

 let y be object;

 assume y in ( rng ssm);

 then y = 1 by A4, TARSKI:def 1;

 hence thesis by INT_1:def 2;

 end;

 then

 reconsider 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 be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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;

 end;

 suppose

 A6: n >= m;

 deffunc F3( Nat) = (n2 div (m2 * (2 |^ ($1 -' 1))));

 ex ppn be FinSequence st ( len ppn) = (n2 + 1) & for k2 be Nat st k2 in ( dom ppn) holds (ppn . k2) = F3(k2) from FINSEQ_1:sch 2;

 then

 consider ppn be FinSequence such that

 A7: ( len ppn) = (n2 + 1) and

 A8: for k2 be 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 object;

 assume y in ( rng ppn);

 then

 consider x be object 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 thesis by A11, INT_1:def 2;

 end;

 then

 reconsider ppn as FinSequence of INT by FINSEQ_1:def 4;

 consider ii0 be Element of NAT such that

 A12: for k2 be 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 F( Nat) = (n2 mod (m2 * (2 |^ ($1 -' 1))));

 deffunc F1( Nat) = (m2 * (2 |^ ($1 -' 1)));



 A14: ( 0 + 1) <= (i0 + 1) by XREAL_1: 7;

 A15:

 now

 (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;

 then (m * (2 |^ n2)) <= n2 by A12;

 then (2 |^ n2) <= n2 by A16, XXREAL_0: 2;

 hence contradiction by A17, NAT_1: 13;

 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

 assume i0 = 0 ;

 then (m2 * 1) > n2 by A13, NEWTON: 4;

 hence contradiction by A6;

 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 be FinSequence st ( len ssn) = (n2 + 1) & for k2 be Nat st k2 in ( dom ssn) holds (ssn . k2) = F(k2) from FINSEQ_1:sch 2;

 then

 consider ssn be FinSequence such that

 A27: ( len ssn) = (n2 + 1) and

 A28: for k2 be 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 object;

 assume y in ( rng ssn);

 then

 consider x be object 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 thesis by A31, INT_1:def 2;

 end;

 then

 reconsider ssn as FinSequence of INT by FINSEQ_1:def 4;



 A32: 1 <= (i0 + 1) by A23, NAT_1: 13;

 ex ssm be FinSequence st ( len ssm) = (n2 + 1) & for k2 be Nat st k2 in ( dom ssm) holds (ssm . k2) = F1(k2) from FINSEQ_1:sch 2;

 then

 consider ssm be FinSequence such that

 A33: ( len ssm) = (n2 + 1) and

 A34: for k2 be 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 object;

 assume y in ( rng ssm);

 then

 consider x be object 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 thesis by A37, INT_1:def 2;

 end;

 then

 reconsider 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 be 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;

 assume that

 A40: 1 <= j and

 A41: j <= i0;

 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

 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));

 (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;

 end;

 thus thesis

 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));

 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 thesis by A75, A77, A81, A86, A90, A84, A88, Th4;

 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 be 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 ;

 assume that

 A94: 1 <= k and

 A95: k < i0;



 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 thesis by A12, A95, A99, A98;

 end;



 A101: for k be Integer st 1 <= k & k < i0 holds (ssm . (k + 1)) = ((ssm . k) * 2) & not (ssm . (k + 1)) > n

 proof

 let k be Integer;

 assume that

 A102: 1 <= k and

 A103: k < i0;

 reconsider kk = k as Element of NAT by A102, INT_1: 3;

 (ssm . (kk + 1)) = ((ssm . kk) * 2) by A93, A102, A103;

 hence thesis by A93, A102, A103;

 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 be 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 be Integer st 1 <= i & i <= n & (for k be Integer st 1 <= k & k n)) & (sm . (i + 1)) = ((sm . i) * 2) & (sm . (i + 1)) > n & (pn . (i + 1)) = 0 & (sn . (i + 1)) = n & (for j be 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;

 end;

 end;

 hence thesis by A1, Def1;

 end;

 theorem :: PRGCOR_1:10



 Th10: for n,m be Integer st n >= 0 & m > 0 holds ( idiv1_prg (n,m)) = (n div m)

 proof

 let n,m be Integer;

 assume that

 A1: n >= 0 and

 A2: m > 0 ;

 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 thesis;

 end;

 theorem :: PRGCOR_1:11



 Th11: for n,m be Integer, n2,m2 be 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, n2,m2 be Element of NAT ;

 thus m = 0 & n2 = n & m2 = m implies (n div m) = 0 & (n2 div m2) = 0 by INT_1: 48;

 thus 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))

 proof

 assume that n >= 0 and

 A1: m < 0 and

 A2: n2 = n and

 A3: m2 = ( - m);

 thus (m2 * (n2 div m2)) = n2 implies (n div m) = ( - (n2 div m2))

 proof

 assume

 A4: (m2 * (n2 div m2)) = n2;

 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, A6, WSIERP_1: 42;

 end;

 thus (m2 * (n2 div m2)) <> n2 implies (n div m) = (( - (n2 div m2)) - 1)

 proof

 assume

 A7: (m2 * (n2 div m2)) <> n2;



 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 thesis by A9;

 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))

 proof

 assume that n < 0 and

 A10: m > 0 and

 A11: n2 = ( - n) and

 A12: m2 = m;

 thus (m2 * (n2 div m2)) = n2 implies (n div m) = ( - (n2 div m2))

 proof



 A13: n2 = ((m2 * (n2 div m2)) + (n2 mod m2)) by A10, A12, NAT_D: 2;

 assume

 A14: (m2 * (n2 div m2)) = n2;

 (n div m) = (( - n2) div m) by A11

 .= ( - (n2 div m2)) by A12, A14, A13, WSIERP_1: 42;

 hence thesis;

 end;

 thus (m2 * (n2 div m2)) <> n2 implies (n div m) = (( - (n2 div m2)) - 1)

 proof

 assume

 A15: (m2 * (n2 div m2)) <> n2;

 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 thesis by A11, A12;

 end;

 end;

 thus n < 0 & m < 0 & n2 = ( - n) & m2 = ( - m) implies (n div m) = (n2 div m2)

 proof

 assume that n < 0 and m < 0 and

 A16: n2 = ( - n) & m2 = ( - m);



 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;

 end;

 end;

 definition

 let n,m be Integer;

 :: PRGCOR_1:def2

 func idiv_prg (n,m) -> Integer means

 : Def2: ex i be Integer st (m = 0 implies it = 0 ) & ( not m = 0 implies (n >= 0 & m > 0 implies it = ( idiv1_prg (n,m))) & ( not (n >= 0 & 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 & 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 & m > 0 ) implies it = ( idiv1_prg (( - n),( - m)))))));

 existence

 proof

 defpred P[ 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 & 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 & 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 & m > 0 ) implies (n div m) = ( idiv1_prg (( - n),( - m)))))));

 per cases ;

 suppose m = 0 ;

 hence thesis;

 end;

 suppose

 A1: m <> 0 ;

 now

 per cases ;

 case

 A2: n >= 0 ;

 now

 per cases by A1;

 case m > 0 ;

 then P[( idiv1_prg (n,m))] by A2, Th10;

 hence ex i be Integer st P[i];

 end;

 case

 A3: m < 0 ;

 then

 reconsider n2 = n, m2 = ( - m) as Element of NAT by A2, INT_1: 3;



 A4: ( - m) > 0 by A3, XREAL_1: 58;

 now

 per cases ;

 case

 A5: (( - m) * ( idiv1_prg (n,( - m)))) = n;



 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 be Integer st P[i] by A3, A5, A6;

 end;

 case

 A7: (( - m) * ( idiv1_prg (n,( - m)))) <> n;



 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 be Integer st P[i] by A3, A7, A8;

 end;

 end;

 hence ex i be Integer st P[i];

 end;

 end;

 hence ex i be Integer st P[i];

 end;

 case

 A9: n < 0 ;

 now

 per cases by A1;

 case

 A10: m < 0 ;



 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 P[( idiv1_prg (( - n),( - m)))] by A9, A11, Th10;

 hence ex i be Integer st P[i];

 end;

 case

 A12: m > 0 ;

 then

 reconsider n2 = ( - n), m2 = m as Element of NAT by A9, INT_1: 3;

 now

 per cases ;

 case

 A13: (m * ( idiv1_prg (( - n),m))) = ( - n);



 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 be Integer st P[i] by A9, A12, A13, A14;

 end;

 case

 A15: (m * ( idiv1_prg (( - n),m))) <> ( - n);



 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 be Integer st P[i] by A9, A12, A15, A16;

 end;

 end;

 hence ex i be Integer st P[i];

 end;

 end;

 hence ex i be Integer st P[i];

 end;

 end;

 hence thesis;

 end;

 end;

 uniqueness ;

 end

 theorem :: PRGCOR_1:12

 for n,m be Integer holds ( idiv_prg (n,m)) = (n div m)

 proof

 let n,m be Integer;

 per cases ;

 suppose

 A1: m = 0 ;

 then ( idiv_prg (n,m)) = 0 by Def2;

 hence thesis by A1, INT_1: 48;

 end;

 suppose

 A2: m <> 0 ;

 now

 per cases ;

 case

 A3: n >= 0 ;

 now

 per cases by A2;

 case

 A4: m > 0 ;



 hence ( idiv_prg (n,m)) = ( idiv1_prg (n,m)) by A3, Def2

 .= (n div m) by A3, A4, Th10;

 end;

 case

 A5: m < 0 ;

 now

 per cases ;

 case

 A6: (( - m) * ( idiv1_prg (n,( - m)))) = n;

 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 thesis by A5, A6, A7, Th11;

 end;

 case

 A8: (( - m) * ( idiv1_prg (n,( - m)))) <> n;

 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 thesis by A5, A8, A9, Th11;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 case

 A10: n < 0 ;

 now

 per cases by A2;

 case

 A11: m < 0 ;

 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 thesis by A13;

 end;

 case

 A14: m > 0 ;

 now

 per cases ;

 case

 A15: (m * ( idiv1_prg (( - n),m))) = ( - n);

 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 thesis by A10, A14, A15, A16, Th11;

 end;

 case

 A17: (m * ( idiv1_prg (( - n),m))) <> ( - n);

 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 thesis by A10, A14, A17, A18, Th11;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;