:: BINARI_4 semantic presentation

theorem E1: :: BINARI_4:1
for b1 being Nat holds
( b1 > 0 implies b1 * 2 >= b1 + 1 )
proof
let c1 be Nat;
assume c1 > 0 ;
then c1 >= 0 + 1 by INT_1:20;
then ( c1 >= 1 & c1 * 2 = c1 + c1 ) ;
hence c1 * 2 >= c1 + 1 by XREAL_1:8;
end;

theorem E2: :: BINARI_4:2
for b1 being Nat holds 2 to_power b1 >= b1
proof
defpred S1[ Nat] means 2 to_power a1 >= a1;
E3: S1[0] ;
E4: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be Nat;
assume E5: 2 to_power c1 >= c1 ;
now
per cases not ( not c1 = 0 & not c1 > 0 ) ;
suppose E6: c1 = 0 ;
then 2 to_power (c1 + 1) = 2 by POWER:30;
hence S1[c1 + 1] by E6;
end;
suppose E6: c1 > 0 ;
E7: (2 to_power c1) * 2 >= c1 * 2 by E5, NAT_1:20;
2 to_power 1 = 2 by POWER:30;
then E8: 2 to_power (c1 + 1) >= c1 * 2 by E7, POWER:32;
c1 * 2 >= c1 + 1 by E6, E1;
hence S1[c1 + 1] by E8, XREAL_1:2;
end;
end;
end;
hence S1[c1 + 1] ;
end;
thus for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E3, E4);
end;

theorem :: BINARI_4:3
for b1 being Nat holds (0* b1) + (0* b1) = 0* b1
proof
let c1 be Nat;
E3: dom addreal = [:REAL ,REAL :] by FUNCT_2:def 1;
rng (0* c1) c= REAL by FINSEQ_1:def 4;
then E4: [:(rng (0* c1)),(rng (0* c1)):] c= dom addreal by E3, ZFMISC_1:119;
E5: dom ((0* c1) + (0* c1)) = dom (addreal .: (0* c1),(0* c1)) by RVSUM_1:def 4
.= (dom (0* c1)) /\ (dom (0* c1)) by E4, FUNCOP_1:84
.= dom (c1 |-> 0) by EUCLID:def 4
.= Seg c1 by FINSEQ_2:68 ;
E6: dom (0* c1) = dom (c1 |-> 0) by EUCLID:def 4
.= Seg c1 by FINSEQ_2:68 ;
for b1 being Nat holds
( b1 in dom (0* c1) implies (0* c1) . b1 = ((0* c1) + (0* c1)) . b1 )
proof
let c2 be Nat;
assume E7: c2 in dom (0* c1) ;
E8: (0* c1) . c2 = (c1 |-> 0) . c2 by EUCLID:def 4
.= 0 by E6, E7, FINSEQ_2:70 ;
then ((0* c1) + (0* c1)) . c2 = 0 + 0 by E5, E6, E7, RVSUM_1:26;
hence (0* c1) . c2 = ((0* c1) + (0* c1)) . c2 by E8;
end;
hence (0* c1) + (0* c1) = 0* c1 by E5, E6, FINSEQ_1:17;
end;

theorem E3: :: BINARI_4:4
for b1, b2, b3 being Nat holds
not ( b3 <= b1 & b1 <= b2 & not b3 = b1 & not ( b3 + 1 <= b1 & b1 <= b2 ) )
proof
let c1, c2 be Nat;
defpred S1[ Nat] means not ( a1 <= c1 & c1 <= c2 & not a1 = c1 & not ( a1 + 1 <= c1 & c1 <= c2 ) );
E4: S1[0] by NAT_1:38;
E5: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c3 be Nat;
assume not ( c3 <= c1 & c1 <= c2 & not c3 = c1 & not ( c3 + 1 <= c1 & c1 <= c2 ) ) ;
assume that E6: c3 + 1 <= c1
and E7: c1 <= c2 ;
not ( not c3 + 1 = c1 & not c3 + 1 < c1 ) by E6, XREAL_1:1;
hence not ( not c3 + 1 = c1 & not ( (c3 + 1) + 1 <= c1 & c1 <= c2 ) ) by E7, NAT_1:38;
end;
thus for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E4, E5);
end;

theorem E4: :: BINARI_4:5
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( ( b2 = 0* b1 & b3 = 0* b1 ) implies ( carry b2,b3 = 0* b1 ) )
proof
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
assume E5: ( c2 = 0* c1 & c3 = 0* c1 ) ;
len (carry c2,c3) = c1 by FINSEQ_2:109;
then 1 <= len (carry c2,c3) by NAT_1:39;
then E6: (carry c2,c3) . 1 = (carry c2,c3) /. 1 by FINSEQ_4:24
.= 0 by BINARITH:def 5, MARGREL1:36 ;
E7: for b1 being Nat holds
( ( b1 <= c1 ) implies ( not 1 < b1 or (carry c2,c3) . b1 = 0 ) )
proof
let c4 be Nat;
assume E8: ( 1 < c4 & c4 <= c1 ) ;
reconsider c5 = c4 - 1 as Nat by E8, INT_1:18;
c5 + 1 = c4 ;
then E9: ( 1 <= c5 & c5 < c1 & c4 = c5 + 1 ) by E8, NAT_1:38;
then E10: ( c5 in Seg c1 & c5 <= len c2 & c5 <= len c3 ) by FINSEQ_1:3, FINSEQ_2:109;
len (0* c1) = len (c1 |-> 0) by EUCLID:def 4
.= c1 by FINSEQ_2:69 ;
then E11: c2 /. c5 = (0* c1) . c5 by E5, E9, FINSEQ_4:24
.= (c1 |-> 0) . c5 by EUCLID:def 4
.= FALSE by E10, FINSEQ_2:70, MARGREL1:36 ;
len (carry c2,c3) = c1 by FINSEQ_2:109;
then (carry c2,c3) . c4 = (carry c2,c3) /. c4 by E8, FINSEQ_4:24
.= ((FALSE '&' FALSE ) 'or' (FALSE '&' ((carry c2,c3) /. c5))) 'or' (FALSE '&' ((carry c2,c3) /. c5)) by E5, E9, E11, BINARITH:def 5
.= (FALSE 'or' (FALSE '&' ((carry c2,c3) /. c5))) 'or' (FALSE '&' ((carry c2,c3) /. c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' ((carry c2,c3) /. c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence (carry c2,c3) . c4 = 0 by MARGREL1:36;
end;
for b1 being Nat holds
( b1 in Seg c1 implies (carry c2,c3) . b1 = (0* c1) . b1 )
proof
let c4 be Nat;
assume E8: c4 in Seg c1 ;
E9: ( 1 <= c4 & c4 <= c1 ) by E8, FINSEQ_1:3;
E10: (0* c1) . c4 = (c1 |-> 0) . c4 by EUCLID:def 4
.= 0 by E8, FINSEQ_2:70 ;
now
per cases ( c4 = 1 or ( 1 + 1 <= c4 & c4 <= c1 ) ) by E9, E3;
suppose c4 = 1 ;
hence (carry c2,c3) . c4 = (0* c1) . c4 by E6, E10;
end;
suppose ( 1 + 1 <= c4 & c4 <= c1 ) ;
then ( 1 < c4 & c4 <= c1 ) by NAT_1:38;
hence (carry c2,c3) . c4 = (0* c1) . c4 by E7, E10;
end;
end;
end;
hence (carry c2,c3) . c4 = (0* c1) . c4 ;
end;
hence carry c2,c3 = 0* c1 by E5, FINSEQ_2:139;
end;

theorem :: BINARI_4:6
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( ( b2 = 0* b1 & b3 = 0* b1 ) implies ( b2 + b3 = 0* b1 ) )
proof
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
assume E5: ( c2 = 0* c1 & c3 = 0* c1 ) ;
for b1 being Nat holds
( b1 in Seg c1 implies (c2 + c3) . b1 = (0* c1) . b1 )
proof
let c4 be Nat;
assume E6: c4 in Seg c1 ;
E7: (0* c1) . c4 = (c1 |-> 0) . c4 by EUCLID:def 4
.= FALSE by E6, FINSEQ_2:70, MARGREL1:36 ;
( len c2 = c1 & len c3 = c1 & len (carry c2,c3) = c1 & len (c2 + c3) = c1 ) by FINSEQ_2:109;
then E8: ( 1 <= c4 & c4 <= len c2 & c4 <= len (carry c2,c3) & c4 <= len (c2 + c3) ) by E6, FINSEQ_1:3;
then E9: c3 /. c4 = FALSE by E5, E7, FINSEQ_4:24;
E10: (carry c2,c3) /. c4 = (carry c2,c3) . c4 by E8, FINSEQ_4:24
.= FALSE by E5, E7, E4 ;
(c2 + c3) . c4 = (c2 + c3) /. c4 by E8, FINSEQ_4:24
.= (FALSE 'xor' FALSE ) 'xor' FALSE by E5, E6, E9, E10, BINARITH:def 8
.= FALSE 'xor' FALSE by BINARITH:14
.= FALSE by BINARITH:14 ;
hence (c2 + c3) . c4 = (0* c1) . c4 by E7;
end;
hence c2 + c3 = 0* c1 by E5, FINSEQ_2:139;
end;

theorem :: BINARI_4:7
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = 0* b1 implies Intval b2 = 0 )
proof
let c1 be non empty Nat;
let c2 be Tuple of c1,BOOLEAN ;
assume E5: c2 = 0* c1 ;
E6: ( 1 <= c1 & c1 <= len c2 ) by FINSEQ_2:109, NAT_1:39;
then E7: c1 in Seg c1 by FINSEQ_1:3;
c2 /. c1 = c2 . c1 by E6, FINSEQ_4:24
.= FALSE by E5, E7, JORDAN2B:2, MARGREL1:def 13 ;
then Intval c2 = Absval c2 by BINARI_2:def 3;
hence Intval c2 = 0 by E5, BINARI_3:7;
end;

theorem E5: :: BINARI_4:8
for b1, b2, b3 being Nat holds
( b1 + b2 <= b3 - 1 implies ( b1 < b3 & b2 < b3 ) )
proof
let c1, c2, c3 be Nat;
assume E6: c1 + c2 <= c3 - 1 ;
c3 <= c3 + c2 by NAT_1:29;
then E7: c3 - c2 <= (c3 + c2) - c2 by XREAL_1:11;
E8: (c1 + c2) - c2 <= (c3 - 1) - c2 by E6, XREAL_1:11;
(c3 - 1) - c2 = (c3 - c2) - 1 ;
then (c3 - 1) - c2 < c3 - c2 by XREAL_1:148;
then (c3 - 1) - c2 < c3 by E7, XREAL_1:2;
hence c1 < c3 by E8, XREAL_1:2;
c3 <= c3 + c1 by NAT_1:29;
then E9: c3 - c1 <= (c3 + c1) - c1 by XREAL_1:11;
E10: (c2 + c1) - c1 <= (c3 - 1) - c1 by E6, XREAL_1:11;
(c3 - 1) - c1 = (c3 - c1) - 1 ;
then (c3 - 1) - c1 < c3 - c1 by XREAL_1:148;
then (c3 - 1) - c1 < c3 by E9, XREAL_1:2;
hence c2 < c3 by E10, XREAL_1:2;
end;

theorem E6: :: BINARI_4:9
for b1, b2, b3 being Integer holds
( ( b1 <= b2 + b3 ) implies ( not b2 < 0 or not b3 < 0 or ( b1 < b2 & b1 < b3 ) ) )
proof
let c1, c2, c3 be Integer;
assume E7: ( c1 <= c2 + c3 & c2 < 0 & c3 < 0 ) ;
then c1 - c3 <= (c2 + c3) - c3 by XREAL_1:11;
then c3 + (c1 + (- c3)) < 0 + c2 by E7, XREAL_1:10;
hence c1 < c2 ;
c1 - c2 <= (c3 + c2) - c2 by E7, XREAL_1:11;
then c2 + (c1 + (- c2)) < 0 + c3 by E7, XREAL_1:10;
hence c1 < c3 ;
end;

theorem E7: :: BINARI_4:10
for b1 being non empty Nat
for b2, b3 being Nat holds
( b2 + b3 <= (2 to_power b1) - 1 implies add_ovfl (b1 -BinarySequence b2),(b1 -BinarySequence b3) = FALSE )
proof
let c1 be non empty Nat;
let c2, c3 be Nat;
assume E8: c2 + c3 <= (2 to_power c1) - 1 ;
set c4 = c1 -BinarySequence c2;
set c5 = c1 -BinarySequence c3;
assume E9: add_ovfl (c1 -BinarySequence c2),(c1 -BinarySequence c3) <> FALSE ;
E10: ( c2 < 2 to_power c1 & c3 < 2 to_power c1 ) by E8, E5;
E11: IFEQ (add_ovfl (c1 -BinarySequence c2),(c1 -BinarySequence c3)),FALSE ,0,(2 to_power c1) = 2 to_power c1 by E9, CQC_LANG:def 1;
E12: (Absval ((c1 -BinarySequence c2) + (c1 -BinarySequence c3))) + (IFEQ (add_ovfl (c1 -BinarySequence c2),(c1 -BinarySequence c3)),FALSE ,0,(2 to_power c1)) = (Absval (c1 -BinarySequence c2)) + (Absval (c1 -BinarySequence c3)) by BINARITH:47
.= c2 + (Absval (c1 -BinarySequence c3)) by E10, BINARI_3:36
.= c2 + c3 by E10, BINARI_3:36 ;
E13: 2 to_power c1 > (2 to_power c1) - 1 by XREAL_1:148;
(Absval ((c1 -BinarySequence c2) + (c1 -BinarySequence c3))) + (2 to_power c1) >= 2 to_power c1 by NAT_1:29;
hence not verum by E8, E11, E12, E13, XREAL_1:2;
end;

theorem E8: :: BINARI_4:11
for b1 being non empty Nat
for b2, b3 being Nat holds
( b2 + b3 <= (2 to_power b1) - 1 implies Absval ((b1 -BinarySequence b2) + (b1 -BinarySequence b3)) = b2 + b3 )
proof
let c1 be non empty Nat;
let c2, c3 be Nat;
assume E9: c2 + c3 <= (2 to_power c1) - 1 ;
set c4 = c1 -BinarySequence c2;
set c5 = c1 -BinarySequence c3;
E10: ( c2 < 2 to_power c1 & c3 < 2 to_power c1 ) by E9, E5;
add_ovfl (c1 -BinarySequence c2),(c1 -BinarySequence c3) = FALSE by E9, E7;
then c1 -BinarySequence c2,c1 -BinarySequence c3 are_summable by BINARITH:def 10;
then Absval ((c1 -BinarySequence c2) + (c1 -BinarySequence c3)) = (Absval (c1 -BinarySequence c2)) + (Absval (c1 -BinarySequence c3)) by BINARITH:48
.= c2 + (Absval (c1 -BinarySequence c3)) by E10, BINARI_3:36 ;
hence Absval ((c1 -BinarySequence c2) + (c1 -BinarySequence c3)) = c2 + c3 by E10, BINARI_3:36;
end;

theorem E9: :: BINARI_4:12
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 /. b1 = TRUE implies Absval b2 >= 2 to_power (b1 -' 1) )
proof
defpred S1[ Nat] means for b1 being Tuple of a1,BOOLEAN holds
( b1 /. a1 = TRUE implies Absval b1 >= 2 to_power (a1 -' 1) );
E10: S1[1]
proof
let c1 be Tuple of 1,BOOLEAN ;
assume E11: c1 /. 1 = TRUE ;
E12: len c1 = 1 by FINSEQ_2:109;
then c1 . 1 = c1 /. 1 by FINSEQ_4:24;
then c1 = <*TRUE *> by E11, E12, FINSEQ_1:57;
then E13: Absval c1 = 1 by BINARITH:42;
2 to_power (1 -' 1) = 2 to_power (1 - 1) by BINARITH:def 3;
hence Absval c1 >= 2 to_power (1 -' 1) by E13, POWER:29;
end;
E11: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume S1[c1] ;
let c2 be Tuple of (c1 + 1),BOOLEAN ;
assume E12: c2 /. (c1 + 1) = TRUE ;
consider c3 being Tuple of c1,BOOLEAN , c4 being Element of BOOLEAN such that
E13: c2 = c3 ^ <*c4*> by FINSEQ_2:137;
E14: c1 + 1 >= 1 by NAT_1:29;
then (c1 + 1) - 1 >= 1 - 1 by XREAL_1:11;
then E15: (c1 + 1) -' 1 = c1 by BINARITH:def 3;
len c2 = c1 + 1 by FINSEQ_2:109;
then E16: c2 /. (c1 + 1) = (c3 ^ <*c4*>) . (c1 + 1) by E13, E14, FINSEQ_4:24
.= c4 by FINSEQ_2:136 ;
Absval c2 = (Absval c3) + (IFEQ c4,FALSE ,0,(2 to_power c1)) by E13, BINARITH:46
.= (Absval c3) + (2 to_power c1) by E12, E16, CQC_LANG:def 1, MARGREL1:38 ;
hence Absval c2 >= 2 to_power ((c1 + 1) -' 1) by E15, NAT_1:29;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E10, E11);
end;

theorem E10: :: BINARI_4:13
for b1 being non empty Nat
for b2, b3 being Nat holds
( b2 + b3 <= (2 to_power (b1 -' 1)) - 1 implies (carry (b1 -BinarySequence b2),(b1 -BinarySequence b3)) /. b1 = FALSE )
proof
let c1 be non empty Nat;
let c2, c3 be Nat;
assume E11: c2 + c3 <= (2 to_power (c1 -' 1)) - 1 ;
set c4 = c1 -BinarySequence c2;
set c5 = c1 -BinarySequence c3;
set c6 = FALSE ;
set c7 = TRUE ;
assume not (carry (c1 -BinarySequence c2),(c1 -BinarySequence c3)) /. c1 = FALSE ;
then E12: (carry (c1 -BinarySequence c2),(c1 -BinarySequence c3)) /. c1 = TRUE by MARGREL1:39;
E13: ( c2 < 2 to_power (c1 -' 1) & c3 < 2 to_power (c1 -' 1) ) by E11, E5;
1 <= c1 by NAT_1:39;
then E14: c1 in Seg c1 by FINSEQ_1:3;
then E15: (c1 -BinarySequence c2) /. c1 = IFEQ ((c2 div (2 to_power (c1 -' 1))) mod 2),0,FALSE ,TRUE by BINARI_3:def 1
.= IFEQ (0 mod 2),0,FALSE ,TRUE by E13, JORDAN4:5
.= IFEQ 0,0,FALSE ,TRUE by GR_CY_1:6
.= FALSE by CQC_LANG:def 1 ;
E16: (c1 -BinarySequence c3) /. c1 = IFEQ ((c3 div (2 to_power (c1 -' 1))) mod 2),0,FALSE ,TRUE by E14, BINARI_3:def 1
.= IFEQ (0 mod 2),0,FALSE ,TRUE by E13, JORDAN4:5
.= IFEQ 0,0,FALSE ,TRUE by GR_CY_1:6
.= FALSE by CQC_LANG:def 1 ;
c1 >= 1 by NAT_1:39;
then c1 - 1 >= 1 - 1 by XREAL_1:11;
then c1 -' 1 = c1 - 1 by BINARITH:def 3;
then c1 -' 1 < c1 by XREAL_1:148;
then 2 to_power (c1 -' 1) < 2 to_power c1 by POWER:44;
then (2 to_power (c1 -' 1)) - 1 < (2 to_power c1) - 1 by REAL_1:92;
then E17: c2 + c3 <= (2 to_power c1) - 1 by E11, XREAL_1:2;
((c1 -BinarySequence c2) + (c1 -BinarySequence c3)) /. c1 = (FALSE 'xor' FALSE ) 'xor' TRUE by E12, E14, E15, E16, BINARITH:def 8
.= FALSE 'xor' TRUE by BINARITH:14
.= TRUE by BINARITH:14 ;
then E18: Absval ((c1 -BinarySequence c2) + (c1 -BinarySequence c3)) >= 2 to_power (c1 -' 1) by E9;
(2 to_power (c1 -' 1)) - 1 < 2 to_power (c1 -' 1) by XREAL_1:148;
then c2 + c3 < 2 to_power (c1 -' 1) by E11, XREAL_1:2;
hence not verum by E17, E18, E8;
end;

theorem E11: :: BINARI_4:14
for b1, b2 being Nat
for b3 being non empty Nat holds
( b1 + b2 <= (2 to_power (b3 -' 1)) - 1 implies Intval ((b3 -BinarySequence b1) + (b3 -BinarySequence b2)) = b1 + b2 )
proof
let c1, c2 be Nat;
let c3 be non empty Nat;
assume E12: c1 + c2 <= (2 to_power (c3 -' 1)) - 1 ;
set c4 = c3 -BinarySequence c1;
set c5 = c3 -BinarySequence c2;
set c6 = FALSE ;
set c7 = TRUE ;
E13: ( c1 < 2 to_power (c3 -' 1) & c2 < 2 to_power (c3 -' 1) ) by E12, E5;
1 <= c3 by NAT_1:39;
then E14: c3 in Seg c3 by FINSEQ_1:3;
then E15: (c3 -BinarySequence c1) /. c3 = IFEQ ((c1 div (2 to_power (c3 -' 1))) mod 2),0,FALSE ,TRUE by BINARI_3:def 1
.= IFEQ (0 mod 2),0,FALSE ,TRUE by E13, JORDAN4:5
.= IFEQ 0,0,FALSE ,TRUE by GR_CY_1:6
.= FALSE by CQC_LANG:def 1 ;
(c3 -BinarySequence c2) /. c3 = IFEQ ((c2 div (2 to_power (c3 -' 1))) mod 2),0,FALSE ,TRUE by E14, BINARI_3:def 1
.= IFEQ (0 mod 2),0,FALSE ,TRUE by E13, JORDAN4:5
.= IFEQ 0,0,FALSE ,TRUE by GR_CY_1:6
.= FALSE by CQC_LANG:def 1 ;
then ((c3 -BinarySequence c1) + (c3 -BinarySequence c2)) /. c3 = (FALSE 'xor' FALSE ) 'xor' ((carry (c3 -BinarySequence c1),(c3 -BinarySequence c2)) /. c3) by E14, E15, BINARITH:def 8
.= FALSE 'xor' ((carry (c3 -BinarySequence c1),(c3 -BinarySequence c2)) /. c3) by BINARITH:14
.= (carry (c3 -BinarySequence c1),(c3 -BinarySequence c2)) /. c3 by BINARITH:14
.= FALSE by E12, E10 ;
then E16: Intval ((c3 -BinarySequence c1) + (c3 -BinarySequence c2)) = Absval ((c3 -BinarySequence c1) + (c3 -BinarySequence c2)) by BINARI_2:def 3;
c3 >= 1 by NAT_1:39;
then c3 - 1 >= 1 - 1 by XREAL_1:11;
then c3 -' 1 = c3 - 1 by BINARITH:def 3;
then c3 -' 1 < c3 by XREAL_1:148;
then 2 to_power (c3 -' 1) < 2 to_power c3 by POWER:44;
then (2 to_power (c3 -' 1)) - 1 < (2 to_power c3) - 1 by REAL_1:92;
then c1 + c2 <= (2 to_power c3) - 1 by E12, XREAL_1:2;
hence Intval ((c3 -BinarySequence c1) + (c3 -BinarySequence c2)) = c1 + c2 by E16, E8;
end;

theorem E12: :: BINARI_4:15
for b1 being Tuple of 1,BOOLEAN holds
( b1 = <*TRUE *> implies Intval b1 = - 1 )
proof
let c1 be Tuple of 1,BOOLEAN ;
assume E13: c1 = <*TRUE *> ;
len c1 = 1 by FINSEQ_2:109;
then c1 /. 1 = c1 . 1 by FINSEQ_4:24
.= TRUE by E13, FINSEQ_1:57 ;
then Intval c1 = (Absval c1) - (2 to_power 1) by BINARI_2:def 3, MARGREL1:38
.= 1 - (2 to_power 1) by E13, BINARITH:42
.= 1 - (1 + 1) by POWER:30
.= 0 - 1 ;
hence Intval c1 = - 1 ;
end;

theorem :: BINARI_4:16
for b1 being Tuple of 1,BOOLEAN holds
( b1 = <*FALSE *> implies Intval b1 = 0 )
proof
let c1 be Tuple of 1,BOOLEAN ;
assume E13: c1 = <*FALSE *> ;
len c1 = 1 by FINSEQ_2:109;
then c1 /. 1 = c1 . 1 by FINSEQ_4:24
.= FALSE by E13, FINSEQ_1:57 ;
then Intval c1 = Absval c1 by BINARI_2:def 3;
hence Intval c1 = 0 by E13, BINARITH:41;
end;

theorem E13: :: BINARI_4:17
for b1 being boolean set holds TRUE 'or' b1 = TRUE
proof
let c1 be boolean set ;
TRUE 'or' c1 = 'not' (('not' TRUE ) '&' ('not' c1)) by BINARITH:def 1
.= 'not' (FALSE '&' ('not' c1)) by MARGREL1:41
.= 'not' FALSE by MARGREL1:49 ;
hence TRUE 'or' c1 = TRUE by MARGREL1:41;
end;

theorem :: BINARI_4:18
for b1 being non empty Nat holds
( 0 <= (2 to_power (b1 -' 1)) - 1 & - (2 to_power (b1 -' 1)) <= 0 )
proof
defpred S1[ Nat] means ( 0 <= (2 to_power (a1 -' 1)) - 1 & - (2 to_power (a1 -' 1)) <= 0 );
1 - 1 = 0 ;
then 2 to_power (1 -' 1) = 2 to_power 0 by BINARITH:def 3
.= 1 by POWER:29 ;
then E14: S1[1] ;
E15: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume E16: ( 0 <= (2 to_power (c1 -' 1)) - 1 & - (2 to_power (c1 -' 1)) <= 0 ) ;
(c1 + 1) -' 1 = c1 by BINARITH:39;
then ( 2 > 1 & c1 -' 1 < (c1 + 1) -' 1 ) by NAT_2:11;
then 2 to_power (c1 -' 1) < 2 to_power ((c1 + 1) -' 1) by POWER:44;
hence S1[c1 + 1] by E16, XREAL_1:11;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E14, E15);
end;

theorem :: BINARI_4:19
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( ( b2 = 0* b1 & b3 = 0* b1 ) implies ( b2,b3 are_summable ) )
proof
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
assume E14: ( c2 = 0* c1 & c3 = 0* c1 ) ;
E15: ( 1 <= c1 & len c2 = c1 ) by FINSEQ_2:109, NAT_1:39;
then E16: c1 in Seg c1 by FINSEQ_1:3;
c2 /. c1 = (0* c1) . c1 by E14, E15, FINSEQ_4:24
.= (c1 |-> 0) . c1 by EUCLID:def 4
.= FALSE by E16, FINSEQ_2:70, MARGREL1:36 ;
then add_ovfl c2,c3 = ((FALSE '&' FALSE ) 'or' (FALSE '&' ((carry c2,c3) /. c1))) 'or' (FALSE '&' ((carry c2,c3) /. c1)) by E14, BINARITH:def 9
.= (FALSE 'or' (FALSE '&' ((carry c2,c3) /. c1))) 'or' (FALSE '&' ((carry c2,c3) /. c1)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' ((carry c2,c3) /. c1)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence c2,c3 are_summable by BINARITH:def 10;
end;

theorem E14: :: BINARI_4:20
for b1 being non empty Nat
for b2 being Integer holds (b2 * b1) mod b1 = 0
proof
let c1 be non empty Nat;
let c2 be Integer;
(c2 * c1) mod c1 = ((c2 mod c1) * (c1 mod c1)) mod c1 by INT_3:15
.= ((c2 mod c1) * (c1 mod c1)) mod c1 by SCMFSA9A:5
.= ((c2 mod c1) * 0) mod c1 by GR_CY_1:5
.= 0 mod c1 by SCMFSA9A:5 ;
hence (c2 * c1) mod c1 = 0 by GR_CY_1:6;
end;

definition
let c1, c2 be Nat;
func MajP a1,a2 -> Nat means :E15: :: BINARI_4:def 1
( 2 to_power a3 >= a2 & a3 >= a1 & for b1 being Nat holds
( ( 2 to_power b1 >= a2 & b1 >= a1 ) implies ( b1 >= a3 ) ) );
existence
ex b1 being Nat st
( 2 to_power b1 >= c2 & b1 >= c1 & for b2 being Nat holds
( ( 2 to_power b2 >= c2 & b2 >= c1 ) implies ( b2 >= b1 ) ) )
proof
per cases not ( not 2 to_power c1 >= c2 & not 2 to_power c1 < c2 ) ;
suppose E15: 2 to_power c1 >= c2 ;
for b1 being Nat holds
( ( 2 to_power b1 >= c2 & b1 >= c1 ) implies ( b1 >= c1 ) ) ;
hence ex b1 being Nat st
( 2 to_power b1 >= c2 & b1 >= c1 & for b2 being Nat holds
( ( 2 to_power b2 >= c2 & b2 >= c1 ) implies ( b2 >= b1 ) ) ) by E15;
end;
suppose E15: 2 to_power c1 < c2 ;
defpred S1[ Nat] means ( 2 to_power a1 >= c2 & a1 >= c1 );
2 to_power c1 >= c1 by E2;
then ( 2 to_power c2 >= c2 & c2 >= c1 ) by E15, E2, XREAL_1:2;
then E16: ex b1 being Nat st
S1[b1] ;
ex b1 being Nat st
( S1[b1] & for b2 being Nat holds
( S1[b2] implies b2 >= b1 ) ) from NAT_1:sch 5(E16);
hence ex b1 being Nat st
( 2 to_power b1 >= c2 & b1 >= c1 & for b2 being Nat holds
( ( 2 to_power b2 >= c2 & b2 >= c1 ) implies ( b2 >= b1 ) ) ) ;
end;
end;
end;
uniqueness
for b1, b2 being Nat holds
( ( 2 to_power b1 >= c2 & b1 >= c1 & for b3 being Nat holds
( ( 2 to_power b3 >= c2 & b3 >= c1 ) implies ( b3 >= b1 ) ) & 2 to_power b2 >= c2 & b2 >= c1 & for b3 being Nat holds
( ( 2 to_power b3 >= c2 & b3 >= c1 ) implies ( b3 >= b2 ) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Nat;
assume that E15: ( 2 to_power c3 >= c2 & c3 >= c1 & for b1 being Nat holds
( ( 2 to_power b1 >= c2 & b1 >= c1 ) implies ( b1 >= c3 ) ) )
and E16: ( 2 to_power c4 >= c2 & c4 >= c1 & for b1 being Nat holds
( ( 2 to_power b1 >= c2 & b1 >= c1 ) implies ( b1 >= c4 ) ) ) ;
( c3 >= c4 & c4 >= c3 ) by E15, E16;
hence c3 = c4 by XREAL_1:1;
end;
end;

:: deftheorem E15 defines MajP BINARI_4:def 1 :
for b1, b2, b3 being Nat holds
( b3 = MajP b1,b2 iff ( 2 to_power b3 >= b2 & b3 >= b1 & for b4 being Nat holds
( ( 2 to_power b4 >= b2 & b4 >= b1 ) implies ( b4 >= b3 ) ) ) );

theorem :: BINARI_4:21
for b1, b2, b3 being Nat holds
( b1 >= b2 implies MajP b3,b1 >= MajP b3,b2 )
proof
let c1, c2, c3 be Nat;
assume E16: c1 >= c2 ;
( 2 to_power (MajP c3,c1) >= c1 & MajP c3,c1 >= c3 ) by E15;
then ( 2 to_power (MajP c3,c1) >= c2 & MajP c3,c1 >= c3 ) by E16, XREAL_1:2;
hence MajP c3,c1 >= MajP c3,c2 by E15;
end;

theorem E16: :: BINARI_4:22
for b1, b2, b3 being Nat holds
( b1 >= b2 implies MajP b1,b3 >= MajP b2,b3 )
proof
let c1, c2, c3 be Nat;
assume E17: c1 >= c2 ;
E18: ( 2 to_power (MajP c1,c3) >= c3 & MajP c1,c3 >= c1 ) by E15;
then MajP c1,c3 >= c2 by E17, XREAL_1:2;
hence MajP c1,c3 >= MajP c2,c3 by E18, E15;
end;

theorem :: BINARI_4:23
for b1 being Nat holds
( b1 >= 1 implies MajP b1,1 = b1 )
proof
let c1 be Nat;
assume c1 >= 1 ;
then c1 >= 0 + 1 ;
then ( 2 > 1 & c1 > 0 ) ;
then E17: ( 2 to_power c1 >= 1 & c1 >= c1 ) by POWER:40;
for b1 being Nat holds
( ( 2 to_power b1 >= 1 & b1 >= c1 ) implies ( b1 >= c1 ) ) ;
hence MajP c1,1 = c1 by E17, E15;
end;

theorem E17: :: BINARI_4:24
for b1, b2 being Nat holds
( b1 <= 2 to_power b2 implies MajP b2,b1 = b2 )
proof
let c1, c2 be Nat;
assume E18: c1 <= 2 to_power c2 ;
for b1 being Nat holds
( ( 2 to_power b1 >= c1 & b1 >= c2 ) implies ( b1 >= c2 ) ) ;
hence MajP c2,c1 = c2 by E18, E15;
end;

theorem :: BINARI_4:25
for b1, b2 being Nat holds
not ( b1 > 2 to_power b2 & not MajP b2,b1 > b2 )
proof
let c1, c2 be Nat;
assume E18: c1 > 2 to_power c2 ;
2 to_power (MajP c2,c1) >= c1 by E15;
then 2 to_power (MajP c2,c1) > 2 to_power c2 by E18, XREAL_1:2;
hence MajP c2,c1 > c2 by PRE_FF:10;
end;

definition
let c1 be Nat;
let c2 be Integer;
func 2sComplement a1,a2 -> Tuple of a1,BOOLEAN equals :E18: :: BINARI_4:def 2
a1 -BinarySequence (abs ((2 to_power (MajP a1,(abs a2))) + a2)) if a2 < 0
otherwise a1 -BinarySequence (abs a2);
correctness
coherence
( ( c2 < 0 implies c1 -BinarySequence (abs ((2 to_power (MajP c1,(abs c2))) + c2)) is Tuple of c1,BOOLEAN ) & ( not c2 < 0 implies c1 -BinarySequence (abs c2) is Tuple of c1,BOOLEAN ) );
consistency
for b1 being Tuple of c1,BOOLEAN holds
verum;
;
end;

:: deftheorem E18 defines 2sComplement BINARI_4:def 2 :
for b1 being Nat
for b2 being Integer holds
( ( b2 < 0 implies 2sComplement b1,b2 = b1 -BinarySequence (abs ((2 to_power (