let z1 be Tuple of 2, BOOLEAN ; ( z1 = <*FALSE*> ^ <*TRUE*> implies Intval z1 = - 2 )
assume A1:
z1 = <*FALSE*> ^ <*TRUE*>
; Intval z1 = - 2
consider k1, k2 being Element of NAT such that
A2:
Binary z1 = <*k1,k2*>
by FINSEQ_2:100;
A3:
z1 = <*FALSE,TRUE*>
by A1, FINSEQ_1:def 9;
then A4:
z1 /. 1 = FALSE
by FINSEQ_4:17;
A5:
z1 /. 2 = TRUE
by A3, FINSEQ_4:17;
then A6: Intval z1 =
(Absval z1) - (2 to_power (1 + 1))
by Def3
.=
(Absval z1) - ((2 to_power 1) * (2 to_power 1))
by POWER:27
.=
(Absval z1) - (2 * (2 to_power 1))
by POWER:25
.=
(Absval z1) - (2 * 2)
by POWER:25
.=
(Absval z1) - 4
;
( 1 in Seg 1 & Seg 1 c= Seg 2 )
by FINSEQ_1:3, FINSEQ_1:5;
then A7: (Binary z1) /. 1 =
IFEQ ((z1 /. 1),FALSE,0,(2 to_power (1 -' 1)))
by BINARITH:def 3
.=
0
by A4, FUNCOP_1:def 8
;
2 in Seg 2
by FINSEQ_1:3;
then A8: (Binary z1) /. 2 =
IFEQ ((z1 /. 2),FALSE,0,(2 to_power (2 -' 1)))
by BINARITH:def 3
.=
2 to_power (2 -' 1)
by A5, FUNCOP_1:def 8
;
2 - 1 = 1
;
then
2 -' 1 = 1
by XREAL_0:def 2;
then A9:
(Binary z1) /. 2 = 2
by A8, POWER:25;
( (Binary z1) /. 1 = k1 & (Binary z1) /. 2 = k2 )
by A2, FINSEQ_4:17;
then Absval z1 =
addnat $$ <*0,2*>
by A2, A7, A9, BINARITH:def 4
.=
addnat $$ (<*0*> ^ <*2*>)
by FINSEQ_1:def 9
.=
addnat . ((addnat $$ <*0*>),(addnat $$ <*2*>))
by FINSOP_1:5
.=
addnat . (0,(addnat $$ <*2*>))
by FINSOP_1:11
.=
addnat . (0,2)
by FINSOP_1:11
.=
0 + 2
by BINOP_2:def 23
.=
2
;
hence
Intval z1 = - 2
by A6; verum