defpred S₁[ Nat] means for k being Nat st k >= 2 holds
for tx, ty, tz, tw being Tuple of $1,(k -SD ) st ( for i being Nat holds
( not i in Seg $1 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);
A1: S₁[1]

proof

let k be Nat; :: thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of 1,(k -SD ) st ( for i being Nat holds
( not i in Seg 1 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) )
assume A2: k >= 2 ; :: thesis: for tx, ty, tz, tw being Tuple of 1,(k -SD ) st ( for i being Nat holds
( not i in Seg 1 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)
let tx, ty, tz, tw be Tuple of 1,(k -SD ); :: thesis: ( ( for i being Nat holds
( not i in Seg 1 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 ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A3: for j being Nat holds
( not j in Seg 1 or ( DigA tx,j = DigA tz,j & DigA ty,j = DigA tw,j ) or ( DigA ty,j = DigA tz,j & DigA tx,j = DigA tw,j ) ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
A4: 1 in Seg 1 by FINSEQ_1:3;
A5: SDDec (tz '+' tw) = DigA (tz '+' tw),1 by Th4
.= Add tz,tw,1,k by A4, RADIX_1:def 14
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry ((DigA tz,(1 -' 1)) + (DigA tw,(1 -' 1)))) by A2, A4, RADIX_1:def 13
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry ((DigA tz,0 ) + (DigA tw,(1 -' 1)))) by XREAL_1:234
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry ((DigA tz,0 ) + (DigA tw,0 ))) by XREAL_1:234
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry ((DigA tz,0 ) + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + (SD_Add_Carry (0 + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA tz,1) + (DigA tw,1)),k) + 0 by RADIX_1:def 10 ;
A6: SDDec (tx '+' ty) = DigA (tx '+' ty),1 by Th4
.= Add tx,ty,1,k by A4, RADIX_1:def 14
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry ((DigA tx,(1 -' 1)) + (DigA ty,(1 -' 1)))) by A2, A4, RADIX_1:def 13
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry ((DigA tx,0 ) + (DigA ty,(1 -' 1)))) by XREAL_1:234
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry ((DigA tx,0 ) + (DigA ty,0 ))) by XREAL_1:234
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry ((DigA tx,0 ) + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + (SD_Add_Carry (0 + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA tx,1) + (DigA ty,1)),k) + 0 by RADIX_1:def 10 ;
A7: ( ( DigA tx,1 = DigA tz,1 & DigA ty,1 = DigA tw,1 ) or ( DigA ty,1 = DigA tz,1 & DigA tx,1 = DigA tw,1 ) ) by A3, A4;
A8: ( DigA tx,1 = DigA tz,1 & DigA ty,1 = DigA tw,1 implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )

proof

assume ( DigA tx,1 = DigA tz,1 & DigA ty,1 = DigA tw,1 ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
then (SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA tx,1) + (DigA ty,1))) * ((Radix k) |^ 1)) by A2, A5, A6, RADIX_2:11;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A2, RADIX_2:11; :: thesis: verum

end;

( DigA ty,1 = DigA tz,1 & DigA tx,1 = DigA tw,1 implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )

proof

assume ( DigA ty,1 = DigA tz,1 & DigA tx,1 = DigA tw,1 ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
(SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA tx,1) + (DigA ty,1))) * ((Radix k) |^ 1)) by A2, A5, A6, A7, RADIX_2:11;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A2, RADIX_2:11; :: thesis: verum

end;

hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A3, A4, A8; :: thesis: verum

end;

A9: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume A10: ( n >= 1 & S₁[n] ) ; :: thesis: S₁[n + 1]
let k be Nat; :: thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of (n + 1),(k -SD ) st ( for i being Nat holds
( not i in Seg (n + 1) 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) )
assume A11: k >= 2 ; :: thesis: for tx, ty, tz, tw being Tuple of (n + 1),(k -SD ) st ( for i being Nat holds
( not i in Seg (n + 1) 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)
let tx, ty, tz, tw be Tuple of (n + 1),(k -SD ); :: thesis: ( ( for i being Nat holds
( not i in Seg (n + 1) 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 ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A12: for i being Nat holds
( not i in Seg (n + 1) 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 ) ) ; :: thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
deffunc H₁( Nat) -> Element of K404() = DigB tx,$1;
consider txn being FinSequence of INT such that
A13: len txn = n and
A14: for i being Nat st i in dom txn holds
txn . i = H₁(i) from FINSEQ_2:sch 1();
A15: dom txn = Seg n by A13, FINSEQ_1:def 3;
rng txn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng txn or z in k -SD )
assume z in rng txn ; :: thesis: z in k -SD
then consider xx being set such that
A16: xx in dom txn and
A17: z = txn . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A16;
A18: dom txn = Seg n by A13, FINSEQ_1:def 3;
A19: z = DigB tx,xx by A14, A16, A17
.= DigA tx,xx by RADIX_1:def 4 ;
xx in Seg (n + 1) by A16, A18, FINSEQ_2:9;
then DigA tx,xx is Element of k -SD by RADIX_1:19;
hence z in k -SD by A19; :: thesis: verum

end;

then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def 4;
A20: for i being Nat st i in Seg n holds
txn . i = tx . i

proof

let i be Nat; :: thesis: ( i in Seg n implies txn . i = tx . i )
assume A21: i in Seg n ; :: thesis: txn . i = tx . i
then A22: i in Seg (n + 1) by FINSEQ_2:9;
txn . i = DigB tx,i by A14, A21, A15
.= DigA tx,i by RADIX_1:def 4 ;
hence txn . i = tx . i by A22, RADIX_1:def 3; :: thesis: verum

end;

deffunc H₂( Nat) -> Element of K404() = DigB ty,$1;
consider tyn being FinSequence of INT such that
A23: len tyn = n and
A24: for i being Nat st i in dom tyn holds
tyn . i = H₂(i) from FINSEQ_2:sch 1();
A25: dom tyn = Seg n by A23, FINSEQ_1:def 3;
rng tyn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng tyn or z in k -SD )
assume z in rng tyn ; :: thesis: z in k -SD
then consider yy being set such that
A26: yy in dom tyn and
A27: z = tyn . yy by FUNCT_1:def 5;
reconsider yy = yy as Element of NAT by A26;
A28: dom tyn = Seg n by A23, FINSEQ_1:def 3;
A29: z = DigB ty,yy by A24, A26, A27
.= DigA ty,yy by RADIX_1:def 4 ;
yy in Seg (n + 1) by A26, A28, FINSEQ_2:9;
then DigA ty,yy is Element of k -SD by RADIX_1:19;
hence z in k -SD by A29; :: thesis: verum

end;

then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def 4;
A30: for i being Nat st i in Seg n holds
tyn . i = ty . i

proof

let i be Nat; :: thesis: ( i in Seg n implies tyn . i = ty . i )
assume A31: i in Seg n ; :: thesis: tyn . i = ty . i
then A32: i in Seg (n + 1) by FINSEQ_2:9;
tyn . i = DigB ty,i by A24, A31, A25
.= DigA ty,i by RADIX_1:def 4 ;
hence tyn . i = ty . i by A32, RADIX_1:def 3; :: thesis: verum

end;

deffunc H₃( Nat) -> Element of K404() = DigB tz,$1;
consider tzn being FinSequence of INT such that
A33: len tzn = n and
A34: for i being Nat st i in dom tzn holds
tzn . i = H₃(i) from FINSEQ_2:sch 1();
A35: dom tzn = Seg n by A33, FINSEQ_1:def 3;
rng tzn c= k -SD

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng tzn or z in k -SD )
assume z in rng tzn ; :: thesis: z in k -SD
then consider zz being set such that
A36: zz in dom tzn and
A37: z = tzn . zz by FUNCT_1:def 5;
reconsider zz = zz as Element of NAT by A36;
A38: dom tzn = Seg n by A33, FINSEQ_1:def 3;
A39: z = DigB tz,zz by A34, A36, A37
.= DigA tz,zz by RADIX_1:def 4 ;
zz in Seg (n + 1) by A36, A38, FINSEQ_2:9;
then DigA tz,zz is Element of k -SD by RADIX_1:19;
hence z in k -SD by A39; :: thesis: verum

end;

then reconsider tzn = tzn as FinSequence of k -SD by FINSEQ_1:def 4;
A40: for i being Nat st i in Seg n holds
tzn . i = tz . i

proof

let i be Nat; :: thesis: ( i in Seg n implies tzn . i = tz . i )
assume A41: i in Seg n ; :: thesis: tzn . i = tz . i
then A42: i in Seg (n + 1) by FINSEQ_2:9;
tzn . i = DigB tz,i by A34, A41, A35
.= DigA tz,i by RADIX_1:def 4 ;
hence tzn . i = tz . i by A42, RADIX_1:def 3; :: thesis: verum

end;

deffunc H₄( Nat) -> Element of K404() = DigB tw,$1;
consider twn being FinSequence of INT such that
A43: len twn = n and
A44: for i being Nat st i in dom twn holds
twn . i = H₄(i) from FINSEQ_2:sch 1();
A45: dom twn = Seg n by A43, FINSEQ_1:def 3;
rng twn c= k -SD

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in rng twn or w in k -SD )
assume w in rng twn ; :: thesis: w in k -SD
then consider ww being set such that
A46: ww in dom twn and
A47: w = twn . ww by FUNCT_1:def 5;
reconsider ww = ww as Element of NAT by A46;
A48: dom twn = Seg n by A43, FINSEQ_1:def 3;
A49: w = DigB tw,ww by A44, A46, A47
.= DigA tw,ww by RADIX_1:def 4 ;
ww in Seg (n + 1) by A46, A48, FINSEQ_2:9;
then DigA tw,ww is Element of k -SD by RADIX_1:19;
hence w in k -SD by A49; :: thesis: verum

end;

then reconsider twn = twn as FinSequence of k -SD by FINSEQ_1:def 4;
A50: for i being Nat st i in Seg n holds
twn . i = tw . i

proof

let i be Nat; :: thesis: ( i in Seg n implies twn . i = tw . i )
assume A51: i in Seg n ; :: thesis: twn . i = tw . i
then A52: i in Seg (n + 1) by FINSEQ_2:9;
twn . i = DigB tw,i by A44, A51, A45
.= DigA tw,i by RADIX_1:def 4 ;
hence twn . i = tw . i by A52, RADIX_1:def 3; :: thesis: verum

end;

reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider txn = txn as Tuple of n,(k -SD ) by A13, FINSEQ_2:110;
reconsider tyn = tyn as Tuple of n,(k -SD ) by A23, FINSEQ_2:110;
reconsider tzn = tzn as Tuple of n,(k -SD ) by A33, FINSEQ_2:110;
reconsider twn = twn as Tuple of n,(k -SD ) by A43, FINSEQ_2:110;
A53: (SDDec txn) + (((Radix k) |^ n) * (DigA tx,(n + 1))) = SDDec tx by A20, RADIX_2:10;
A54: (SDDec tyn) + (((Radix k) |^ n) * (DigA ty,(n + 1))) = SDDec ty by A30, RADIX_2:10;
A55: (SDDec tzn) + (((Radix k) |^ n) * (DigA tz,(n + 1))) = SDDec tz by A40, RADIX_2:10;
A56: (SDDec twn) + (((Radix k) |^ n) * (DigA tw,(n + 1))) = SDDec tw by A50, RADIX_2:10;
for i being Nat holds
( not i in Seg n or ( DigA txn,i = DigA tzn,i & DigA tyn,i = DigA twn,i ) or ( DigA tyn,i = DigA tzn,i & DigA txn,i = DigA twn,i ) )

proof

let i be Nat; :: thesis: ( not i in Seg n or ( DigA txn,i = DigA tzn,i & DigA tyn,i = DigA twn,i ) or ( DigA tyn,i = DigA tzn,i & DigA txn,i = DigA twn,i ) )
assume A57: i in Seg n ; :: thesis: ( ( DigA txn,i = DigA tzn,i & DigA tyn,i = DigA twn,i ) or ( DigA tyn,i = DigA tzn,i & DigA txn,i = DigA twn,i ) )
then A58: ( 1 <= i & i <= n ) by FINSEQ_1:3;
then i <= n + 1 by NAT_1:12;
then A59: i in Seg (n + 1) by A58, FINSEQ_1:3;
then A60: DigA tx,i = tx . i by RADIX_1:def 3
.= txn . i by A20, A57
.= DigA txn,i by A57, RADIX_1:def 3 ;
A61: DigA ty,i = ty . i by A59, RADIX_1:def 3
.= tyn . i by A30, A57
.= DigA tyn,i by A57, RADIX_1:def 3 ;
A62: DigA tz,i = tz . i by A59, RADIX_1:def 3
.= tzn . i by A40, A57
.= DigA tzn,i by A57, RADIX_1:def 3 ;
DigA tw,i = tw . i by A59, RADIX_1:def 3
.= twn . i by A50, A57
.= DigA twn,i by A57, RADIX_1:def 3 ;
hence ( ( DigA txn,i = DigA tzn,i & DigA tyn,i = DigA twn,i ) or ( DigA tyn,i = DigA tzn,i & DigA txn,i = DigA twn,i ) ) by A12, A59, A60, A61, A62; :: thesis: verum

end;

then A63: (SDDec tzn) + (SDDec twn) = (SDDec txn) + (SDDec tyn) by A10, A11;
n + 1 in Seg (n + 1) by FINSEQ_1:5;
then ( ( DigA tx,(n + 1) = DigA tz,(n + 1) & DigA ty,(n + 1) = DigA tw,(n + 1) ) or ( DigA ty,(n + 1) = DigA tz,(n + 1) & DigA tx,(n + 1) = DigA tw,(n + 1) ) ) by A12;
hence (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A53, A54, A55, A56, A63; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A1, A9);
hence 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) ; :: thesis: verum