:: Correctness of Non Overwriting Programs. {P}art {I}
:: by Yatsuka Nakamura
::
:: Received December 5, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

theorem Th1: :: PRGCOR_1:1
for n, m, k being Element of NAT holds (n + k) -' (m + k) = n -' m
proof end;

theorem Th2: :: PRGCOR_1:2
for n, k being Element of NAT st k > 0 & n mod (2 * k) >= k holds
( (n mod (2 * k)) - k = n mod k & (n mod k) + k = n mod (2 * k) )
proof end;

theorem Th3: :: PRGCOR_1:3
for n, k being Element of NAT st k > 0 & n mod (2 * k) >= k holds
n div k = ((n div (2 * k)) * 2) + 1
proof end;

theorem Th4: :: PRGCOR_1:4
for n, k being Element of NAT st k > 0 & n mod (2 * k) < k holds
n mod (2 * k) = n mod k
proof end;

theorem Th5: :: PRGCOR_1:5
for n, k being Element of NAT st k > 0 & n mod (2 * k) < k holds
n div k = (n div (2 * k)) * 2
proof end;

registration
let C be set ;
let f be PartFunc of C,INT;
let x be set ;
cluster f . x -> integer ;
coherence
f . x is integer
proof end;
end;

theorem Th6: :: PRGCOR_1:6
for m, n being Element of NAT st m > 0 holds
ex i being Element of NAT st
( ( for k2 being Element of NAT st k2 < i holds
m * (2 |^ k2) <= n ) & m * (2 |^ i) > n )
proof end;

theorem Th7: :: PRGCOR_1:7
for i being Integer
for f being FinSequence st 1 <= i & i <= len f holds
i in dom f
proof end;

definition
let n, m be Integer;
assume that
A1: n >= 0 and
A2: m > 0 ;
func idiv1_prg (n,m) -> Integer means :Def1: :: PRGCOR_1:def 1
 ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies it = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & it = pn . 1 ) ) ) );
existence
ex b1 being Integer ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) )
proof end;
uniqueness
for b1, b2 being Integer st ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) ) & ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b2 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b2 = pn . 1 ) ) ) ) holds
b1 = b2
proof end;
end;

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

theorem :: PRGCOR_1:8
for n, m being Integer st n >= 0 holds
for sm, sn, pn being FinSequence of INT
for i being Integer st len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( not n < m implies ( sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & idiv1_prg (n,m) = pn . 1 ) ) holds
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies idiv1_prg (n,m) = 0 ) & ( not n < m implies ( 1 in dom sm & sm . 1 = m & 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( k + 1 in dom sm & k in dom sm & sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & i + 1 in dom sm & i in dom sm & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & i + 1 in dom pn & pn . (i + 1) = 0 & i + 1 in dom sn & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( (i + 1) - (j - 1) in dom sn & (i + 1) - j in dom sm & ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - j in dom sm & sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( (i + 1) - j in dom sn & (i + 1) - (j - 1) in dom sn & sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & (i + 1) - j in dom pn & (i + 1) - (j - 1) in dom pn & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & 1 in dom pn & idiv1_prg (n,m) = pn . 1 ) ) )
proof end;

theorem Th9: :: PRGCOR_1:9
for n, m being Element of NAT st m > 0 holds
idiv1_prg (n,m) = n div m
proof end;

theorem Th10: :: PRGCOR_1:10
for n, m being Integer st n >= 0 & m > 0 holds
idiv1_prg (n,m) = n div m
proof end;

theorem Th11: :: PRGCOR_1:11
for n, m being Integer
for n2, m2 being Element of NAT holds
( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )
proof end;

definition
let n, m be Integer;
func idiv_prg (n,m) -> Integer means :Def2: :: PRGCOR_1:def 2
 ex i being Integer st
( ( m = 0 implies it = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies it = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies it = - i ) & ( (- m) * i <> n implies it = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies it = - i ) & ( m * i <> - n implies it = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies it = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) );
existence
ex b1, i being Integer st
( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Integer st ex i being Integer st
( ( m = 0 implies b1 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b1 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b1 = - i ) & ( (- m) * i <> n implies b1 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b1 = - i ) & ( m * i <> - n implies b1 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b1 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) & ex i being Integer st
( ( m = 0 implies b2 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b2 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b2 = - i ) & ( (- m) * i <> n implies b2 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b2 = - i ) & ( m * i <> - n implies b2 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b2 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines idiv_prg PRGCOR_1:def 2 :
for n, m, b3 being Integer holds
( b3 = idiv_prg (n,m) iff ex i being Integer st
( ( m = 0 implies b3 = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b3 = idiv1_prg (n,m) ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg (n,(- m)) & ( (- m) * i = n implies b3 = - i ) & ( (- m) * i <> n implies b3 = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg ((- n),m) & ( m * i = - n implies b3 = - i ) & ( m * i <> - n implies b3 = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b3 = idiv1_prg ((- n),(- m)) ) ) ) ) ) ) ) ) );

theorem :: PRGCOR_1:12
for n, m being Integer holds idiv_prg (n,m) = n div m
proof end;