let n be non zero Nat; :: thesis: for k being Nat st k + 1 < 2 to_power n holds
add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE
let k be Nat; :: thesis: ( k + 1 < 2 to_power n implies add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE )
assume A1: k + 1 < 2 to_power n ; :: thesis: add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE
then A2: k < 2 to_power n by NAT_1:13;
0* n in BOOLEAN * by Th4;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider y = 0* n as Tuple of n, BOOLEAN ;
k < (2 to_power n) - 1 by A1, XREAL_1:20;
then n -BinarySequence k <> 'not' y by A2, Lm4;
then add_ovfl ((n -BinarySequence k),(Bin1 n)) <> TRUE by Th23;
hence add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by XBOOLEAN:def 3; :: thesis: verum