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:120;
A3:
z1 = <*TRUE,TRUE*>
by A1, FINSEQ_1:def 9;
then A4:
z1 /. 1 <> FALSE
by FINSEQ_4:26;
A5:
z1 /. 2 <> FALSE
by A3, FINSEQ_4:26;
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:32
.=
(Absval z1) - (2 * (2 to_power 1))
by POWER:30
.=
(Absval z1) - (2 * 2)
by POWER:30
.=
(Absval z1) - 4
;
( 1 in Seg 1 & Seg 1 c= Seg 2 )
by FINSEQ_1:5, FINSEQ_1:7;
then A8: (Binary z1) /. 1 =
IFEQ ((z1 /. 1),FALSE,0,(2 to_power (1 -' 1)))
by BINARITH:def 6
.=
2 to_power (1 -' 1)
by A4, FUNCOP_1:def 8
;
1 - 1 = 0
;
then
1 -' 1 = 0
by XREAL_0:def 2;
then A11:
(Binary z1) /. 1 = 1
by A8, POWER:29;
2 in Seg 2
by FINSEQ_1:5;
then A13: (Binary z1) /. 2 =
IFEQ ((z1 /. 2),FALSE,0,(2 to_power (2 -' 1)))
by BINARITH:def 6
.=
2 to_power (2 -' 1)
by A5, FUNCOP_1:def 8
;
2 - 1 = 1
;
then
2 -' 1 = 1
by XREAL_0:def 2;
then A16:
(Binary z1) /. 2 = 2
by A13, POWER:30;
( (Binary z1) /. 1 = k1 & (Binary z1) /. 2 = k2 )
by A2, FINSEQ_4:26;
then Absval z1 =
addnat $$ <*1,2*>
by A2, A11, A16, 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 A6; verum