let n be non empty 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 Th5;
then A3: 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then reconsider y = 0* n as Tuple of n, BOOLEAN by A3, FINSEQ_2:110;
k < (2 to_power n) - 1 by A1, XREAL_1:22;
then n -BinarySequence k <> 'not' y by A2, Lm4;
then add_ovfl (n -BinarySequence k),(Bin1 n) <> TRUE by Th24;
hence add_ovfl (n -BinarySequence k),(Bin1 n) = FALSE by XBOOLEAN:def 3; :: thesis: verum