begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
begin
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
begin
Lm1:
for k being Nat st 2 <= k holds
SD_Add_Carry ((Radix k) - 1) = 1
Lm2:
for n, k, i being Nat st k >= 2 & i in Seg n holds
SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0
theorem Th12:
theorem
theorem Th14:
for
n being
Nat st
n >= 1 holds
for
k being
Nat st
k >= 2 holds
for
tx,
ty,
tz,
tw being
Tuple of
n,
k -SD st ( for
i being
Nat holds
( not
i in Seg n or (
DigA tx,
i = DigA tz,
i &
DigA ty,
i = DigA tw,
i ) or (
DigA ty,
i = DigA tz,
i &
DigA tx,
i = DigA tw,
i ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
theorem
for
n,
k being
Nat st
n >= 1 &
k >= 2 holds
for
tx,
ty,
tz being
Tuple of
n,
k -SD st ( for
i being
Nat holds
( not
i in Seg n or (
DigA tx,
i = DigA tz,
i &
DigA ty,
i = 0 ) or (
DigA ty,
i = DigA tz,
i &
DigA tx,
i = 0 ) ) ) holds
(SDDec tz) + (SDDec (DecSD 0 ,n,k)) = (SDDec tx) + (SDDec ty)
begin
:: deftheorem Def1 defines SDMinDigit RADIX_5:def 1 :
for i, m, k being Nat st k >= 2 holds
( ( 1 <= i & i < m implies SDMinDigit m,k,i = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit m,k,i = 0 ) );
definition
let n,
m,
k be
Nat;
func SDMin n,
m,
k -> Tuple of
n,
k -SD means :
Def2:
for
i being
Nat st
i in Seg n holds
DigA it,
i = SDMinDigit m,
k,
i;
existence
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA b1,i = SDMinDigit m,k,i
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA b1,i = SDMinDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = SDMinDigit m,k,i ) holds
b1 = b2
end;
:: deftheorem Def2 defines SDMin RADIX_5:def 2 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = SDMin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = SDMinDigit m,k,i );
:: deftheorem Def3 defines SDMaxDigit RADIX_5:def 3 :
for i, m, k being Nat st k >= 2 holds
( ( 1 <= i & i < m implies SDMaxDigit m,k,i = (Radix k) - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit m,k,i = 0 ) );
definition
let n,
m,
k be
Nat;
func SDMax n,
m,
k -> Tuple of
n,
k -SD means :
Def4:
for
i being
Nat st
i in Seg n holds
DigA it,
i = SDMaxDigit m,
k,
i;
existence
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA b1,i = SDMaxDigit m,k,i
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA b1,i = SDMaxDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = SDMaxDigit m,k,i ) holds
b1 = b2
end;
:: deftheorem Def4 defines SDMax RADIX_5:def 4 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = SDMax n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = SDMaxDigit m,k,i );
:: deftheorem Def5 defines FminDigit RADIX_5:def 5 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FminDigit m,k,i = 1 ) & ( not i = m implies FminDigit m,k,i = 0 ) );
definition
let n,
m,
k be
Nat;
func Fmin n,
m,
k -> Tuple of
n,
k -SD means :
Def6:
for
i being
Nat st
i in Seg n holds
DigA it,
i = FminDigit m,
k,
i;
existence
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA b1,i = FminDigit m,k,i
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA b1,i = FminDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = FminDigit m,k,i ) holds
b1 = b2
end;
:: deftheorem Def6 defines Fmin RADIX_5:def 6 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = Fmin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FminDigit m,k,i );
:: deftheorem Def7 defines FmaxDigit RADIX_5:def 7 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FmaxDigit m,k,i = (Radix k) - 1 ) & ( not i = m implies FmaxDigit m,k,i = 0 ) );
definition
let n,
m,
k be
Nat;
func Fmax n,
m,
k -> Tuple of
n,
k -SD means :
Def8:
for
i being
Nat st
i in Seg n holds
DigA it,
i = FmaxDigit m,
k,
i;
existence
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA b1,i = FmaxDigit m,k,i
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA b1,i = FmaxDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = FmaxDigit m,k,i ) holds
b1 = b2
end;
:: deftheorem Def8 defines Fmax RADIX_5:def 8 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = Fmax n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FmaxDigit m,k,i );
begin
theorem Th16:
theorem
theorem
theorem