let k be Nat; :: thesis: for i1 being Integer st 2 <= k & i1 in k -SD holds

let i1 be Integer; :: thesis: ( 2 <= k & i1 in k -SD implies ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) )
assume that
A1: 2 <= k and
A2: i1 in k -SD ; :: thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
A3: ( (- ()) + 1 <= i1 & 1 <= k ) by ;
per cases ( i1 < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= i1 & i1 < Radix (k -' 1) ) or Radix (k -' 1) <= i1 ) ;
case A4: i1 < - (Radix (k -' 1)) ; :: thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
then i1 + 1 <= - (Radix (k -' 1)) by INT_1:7;
then i1 <= (- (Radix (k -' 1))) - 1 by XREAL_1:19;
then i1 + () <= () + ((- (Radix (k -' 1))) - 1) by XREAL_1:7;
then A5: i1 + () <= (() - (Radix (k -' 1))) - 1 ;
SDSub_Add_Carry (i1,k) = - 1 by ;
hence ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by ; :: thesis: verum
end;
case A6: ( - (Radix (k -' 1)) <= i1 & i1 < Radix (k -' 1) ) ; :: thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
then ( SDSub_Add_Carry (i1,k) = 0 & i1 + 1 <= Radix (k -' 1) ) by ;
hence ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by ; :: thesis: verum
end;
case A7: Radix (k -' 1) <= i1 ; :: thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
i1 <= () + (- 1) by ;
then A8: ( 0 - 1 <= (Radix (k -' 1)) - 1 & i1 - () <= - 1 ) by ;
( SDSub_Add_Carry (i1,k) = 1 & (Radix (k -' 1)) + (- ()) <= i1 + (- ()) ) by ;
hence ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by ; :: thesis: verum
end;
end;
end;
hence ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) ; :: thesis: verum