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))

A2: (z ^ <*d*>) /. (m + 1) = FALSE by A1, BINARITH:3;
A3: Intval (z ^ <*d*>) = Absval (z ^ <*d*>) by A2, 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 ;
A4: (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) = (Absval z) - 0 by A1, FUNCOP_1:def 8
.= Absval z ;
thus Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) by A3, A4; :: thesis: verum

end;

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

A6: (z ^ <*d*>) /. (m + 1) <> FALSE by A5, BINARITH:3;
A7: Intval (z ^ <*d*>) = (Absval (z ^ <*d*>)) - (2 to_power (m + 1)) by A6, 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) ;
thus Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0 ,(2 to_power m)) by A5, A7, FUNCOP_1:def 8; :: thesis: verum

end;

end;