let l, m be Nat; :: thesis: for n being non zero Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
let n be non zero 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
A2: l < 2 to_power (n -' 1) by A1, Th8;
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
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;
A4: m < 2 to_power (n -' 1) by A1, Th8;
1 <= n by NAT_1:14;
then A5: n in Seg n by FINSEQ_1:1;
then A6: (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 A4, 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 A5, 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 A5, A6, BINARITH:def 5
.= FALSE by A1, Th13 ;
then Intval ((n -BinarySequence l) + (n -BinarySequence m)) = Absval ((n -BinarySequence l) + (n -BinarySequence m)) by BINARI_2:def 3;
hence Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A1, A3, Th11, XXREAL_0:2; :: thesis: verum