let n be non empty 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 )
assume A1: l + m <= (2 to_power (n -' 1)) - 1 ; :: thesis: (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 not (carry (n -BinarySequence l),(n -BinarySequence m)) /. n = FALSE ; :: thesis: contradiction
then A2: (carry (n -BinarySequence l),(n -BinarySequence m)) /. n = TRUE by XBOOLEAN:def 3;
A3: ( l < 2 to_power (n -' 1) & m < 2 to_power (n -' 1) ) by A1, Th8;
1 <= n by NAT_1:14;
then A4: n in Seg n by FINSEQ_1:3;
then A5: (n -BinarySequence l) /. n = IFEQ ((l div (2 to_power (n -' 1))) mod 2),0 ,FALSE ,TRUE by BINARI_3:def 1
.= IFEQ (0 mod 2),0 ,FALSE ,TRUE by A3, NAT_D:27
.= IFEQ 0 ,0 ,FALSE ,TRUE by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
A6: (n -BinarySequence m) /. n = IFEQ ((m div (2 to_power (n -' 1))) mod 2),0 ,FALSE ,TRUE by A4, BINARI_3:def 1
.= IFEQ (0 mod 2),0 ,FALSE ,TRUE by A3, NAT_D:27
.= IFEQ 0 ,0 ,FALSE ,TRUE by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:11;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n -' 1) < 2 to_power n by POWER:44, XREAL_1:148;
then A7: (2 to_power (n -' 1)) - 1 < (2 to_power n) - 1 by XREAL_1:16;
((n -BinarySequence l) + (n -BinarySequence m)) /. n = (FALSE 'xor' FALSE ) 'xor' TRUE by A2, A4, A5, A6, BINARITH:def 8
.= 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:148, XXREAL_0:2;
hence contradiction by A1, A7, A8, Th11, XXREAL_0:2; :: thesis: verum