let z1 be Tuple of 2,BOOLEAN ; :: thesis: ( z1 = <*TRUE *> ^ <*TRUE *> implies Intval z1 = - 1 )
assume A1: z1 = <*TRUE *> ^ <*TRUE *> ; :: thesis: Intval z1 = - 1
consider k1, k2 being Element of NAT such that
A2: Binary z1 = <*k1,k2*> by FINSEQ_2:120;
z1 = <*TRUE ,TRUE *> by A1, FINSEQ_1:def 9;
then A3: ( z1 /. 1 <> FALSE & z1 /. 2 <> FALSE ) by FINSEQ_4:26;
then A4: Intval z1 = (Absval z1) - (2 to_power (1 + 1)) by Def3
.= (Absval z1) - ((2 to_power 1) * (2 to_power 1)) by POWER:32
.= (Absval z1) - (2 * (2 to_power 1)) by POWER:30
.= (Absval z1) - (2 * 2) by POWER:30
.= (Absval z1) - 4 ;
A5: 1 in Seg 1 by FINSEQ_1:5;
Seg 1 c= Seg 2 by FINSEQ_1:7;
then A6: (Binary z1) /. 1 = IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1)) by A5, BINARITH:def 6
.= 2 to_power (1 -' 1) by A3, FUNCOP_1:def 8 ;
1 - 1 = 0 ;
then 1 -' 1 = 0 by XREAL_0:def 2;
then A7: (Binary z1) /. 1 = 1 by A6, POWER:29;
A8: (Binary z1) /. 1 = k1 by A2, FINSEQ_4:26;
2 in Seg 2 by FINSEQ_1:5;
then A9: (Binary z1) /. 2 = IFEQ (z1 /. 2),FALSE ,0 ,(2 to_power (2 -' 1)) by BINARITH:def 6
.= 2 to_power (2 -' 1) by A3, FUNCOP_1:def 8 ;
2 - 1 = 1 ;
then 2 -' 1 = 1 by XREAL_0:def 2;
then A10: (Binary z1) /. 2 = 2 by A9, POWER:30;
(Binary z1) /. 2 = k2 by A2, FINSEQ_4:26;
then Absval z1 = addnat $$ <*1,2*> by A2, A7, A8, A10, 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 z1 = - 1 by A4; :: thesis: verum