:: Correctness of Non Overwriting Programs. {P}art {I}
:: by Yatsuka Nakamura
::
:: Received December 5, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, INT_1,
RELAT_1, NAT_1, FUNCT_1, NEWTON, FINSEQ_1, FUNCOP_1, TARSKI, PRGCOR_1;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1,
FINSEQ_1, INT_1, RELSET_1, FUNCOP_1, PARTFUN1, NAT_1, NAT_D, NEWTON;
constructors XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, BINARITH, RELSET_1,
FUNCOP_1, VALUED_0;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
VALUED_0, FINSEQ_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions TARSKI;
theorems FINSEQ_1, NAT_1, FUNCT_1, XCMPLX_1, PRE_FF, INT_1, NEWTON, CARD_4,
FINSEQ_3, FUNCOP_1, TARSKI, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, WSIERP_1,
XREAL_0;
schemes NAT_1, FINSEQ_1;
begin
::----------------------
::----------------------
:: Non overwriting program is a program where each variable used in it
::is written only just one time, but the control variables used for
::for-statement are exceptional. Contrarily, variables are allowed
::to be read many times.
:: There are other restriction for non overwriting program. For statements,
::only the followings are allowed: substituting-statement, if-else-statement,
::for-statement(with break and without break), function(correct one)-call
::-statement and return-statement.
:: Grammars of non overwriting program is like one of C-language.
:: For type of variables, 'int','real","char" and "float" can be used, and
::and array of them can also be used. For operation, "+", "-" and "*"
::are used for a type int, "+","-","*" and "/" are used for a type float.
:: User can also define structures like in C.
:: Non overwriting program can be translated to (predicative) logic
::formula in definition part to define functions. If a new function
::is correctly defined, a corresponding program is correct, if it does not use
::arrays. If it uses arrays, area check is necessary in the following
::theorem.
:: Semantic correctness is shown by some theorems following the definition.
::These theorems must tie up the result of the program and mathematical concepts
::introduced before.
:: Correctness is proven function-wise. We must use only
::correctness-proven functions to define a new function(to write a new
::program as a form of a function).
:: Here, we present two program of division function of two natural
::numbers and of two integers. An algorithm is checked for each case, by
::proving correctness of the definitions.
:: We also do an area check of index of arrays used in one of the programs.
::---------
:: type correspondence:
:: int .....> Integer
:: float .....> Real
:: char ......> Subset of A
::---------
:: statement correspondence:
:: We use tr(statement_i) for translated logic formula corresponding
:: to statement_i.
:: i=j+k-l; ....> i=j+k-l
:: i=j*k; ....> i=j*k
:: x=y*z/s; ....> x=y*z/s
:: statement_1;statement2;statement3;...
:: .......> tr(statement_1)& tr(statement_2)& tr(statement_3)&...
:: if (statement_1){statement_2;statement_3;...}
:: .......> tr(statement_1) implies tr(statement_2)& tr(statement_3)&..;
:: if (statement_1){statement_2;statement_3;...} else statement_4;
:: .......> (tr(statement_1) implies tr(statement_2)& tr(statement_3)&..)&
:: (not tr(statement_1) implies tr(statement_4));
:: for (i=1;i++;i<=n)statement_1;
:: .......> for i being Integer st 1<=i & i<=n holds tr(statement_1);
:: for (i=1;i++;i<=n){statement_1;statement_2;...;if (statement_3)break;}
:: .......> (ex j being Integer st 1<=j & j<=n &
:: (for i being Integer st 1<=i & i<j holds
:: tr(statement_1 for i)& tr(statement_2 for i)&...
:: & not (statement_3 for i))&
:: &tr(statement_1 for j)& tr(statement_2 for j)&...
:: &statement_3 for j)
:: or
:: (for i being Integer st 1<=i & i<=n holds
:: tr(statement_1 for i)& tr(statement_2 for i)&...
:: & not (statement_3 for i));
:: ***If "break" is expected in the above "for statement",
:: then "or" part can be deleted.
::------
:: arrays correspondence:
:: int a[n+1] .....> ex a being FinSequence of INT st len a=n & ...;
:: float x[n+1] .....> ex x being FinSequence of REAL st len x=n & ...;
:: Declaration of variables corresponds to existential statement.
::------
:: various correctness problem:
:: 1. mathematical algorithm .....> a function is well defined in Mizar
:: 2. semantic correctness .....> by theorems connecting it with
:: other mathematical or computational concepts in Mizar
:: 3. area check of variable of array .....> by a theorem checking
:: the area, in Mizar
:: 4. Is the translation to logic formula correct?
:: ......> by other methods outside of Mizar
:: 5. overflow problem .....> by other theorems, maybe in Mizar
:: 6. error about float .....> avoid "=" sign in if clause,
:: or corresponding float to other types not Real
:: 7. translation of usual programs to non overwriting programs
:: ......> by other methods outside of Mizar
::------
:: other comments:
:: A concept of non overwriting is important, not only
:: because of proving correctness, but because of debugging and
:: safety of data.
:: As memory is now cheap enough, it is wise to save all history of
:: variables in a program.
::-------------------------
::-------------------------
theorem Th1:
for n,m,k being 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 Th2:
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;
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 Th3:
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;
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 Th4:
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;
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 Th5:
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;
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 Th6:
for m,n being Element of NAT st m>0 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;
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 being Nat st P[k];
ex k being Nat st P[k] & for j being Nat st P[j] holds k<=j from NAT_1:
sch 5(A4);
then consider k being Nat such that
A5: P[k] and
A6: for j being Nat st P[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 thesis by A5;
end;
theorem Th7:
for i being Integer,f being 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;
:: Overwrting program to divide n by m (n>=0&m>0),where division / used is
:: special, because it is achieved by shifting a word.
:: int idiv1_prg(int n,int m){
:: int sm,sn,pn,i,j;
:: if(n<m){return 0;}
:: sm=m;
:: for (i=1;i<=n;i++){sm=sm*2; if (sm >n)break;}
:: pn=0;sn=n;sm=sm/2;
:: for (j=1;j<=i;j++){
:: if(sn>=sm){sn=sn-sm;sm=sm/2;pn=pn*2+1;} else {sm=sm/2;pn=pn*2;}
:: }
:: return pn;
:: }
:: Non overwrting program same as above, assuming n>=0 & m>0
:: int idiv1_prg(int n,int m){
:: int sm[n+1+1],sn[n+1+1],pn[n+1+1],i,j;
:: if (n<m){return 0;}
:: sm[1]=m;
:: for (i=1;i<=n;i++){
:: sm[i+1]=sm[i]*2;
:: if(sm[i+1]>n){break;}
:: }
:: pn[i+1]=0;sn[i+1]=n;
:: for (j=1;j<=i;j++){
:: if(sn[i+1-(j-1)]>=sm[i+1-j]){sn[i+1-j]=sn[i+1-(j-1)]-sm[i+1-j];
:: pn[i+1-j]=pn[i+1-(j-1)]*2+1;}
:: else {sn[i+1-j]=sn[i+1-(j-1)]; pn[i+1-j]=pn[i+1-(j-1)]*2;}
:: }
:: return pn[1];
:: }
definition
let n,m be Integer;
assume that
A1: n>=0 and
A2: m>0;
func idiv1_prg(n,m) -> Integer means
:Def1:
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
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 being FinSequence st len ppn=n2+1 & for k2 being Nat st k2
in dom ppn holds ppn.k2= F3(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 object;
assume y in rng ppn;
then consider x being 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 being FinSequence st len ssm=n2+1 & for k2 being Nat st k2
in dom ssm holds ssm.k2=F1(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 object;
assume y in rng ssm;
then consider x being 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 being FinSequence st len ssn=n2+1 & for k2 being Nat st k2
in dom ssn holds ssn.k2=F(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 object;
assume y in rng ssn;
then consider x being 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 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
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 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;
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,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 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;
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 being 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 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 );
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
per cases;
suppose
n<m;
hence thesis by A111,A113;
end;
suppose
A115: n>=m;
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 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 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
assume
A133: i2<i1;
A134: for k being 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 being 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 being 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 being 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 being 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 being 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 being 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 being Nat holds P2[jj] from NAT_1:sch 2(A173,A166);
A175: for jj being 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 being 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 being Nat holds P3[jj] from NAT_1:sch 2(A197,A178);
A199: for kk being 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 being Nat holds P4[jj] from NAT_1:sch 2(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;
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;
:: The following theorem is about array index area checking.
:: Each index of an array appeared in the program is checked
:: at the place just in front of the place the array is used,
:: if it remains in the defined area of array.
theorem
for n,m being Integer st n>=0 holds for sm,sn,pn being FinSequence of
INT,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;
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 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;
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;
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;
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 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;
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 Th9:
for n,m being 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 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;
end;
suppose
A6: n>=m;
deffunc F3(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= F3(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 object;
assume y in rng ppn;
then consider x being 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 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 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 being FinSequence st len ssn=n2+1 & for k2 being Nat st k2
in dom ssn holds ssn.k2=F(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 object;
assume y in rng ssn;
then consider x being 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 being FinSequence st len ssm=n2+1 & for k2 being Nat st k2
in dom ssm holds ssm.k2=F1(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 object;
assume y in rng ssm;
then consider x being 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 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;
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,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 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;
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 being 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 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;
end;
end;
hence thesis by A1,Def1;
end;
theorem Th10:
for n,m being 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 Th11:
for n,m being Integer,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,n2,m2 be Element of NAT;
thus m=0 & n2=n & m2=m implies n div m=0 & n2 div m2=0;
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;
::
:: int idiv_prg(int n,int m){
:: int i;
:: if (m==0){return 0;}
:: if (n>=0 && m>0){return idiv1_prg(n,m);}
:: if (n>=0 && m<0){
:: i= idiv1_prg(n,-m);
:: if((-m)*i==n){return -i;} else{return -i-1;}
:: }
:: if (n<0 && m>0){
:: i= idiv1_prg(-n,m);
:: if(m*i== -n){return -i;} else{return -i-1;}
:: }
:: return idiv1_prg(-n,-m);
:: }
::
:: One time writing program
:: Same as above.
definition
let n,m be Integer;
func idiv_prg(n,m) -> Integer means
:Def2:
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 & 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 being 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 being 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 being Integer st P[i] by A3,A7,A8;
end;
end;
hence ex i being Integer st P[i];
end;
end;
hence ex i being 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 being 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 being 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 being Integer st P[i] by A9,A12,A15,A16;
end;
end;
hence ex i being Integer st P[i];
end;
end;
hence ex i being Integer st P[i];
end;
end;
hence thesis;
end;
end;
uniqueness;
end;
theorem
for n,m being 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;
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;