let n be non zero Nat; for z being Tuple of n, BOOLEAN
for d being Element of BOOLEAN holds Absval (z ^ <*d*>) = (Absval z) + (IFEQ (d,FALSE,0,(2 to_power n)))
let z be Tuple of n, BOOLEAN ; for d being Element of BOOLEAN holds Absval (z ^ <*d*>) = (Absval z) + (IFEQ (d,FALSE,0,(2 to_power n)))
let d be Element of BOOLEAN ; Absval (z ^ <*d*>) = (Absval z) + (IFEQ (d,FALSE,0,(2 to_power n)))
for i being Nat st i in Seg (n + 1) holds
((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i = IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1)))
proof
A1:
Seg (n + 1) = (Seg n) \/ {.(n + 1).}
by FINSEQ_1:9;
let i be
Nat;
( i in Seg (n + 1) implies ((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i = IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1))) )
assume A2:
i in Seg (n + 1)
;
((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i = IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1)))
per cases
( i in Seg n or i in {.(n + 1).} )
by A2, A1, XBOOLE_0:def 3;
suppose A3:
i in Seg n
;
((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i = IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1)))hence ((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i =
(Binary z) /. i
by Th1
.=
IFEQ (
(z /. i),
FALSE,
0,
(2 to_power (i -' 1)))
by A3, Def3
.=
IFEQ (
((z ^ <*d*>) /. i),
FALSE,
0,
(2 to_power (i -' 1)))
by A3, Th1
;
verum end; suppose
i in {.(n + 1).}
;
((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i = IFEQ (((z ^ <*d*>) /. i),FALSE,0,(2 to_power (i -' 1)))then A4:
i = n + 1
by TARSKI:def 1;
hence ((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>) /. i =
IFEQ (
d,
FALSE,
0,
(2 to_power n))
by Th2
.=
IFEQ (
((z ^ <*d*>) /. i),
FALSE,
0,
(2 to_power n))
by A4, Th2
.=
IFEQ (
((z ^ <*d*>) /. i),
FALSE,
0,
(2 to_power (i -' 1)))
by A4, NAT_D:34
;
verum end; end;
end;
hence Absval (z ^ <*d*>) =
addnat $$ ((Binary z) ^ <*(IFEQ (d,FALSE,0,(2 to_power n)))*>)
by Def3
.=
addnat . ((addnat $$ (Binary z)),(IFEQ (d,FALSE,0,(2 to_power n))))
by FINSOP_1:4
.=
(Absval z) + (IFEQ (d,FALSE,0,(2 to_power n)))
by BINOP_2:def 23
;
verum