:: BINARI_2 semantic presentation

definition
let c1 be non empty set ;
let c2 be non empty Subset of c1;
let c3, c4 be set ;
let c5, c6 be Element of c2;
redefine func IFEQ as IFEQ c3,c4,c5,c6 -> Element of a2;
coherence
IFEQ c3,c4,c5,c6 is Element of c2
proof
not ( not c3 = c4 & not c3 <> c4 ) ;
hence IFEQ c3,c4,c5,c6 is Element of c2 by CQC_LANG:def 1;
end;
end;

E1: for b1 being Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( ( len b2 = b1 & len b3 = b1 & ( for b4 being Nat holds
( b4 in Seg b1 implies b2 /. b4 = b3 /. b4 ) ) ) implies ( b2 = b3 ) )
proof
let c1 be Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
assume that
E2: ( len c2 = c1 & len c3 = c1 ) and
E3: for b1 being Nat holds
( b1 in Seg c1 implies c2 /. b1 = c3 /. b1 ) ;
for b1 being Nat holds
( b1 in Seg c1 implies c2 . b1 = c3 . b1 )
proof
let c4 be Nat;
assume E4: c4 in Seg c1 ;
then ( c4 in dom c2 & c4 in dom c3 ) by E2, FINSEQ_1:def 3;
then ( c2 /. c4 = c2 . c4 & c3 /. c4 = c3 . c4 ) by FINSEQ_4:def 4;
hence c2 . c4 = c3 . c4 by E3, E4;
end;
hence c2 = c3 by E2, FINSEQ_2:10;
end;

definition
let c1 be Nat;
func Bin1 c1 -> Tuple of a1,BOOLEAN means :E2: :: BINARI_2:def 1
for b1 being Nat holds
( b1 in Seg a1 implies a2 /. b1 = IFEQ b1,1,TRUE ,FALSE );
existence
ex b1 being Tuple of c1,BOOLEAN st
for b2 being Nat holds
( b2 in Seg c1 implies b1 /. b2 = IFEQ b2,1,TRUE ,FALSE )
proof
deffunc H1( set ) -> Element of BOOLEAN = IFEQ a1,1,TRUE ,FALSE ;
consider c2 being FinSequence of BOOLEAN such that
E2: len c2 = c1 and
E3: for b1 being Nat holds
( b1 in Seg c1 implies c2 . b1 = H1(b1) ) from FINSEQ_2:sch 1();
 reconsider c3 = c2 as Tuple of c1,BOOLEAN by E2, FINSEQ_2:110;
take c3 ;
let c4 be Nat;
assume E4: c4 in Seg c1 ;
then c4 in dom c3 by E2, FINSEQ_1:def 3;
hence c3 /. c4 = c3 . c4 by FINSEQ_4:def 4
.= IFEQ c4,1,TRUE ,FALSE by E3, E4 ;

end;
uniqueness
for b1, b2 being Tuple of c1,BOOLEAN holds
( ( ( for b3 being Nat holds
( b3 in Seg c1 implies b1 /. b3 = IFEQ b3,1,TRUE ,FALSE ) ) & ( for b3 being Nat holds
( b3 in Seg c1 implies b2 /. b3 = IFEQ b3,1,TRUE ,FALSE ) ) ) implies ( b1 = b2 ) )
proof
let c2, c3 be Tuple of c1,BOOLEAN ;
assume that
E2: for b1 being Nat holds
( b1 in Seg c1 implies c2 /. b1 = IFEQ b1,1,TRUE ,FALSE ) and
E3: for b1 being Nat holds
( b1 in Seg c1 implies c3 /. b1 = IFEQ b1,1,TRUE ,FALSE ) ;
E4: ( len c2 = c1 & len c3 = c1 ) by FINSEQ_2:109;
now
let c4 be Nat;
assume E5: c4 in Seg c1 ;
then E6: ( c4 in dom c2 & c4 in dom c3 ) by E4, FINSEQ_1:def 3;
hence c2 . c4 = c2 /. c4 by FINSEQ_4:def 4
.= IFEQ c4,1,TRUE ,FALSE by E2, E5
.= c3 /. c4 by E3, E5
.= c3 . c4 by E6, FINSEQ_4:def 4 ;

end;
hence c2 = c3 by E4, FINSEQ_2:10;
end;
end;

:: deftheorem E2 defines Bin1 BINARI_2:def 1 :
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = Bin1 b1 iff for b3 being Nat holds
( b3 in Seg b1 implies b2 /. b3 = IFEQ b3,1,TRUE ,FALSE ) );

definition
let c1 be non empty Nat;
let c2 be Tuple of c1,BOOLEAN ;
func Neg2 c2 -> Tuple of a1,BOOLEAN equals :: BINARI_2:def 2
('not' a2) + (Bin1 a1);
correctness
coherence
('not' c2) + (Bin1 c1) is Tuple of c1,BOOLEAN ;
;
end;

:: deftheorem defines Neg2 BINARI_2:def 2 :
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds Neg2 b2 = ('not' b2) + (Bin1 b1);

definition
let c1 be Nat;
let c2 be Tuple of c1,BOOLEAN ;
func Intval c2 -> Integer equals :E3: :: BINARI_2:def 3
 Absval a2 if a2 /. a1 = FALSE
otherwise (Absval a2) - (2 to_power a1);
correctness
coherence
( ( c2 /. c1 = FALSE implies Absval c2 is Integer ) & ( not c2 /. c1 = FALSE implies (Absval c2) - (2 to_power c1) is Integer ) );
consistency
for b1 being Integer holds
verum;
;
end;

:: deftheorem E3 defines Intval BINARI_2:def 3 :
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds
( ( b2 /. b1 = FALSE implies Intval b2 = Absval b2 ) & ( not b2 /. b1 = FALSE implies Intval b2 = (Absval b2) - (2 to_power b1) ) );

definition
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
func Int_add_ovfl c2,c3 -> Element of BOOLEAN equals :: BINARI_2:def 4
(('not' (a2 /. a1)) '&' ('not' (a3 /. a1))) '&' ((carry a2,a3) /. a1);
correctness
coherence
(('not' (c2 /. c1)) '&' ('not' (c3 /. c1))) '&' ((carry c2,c3) /. c1) is Element of BOOLEAN ;
;
end;

:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds Int_add_ovfl b2,b3 = (('not' (b2 /. b1)) '&' ('not' (b3 /. b1))) '&' ((carry b2,b3) /. b1);

definition
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
func Int_add_udfl c2,c3 -> Element of BOOLEAN equals :: BINARI_2:def 5
((a2 /. a1) '&' (a3 /. a1)) '&' ('not' ((carry a2,a3) /. a1));
correctness
coherence
((c2 /. c1) '&' (c3 /. c1)) '&' ('not' ((carry c2,c3) /. c1)) is Element of BOOLEAN ;
;
end;

:: deftheorem defines Int_add_udfl BINARI_2:def 5 :
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds Int_add_udfl b2,b3 = ((b2 /. b1) '&' (b3 /. b1)) '&' ('not' ((carry b2,b3) /. b1));

theorem :: BINARI_2:1
canceled;

theorem :: BINARI_2:2
canceled;

theorem :: BINARI_2:3
for b1 being Tuple of 2,BOOLEAN holds
( b1 = <*FALSE *> ^ <*FALSE *> implies Intval b1 = 0 )
proof
let c1 be Tuple of 2,BOOLEAN ;
assume E4: c1 = <*FALSE *> ^ <*FALSE *> ;
consider c2, c3 being Nat such that
E5: Binary c1 = <*c2,c3*> by FINSEQ_2:120;
c1 = <*FALSE ,FALSE *> by E4, FINSEQ_1:def 9;
then E6: ( c1 /. 1 = FALSE & c1 /. 2 = FALSE ) by FINSEQ_4:26;
E7: 1 in Seg 1 by FINSEQ_1:5;
Seg 1 c= Seg 2 by FINSEQ_1:7;
then E8: (Binary c1) /. 1 = IFEQ (c1 /. 1),FALSE ,0,(2 to_power (1 -' 1)) by E7, BINARITH:def 6
.= 0 by E6, CQC_LANG:def 1 ;
E9: (Binary c1) /. 1 = c2 by E5, FINSEQ_4:26;
2 in Seg 2 by FINSEQ_1:5;
then E10: (Binary c1) /. 2 = IFEQ (c1 /. 2),FALSE ,0,(2 to_power (2 -' 1)) by BINARITH:def 6
.= 0 by E6, CQC_LANG:def 1 ;
(Binary c1) /. 2 = c3 by E5, FINSEQ_4:26;
then Absval c1 = addnat $$ <*0,0*> by E5, E8, E9, E10, BINARITH:def 7
.= addnat $$ (<*0*> ^ <*0*>) by FINSEQ_1:def 9
.= addnat . (addnat $$ <*0*>),(addnat $$ <*0*>) by FINSOP_1:6
.= addnat . 0,(addnat $$ <*0*>) by FINSOP_1:12
.= addnat . 0,0 by FINSOP_1:12
.= 0 + 0 by BINOP_2:def 23
.= 0 ;
hence Intval c1 = 0 by E6, E3;
end;

theorem E4: :: BINARI_2:4
for b1 being Tuple of 2,BOOLEAN holds
( b1 = <*TRUE *> ^ <*FALSE *> implies Intval b1 = 1 )
proof
let c1 be Tuple of 2,BOOLEAN ;
assume E5: c1 = <*TRUE *> ^ <*FALSE *> ;
consider c2, c3 being Nat such that
E6: Binary c1 = <*c2,c3*> by FINSEQ_2:120;
c1 = <*TRUE ,FALSE *> by E5, FINSEQ_1:def 9;
then E7: ( c1 /. 1 = TRUE & c1 /. 2 = FALSE ) by FINSEQ_4:26;
E8: 1 in Seg 1 by FINSEQ_1:5;
Seg 1 c= Seg 2 by FINSEQ_1:7;
then E9: (Binary c1) /. 1 = IFEQ (c1 /. 1),FALSE ,0,(2 to_power (1 -' 1)) by E8, BINARITH:def 6
.= 2 to_power (1 -' 1) by E7, CQC_LANG:def 1, MARGREL1:38 ;
1 - 1 = 0 ;
then 1 -' 1 = 0 by BINARITH:def 3;
then E10: (Binary c1) /. 1 = 1 by E9, POWER:29;
E11: (Binary c1) /. 1 = c2 by E6, FINSEQ_4:26;
2 in Seg 2 by FINSEQ_1:5;
then E12: (Binary c1) /. 2 = IFEQ (c1 /. 2),FALSE ,0,(2 to_power (2 -' 1)) by BINARITH:def 6
.= 0 by E7, CQC_LANG:def 1 ;
(Binary c1) /. 2 = c3 by E6, FINSEQ_4:26;
then Absval c1 = addnat $$ <*1,0*> by E6, E10, E11, E12, BINARITH:def 7
.= addnat $$ (<*1*> ^ <*0*>) by FINSEQ_1:def 9
.= addnat . (addnat $$ <*1*>),(addnat $$ <*0*>) by FINSOP_1:6
.= addnat . 1,(addnat $$ <*0*>) by FINSOP_1:12
.= addnat . 1,0 by FINSOP_1:12
.= 1 + 0 by BINOP_2:def 23
.= 1 ;
hence Intval c1 = 1 by E7, E3;
end;

theorem :: BINARI_2:5
for b1 being Tuple of 2,BOOLEAN holds
( b1 = <*FALSE *> ^ <*TRUE *> implies Intval b1 = - 2 )
proof
let c1 be Tuple of 2,BOOLEAN ;
assume E5: c1 = <*FALSE *> ^ <*TRUE *> ;
consider c2, c3 being Nat such that
E6: Binary c1 = <*c2,c3*> by FINSEQ_2:120;
c1 = <*FALSE ,TRUE *> by E5, FINSEQ_1:def 9;
then E7: ( c1 /. 1 = FALSE & c1 /. 2 = TRUE ) by FINSEQ_4:26;
then E8: Intval c1 = (Absval c1) - (2 to_power (1 + 1)) by E3, MARGREL1:38
.= (Absval c1) - ((2 to_power 1) * (2 to_power 1)) by POWER:32
.= (Absval c1) - (2 * (2 to_power 1)) by POWER:30
.= (Absval c1) - (2 * 2) by POWER:30
.= (Absval c1) - 4 ;
E9: 1 in Seg 1 by FINSEQ_1:5;
Seg 1 c= Seg 2 by FINSEQ_1:7;
then E10: (Binary c1) /. 1 = IFEQ (c1 /. 1),FALSE ,0,(2 to_power (1 -' 1)) by E9, BINARITH:def 6
.= 0 by E7, CQC_LANG:def 1 ;
E11: (Binary c1) /. 1 = c2 by E6, FINSEQ_4:26;
2 in Seg 2 by FINSEQ_1:5;
then E12: (Binary c1) /. 2 = IFEQ (c1 /. 2),FALSE ,0,(2 to_power (2 -' 1)) by BINARITH:def 6
.= 2 to_power (2 -' 1) by E7, CQC_LANG:def 1, MARGREL1:38 ;
2 - 1 = 1 ;
then 2 -' 1 = 1 by BINARITH:def 3;
then E13: (Binary c1) /. 2 = 2 by E12, POWER:30;
(Binary c1) /. 2 = c3 by E6, FINSEQ_4:26;
then Absval c1 = addnat $$ <*0,2*> by E6, E10, E11, E13, BINARITH:def 7
.= addnat $$ (<*0*> ^ <*2*>) by FINSEQ_1:def 9
.= addnat . (addnat $$ <*0*>),(addnat $$ <*2*>) by FINSOP_1:6
.= addnat . 0,(addnat $$ <*2*>) by FINSOP_1:12
.= addnat . 0,2 by FINSOP_1:12
.= 0 + 2 by BINOP_2:def 23
.= 2 ;
hence Intval c1 = - 2 by E8;
end;

theorem :: BINARI_2:6
for b1 being Tuple of 2,BOOLEAN holds
( b1 = <*TRUE *> ^ <*TRUE *> implies Intval b1 = - 1 )
proof
let c1 be Tuple of 2,BOOLEAN ;
assume E5: c1 = <*TRUE *> ^ <*TRUE *> ;
consider c2, c3 being Nat such that
E6: Binary c1 = <*c2,c3*> by FINSEQ_2:120;
c1 = <*TRUE ,TRUE *> by E5, FINSEQ_1:def 9;
then E7: ( c1 /. 1 <> FALSE & c1 /. 2 <> FALSE ) by FINSEQ_4:26, MARGREL1:38;
then E8: Intval c1 = (Absval c1) - (2 to_power (1 + 1)) by E3
.= (Absval c1) - ((2 to_power 1) * (2 to_power 1)) by POWER:32
.= (Absval c1) - (2 * (2 to_power 1)) by POWER:30
.= (Absval c1) - (2 * 2) by POWER:30
.= (Absval c1) - 4 ;
E9: 1 in Seg 1 by FINSEQ_1:5;
Seg 1 c= Seg 2 by FINSEQ_1:7;
then E10: (Binary c1) /. 1 = IFEQ (c1 /. 1),FALSE ,0,(2 to_power (1 -' 1)) by E9, BINARITH:def 6
.= 2 to_power (1 -' 1) by E7, CQC_LANG:def 1 ;
1 - 1 = 0 ;
then 1 -' 1 = 0 by BINARITH:def 3;
then E11: (Binary c1) /. 1 = 1 by E10, POWER:29;
E12: (Binary c1) /. 1 = c2 by E6, FINSEQ_4:26;
2 in Seg 2 by FINSEQ_1:5;
then E13: (Binary c1) /. 2 = IFEQ (c1 /. 2),FALSE ,0,(2 to_power (2 -' 1)) by BINARITH:def 6
.= 2 to_power (2 -' 1) by E7, CQC_LANG:def 1 ;
2 - 1 = 1 ;
then 2 -' 1 = 1 by BINARITH:def 3;
then E14: (Binary c1) /. 2 = 2 by E13, POWER:30;
(Binary c1) /. 2 = c3 by E6, FINSEQ_4:26;
then Absval c1 = addnat $$ <*1,2*> by E6, E11, E12, E14, BINARITH:def 7
.= addnat $$ (<*1*> ^ <*2*>) by FINSEQ_1:def 9
.= addnat . (addnat $$ <*1*>),(addnat $$ <*2*>) by FINSOP_1:6
.= addnat . 1,(addnat $$ <*2*>) by FINSOP_1:12
.= addnat . 1,2 by FINSOP_1:12
.= 1 + 2 by BINOP_2:def 23
.= 3 ;
hence Intval c1 = - 1 by E8;
end;

theorem E5: :: BINARI_2:7
for b1, b2 being Nat holds
( ( b2 in Seg b1 & b2 = 1 ) implies ( (Bin1 b1) /. b2 = TRUE ) )
proof
let c1, c2 be Nat;
assume that
E6: c2 in Seg c1 and
E7: c2 = 1 ;
thus (Bin1 c1) /. c2 = IFEQ c2,1,TRUE ,FALSE by E6, E2
.= TRUE by E7, CQC_LANG:def 1 ;
end;

theorem E6: :: BINARI_2:8
for b1, b2 being Nat holds
( ( b2 in Seg b1 ) implies ( not b2 <> 1 or (Bin1 b1) /. b2 = FALSE ) )
proof
let c1, c2 be Nat;
assume that
E7: c2 in Seg c1 and
E8: c2 <> 1 ;
thus (Bin1 c1) /. c2 = IFEQ c2,1,TRUE ,FALSE by E7, E2
.= FALSE by E8, CQC_LANG:def 1 ;
end;

theorem E7: :: BINARI_2:9
for b1 being non empty Nat holds Bin1 (b1 + 1) = (Bin1 b1) ^ <*FALSE *>
proof
let c1 be non empty Nat;
E8: len (Bin1 (c1 + 1)) = c1 + 1 by FINSEQ_2:109;
E9: len ((Bin1 c1) ^ <*FALSE *>) = c1 + 1 by FINSEQ_2:109;
for b1 being Nat holds
( b1 in Seg (c1 + 1) implies (Bin1 (c1 + 1)) /. b1 = ((Bin1 c1) ^ <*FALSE *>) /. b1 )
proof
let c2 be Nat;
assume E10: c2 in Seg (c1 + 1) ;
per cases ( c2 in Seg c1 or c2 = c1 + 1 ) by E10, FINSEQ_2:8;
suppose E11: c2 in Seg c1 ;
thus (Bin1 (c1 + 1)) /. c2 = ((Bin1 c1) ^ <*FALSE *>) /. c2
proof
per cases not ( not c2 = 1 & not c2 <> 1 ) ;
suppose E12: c2 = 1 ;
((Bin1 c1) ^ <*FALSE *>) /. c2 = (Bin1 c1) /. c2 by E11, BINARITH:2
.= TRUE by E11, E12, E5 ;
hence (Bin1 (c1 + 1)) /. c2 = ((Bin1 c1) ^ <*FALSE *>) /. c2 by E10, E12, E5;
end;
suppose E12: c2 <> 1 ;
((Bin1 c1) ^ <*FALSE *>) /. c2 = (Bin1 c1) /. c2 by E11, BINARITH:2
.= FALSE by E11, E12, E6 ;
hence (Bin1 (c1 + 1)) /. c2 = ((Bin1 c1) ^ <*FALSE *>) /. c2 by E10, E12, E6;
end;
end;
end;
end;
suppose E11: c2 = c1 + 1 ;
1 <= c1 by NAT_1:39;
then 1 <> c1 + 1 by NAT_1:38;
then (Bin1 (c1 + 1)) /. c2 = FALSE by E10, E11, E6;
hence (Bin1 (c1 + 1)) /. c2 = ((Bin1 c1) ^ <*FALSE *>) /. c2 by E11, BINARITH:3;
end;
end;
end;
hence Bin1 (c1 + 1) = (Bin1 c1) ^ <*FALSE *> by E8, E9, E1;
end;

theorem E8: :: BINARI_2:10
for b1 being non empty Nat holds Intval ((Bin1 b1) ^ <*FALSE *>) = 1
proof
defpred S1[ non empty Nat] means Intval ((Bin1 a1) ^ <*FALSE *>) = 1;
E9: S1[1]
proof
consider c1 being Element of BOOLEAN such that
E10: Bin1 1 = <*c1*> by FINSEQ_2:117;
E11: (Bin1 1) /. 1 = c1 by E10, FINSEQ_4:25;
1 in Seg 1 by FINSEQ_1:5;
then Bin1 1 = <*TRUE *> by E10, E11, E5;
hence S1[1] by E4;
end;
E10: now
let c1 be non empty Nat;
assume E11: S1[c1] ;
((Bin1 c1) ^ <*FALSE *>) /. (c1 + 1) = FALSE by BINARITH:3;
then E12: Absval ((Bin1 c1) ^ <*FALSE *>) = 1 by E11, E3;
((Bin1 (c1 + 1)) ^ <*FALSE *>) /. ((c1 + 1) + 1) = FALSE by BINARITH:3;
then Intval ((Bin1 (c1 + 1)) ^ <*FALSE *>) = Absval ((Bin1 (c1 + 1)) ^ <*FALSE *>) by E3
.= Absval (((Bin1 c1) ^ <*FALSE *>) ^ <*FALSE *>) by E7
.= (Absval ((Bin1 c1) ^ <*FALSE *>)) + (IFEQ FALSE ,FALSE ,0,(2 to_power (c1 + 1))) by BINARITH:46
.= 1 + 0 by E12, CQC_LANG:def 1
.= 1 ;
hence S1[c1 + 1] ;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E9, E10);
end;

theorem E9: :: BINARI_2:11
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN
for b3 being Element of BOOLEAN holds 'not' (b2 ^ <*b3*>) = ('not' b2) ^ <*('not' b3)*>
proof
let c1 be non empty Nat;
let c2 be Tuple of c1,BOOLEAN ;
let c3 be Element of BOOLEAN ;
E10: len ('not' (c2 ^ <*c3*>)) = c1 + 1 by FINSEQ_2:109;
E11: len (('not' c2) ^ <*('not' c3)*>) = c1 + 1 by FINSEQ_2:109;
for b1 being Nat holds
( b1 in Seg (c1 + 1) implies ('not' (c2 ^ <*c3*>)) /. b1 = (('not' c2) ^ <*('not' c3)*>) /. b1 )
proof
let c4 be Nat;
assume E12: c4 in Seg (c1 + 1) ;
per cases ( c4 in Seg c1 or c4 = c1 + 1 ) by E12, FINSEQ_2:8;
suppose E13: c4 in Seg c1 ;
E14: ('not' (c2 ^ <*c3*>)) /. c4 = 'not' ((c2 ^ <*c3*>) /. c4) by E12, BINARITH:def 4
.= 'not' (c2 /. c4) by E13, BINARITH:2 ;
(('not' c2) ^ <*('not' c3)*>) /. c4 = ('not' c2) /. c4 by E13, BINARITH:2
.= 'not' (c2 /. c4) by E13, BINARITH:def 4 ;
hence ('not' (c2 ^ <*c3*>)) /. c4 = (('not' c2) ^ <*('not' c3)*>) /. c4 by E14;
end;
suppose E13: c4 = c1 + 1 ;
('not' (c2 ^ <*c3*>)) /. c4 = 'not' ((c2 ^ <*c3*>) /. c4) by E12, BINARITH:def 4
.= 'not' c3 by E13, BINARITH:3 ;
hence ('not' (c2 ^ <*c3*>)) /. c4 = (('not' c2) ^ <*('not' c3)*>) /. c4 by E13, BINARITH:3;
end;
end;
end;
hence 'not' (c2 ^ <*c3*>) = ('not' c2) ^ <*('not' c3)*> by E10, E11, E1;
end;

theorem E10: :: BINARI_2:12
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN
for b3 being Element of BOOLEAN holds Intval (b2 ^ <*b3*>) = (Absval b2) - (IFEQ b3,FALSE ,0,(2 to_power b1))
proof
let c1 be non empty Nat;
let c2 be Tuple of c1,BOOLEAN ;
let c3 be Element of BOOLEAN ;
per cases ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
suppose E11: c3 = FALSE ;
then (c2 ^ <*c3*>) /. (c1 + 1) = FALSE by BINARITH:3;
then E12: Intval (c2 ^ <*c3*>) = Absval (c2 ^ <*c3*>) by E3
.= (Absval c2) + (IFEQ c3,FALSE ,0,(2 to_power c1)) by BINARITH:46
.= (Absval c2) + 0 by E11, CQC_LANG:def 1
.= Absval c2 ;
(Absval c2) - (IFEQ c3,FALSE ,0,(2 to_power c1)) = (Absval c2) - 0 by E11, CQC_LANG:def 1
.= Absval c2 ;
hence Intval (c2 ^ <*c3*>) = (Absval c2) - (IFEQ c3,FALSE ,0,(2 to_power c1)) by E12;
end;
suppose E11: c3 = TRUE ;
then (c2 ^ <*c3*>) /. (c1 + 1) <> FALSE by BINARITH:3, MARGREL1:38;
then Intval (c2 ^ <*c3*>) = (Absval (c2 ^ <*c3*>)) - (2 to_power (c1 + 1)) by E3
.= ((Absval c2) + (IFEQ c3,FALSE ,0,(2 to_power c1))) - (2 to_power (c1 + 1)) by BINARITH:46
.= ((Absval c2) + (2 to_power c1)) - (2 to_power (c1 + 1)) by E11, CQC_LANG:def 1, MARGREL1:38
.= ((Absval c2) + (2 to_power c1)) - ((2 to_power c1) * (2 to_power 1)) by POWER:32
.= ((Absval c2) + (2 to_power c1)) - (2 * (2 to_power c1)) by POWER:30
.= (Absval c2) - (2 to_power c1) ;
hence Intval (c2 ^ <*c3*>) = (Absval c2) - (IFEQ c3,FALSE ,0,(2 to_power c1)) by E11, CQC_LANG:def 1, MARGREL1:38;
end;
end;
end;

theorem E11: :: BINARI_2:13
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN
for b4, b5 being Element of BOOLEAN holds ((Intval ((b2 ^ <*b4*>) + (b3 ^ <*b5*>))) + (IFEQ (Int_add_ovfl (b2 ^ <*b4*>),(b3 ^ <*b5*>)),FALSE ,0,(2 to_power (b1 + 1)))) - (IFEQ (Int_add_udfl (b2 ^ <*b4*>),(b3 ^ <*b5*>)),FALSE ,0,(2 to_power (b1 + 1))) = (Intval (b2 ^ <*b4*>)) + (Intval (b3 ^ <*b5*>))
proof
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
let c4, c5 be Element of BOOLEAN ;
set c6 = FALSE ;
set c7 = TRUE ;
E12: Absval (c2 + c3) = ((Absval c2) + (Absval c3)) - (IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1))
proof
set c8 = Absval (c2 + c3);
set c9 = IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1);
((Absval (c2 + c3)) + (IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1))) - (IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1)) = Absval (c2 + c3) ;
hence Absval (c2 + c3) = ((Absval c2) + (Absval c3)) - (IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1)) by BINARITH:47;
end;
E13: Intval ((c2 ^ <*c4*>) + (c3 ^ <*c5*>)) = Intval ((c2 + c3) ^ <*((c4 'xor' c5) 'xor' (add_ovfl c2,c3))*>) by BINARITH:45
.= (((Absval c2) + (Absval c3)) - (IFEQ (add_ovfl c2,c3),FALSE ,0,(2 to_power c1))) - (IFEQ ((c4 'xor' c5) 'xor' (add_ovfl c2,c3)),FALSE ,0,(2 to_power c1)) by E12, E10 ;
E14: Int_add_ovfl (c2 ^ <*c4*>),(c3 ^ <*c5*>) = (('not' ((c2 ^ <*c4*>) /. (c1 + 1))) '&' ('not' ((c3 ^ <*c5*>) /. (c1 + 1)))) '&' ((carry (c2 ^ <*c4*>),(c3 ^ <*c5*>)) /. (c1 + 1))
.= (('not' c4) '&' ('not' ((c3 ^ <*c5*>) /. (c1 + 1)))) '&' ((carry (c2 ^ <*c4*>),(c3 ^ <*c5*>)) /. (c1 + 1)) by BINARITH:3
.= (('not' c4) '&' ('not' c5)) '&' ((carry (c2 ^ <*c4*>),(c3 ^ <*c5*>)) /. (c1 + 1)) by BINARITH:3
.= (('not' c4) '&' ('not' c5)) '&' (add_ovfl c2,c3) by BINARITH:44 ;
E15: Int_add_udfl (c2 ^ <*c4*>),(c3 ^ <*c5*>) = (((c2 ^ <*c4*>) /. (c1 + 1)) '&' ((c3 ^ <*c5*>) /. (c1 + 1))) '&' ('not' ((carry (c2 ^ <*c4*>),(c3 ^ <*c5*>)) /. (c1 + 1)))
.= (c4 '&' ((c3 ^ <*c5*>) /. (c1 + 1))) '&' ('not' ((carry (c2 ^ <*c4*>),(c3 ^ <*c5*>)) /. (c1 + 1))) by BINARITH:3
.= (c4 '&' c5) '&' ('not' ((carry (c2 ^