:: RADIX_5 semantic presentation

theorem Th1: :: RADIX_5:1
for b1 being Nat st b1 >= 2 holds
(Radix b1) - 1 in b1 -SD
proof end;

theorem Th2: :: RADIX_5:2
for b1, b2 being Nat st b1 > 1 & b1 in Seg b2 holds
b1 -' 1 in Seg b2
proof end;

theorem Th3: :: RADIX_5:3
for b1 being Nat st 2 <= b1 holds
4 <= Radix b1
proof end;

theorem Th4: :: RADIX_5:4
for b1 being Nat
for b2 being Tuple of 1,(b1 -SD ) holds SDDec b2 = DigA b2,1
proof end;

theorem Th5: :: RADIX_5:5
for b1, b2, b3 being Nat st b1 in Seg b3 holds
DigA (DecSD 0,b3,b2),b1 = 0
proof end;

theorem Th6: :: RADIX_5:6
for b1, b2 being Nat st b1 >= 1 holds
SDDec (DecSD 0,b1,b2) = 0
proof end;

theorem Th7: :: RADIX_5:7
for b1, b2 being Nat st 1 in Seg b2 & b1 >= 2 holds
DigA (DecSD 1,b2,b1),1 = 1
proof end;

theorem Th8: :: RADIX_5:8
for b1, b2, b3 being Nat st b1 in Seg b3 & b1 > 1 & b2 >= 2 holds
DigA (DecSD 1,b3,b2),b1 = 0
proof end;

theorem Th9: :: RADIX_5:9
for b1, b2 being Nat st b1 >= 1 & b2 >= 2 holds
SDDec (DecSD 1,b1,b2) = 1
proof end;

theorem Th10: :: RADIX_5:10
for b1 being Nat st b1 >= 2 holds
SD_Add_Carry (Radix b1) = 1
proof end;

theorem Th11: :: RADIX_5:11
for b1 being Nat st b1 >= 2 holds
SD_Add_Data (Radix b1),b1 = 0
proof end;

Lemma10: for b1 being Nat st 2 <= b1 holds
SD_Add_Carry ((Radix b1) - 1) = 1
proof end;

Lemma11: for b1, b2, b3 being Nat st b2 >= 2 & b3 in Seg b1 holds
SD_Add_Carry (DigA (DecSD 1,b1,b2),b3) = 0
proof end;

theorem Th12: :: RADIX_5:12
for b1 being Nat st b1 >= 1 holds
for b2 being Nat
for b3, b4 being Tuple of b1,(b2 -SD ) st ( for b5 being Nat st b5 in Seg b1 holds
DigA b3,b5 = DigA b4,b5 ) holds
SDDec b3 = SDDec b4
proof end;

theorem Th13: :: RADIX_5:13
for b1 being Nat st b1 >= 1 holds
for b2 being Nat
for b3, b4 being Tuple of b1,(b2 -SD ) st ( for b5 being Nat st b5 in Seg b1 holds
DigA b3,b5 >= DigA b4,b5 ) holds
SDDec b3 >= SDDec b4
proof end;

theorem Th14: :: RADIX_5:14
for b1 being Nat st b1 >= 1 holds
for b2 being Nat st b2 >= 2 holds
for b3, b4, b5, b6 being Tuple of b1,(b2 -SD ) st ( for b7 being Nat holds
( not b7 in Seg b1 or ( DigA b3,b7 = DigA b5,b7 & DigA b4,b7 = DigA b6,b7 ) or ( DigA b4,b7 = DigA b5,b7 & DigA b3,b7 = DigA b6,b7 ) ) ) holds
(SDDec b5) + (SDDec b6) = (SDDec b3) + (SDDec b4)
proof end;

theorem Th15: :: RADIX_5:15
for b1, b2 being Nat st b1 >= 1 & b2 >= 2 holds
for b3, b4, b5 being Tuple of b1,(b2 -SD ) st ( for b6 being Nat holds
( not b6 in Seg b1 or ( DigA b3,b6 = DigA b5,b6 & DigA b4,b6 = 0 ) or ( DigA b4,b6 = DigA b5,b6 & DigA b3,b6 = 0 ) ) ) holds
(SDDec b5) + (SDDec (DecSD 0,b1,b2)) = (SDDec b3) + (SDDec b4)
proof end;

definition
let c1, c2, c3 be Nat;
assume E14: c3 >= 2 ;
func SDMinDigit c2,c3,c1 -> Element of a3 -SD equals :Def1: :: RADIX_5:def 1
(- (Radix a3)) + 1 if ( 1 <= a1 & a1 < a2 )
otherwise 0;
coherence
( ( 1 <= c1 & c1 < c2 implies (- (Radix c3)) + 1 is Element of c3 -SD ) & ( ( not 1 <= c1 or not c1 < c2 ) implies 0 is Element of c3 -SD ) )
proof end;
consistency
for b1 being Element of c3 -SD holds verum ;
end;

:: deftheorem Def1 defines SDMinDigit RADIX_5:def 1 :
for b1, b2, b3 being Nat st b3 >= 2 holds
( ( 1 <= b1 & b1 < b2 implies SDMinDigit b2,b3,b1 = (- (Radix b3)) + 1 ) & ( ( not 1 <= b1 or not b1 < b2 ) implies SDMinDigit b2,b3,b1 = 0 ) );

definition
let c1, c2, c3 be Nat;
func SDMin c1,c2,c3 -> Tuple of a1,(a3 -SD ) means :Def2: :: RADIX_5:def 2
for b1 being Nat st b1 in Seg a1 holds
DigA a4,b1 = SDMinDigit a2,a3,b1;
existence
ex b1 being Tuple of c1,(c3 -SD ) st
for b2 being Nat st b2 in Seg c1 holds
DigA b1,b2 = SDMinDigit c2,c3,b2
proof end;
uniqueness
for b1, b2 being Tuple of c1,(c3 -SD ) st ( for b3 being Nat st b3 in Seg c1 holds
DigA b1,b3 = SDMinDigit c2,c3,b3 ) & ( for b3 being Nat st b3 in Seg c1 holds
DigA b2,b3 = SDMinDigit c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SDMin RADIX_5:def 2 :
for b1, b2, b3 being Nat
for b4 being Tuple of b1,(b3 -SD ) holds
( b4 = SDMin b1,b2,b3 iff for b5 being Nat st b5 in Seg b1 holds
DigA b4,b5 = SDMinDigit b2,b3,b5 );

definition
let c1, c2, c3 be Nat;
assume E16: c3 >= 2 ;
func SDMaxDigit c2,c3,c1 -> Element of a3 -SD equals :Def3: :: RADIX_5:def 3
(Radix a3) - 1 if ( 1 <= a1 & a1 < a2 )
otherwise 0;
coherence
( ( 1 <= c1 & c1 < c2 implies (Radix c3) - 1 is Element of c3 -SD ) & ( ( not 1 <= c1 or not c1 < c2 ) implies 0 is Element of c3 -SD ) ) by E16, Th1, RADIX_1:16;
consistency
for b1 being Element of c3 -SD holds verum ;
end;

:: deftheorem Def3 defines SDMaxDigit RADIX_5:def 3 :
for b1, b2, b3 being Nat st b3 >= 2 holds
( ( 1 <= b1 & b1 < b2 implies SDMaxDigit b2,b3,b1 = (Radix b3) - 1 ) & ( ( not 1 <= b1 or not b1 < b2 ) implies SDMaxDigit b2,b3,b1 = 0 ) );

definition
let c1, c2, c3 be Nat;
func SDMax c1,c2,c3 -> Tuple of a1,(a3 -SD ) means :Def4: :: RADIX_5:def 4
for b1 being Nat st b1 in Seg a1 holds
DigA a4,b1 = SDMaxDigit a2,a3,b1;
existence
ex b1 being Tuple of c1,(c3 -SD ) st
for b2 being Nat st b2 in Seg c1 holds
DigA b1,b2 = SDMaxDigit c2,c3,b2
proof end;
uniqueness
for b1, b2 being Tuple of c1,(c3 -SD ) st ( for b3 being Nat st b3 in Seg c1 holds
DigA b1,b3 = SDMaxDigit c2,c3,b3 ) & ( for b3 being Nat st b3 in Seg c1 holds
DigA b2,b3 = SDMaxDigit c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines SDMax RADIX_5:def 4 :
for b1, b2, b3 being Nat
for b4 being Tuple of b1,(b3 -SD ) holds
( b4 = SDMax b1,b2,b3 iff for b5 being Nat st b5 in Seg b1 holds
DigA b4,b5 = SDMaxDigit b2,b3,b5 );

definition
let c1, c2, c3 be Nat;
assume E18: c3 >= 2 ;
func FminDigit c2,c3,c1 -> Element of a3 -SD equals :Def5: :: RADIX_5:def 5
1 if a1 = a2
otherwise 0;
coherence
( ( c1 = c2 implies 1 is Element of c3 -SD ) & ( not c1 = c2 implies 0 is Element of c3 -SD ) )
proof end;
consistency
for b1 being Element of c3 -SD holds verum ;
end;

:: deftheorem Def5 defines FminDigit RADIX_5:def 5 :
for b1, b2, b3 being Nat st b3 >= 2 holds
( ( b1 = b2 implies FminDigit b2,b3,b1 = 1 ) & ( not b1 = b2 implies FminDigit b2,b3,b1 = 0 ) );

definition
let c1, c2, c3 be Nat;
func Fmin c1,c2,c3 -> Tuple of a1,(a3 -SD ) means :Def6: :: RADIX_5:def 6
for b1 being Nat st b1 in Seg a1 holds
DigA a4,b1 = FminDigit a2,a3,b1;
existence
ex b1 being Tuple of c1,(c3 -SD ) st
for b2 being Nat st b2 in Seg c1 holds
DigA b1,b2 = FminDigit c2,c3,b2
proof end;
uniqueness
for b1, b2 being Tuple of c1,(c3 -SD ) st ( for b3 being Nat st b3 in Seg c1 holds
DigA b1,b3 = FminDigit c2,c3,b3 ) & ( for b3 being Nat st b3 in Seg c1 holds
DigA b2,b3 = FminDigit c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Fmin RADIX_5:def 6 :
for b1, b2, b3 being Nat
for b4 being Tuple of b1,(b3 -SD ) holds
( b4 = Fmin b1,b2,b3 iff for b5 being Nat st b5 in Seg b1 holds
DigA b4,b5 = FminDigit b2,b3,b5 );

definition
let c1, c2, c3 be Nat;
assume E20: c3 >= 2 ;
func FmaxDigit c2,c3,c1 -> Element of a3 -SD equals :Def7: :: RADIX_5:def 7
(Radix a3) - 1 if a1 = a2
otherwise 0;
coherence
( ( c1 = c2 implies (Radix c3) - 1 is Element of c3 -SD ) & ( not c1 = c2 implies 0 is Element of c3 -SD ) ) by E20, Th1, RADIX_1:16;
consistency
for b1 being Element of c3 -SD holds verum ;
end;

:: deftheorem Def7 defines FmaxDigit RADIX_5:def 7 :
for b1, b2, b3 being Nat st b3 >= 2 holds
( ( b1 = b2 implies FmaxDigit b2,b3,b1 = (Radix b3) - 1 ) & ( not b1 = b2 implies FmaxDigit b2,b3,b1 = 0 ) );

definition
let c1, c2, c3 be Nat;
func Fmax c1,c2,c3 -> Tuple of a1,(a3 -SD ) means :Def8: :: RADIX_5:def 8
for b1 being Nat st b1 in Seg a1 holds
DigA a4,b1 = FmaxDigit a2,a3,b1;
existence
ex b1 being Tuple of c1,(c3 -SD ) st
for b2 being Nat st b2 in Seg c1 holds
DigA b1,b2 = FmaxDigit c2,c3,b2
proof end;
uniqueness
for b1, b2 being Tuple of c1,(c3 -SD ) st ( for b3 being Nat st b3 in Seg c1 holds
DigA b1,b3 = FmaxDigit c2,c3,b3 ) & ( for b3 being Nat st b3 in Seg c1 holds
DigA b2,b3 = FmaxDigit c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Fmax RADIX_5:def 8 :
for b1, b2, b3 being Nat
for b4 being Tuple of b1,(b3 -SD ) holds
( b4 = Fmax b1,b2,b3 iff for b5 being Nat st b5 in Seg b1 holds
DigA b4,b5 = FmaxDigit b2,b3,b5 );

theorem Th16: :: RADIX_5:16
for b1, b2, b3 being Nat st b1 >= 1 & b3 >= 2 & b2 in Seg b1 holds
for b4 being Nat st b4 in Seg b1 holds
(DigA (SDMax b1,b2,b3),b4) + (DigA (SDMin b1,b2,b3),b4) = 0
proof end;

theorem Th17: :: RADIX_5:17
for b1 being Nat st b1 >= 1 holds
for b2, b3 being Nat st b2 in Seg b1 & b3 >= 2 holds
(SDDec (SDMax b1,b2,b3)) + (SDDec (SDMin b1,b2,b3)) = SDDec (DecSD 0,b1,b3)
proof end;

theorem Th18: :: RADIX_5:18
for b1 being Nat st b1 >= 1 holds
for b2, b3 being Nat st b2 in Seg b1 & b3 >= 2 holds
SDDec (Fmin b1,b2,b3) = (SDDec (SDMax b1,b2,b3)) + (SDDec (DecSD 1,b1,b3))
proof end;

theorem Th19: :: RADIX_5:19
for b1, b2, b3 being Nat st b2 in Seg b1 & b3 >= 2 holds
SDDec (Fmin (b1 + 1),(b2 + 1),b3) = (SDDec (Fmin (b1 + 1),b2,b3)) + (SDDec (Fmax (b1 + 1),b2,b3))
proof end;