let l, m be Nat; :: thesis: for n being non empty Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
let n be non empty Nat; :: thesis: ( l + m <= (2 to_power (n -' 1)) - 1 implies Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m )
assume A1: l + m <= (2 to_power (n -' 1)) - 1 ; :: thesis: Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
A2: ( l < 2 to_power (n -' 1) & m < 2 to_power (n -' 1) ) by A1, Th8;
1 <= n by NAT_1:14;
then A3: n in Seg n by FINSEQ_1:3;
then A4: (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 A2, NAT_D:27
.= IFEQ 0 ,0 ,FALSE ,TRUE by NAT_D:26
.= FALSE by FUNCOP_1:def 8 ;
(n -BinarySequence m) /. n = IFEQ ((m div (2 to_power (n -' 1))) mod 2),0 ,FALSE ,TRUE by A3, 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' ((carry (n -BinarySequence l),(n -BinarySequence m)) /. n) by A3, A4, BINARITH:def 8
.= FALSE by A1, Th13 ;
then A5: Intval ((n -BinarySequence l) + (n -BinarySequence m)) = Absval ((n -BinarySequence l) + (n -BinarySequence m)) by BINARI_2:def 3;
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 (2 to_power (n -' 1)) - 1 < (2 to_power n) - 1 by XREAL_1:16;
hence Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A1, A5, Th11, XXREAL_0:2; :: thesis: verum