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