let m be non empty Nat; :: thesis: for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m))
let z be Tuple of m, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m))
let d be Element of BOOLEAN ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m))

per cases ( d = FALSE or d = TRUE ) by XBOOLEAN:def 3;

suppose A1: d = FALSE ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m))

then (z ^ <*d*>) /. (m + 1) = FALSE by BINARITH:3;
then A3: Intval (z ^ <*d*>) = Absval (z ^ <*d*>) by Def3
.= (Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power m)) by BINARITH:46
.= (Absval z) + 0 by A1, FUNCOP_1:def 8
.= Absval z ;
(Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) = (Absval z) - 0 by A1, FUNCOP_1:def 8
.= Absval z ;
hence Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) by A3; :: thesis: verum

end;

suppose A5: d = TRUE ; :: thesis: Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m))

then (z ^ <*d*>) /. (m + 1) <> FALSE by BINARITH:3;
then Intval (z ^ <*d*>) = (Absval (z ^ <*d*>)) - (2 to_power (m + 1)) by Def3
.= ((Absval z) + (IFEQ d,FALSE ,0 ,(2 to_power m))) - (2 to_power (m + 1)) by BINARITH:46
.= ((Absval z) + (2 to_power m)) - (2 to_power (m + 1)) by A5, FUNCOP_1:def 8
.= ((Absval z) + (2 to_power m)) - ((2 to_power m) * (2 to_power 1)) by POWER:32
.= ((Absval z) + (2 to_power m)) - (2 * (2 to_power m)) by POWER:30
.= (Absval z) - (2 to_power m) ;
hence Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) by A5, FUNCOP_1:def 8; :: thesis: verum

end;

end;