let x be Integer; :: thesis: for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
let k be Nat; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
per cases ( x < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) or x >= Radix (k -' 1) ) ;
suppose x < - (Radix (k -' 1)) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum
end;
suppose ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum
end;
suppose x >= Radix (k -' 1) ; :: thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; :: thesis: verum
end;
end;