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;
A4:
z1 /. 1 <> FALSE
by A3, FINSEQ_4:26;
A5:
z1 /. 2 <> FALSE
by A3, FINSEQ_4:26;
A6: Intval z1 =
(Absval z1) - (2 to_power (1 + 1))
by A5, 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
;
A7:
( 1 in Seg 1 & Seg 1 c= Seg 2 )
by FINSEQ_1:5, FINSEQ_1:7;
A8: (Binary z1) /. 1 =
IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1))
by A7, BINARITH:def 6
.=
2 to_power (1 -' 1)
by A4, FUNCOP_1:def 8
;
A9:
1 - 1 = 0
;
A10:
1 -' 1 = 0
by A9, XREAL_0:def 2;
A11:
(Binary z1) /. 1 = 1
by A8, A10, POWER:29;
A12:
2 in Seg 2
by FINSEQ_1:5;
A13: (Binary z1) /. 2 =
IFEQ (z1 /. 2),FALSE ,0 ,(2 to_power (2 -' 1))
by A12, BINARITH:def 6
.=
2 to_power (2 -' 1)
by A5, FUNCOP_1:def 8
;
A14:
2 - 1 = 1
;
A15:
2 -' 1 = 1
by A14, XREAL_0:def 2;
A16:
(Binary z1) /. 2 = 2
by A13, A15, POWER:30;
A17:
( (Binary z1) /. 1 = k1 & (Binary z1) /. 2 = k2 )
by A2, FINSEQ_4:26;
A18: Absval z1 =
addnat $$ <*1,2*>
by A2, A11, A16, A17, 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
;
thus
Intval z1 = - 1
by A6, A18; verum