:: RADIX_4 semantic presentation

theorem Th1: :: RADIX_4:1

for b₁ being Nat st 2 <= b₁ holds
2 < Radix b₁

proof end;

Lemma2: for b₁ being Nat
for b₂ being Integer st b₂ in b₁ -SD_Sub_S holds
( b₂ >= - (Radix (b₁ -' 1)) & b₂ <= (Radix (b₁ -' 1)) - 1 )

proof end;

Lemma3: for b₁, b₂, b₃, b₄ being Nat st b₄ in Seg b₁ holds
DigA (DecSD b₂,(b₁ + 1),b₃),b₄ = DigA (DecSD b₂,b₁,b₃),b₄

proof end;

Lemma4: for b₁, b₂, b₃ being Nat st b₃ >= 1 & b₂ is_represented_by b₃ + 1,b₁ holds
DigA (DecSD (b₂ mod ((Radix b₁) |^ b₃)),b₃,b₁),b₃ = DigA (DecSD b₂,b₃,b₁),b₃

proof end;

theorem Th2: :: RADIX_4:2

for b₁, b₂ being Integer
for b₃ being Nat st 3 <= b₃ holds
SDSub_Add_Carry ((SDSub_Add_Carry b₁,b₃) + (SDSub_Add_Carry b₂,b₃)),b₃ = 0

proof end;

theorem Th3: :: RADIX_4:3

for b₁, b₂, b₃ being Nat st 2 <= b₁ holds
DigA_SDSub (SD2SDSub (DecSD b₂,b₃,b₁)),(b₃ + 1) = SDSub_Add_Carry (DigA (DecSD b₂,b₃,b₁),b₃),b₁

proof end;

theorem Th4: :: RADIX_4:4

for b₁, b₂ being Nat st 2 <= b₁ & b₂ is_represented_by 1,b₁ holds
DigA_SDSub (SD2SDSub (DecSD b₂,1,b₁)),(1 + 1) = SDSub_Add_Carry b₂,b₁

proof end;

theorem Th5: :: RADIX_4:5

for b₁, b₂, b₃ being Nat st b₃ >= 1 & b₁ >= 3 & b₂ is_represented_by b₃ + 1,b₁ holds
DigA_SDSub (SD2SDSub (DecSD (b₂ mod ((Radix b₁) |^ b₃)),b₃,b₁)),(b₃ + 1) = SDSub_Add_Carry (DigA (DecSD b₂,b₃,b₁),b₃),b₁

proof end;

theorem Th6: :: RADIX_4:6

for b₁, b₂ being Nat st 2 <= b₁ & b₂ is_represented_by 1,b₁ holds
DigA_SDSub (SD2SDSub (DecSD b₂,1,b₁)),1 = b₂ - ((SDSub_Add_Carry b₂,b₁) * (Radix b₁))

proof end;

theorem Th7: :: RADIX_4:7

for b₁, b₂, b₃ being Nat st b₃ >= 1 & b₁ >= 2 & b₂ is_represented_by b₃ + 1,b₁ holds
((Radix b₁) |^ b₃) * (DigA_SDSub (SD2SDSub (DecSD b₂,(b₃ + 1),b₁)),(b₃ + 1)) = ((((Radix b₁) |^ b₃) * (DigA (DecSD b₂,(b₃ + 1),b₁),(b₃ + 1))) - (((Radix b₁) |^ (b₃ + 1)) * (SDSub_Add_Carry (DigA (DecSD b₂,(b₃ + 1),b₁),(b₃ + 1)),b₁))) + (((Radix b₁) |^ b₃) * (SDSub_Add_Carry (DigA (DecSD b₂,(b₃ + 1),b₁),b₃),b₁))

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄, c₅ be Tuple of c₂,(c₃ -SD_Sub );
assume E11: ( c₁ in Seg c₂ & c₃ >= 2 ) ;
func SDSubAddDigit c₄,c₅,c₁,c₃ -> Element of a₃ -SD_Sub equals :Def1: :: RADIX_4:def 1
(SDSub_Add_Data ((DigA_SDSub a₄,a₁) + (DigA_SDSub a₅,a₁)),a₃) + (SDSub_Add_Carry ((DigA_SDSub a₄,(a₁ -' 1)) + (DigA_SDSub a₅,(a₁ -' 1))),a₃);
coherence

proof end;

end;

:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def 1 :

definition

let c₁, c₂ be Nat;
let c₃, c₄ be Tuple of c₁,(c₂ -SD_Sub );
func c₃ '+' c₄ -> Tuple of a₁,(a₂ -SD_Sub ) means :Def2: :: RADIX_4:def 2
for b₁ being Nat st b₁ in Seg a₁ holds
DigA_SDSub a₅,b₁ = SDSubAddDigit a₃,a₄,b₁,a₂;
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines '+' RADIX_4:def 2 :

theorem Th8: :: RADIX_4:8

for b₁, b₂, b₃, b₄, b₅ being Nat st b₅ in Seg b₁ & 2 <= b₂ holds
SDSubAddDigit (SD2SDSub (DecSD b₃,(b₁ + 1),b₂)),(SD2SDSub (DecSD b₄,(b₁ + 1),b₂)),b₅,b₂ = SDSubAddDigit (SD2SDSub (DecSD (b₃ mod ((Radix b₂) |^ b₁)),b₁,b₂)),(SD2SDSub (DecSD (b₄ mod ((Radix b₂) |^ b₁)),b₁,b₂)),b₅,b₂

proof end;

theorem Th9: :: RADIX_4:9

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃, b₄ being Nat st b₂ >= 3 & b₃ is_represented_by b₁,b₂ & b₄ is_represented_by b₁,b₂ holds
b₃ + b₄ = SDSub2IntOut ((SD2SDSub (DecSD b₃,b₁,b₂)) '+' (SD2SDSub (DecSD b₄,b₁,b₂)))

proof end;