:: RADIX_6 semantic presentation

Lemma1: for b₁ being Nat st b₁ >= 1 holds
b₁ + 2 > 1

proof end;

theorem Th1: :: RADIX_6:1

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃ being Nat st b₂ >= 1 & b₃ >= 2 holds
SDDec (Fmin (b₂ + b₁),b₂,b₃) = SDDec (Fmin b₂,b₂,b₃)

proof end;

theorem Th2: :: RADIX_6:2

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
SDDec (Fmin b₁,b₁,b₂) > 0

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of (c₂ + 2),(c₃ -SD );
assume E3: c₁ in Seg (c₂ + 2) ;
func M0Digit c₄,c₁ -> Element of a₃ -SD equals :Def1: :: RADIX_6:def 1
a₄ . a₁ if a₁ >= a₂
0 if a₁ < a₂
;
coherence

proof end;

consistency ;

end;

:: deftheorem Def1 defines M0Digit RADIX_6:def 1 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of (c₁ + 2),(c₂ -SD );
func M0 c₃ -> Tuple of (a₁ + 2),(a₂ -SD ) means :Def2: :: RADIX_6:def 2
for b₁ being Nat st b₁ in Seg (a₁ + 2) holds
DigA a₄,b₁ = M0Digit a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines M0 RADIX_6:def 2 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of (c₂ + 2),(c₃ -SD );
assume that
E5: c₃ >= 2 and
E6: c₁ in Seg (c₂ + 2) ;
func MmaxDigit c₄,c₁ -> Element of a₃ -SD equals :Def3: :: RADIX_6:def 3
a₄ . a₁ if a₁ >= a₂
(Radix a₃) - 1 if a₁ < a₂
;
coherence

proof end;

consistency ;

end;

:: deftheorem Def3 defines MmaxDigit RADIX_6:def 3 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of (c₁ + 2),(c₂ -SD );
func Mmax c₃ -> Tuple of (a₁ + 2),(a₂ -SD ) means :Def4: :: RADIX_6:def 4
for b₁ being Nat st b₁ in Seg (a₁ + 2) holds
DigA a₄,b₁ = MmaxDigit a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Mmax RADIX_6:def 4 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of (c₂ + 2),(c₃ -SD );
assume that
E7: c₃ >= 2 and
E8: c₁ in Seg (c₂ + 2) ;
func MminDigit c₄,c₁ -> Element of a₃ -SD equals :Def5: :: RADIX_6:def 5
a₄ . a₁ if a₁ >= a₂
(- (Radix a₃)) + 1 if a₁ < a₂
;
coherence

proof end;

consistency ;

end;

:: deftheorem Def5 defines MminDigit RADIX_6:def 5 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of (c₁ + 2),(c₂ -SD );
func Mmin c₃ -> Tuple of (a₁ + 2),(a₂ -SD ) means :Def6: :: RADIX_6:def 6
for b₁ being Nat st b₁ in Seg (a₁ + 2) holds
DigA a₄,b₁ = MminDigit a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Mmin RADIX_6:def 6 :

theorem Th3: :: RADIX_6:3

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds SDDec (Mmax b₃) >= SDDec b₃

proof end;

theorem Th4: :: RADIX_6:4

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds SDDec b₃ >= SDDec (Mmin b₃)

proof end;

definition

let c₁, c₂ be Nat;
let c₃ be Integer;
pred c₃ needs_digits_of c₁,c₂ means :Def7: :: RADIX_6:def 7
( a₃ < (Radix a₂) |^ a₁ & a₃ >= (Radix a₂) |^ (a₁ -' 1) );

end;

:: deftheorem Def7 defines needs_digits_of RADIX_6:def 7 :

theorem Th5: :: RADIX_6:5

for b₁, b₂, b₃, b₄ being Nat st b₄ in Seg b₂ holds
DigA (DecSD b₁,b₂,b₃),b₄ >= 0

proof end;

theorem Th6: :: RADIX_6:6

for b₁, b₂, b₃ being Nat st b₁ >= 1 & b₂ >= 2 & b₃ needs_digits_of b₁,b₂ holds
DigA (DecSD b₃,b₁,b₂),b₁ > 0

proof end;

theorem Th7: :: RADIX_6:7

for b₁, b₂, b₃ being Nat st b₂ >= 1 & b₃ >= 2 & b₁ needs_digits_of b₂,b₃ holds
b₁ >= SDDec (Fmin (b₂ + 2),b₂,b₃)

proof end;

theorem Th8: :: RADIX_6:8

for b₁, b₂, b₃ being Integer st b₂ < b₁ + b₃ & b₃ > 0 holds
ex b₄ being Integer st
( - b₃ < b₁ - (b₄ * b₃) & b₂ - (b₄ * b₃) < b₃ )

proof end;

theorem Th9: :: RADIX_6:9

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds (SDDec (Mmax b₃)) + (SDDec (DecSD 0,(b₁ + 2),b₂)) = (SDDec (M0 b₃)) + (SDDec (SDMax (b₁ + 2),b₁,b₂))

proof end;

theorem Th10: :: RADIX_6:10

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds SDDec (Mmax b₃) < (SDDec (M0 b₃)) + (SDDec (Fmin (b₁ + 2),b₁,b₂))

proof end;

theorem Th11: :: RADIX_6:11

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds (SDDec (Mmin b₃)) + (SDDec (DecSD 0,(b₁ + 2),b₂)) = (SDDec (M0 b₃)) + (SDDec (SDMin (b₁ + 2),b₁,b₂))

proof end;

theorem Th12: :: RADIX_6:12

for b₁, b₂ being Nat
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 holds
(SDDec (M0 b₃)) + (SDDec (DecSD 0,(b₁ + 2),b₂)) = (SDDec (Mmin b₃)) + (SDDec (SDMax (b₁ + 2),b₁,b₂))

proof end;

theorem Th13: :: RADIX_6:13

for b₁, b₂ being Nat st b₁ >= 1 & b₂ >= 2 holds
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) holds SDDec (M0 b₃) < (SDDec (Mmin b₃)) + (SDDec (Fmin (b₁ + 2),b₁,b₂))

proof end;

theorem Th14: :: RADIX_6:14

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 & b₃ needs_digits_of b₁,b₂ holds
ex b₅ being Integer st
( - b₃ < (SDDec (M0 b₄)) - (b₅ * b₃) & (SDDec (Mmax b₄)) - (b₅ * b₃) < b₃ )

proof end;

theorem Th15: :: RADIX_6:15

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 & b₃ needs_digits_of b₁,b₂ holds
ex b₅ being Integer st
( - b₃ < (SDDec (Mmin b₄)) - (b₅ * b₃) & (SDDec (M0 b₄)) - (b₅ * b₃) < b₃ )

proof end;

theorem Th16: :: RADIX_6:16

for b₁, b₂ being Nat
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 & not ( SDDec (M0 b₃) <= SDDec b₃ & SDDec b₃ <= SDDec (Mmax b₃) ) holds
( SDDec (Mmin b₃) <= SDDec b₃ & SDDec b₃ < SDDec (M0 b₃) )

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of (c₂ + 2),(c₃ -SD );
assume E21: c₁ in Seg (c₂ + 2) ;
func MmaskDigit c₄,c₁ -> Element of a₃ -SD equals :Def8: :: RADIX_6:def 8
a₄ . a₁ if a₁ < a₂
0 if a₁ >= a₂
;
coherence

proof end;

consistency ;

end;

:: deftheorem Def8 defines MmaskDigit RADIX_6:def 8 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of (c₁ + 2),(c₂ -SD );
func Mmask c₃ -> Tuple of (a₁ + 2),(a₂ -SD ) means :Def9: :: RADIX_6:def 9
for b₁ being Nat st b₁ in Seg (a₁ + 2) holds
DigA a₄,b₁ = MmaskDigit a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Mmask RADIX_6:def 9 :

theorem Th17: :: RADIX_6:17

for b₁, b₂ being Nat
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 holds
(SDDec (M0 b₃)) + (SDDec (Mmask b₃)) = (SDDec b₃) + (SDDec (DecSD 0,(b₁ + 2),b₂))

proof end;

theorem Th18: :: RADIX_6:18

for b₁, b₂ being Nat
for b₃ being Tuple of (b₁ + 2),(b₂ -SD ) st b₁ >= 1 & b₂ >= 2 & SDDec (Mmask b₃) > 0 holds
SDDec b₃ > SDDec (M0 b₃)

proof end;

definition

let c₁, c₂, c₃ be Nat;
assume E24: c₃ >= 2 ;
func FSDMinDigit c₂,c₃,c₁ -> Element of a₃ -SD equals :Def10: :: RADIX_6:def 10
0 if a₁ > a₂
1 if a₁ = a₂
otherwise (- (Radix a₃)) + 1;
coherence

proof end;

consistency ;

end;

:: deftheorem Def10 defines FSDMinDigit RADIX_6:def 10 :

definition

let c₁, c₂, c₃ be Nat;
func FSDMin c₁,c₂,c₃ -> Tuple of a₁,(a₃ -SD ) means :Def11: :: RADIX_6:def 11
for b₁ being Nat st b₁ in Seg a₁ holds
DigA a₄,b₁ = FSDMinDigit a₂,a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines FSDMin RADIX_6:def 11 :

theorem Th19: :: RADIX_6:19

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃ being Nat st b₂ in Seg b₁ & b₃ >= 2 holds
SDDec (FSDMin b₁,b₂,b₃) = 1

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of (c₂ + 2),(c₃ -SD );
pred c₄ is_Zero_over c₁ means :Def12: :: RADIX_6:def 12
for b₁ being Nat st b₁ > a₁ holds
DigA a₄,b₁ = 0;

end;

:: deftheorem Def12 defines is_Zero_over RADIX_6:def 12 :

theorem Th20: :: RADIX_6:20

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃ being Nat
for b₄ being Tuple of (b₁ + 2),(b₃ -SD ) st b₃ >= 2 & b₂ in Seg (b₁ + 2) & Mmask b₄ is_Zero_over b₂ & DigA (Mmask b₄),b₂ > 0 holds
SDDec (Mmask b₄) > 0

proof end;