let n be non zero Nat; :: thesis: for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
let l, m be Nat; :: thesis: ( l + m <= (2 to_power (n -' 1)) - 1 implies (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE )
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
assume A1: l + m <= (2 to_power (n -' 1)) - 1 ; :: thesis: (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
then A2: l < 2 to_power (n -' 1) by Th8;
n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n -' 1) < 2 to_power n by POWER:39, XREAL_1:146;
then A3: (2 to_power (n -' 1)) - 1 < (2 to_power n) - 1 by XREAL_1:14;
assume not (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE ; :: thesis: contradiction
then A4: (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = TRUE by XBOOLEAN:def 3;
A5: m < 2 to_power (n -' 1) by A1, Th8;
1 <= n by NAT_1:14;
then A6: n in Seg n by FINSEQ_1:1;
then A7: (n -BinarySequence m) /. n = IFEQ (((m div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def 1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A5, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
(n -BinarySequence l) /. n = IFEQ (((l div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by A6, BINARI_3:def 1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A2, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
then ((n -BinarySequence l) + (n -BinarySequence m)) /. n = (FALSE 'xor' FALSE) 'xor' TRUE by A4, A6, A7, BINARITH:def 5
.= TRUE ;
then A8: Absval ((n -BinarySequence l) + (n -BinarySequence m)) >= 2 to_power (n -' 1) by Th12;
l + m < 2 to_power (n -' 1) by A1, XREAL_1:146, XXREAL_0:2;
hence contradiction by A1, A3, A8, Th11, XXREAL_0:2; :: thesis: verum