:: PRGCOR_1 semantic presentation

theorem Th1: :: PRGCOR_1:1
for b1, b2, b3 being Nat holds (b1 + b3) -' (b2 + b3) = b1 -' b2
proof end;

theorem Th2: :: PRGCOR_1:2
for b1, b2 being Nat st b2 > 0 & b1 mod (2 * b2) >= b2 holds
( (b1 mod (2 * b2)) - b2 = b1 mod b2 & (b1 mod b2) + b2 = b1 mod (2 * b2) )
proof end;

theorem Th3: :: PRGCOR_1:3
for b1, b2 being Nat st b2 > 0 & b1 mod (2 * b2) >= b2 holds
b1 div b2 = ((b1 div (2 * b2)) * 2) + 1
proof end;

theorem Th4: :: PRGCOR_1:4
for b1, b2 being Nat st b2 > 0 & b1 mod (2 * b2) < b2 holds
b1 mod (2 * b2) = b1 mod b2
proof end;

theorem Th5: :: PRGCOR_1:5
for b1, b2 being Nat st b2 > 0 & b1 mod (2 * b2) < b2 holds
b1 div b2 = (b1 div (2 * b2)) * 2
proof end;

registration
let c1 be set ;
let c2 be PartFunc of c1, INT ;
let c3 be set ;
cluster a2 . a3 -> integer ;
coherence
c2 . c3 is integer
proof end;
end;

theorem Th6: :: PRGCOR_1:6
for b1, b2 being Nat st b1 > 0 holds
ex b3 being Nat st
( ( for b4 being Nat st b4 < b3 holds
b1 * (2 |^ b4) <= b2 ) & b1 * (2 |^ b3) > b2 )
proof end;

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

definition
let c1, c2 be Integer;
assume E8: ( c1 >= 0 & c2 > 0 ) ;
func idiv1_prg c1,c2 -> Integer means :Def1: :: PRGCOR_1:def 1
ex b1, b2, b3 being FinSequence of INT st
( len b1 = a1 + 1 & len b2 = a1 + 1 & len b3 = a1 + 1 & ( a1 < a2 implies a3 = 0 ) & ( not a1 < a2 implies ( b1 . 1 = a2 & ex b4 being Integer st
( 1 <= b4 & b4 <= a1 & ( for b5 being Integer st 1 <= b5 & b5 < b4 holds
( b1 . (b5 + 1) = (b1 . b5) * 2 & not b1 . (b5 + 1) > a1 ) ) & b1 . (b4 + 1) = (b1 . b4) * 2 & b1 . (b4 + 1) > a1 & b3 . (b4 + 1) = 0 & b2 . (b4 + 1) = a1 & ( for b5 being Integer st 1 <= b5 & b5 <= b4 holds
( ( b2 . ((b4 + 1) - (b5 - 1)) >= b1 . ((b4 + 1) - b5) implies ( b2 . ((b4 + 1) - b5) = (b2 . ((b4 + 1) - (b5 - 1))) - (b1 . ((b4 + 1) - b5)) & b3 . ((b4 + 1) - b5) = ((b3 . ((b4 + 1) - (b5 - 1))) * 2) + 1 ) ) & ( not b2 . ((b4 + 1) - (b5 - 1)) >= b1 . ((b4 + 1) - b5) implies ( b2 . ((b4 + 1) - b5) = b2 . ((b4 + 1) - (b5 - 1)) & b3 . ((b4 + 1) - b5) = (b3 . ((b4 + 1) - (b5 - 1))) * 2 ) ) ) ) & a3 = b3 . 1 ) ) ) );
existence
ex b1 being Integerex b2, b3, b4 being FinSequence of INT st
( len b2 = c1 + 1 & len b3 = c1 + 1 & len b4 = c1 + 1 & ( c1 < c2 implies b1 = 0 ) & ( not c1 < c2 implies ( b2 . 1 = c2 & ex b5 being Integer st
( 1 <= b5 & b5 <= c1 & ( for b6 being Integer st 1 <= b6 & b6 < b5 holds
( b2 . (b6 + 1) = (b2 . b6) * 2 & not b2 . (b6 + 1) > c1 ) ) & b2 . (b5 + 1) = (b2 . b5) * 2 & b2 . (b5 + 1) > c1 & b4 . (b5 + 1) = 0 & b3 . (b5 + 1) = c1 & ( for b6 being Integer st 1 <= b6 & b6 <= b5 holds
( ( b3 . ((b5 + 1) - (b6 - 1)) >= b2 . ((b5 + 1) - b6) implies ( b3 . ((b5 + 1) - b6) = (b3 . ((b5 + 1) - (b6 - 1))) - (b2 . ((b5 + 1) - b6)) & b4 . ((b5 + 1) - b6) = ((b4 . ((b5 + 1) - (b6 - 1))) * 2) + 1 ) ) & ( not b3 . ((b5 + 1) - (b6 - 1)) >= b2 . ((b5 + 1) - b6) implies ( b3 . ((b5 + 1) - b6) = b3 . ((b5 + 1) - (b6 - 1)) & b4 . ((b5 + 1) - b6) = (b4 . ((b5 + 1) - (b6 - 1))) * 2 ) ) ) ) & b1 = b4 . 1 ) ) ) )
proof end;
uniqueness
for b1, b2 being Integer st ex b3, b4, b5 being FinSequence of INT st
( len b3 = c1 + 1 & len b4 = c1 + 1 & len b5 = c1 + 1 & ( c1 < c2 implies b1 = 0 ) & ( not c1 < c2 implies ( b3 . 1 = c2 & ex b6 being Integer st
( 1 <= b6 & b6 <= c1 & ( for b7 being Integer st 1 <= b7 & b7 < b6 holds
( b3 . (b7 + 1) = (b3 . b7) * 2 & not b3 . (b7 + 1) > c1 ) ) & b3 . (b6 + 1) = (b3 . b6) * 2 & b3 . (b6 + 1) > c1 & b5 . (b6 + 1) = 0 & b4 . (b6 + 1) = c1 & ( for b7 being Integer st 1 <= b7 & b7 <= b6 holds
( ( b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = (b4 . ((b6 + 1) - (b7 - 1))) - (b3 . ((b6 + 1) - b7)) & b5 . ((b6 + 1) - b7) = ((b5 . ((b6 + 1) - (b7 - 1))) * 2) + 1 ) ) & ( not b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = b4 . ((b6 + 1) - (b7 - 1)) & b5 . ((b6 + 1) - b7) = (b5 . ((b6 + 1) - (b7 - 1))) * 2 ) ) ) ) & b1 = b5 . 1 ) ) ) ) & ex b3, b4, b5 being FinSequence of INT st
( len b3 = c1 + 1 & len b4 = c1 + 1 & len b5 = c1 + 1 & ( c1 < c2 implies b2 = 0 ) & ( not c1 < c2 implies ( b3 . 1 = c2 & ex b6 being Integer st
( 1 <= b6 & b6 <= c1 & ( for b7 being Integer st 1 <= b7 & b7 < b6 holds
( b3 . (b7 + 1) = (b3 . b7) * 2 & not b3 . (b7 + 1) > c1 ) ) & b3 . (b6 + 1) = (b3 . b6) * 2 & b3 . (b6 + 1) > c1 & b5 . (b6 + 1) = 0 & b4 . (b6 + 1) = c1 & ( for b7 being Integer st 1 <= b7 & b7 <= b6 holds
( ( b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = (b4 . ((b6 + 1) - (b7 - 1))) - (b3 . ((b6 + 1) - b7)) & b5 . ((b6 + 1) - b7) = ((b5 . ((b6 + 1) - (b7 - 1))) * 2) + 1 ) ) & ( not b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = b4 . ((b6 + 1) - (b7 - 1)) & b5 . ((b6 + 1) - b7) = (b5 . ((b6 + 1) - (b7 - 1))) * 2 ) ) ) ) & b2 = b5 . 1 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines idiv1_prg PRGCOR_1:def 1 :
for b1, b2 being Integer st b1 >= 0 & b2 > 0 holds
for b3 being Integer holds
( b3 = idiv1_prg b1,b2 iff ex b4, b5, b6 being FinSequence of INT st
( len b4 = b1 + 1 & len b5 = b1 + 1 & len b6 = b1 + 1 & ( b1 < b2 implies b3 = 0 ) & ( not b1 < b2 implies ( b4 . 1 = b2 & ex b7 being Integer st
( 1 <= b7 & b7 <= b1 & ( for b8 being Integer st 1 <= b8 & b8 < b7 holds
( b4 . (b8 + 1) = (b4 . b8) * 2 & not b4 . (b8 + 1) > b1 ) ) & b4 . (b7 + 1) = (b4 . b7) * 2 & b4 . (b7 + 1) > b1 & b6 . (b7 + 1) = 0 & b5 . (b7 + 1) = b1 & ( for b8 being Integer st 1 <= b8 & b8 <= b7 holds
( ( b5 . ((b7 + 1) - (b8 - 1)) >= b4 . ((b7 + 1) - b8) implies ( b5 . ((b7 + 1) - b8) = (b5 . ((b7 + 1) - (b8 - 1))) - (b4 . ((b7 + 1) - b8)) & b6 . ((b7 + 1) - b8) = ((b6 . ((b7 + 1) - (b8 - 1))) * 2) + 1 ) ) & ( not b5 . ((b7 + 1) - (b8 - 1)) >= b4 . ((b7 + 1) - b8) implies ( b5 . ((b7 + 1) - b8) = b5 . ((b7 + 1) - (b8 - 1)) & b6 . ((b7 + 1) - b8) = (b6 . ((b7 + 1) - (b8 - 1))) * 2 ) ) ) ) & b3 = b6 . 1 ) ) ) ) );

theorem Th8: :: PRGCOR_1:8
for b1, b2 being Integer st b1 >= 0 & b2 > 0 holds
for b3, b4, b5 being FinSequence of INT
for b6 being Integer st len b3 = b1 + 1 & len b4 = b1 + 1 & len b5 = b1 + 1 & ( not b1 < b2 implies ( b3 . 1 = b2 & 1 <= b6 & b6 <= b1 & ( for b7 being Integer st 1 <= b7 & b7 < b6 holds
( b3 . (b7 + 1) = (b3 . b7) * 2 & not b3 . (b7 + 1) > b1 ) ) & b3 . (b6 + 1) = (b3 . b6) * 2 & b3 . (b6 + 1) > b1 & b5 . (b6 + 1) = 0 & b4 . (b6 + 1) = b1 & ( for b7 being Integer st 1 <= b7 & b7 <= b6 holds
( ( b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = (b4 . ((b6 + 1) - (b7 - 1))) - (b3 . ((b6 + 1) - b7)) & b5 . ((b6 + 1) - b7) = ((b5 . ((b6 + 1) - (b7 - 1))) * 2) + 1 ) ) & ( not b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( b4 . ((b6 + 1) - b7) = b4 . ((b6 + 1) - (b7 - 1)) & b5 . ((b6 + 1) - b7) = (b5 . ((b6 + 1) - (b7 - 1))) * 2 ) ) ) ) & idiv1_prg b1,b2 = b5 . 1 ) ) holds
( len b3 = b1 + 1 & len b4 = b1 + 1 & len b5 = b1 + 1 & ( b1 < b2 implies idiv1_prg b1,b2 = 0 ) & ( not b1 < b2 implies ( 1 in dom b3 & b3 . 1 = b2 & 1 <= b6 & b6 <= b1 & ( for b7 being Integer st 1 <= b7 & b7 < b6 holds
( b7 + 1 in dom b3 & b7 in dom b3 & b3 . (b7 + 1) = (b3 . b7) * 2 & not b3 . (b7 + 1) > b1 ) ) & b6 + 1 in dom b3 & b6 in dom b3 & b3 . (b6 + 1) = (b3 . b6) * 2 & b3 . (b6 + 1) > b1 & b6 + 1 in dom b5 & b5 . (b6 + 1) = 0 & b6 + 1 in dom b4 & b4 . (b6 + 1) = b1 & ( for b7 being Integer st 1 <= b7 & b7 <= b6 holds
( (b6 + 1) - (b7 - 1) in dom b4 & (b6 + 1) - b7 in dom b3 & ( b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( (b6 + 1) - b7 in dom b4 & (b6 + 1) - b7 in dom b3 & b4 . ((b6 + 1) - b7) = (b4 . ((b6 + 1) - (b7 - 1))) - (b3 . ((b6 + 1) - b7)) & (b6 + 1) - b7 in dom b5 & (b6 + 1) - (b7 - 1) in dom b5 & b5 . ((b6 + 1) - b7) = ((b5 . ((b6 + 1) - (b7 - 1))) * 2) + 1 ) ) & ( not b4 . ((b6 + 1) - (b7 - 1)) >= b3 . ((b6 + 1) - b7) implies ( (b6 + 1) - b7 in dom b4 & (b6 + 1) - (b7 - 1) in dom b4 & b4 . ((b6 + 1) - b7) = b4 . ((b6 + 1) - (b7 - 1)) & (b6 + 1) - b7 in dom b5 & (b6 + 1) - (b7 - 1) in dom b5 & b5 . ((b6 + 1) - b7) = (b5 . ((b6 + 1) - (b7 - 1))) * 2 ) ) ) ) & 1 in dom b5 & idiv1_prg b1,b2 = b5 . 1 ) ) )
proof end;

theorem Th9: :: PRGCOR_1:9
for b1, b2 being Nat st b2 > 0 holds
idiv1_prg b1,b2 = b1 div b2
proof end;

theorem Th10: :: PRGCOR_1:10
for b1, b2 being Integer st b1 >= 0 & b2 > 0 holds
idiv1_prg b1,b2 = b1 div b2
proof end;

theorem Th11: :: PRGCOR_1:11
for b1, b2 being Integer
for b3, b4 being Nat holds
( ( b2 = 0 & b3 = b1 & b4 = b2 implies ( b1 div b2 = 0 & b3 div b4 = 0 ) ) & ( b1 >= 0 & b2 > 0 & b3 = b1 & b4 = b2 implies b1 div b2 = b3 div b4 ) & ( b1 >= 0 & b2 < 0 & b3 = b1 & b4 = - b2 implies ( ( b4 * (b3 div b4) = b3 implies b1 div b2 = - (b3 div b4) ) & ( b4 * (b3 div b4) <> b3 implies b1 div b2 = (- (b3 div b4)) - 1 ) ) ) & ( b1 < 0 & b2 > 0 & b3 = - b1 & b4 = b2 implies ( ( b4 * (b3 div b4) = b3 implies b1 div b2 = - (b3 div b4) ) & ( b4 * (b3 div b4) <> b3 implies b1 div b2 = (- (b3 div b4)) - 1 ) ) ) & ( b1 < 0 & b2 < 0 & b3 = - b1 & b4 = - b2 implies b1 div b2 = b3 div b4 ) )
proof end;

definition
let c1, c2 be Integer;
func idiv_prg c1,c2 -> Integer means :Def2: :: PRGCOR_1:def 2
ex b1 being Integer st
( ( a2 = 0 implies a3 = 0 ) & ( not a2 = 0 implies ( ( a1 >= 0 & a2 > 0 implies a3 = idiv1_prg a1,a2 ) & ( ( not a1 >= 0 or not a2 > 0 ) implies ( ( a1 >= 0 & a2 < 0 implies ( b1 = idiv1_prg a1,(- a2) & ( (- a2) * b1 = a1 implies a3 = - b1 ) & ( (- a2) * b1 <> a1 implies a3 = (- b1) - 1 ) ) ) & ( ( not a1 >= 0 or not a2 < 0 ) implies ( ( a1 < 0 & a2 > 0 implies ( b1 = idiv1_prg (- a1),a2 & ( a2 * b1 = - a1 implies a3 = - b1 ) & ( a2 * b1 <> - a1 implies a3 = (- b1) - 1 ) ) ) & ( ( not a1 < 0 or not a2 > 0 ) implies a3 = idiv1_prg (- a1),(- a2) ) ) ) ) ) ) ) );
existence
ex b1, b2 being Integer st
( ( c2 = 0 implies b1 = 0 ) & ( not c2 = 0 implies ( ( c1 >= 0 & c2 > 0 implies b1 = idiv1_prg c1,c2 ) & ( ( not c1 >= 0 or not c2 > 0 ) implies ( ( c1 >= 0 & c2 < 0 implies ( b2 = idiv1_prg c1,(- c2) & ( (- c2) * b2 = c1 implies b1 = - b2 ) & ( (- c2) * b2 <> c1 implies b1 = (- b2) - 1 ) ) ) & ( ( not c1 >= 0 or not c2 < 0 ) implies ( ( c1 < 0 & c2 > 0 implies ( b2 = idiv1_prg (- c1),c2 & ( c2 * b2 = - c1 implies b1 = - b2 ) & ( c2 * b2 <> - c1 implies b1 = (- b2) - 1 ) ) ) & ( ( not c1 < 0 or not c2 > 0 ) implies b1 = idiv1_prg (- c1),(- c2) ) ) ) ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Integer st ex b3 being Integer st
( ( c2 = 0 implies b1 = 0 ) & ( not c2 = 0 implies ( ( c1 >= 0 & c2 > 0 implies b1 = idiv1_prg c1,c2 ) & ( ( not c1 >= 0 or not c2 > 0 ) implies ( ( c1 >= 0 & c2 < 0 implies ( b3 = idiv1_prg c1,(- c2) & ( (- c2) * b3 = c1 implies b1 = - b3 ) & ( (- c2) * b3 <> c1 implies b1 = (- b3) - 1 ) ) ) & ( ( not c1 >= 0 or not c2 < 0 ) implies ( ( c1 < 0 & c2 > 0 implies ( b3 = idiv1_prg (- c1),c2 & ( c2 * b3 = - c1 implies b1 = - b3 ) & ( c2 * b3 <> - c1 implies b1 = (- b3) - 1 ) ) ) & ( ( not c1 < 0 or not c2 > 0 ) implies b1 = idiv1_prg (- c1),(- c2) ) ) ) ) ) ) ) ) & ex b3 being Integer st
( ( c2 = 0 implies b2 = 0 ) & ( not c2 = 0 implies ( ( c1 >= 0 & c2 > 0 implies b2 = idiv1_prg c1,c2 ) & ( ( not c1 >= 0 or not c2 > 0 ) implies ( ( c1 >= 0 & c2 < 0 implies ( b3 = idiv1_prg c1,(- c2) & ( (- c2) * b3 = c1 implies b2 = - b3 ) & ( (- c2) * b3 <> c1 implies b2 = (- b3) - 1 ) ) ) & ( ( not c1 >= 0 or not c2 < 0 ) implies ( ( c1 < 0 & c2 > 0 implies ( b3 = idiv1_prg (- c1),c2 & ( c2 * b3 = - c1 implies b2 = - b3 ) & ( c2 * b3 <> - c1 implies b2 = (- b3) - 1 ) ) ) & ( ( not c1 < 0 or not c2 > 0 ) implies b2 = idiv1_prg (- c1),(- c2) ) ) ) ) ) ) ) ) holds
b1 = b2 ;
end;

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

theorem Th12: :: PRGCOR_1:12
for b1, b2 being Integer holds idiv_prg b1,b2 = b1 div b2
proof end;