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