:: BINARI_3 semantic presentation

theorem E1: :: BINARI_3:1
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds
Absval b2 < 2 to_power b1
proof
defpred S1[ non empty Nat] means for b1 being Tuple of a1,BOOLEAN holds
Absval b1 < 2 to_power a1;
E2: S1[1]
proof
let c1 be Tuple of 1,BOOLEAN ;
consider c2 being Element of BOOLEAN such that
E3: c1 = <*c2*> by FINSEQ_2:117;
( c2 = TRUE or c2 = FALSE ) by MARGREL1:39;
then ( Absval c1 = 1 or Absval c1 = 0 ) by E3, BINARITH:41, BINARITH:42;
then Absval c1 < 2 ;
hence Absval c1 < 2 to_power 1 by POWER:30;
end;
E3: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume E4: S1[c1] ;
let c2 be Tuple of (c1 + 1),BOOLEAN ;
consider c3 being Tuple of c1,BOOLEAN , c4 being Element of BOOLEAN such that
E5: c2 = c3 ^ <*c4*> by FINSEQ_2:137;
E6: Absval c2 = (Absval c3) + (IFEQ c4,FALSE ,0,(2 to_power c1)) by E5, BINARITH:46;
c1 < c1 + 1 by NAT_1:38;
then E7: 2 to_power c1 < 2 to_power (c1 + 1) by POWER:44;
E8: Absval c3 < 2 to_power c1 by E4;
per cases ( c4 = FALSE or c4 = TRUE ) by MARGREL1:39;
suppose c4 = FALSE ;
then Absval c2 = (Absval c3) + 0 by E6, CQC_LANG:def 1;
then Absval c2 < 2 to_power c1 by E4;
then (Absval c2) + (2 to_power c1) < (2 to_power c1) + (2 to_power (c1 + 1)) by E7, XREAL_1:10;
hence Absval c2 < 2 to_power (c1 + 1) by XREAL_1:8;
end;
suppose c4 = TRUE ;
then Absval c2 = (Absval c3) + (2 to_power c1) by E6, CQC_LANG:def 1, MARGREL1:38;
then Absval c2 < (2 to_power c1) + (2 to_power c1) by E8, XREAL_1:8;
then Absval c2 < (2 to_power c1) * 2 ;
then Absval c2 < (2 to_power c1) * (2 to_power 1) by POWER:30;
hence Absval c2 < 2 to_power (c1 + 1) by POWER:32;
end;
end;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E2, E3);
end;

theorem E2: :: BINARI_3:2
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( Absval b2 = Absval b3 implies b2 = b3 )
proof
defpred S1[ non empty Nat] means for b1, b2 being Tuple of a1,BOOLEAN holds
( Absval b1 = Absval b2 implies b1 = b2 );
E3: S1[1]
proof
let c1, c2 be Tuple of 1,BOOLEAN ;
consider c3 being Element of BOOLEAN such that
E4: c1 = <*c3*> by FINSEQ_2:117;
consider c4 being Element of BOOLEAN such that
E5: c2 = <*c4*> by FINSEQ_2:117;
assume E6: Absval c1 = Absval c2 ;
assume E7: c1 <> c2 ;
per cases ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
suppose E8: c3 = FALSE ;
then c4 = TRUE by E4, E5, E7, MARGREL1:39;
then ( Absval c1 = 0 & Absval c2 = 1 ) by E4, E5, E8, BINARITH:41, BINARITH:42;
hence not verum by E6;
end;
suppose E8: c3 = TRUE ;
then c4 = FALSE by E4, E5, E7, MARGREL1:39;
then ( Absval c1 = 1 & Absval c2 = 0 ) by E4, E5, E8, BINARITH:41, BINARITH:42;
hence not verum by E6;
end;
end;
end;
E4: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume E5: for b1, b2 being Tuple of c1,BOOLEAN holds
( Absval b1 = Absval b2 implies b1 = b2 ) ;
let c2, c3 be Tuple of (c1 + 1),BOOLEAN ;
consider c4 being Tuple of c1,BOOLEAN , c5 being Element of BOOLEAN such that
E6: c2 = c4 ^ <*c5*> by FINSEQ_2:137;
consider c6 being Tuple of c1,BOOLEAN , c7 being Element of BOOLEAN such that
E7: c3 = c6 ^ <*c7*> by FINSEQ_2:137;
assume E8: Absval c2 = Absval c3 ;
E9: (Absval c4) + (IFEQ c5,FALSE ,0,(2 to_power c1)) = Absval c2 by E6, BINARITH:46
.= (Absval c6) + (IFEQ c7,FALSE ,0,(2 to_power c1)) by E7, E8, BINARITH:46 ;
E10: c5 = c7
proof
assume E11: c5 <> c7 ;
per cases ( c5 = FALSE or c5 = TRUE ) by MARGREL1:39;
suppose E12: c5 = FALSE ;
then E13: IFEQ c7,FALSE ,0,(2 to_power c1) = 2 to_power c1 by E11, CQC_LANG:def 1;
IFEQ c5,FALSE ,0,(2 to_power c1) = 0 by E12, CQC_LANG:def 1;
then Absval c4 >= 2 to_power c1 by E9, E13, NAT_1:29;
hence not verum by E1;
end;
suppose E12: c5 = TRUE ;
then c7 = FALSE by E11, MARGREL1:39;
then E13: IFEQ c7,FALSE ,0,(2 to_power c1) = 0 by CQC_LANG:def 1;
IFEQ c5,FALSE ,0,(2 to_power c1) = 2 to_power c1 by E12, CQC_LANG:def 1, MARGREL1:38;
then Absval c6 >= 2 to_power c1 by E9, E13, NAT_1:29;
hence not verum by E1;
end;
end;
end;
then Absval c4 = Absval c6 by E9;
hence c2 = c3 by E5, E6, E7, E10;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E3, E4);
end;

theorem :: BINARI_3:3
for b1, b2 being FinSequence holds
( Rev b1 = Rev b2 implies b1 = b2 )
proof
let c1, c2 be FinSequence;
assume E3: Rev c1 = Rev c2 ;
thus c1 = Rev (Rev c1) by FINSEQ_6:29
.= c2 by E3, FINSEQ_6:29 ;
end;

theorem E3: :: BINARI_3:4
for b1 being Nat holds 0* (b1 + 1) = (0* b1) ^ <*0*>
proof
let c1 be Nat;
thus 0* (c1 + 1) = (c1 + 1) |-> 0 by EUCLID:def 4
.= (c1 |-> 0) ^ <*0*> by FINSEQ_2:74
.= (0* c1) ^ <*0*> by EUCLID:def 4 ;
end;

theorem E4: :: BINARI_3:5
for b1 being Nat holds 0* b1 in BOOLEAN *
proof
let c1 be Nat;
c1 |-> 0 is FinSequence of BOOLEAN by FINSEQ_2:77, MARGREL1:def 13;
then 0* c1 is FinSequence of BOOLEAN by EUCLID:def 4;
hence 0* c1 in BOOLEAN * by FINSEQ_1:def 11;
end;

theorem E5: :: BINARI_3:6
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = 0* b1 implies 'not' b2 = b1 |-> 1 )
proof
let c1 be Nat;
let c2 be Tuple of c1,BOOLEAN ;
assume E6: c2 = 0* c1 ;
E7: len ('not' c2) = c1 by FINSEQ_2:109
.= len (c1 |-> 1) by FINSEQ_2:69 ;
now
let c3 be Nat;
assume that E8: 1 <= c3
and E9: c3 <= len ('not' c2) ;
E10: ( len ('not' c2) = c1 & len c2 = c1 ) by FINSEQ_2:109;
then E11: c3 in Seg c1 by E8, E9, FINSEQ_1:3;
E12: c2 . c3 = (c1 |-> 0) . c3 by E6, EUCLID:def 4
.= FALSE by E11, FINSEQ_2:70, MARGREL1:36 ;
thus ('not' c2) . c3 = ('not' c2) /. c3 by E8, E9, FINSEQ_4:24
.= 'not' (c2 /. c3) by E11, BINARITH:def 4
.= 'not' FALSE by E8, E9, E10, E12, FINSEQ_4:24
.= 1 by MARGREL1:36, MARGREL1:41
.= (c1 |-> 1) . c3 by E11, FINSEQ_2:70 ;
end;
hence 'not' c2 = c1 |-> 1 by E7, FINSEQ_1:18;
end;

theorem E6: :: BINARI_3:7
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = 0* b1 implies Absval b2 = 0 )
proof
defpred S1[ Nat] means for b1 being Tuple of a1,BOOLEAN holds
( b1 = 0* a1 implies Absval b1 = 0 );
E7: S1[1]
proof
let c1 be Tuple of 1,BOOLEAN ;
assume c1 = 0* 1 ;
then c1 = 1 |-> 0 by EUCLID:def 4
.= <*FALSE *> by FINSEQ_2:73, MARGREL1:36 ;
hence Absval c1 = 0 by BINARITH:41;
end;
E8: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume E9: for b1 being Tuple of c1,BOOLEAN holds
( b1 = 0* c1 implies Absval b1 = 0 ) ;
let c2 be Tuple of (c1 + 1),BOOLEAN ;
0* c1 in BOOLEAN * by E4;
then E10: 0* c1 is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* c1) = c1 by JORDAN2B:8;
then reconsider c3 = 0* c1 as Tuple of c1,BOOLEAN by E10, FINSEQ_2:110;
assume c2 = 0* (c1 + 1) ;
hence Absval c2 = Absval (c3 ^ <*FALSE *>) by E3, MARGREL1:36
.= (Absval c3) + (IFEQ FALSE ,FALSE ,0,(2 to_power c1)) by BINARITH:46
.= 0 + (IFEQ FALSE ,FALSE ,0,(2 to_power c1)) by E9
.= 0 by CQC_LANG:def 1 ;

end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E7, E8);
end;

theorem :: BINARI_3:8
for b1 being non empty Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = 0* b1 implies Absval ('not' b2) = (2 to_power b1) - 1 )
proof
let c1 be non empty Nat;
let c2 be Tuple of c1,BOOLEAN ;
assume E7: c2 = 0* c1 ;
thus Absval ('not' c2) = ((- (Absval c2)) + (2 to_power c1)) - 1 by BINARI_2:15
.= ((- 0) + (2 to_power c1)) - 1 by E7, E6
.= (2 to_power c1) - 1 ;
end;

theorem :: BINARI_3:9
for b1 being Nat holds Rev (0* b1) = 0* b1
proof
let c1 be Nat;
E7: dom (Rev (0* c1)) = Seg (len (Rev (0* c1))) by FINSEQ_1:def 3
.= Seg (len (0* c1)) by FINSEQ_5:def 3
.= dom (0* c1) by FINSEQ_1:def 3 ;
now
let c2 be Nat;
assume E8: c2 in dom (0* c1) ;
then c2 in Seg (len (0* c1)) by FINSEQ_1:def 3;
then E9: c2 in Seg c1 by EUCLID:2;
then (c1 - c2) + 1 in Seg c1 by FINSEQ_5:2;
then E10: ((len (0* c1)) - c2) + 1 in Seg c1 by EUCLID:2;
thus (Rev (0* c1)) . c2 = (0* c1) . (((len (0* c1)) - c2) + 1) by E8, FINSEQ_5:61
.= (c1 |-> 0) . (((len (0* c1)) - c2) + 1) by EUCLID:def 4
.= 0 by E10, FINSEQ_2:70
.= (c1 |-> 0) . c2 by E9, FINSEQ_2:70
.= (0* c1) . c2 by EUCLID:def 4 ;
end;
hence Rev (0* c1) = 0* c1 by E7, FINSEQ_1:17;
end;

theorem :: BINARI_3:10
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds
( b2 = 0* b1 implies Rev ('not' b2) = 'not' b2 )
proof
let c1 be Nat;
let c2 be Tuple of c1,BOOLEAN ;
assume E7: c2 = 0* c1 ;
E8: dom (Rev ('not' c2)) = Seg (len (Rev ('not' c2))) by FINSEQ_1:def 3
.= Seg (len ('not' c2)) by FINSEQ_5:def 3
.= dom ('not' c2) by FINSEQ_1:def 3 ;
now
let c3 be Nat;
assume E9: c3 in dom ('not' c2) ;
then c3 in Seg (len ('not' c2)) by FINSEQ_1:def 3;
then E10: c3 in Seg c1 by FINSEQ_2:109;
then (c1 - c3) + 1 in Seg c1 by FINSEQ_5:2;
then E11: ((len ('not' c2)) - c3) + 1 in Seg c1 by FINSEQ_2:109;
thus (Rev ('not' c2)) . c3 = ('not' c2) . (((len ('not' c2)) - c3) + 1) by E9, FINSEQ_5:61
.= (c1 |-> 1) . (((len ('not' c2)) - c3) + 1) by E7, E5
.= 1 by E11, FINSEQ_2:70
.= (c1 |-> 1) . c3 by E10, FINSEQ_2:70
.= ('not' c2) . c3 by E7, E5 ;
end;
hence Rev ('not' c2) = 'not' c2 by E8, FINSEQ_1:17;
end;

theorem E7: :: BINARI_3:11
Bin1 1 = <*TRUE *>
proof
consider c1 being Element of BOOLEAN such that
E8: Bin1 1 = <*c1*> by FINSEQ_2:117;
1 in Seg 1 by FINSEQ_1:5;
then (Bin1 1) /. 1 = TRUE by BINARI_2:7;
hence Bin1 1 = <*TRUE *> by E8, FINSEQ_4:25;
end;

theorem E8: :: BINARI_3:12
for b1 being non empty Nat holds Absval (Bin1 b1) = 1
proof
defpred S1[ Nat] means Absval (Bin1 a1) = 1;
E9: S1[1] by E7, BINARITH:42;
E10: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c1 be non empty Nat;
assume E11: Absval (Bin1 c1) = 1 ;
thus Absval (Bin1 (c1 + 1)) = Absval ((Bin1 c1) ^ <*FALSE *>) by BINARI_2:9
.= (Absval (Bin1 c1)) + (IFEQ FALSE ,FALSE ,0,(2 to_power c1)) by BINARITH:46
.= (Absval (Bin1 c1)) + 0 by CQC_LANG:def 1
.= 1 by E11 ;
end;
thus for b1 being non empty Nat holds
S1[b1] from BINARITH:sch 1(E9, E10);
end;

theorem E9: :: BINARI_3:13
for b1, b2 being Element of BOOLEAN holds
( not ( b1 'or' b2 = TRUE & not b1 = TRUE & not b2 = TRUE ) & ( ( b1 = TRUE or b2 = TRUE ) implies b1 'or' b2 = TRUE ) & ( b1 'or' b2 = FALSE implies ( b1 = FALSE & b2 = FALSE ) ) & ( ( b1 = FALSE & b2 = FALSE ) implies ( b1 'or' b2 = FALSE ) ) )
proof
let c1, c2 be Element of BOOLEAN ;
thus not ( c1 'or' c2 = TRUE & not c1 = TRUE & not c2 = TRUE )
proof
assume c1 'or' c2 = TRUE ;
then ('not' c1) '&' ('not' c2) = 'not' TRUE by BINARITH:10;
then ('not' c1) '&' ('not' c2) = FALSE by MARGREL1:41;
then ( 'not' c1 = FALSE or 'not' c2 = FALSE ) by MARGREL1:45;
hence ( c1 = TRUE or c2 = TRUE ) by MARGREL1:41;
end;
thus ( ( c1 = TRUE or c2 = TRUE ) implies c1 'or' c2 = TRUE ) by BINARITH:19;
thus ( c1 'or' c2 = FALSE implies ( c1 = FALSE & c2 = FALSE ) )
proof
assume c1 'or' c2 = FALSE ;
then ('not' c1) '&' ('not' c2) = 'not' FALSE by BINARITH:10;
then ('not' c1) '&' ('not' c2) = TRUE by MARGREL1:41;
then ( 'not' c1 = TRUE & 'not' c2 = TRUE ) by MARGREL1:45;
hence ( c1 = FALSE & c2 = FALSE ) by MARGREL1:41;
end;
thus ( ( c1 = FALSE & c2 = FALSE ) implies ( c1 'or' c2 = FALSE ) ) by BINARITH:7;
end;

theorem E10: :: BINARI_3:14
for b1, b2 being Element of BOOLEAN holds
( add_ovfl <*b1*>,<*b2*> = TRUE iff ( b1 = TRUE & b2 = TRUE ) )
proof
let c1, c2 be Element of BOOLEAN ;
thus ( add_ovfl <*c1*>,<*c2*> = TRUE implies ( c1 = TRUE & c2 = TRUE ) )
proof
assume add_ovfl <*c1*>,<*c2*> = TRUE ;
then (((<*c1*> /. 1) '&' (<*c2*> /. 1)) 'or' ((<*c1*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1))) 'or' ((<*c2*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1)) = TRUE by BINARITH:def 9;
then E11: ( ((<*c1*> /. 1) '&' (<*c2*> /. 1)) 'or' ((<*c1*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1)) = TRUE or (<*c2*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1) = TRUE ) by E9;
now
per cases not ( not (<*c1*> /. 1) '&' (<*c2*> /. 1) = TRUE & not (<*c1*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1) = TRUE & not (<*c2*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1) = TRUE ) by E11, E9;
suppose (<*c1*> /. 1) '&' (<*c2*> /. 1) = TRUE ;
then ( <*c1*> /. 1 = TRUE & <*c2*> /. 1 = TRUE ) by MARGREL1:45;
hence ( c1 = TRUE & c2 = TRUE ) by FINSEQ_4:25;
end;
suppose (<*c1*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1) = TRUE ;
then (carry <*c1*>,<*c2*>) /. 1 = TRUE by MARGREL1:45;
hence ( c1 = TRUE & c2 = TRUE ) by BINARITH:def 5, MARGREL1:38;
end;
suppose (<*c2*> /. 1) '&' ((carry <*c1*>,<*c2*>) /. 1) = TRUE ;
then (carry <*c1*>,<*c2*>) /. 1 = TRUE by MARGREL1:45;
hence ( c1 = TRUE & c2 = TRUE ) by BINARITH:def 5, MARGREL1:38;
end;
end;
end;
hence ( c1 = TRUE & c2 = TRUE ) ;
end;
assume that E11: c1 = TRUE
and E12: c2 = TRUE ;
<*TRUE *> /. 1 = TRUE by FINSEQ_4:25;
then (<*TRUE *> /. 1) '&' (<*TRUE *> /. 1) = TRUE by MARGREL1:45;
then E13: ((<*TRUE *> /. 1) '&' (<*TRUE *> /. 1)) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1)) = TRUE by BINARITH:19;
thus add_ovfl <*c1*>,<*c2*> = (((<*TRUE *> /. 1) '&' (<*TRUE *> /. 1)) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1))) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1)) by E11, E12, BINARITH:def 9
.= TRUE by E13, BINARITH:19 ;
end;

theorem E11: :: BINARI_3:15
'not' <*FALSE *> = <*TRUE *>
proof
now
let c1 be Nat;
assume E12: c1 in Seg 1 ;
then E13: c1 = 1 by FINSEQ_1:4, TARSKI:def 1;
len <*FALSE *> = 1 by FINSEQ_2:109;
then E14: <*FALSE *> /. c1 = <*FALSE *> . 1 by E13, FINSEQ_4:24;
len ('not' <*FALSE *>) = 1 by FINSEQ_2:109;
hence ('not' <*FALSE *>) . c1 = ('not' <*FALSE *>) /. c1 by E13, FINSEQ_4:24
.= 'not' (<*FALSE *> /. c1) by E12, BINARITH:def 4
.= 'not' FALSE by E14, FINSEQ_1:57
.= TRUE by MARGREL1:41
.= <*TRUE *> . c1 by E13, FINSEQ_1:57 ;

end;
hence 'not' <*FALSE *> = <*TRUE *> by FINSEQ_2:139;
end;

theorem :: BINARI_3:16
'not' <*TRUE *> = <*FALSE *>
proof
now
let c1 be Nat;
assume E12: c1 in Seg 1 ;
then E13: c1 = 1 by FINSEQ_1:4, TARSKI:def 1;
len <*TRUE *> = 1 by FINSEQ_2:109;
then E14: <*TRUE *> /. c1 = <*TRUE *> . 1 by E13, FINSEQ_4:24;
len ('not' <*TRUE *>) = 1 by FINSEQ_2:109;
hence ('not' <*TRUE *>) . c1 = ('not' <*TRUE *>) /. c1 by E13, FINSEQ_4:24
.= 'not' (<*TRUE *> /. c1) by E12, BINARITH:def 4
.= 'not' TRUE by E14, FINSEQ_1:57
.= FALSE by MARGREL1:41
.= <*FALSE *> . c1 by E13, FINSEQ_1:57 ;

end;
hence 'not' <*TRUE *> = <*FALSE *> by FINSEQ_2:139;
end;

theorem :: BINARI_3:17
<*FALSE *> + <*FALSE *> = <*FALSE *>
proof
add_ovfl <*FALSE *>,<*FALSE *> <> TRUE by E10, MARGREL1:38;
then add_ovfl <*FALSE *>,<*FALSE *> = FALSE by MARGREL1:39;
then <*FALSE *>,<*FALSE *> are_summable by BINARITH:def 10;
then Absval (<*FALSE *> + <*FALSE *>) = (Absval <*FALSE *>) + (Absval <*FALSE *>) by BINARITH:48
.= (Absval <*FALSE *>) + 0 by BINARITH:41
.= Absval <*FALSE *> ;
hence <*FALSE *> + <*FALSE *> = <*FALSE *> by E2;
end;

theorem E12: :: BINARI_3:18
( <*FALSE *> + <*TRUE *> = <*TRUE *> & <*TRUE *> + <*FALSE *> = <*TRUE *> )
proof
add_ovfl <*FALSE *>,<*TRUE *> <> TRUE by E10, MARGREL1:38;
then add_ovfl <*FALSE *>,<*TRUE *> = FALSE by MARGREL1:39;
then <*FALSE *>,<*TRUE *> are_summable by BINARITH:def 10;
then Absval (<*FALSE *> + <*TRUE *>) = (Absval <*FALSE *>) + (Absval <*TRUE *>) by BINARITH:48
.= (Absval <*FALSE *>) + 1 by BINARITH:42
.= 0 + 1 by BINARITH:41
.= Absval <*TRUE *> by BINARITH:42 ;
hence <*FALSE *> + <*TRUE *> = <*TRUE *> by E2;
add_ovfl <*TRUE *>,<*FALSE *> <> TRUE by E10, MARGREL1:38;
then add_ovfl <*TRUE *>,<*FALSE *> = FALSE by MARGREL1:39;
then <*TRUE *>,<*FALSE *> are_summable by BINARITH:def 10;
then Absval (<*TRUE *> + <*FALSE *>) = (Absval <*TRUE *>) + (Absval <*FALSE *>) by BINARITH:48
.= (Absval <*TRUE *>) + 0 by BINARITH:41
.= Absval <*TRUE *> ;
hence <*TRUE *> + <*FALSE *> = <*TRUE *> by E2;
end;

theorem :: BINARI_3:19
<*TRUE *> + <*TRUE *> = <*FALSE *>
proof
E13: add_ovfl <*TRUE *>,<*TRUE *> = TRUE by E10;
Absval (<*TRUE *> + <*TRUE *>) = ((Absval (<*TRUE *> + <*TRUE *>)) + 2) - 2
.= ((Absval (<*TRUE *> + <*TRUE *>)) + (2 to_power 1)) - 2 by POWER:30
.= ((Absval (<*TRUE *> + <*TRUE *>)) + (IFEQ (add_ovfl <*TRUE *>,<*TRUE *>),FALSE ,0,(2 to_power 1))) - 2 by E13, CQC_LANG:def 1, MARGREL1:38
.= ((Absval <*TRUE *>) + (Absval <*TRUE *>)) - 2 by BINARITH:47
.= ((Absval <*TRUE *>) + 1) - 2 by BINARITH:42
.= (1 + 1) - 2 by BINARITH:42
.= Absval <*FALSE *> by BINARITH:41 ;
hence <*TRUE *> + <*TRUE *> = <*FALSE *> by E2;
end;

theorem E13: :: BINARI_3:20
for b1 being non empty Nat
for b2, b3 being Tuple of b1,BOOLEAN holds
( ( b2 /. b1 = TRUE & (carry b2,(Bin1 b1)) /. b1 = TRUE ) implies ( for b4 being non empty Nat holds
( ( b4 <= b1 ) implies ( not b4 <> 1 or ( b2 /. b4 = TRUE & (carry b2,(Bin1 b1)) /. b4 = TRUE ) ) ) ) )
proof
let c1 be non empty Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
assume that E14: c2 /. c1 = TRUE
and E15: (carry c2,(Bin1 c1)) /. c1 = TRUE ;
let c4 be non empty Nat;
E16: 1 <= c1 by NAT_1:39;
assume that E17: c4 <> 1
and E18: c4 <= c1 ;
defpred S1[ Nat] means ( a1 in Seg (c1 -' 1) implies ( c2 /. ((c1 -' a1) + 1) = TRUE & (carry c2,(Bin1 c1)) /. ((c1 -' a1) + 1) = TRUE ) );
E19: S1[1] by E14, E15, E16, AMI_5:4;
E20: for b1 being non empty Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c5 be non empty Nat;
assume that E21: S1[c5]
and E22: c5 + 1 in Seg (c1 -' 1) ;
E23: ( 1 <= c5 + 1 & c5 + 1 <= c1 -' 1 ) by E22, FINSEQ_1:3;
E24: 1 <= c5 by NAT_1:39;
E25: c5 < c1 -' 1 by E23, NAT_1:38;
then c5 < c1 - 1 by E16, BINARITH:50;
then c5 + 1 < c1 by XREAL_1:22;
then E26: c5 < c1 by NAT_1:38;
E27: c1 -' c5 < c1 by NAT_2:11;
c5 + 1 <= c1 - 1 by E16, E23, BINARITH:50;
then 1 <= (c1 - 1) - c5 by XREAL_1:21;
then 1 <= (c1 - c5) - 1 ;
then 1 + 1 <= c1 - c5 by XREAL_1:21;
then 1 + 1 <= c1 -' c5 by E26, BINARITH:50;
then E28: c1 -' c5 > 1 by NAT_1:38;
then c1 -' c5 in Seg c1 by E27, FINSEQ_1:3;
then (Bin1 c1) /. (c1 -' c5) = FALSE by E28, BINARI_2:8;
then E29: ( (c2 /. (c1 -' c5)) '&' ((Bin1 c1) /. (c1 -' c5)) = FALSE & ((Bin1 c1) /. (c1 -' c5)) '&' ((carry c2,(Bin1 c1)) /. (c1 -' c5)) = FALSE ) by MARGREL1:45;
TRUE = (((c2 /. (c1 -' c5)) '&' ((Bin1 c1) /. (c1 -' c5))) 'or' ((c2 /. (c1 -' c5)) '&' ((carry c2,(Bin1 c1)) /. (c1 -' c5)))) 'or' (((Bin1 c1) /. (c1 -' c5)) '&' ((carry c2,(Bin1 c1)) /. (c1 -' c5))) by E21, E24, E25, E27, E28, BINARITH:def 5, FINSEQ_1:3
.= ((c2 /. (c1 -' c5)) '&' ((Bin1 c1) /. (c1 -' c5))) 'or' ((c2 /. (c1 -' c5)) '&' ((carry c2,(Bin1 c1)) /. (c1 -' c5))) by E29, BINARITH:7
.= (c2 /. (c1 -' c5)) '&' ((carry c2,(Bin1 c1)) /. (c1 -' c5)) by E29, BINARITH:7 ;
then E30: ( c2 /. (c1 -' c5) = TRUE & (carry c2,(Bin1 c1)) /. (c1 -' c5) = TRUE ) by MARGREL1:45;
hence c2 /. ((c1 -' (c5 + 1)) + 1)