:: BINARI_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let X be non empty set ;
let D be non empty Subset of X;
let x, y be set ;
let a, b be Element of D;
:: original: IFEQ
redefine func IFEQ x,y,a,b -> Element of D;
coherence
IFEQ x,y,a,b is Element of D
proof end;
end;

Lm1: for n being Nat
for p, q being Tuple of n,BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
proof end;

definition
let n be Nat;
func Bin1 n -> Tuple of n,BOOLEAN means :Def1: :: BINARI_2:def 1
for i being Nat st i in Seg n holds
it /. i = IFEQ i,1,TRUE ,FALSE ;
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ i,1,TRUE ,FALSE
proof end;
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ i,1,TRUE ,FALSE ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ i,1,TRUE ,FALSE ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :
for n being Nat
for b2 being Tuple of n,BOOLEAN holds
( b2 = Bin1 n iff for i being Nat st i in Seg n holds
b2 /. i = IFEQ i,1,TRUE ,FALSE );

definition
let n be non empty Nat;
let x be Tuple of n,BOOLEAN ;
func Neg2 x -> Tuple of n,BOOLEAN equals :: BINARI_2:def 2
('not' x) + (Bin1 n);
correctness
coherence
('not' x) + (Bin1 n) is Tuple of n,BOOLEAN
;
;
end;

:: deftheorem defines Neg2 BINARI_2:def 2 :
for n being non empty Nat
for x being Tuple of n,BOOLEAN holds Neg2 x = ('not' x) + (Bin1 n);

definition
let n be Nat;
let x be Tuple of n,BOOLEAN ;
func Intval x -> Integer equals :Def3: :: BINARI_2:def 3
Absval x if x /. n = FALSE
otherwise (Absval x) - (2 to_power n);
correctness
coherence
( ( x /. n = FALSE implies Absval x is Integer ) & ( not x /. n = FALSE implies (Absval x) - (2 to_power n) is Integer ) )
;
consistency
for b1 being Integer holds verum
;
;
end;

:: deftheorem Def3 defines Intval BINARI_2:def 3 :
for n being Nat
for x being Tuple of n,BOOLEAN holds
( ( x /. n = FALSE implies Intval x = Absval x ) & ( not x /. n = FALSE implies Intval x = (Absval x) - (2 to_power n) ) );

definition
let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
func Int_add_ovfl z1,z2 -> Element of BOOLEAN equals :: BINARI_2:def 4
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry z1,z2) /. n);
correctness
coherence
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry z1,z2) /. n) is Element of BOOLEAN
;
;
end;

:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :
for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN holds Int_add_ovfl z1,z2 = (('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry z1,z2) /. n);

definition
let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
func Int_add_udfl z1,z2 -> Element of BOOLEAN equals :: BINARI_2:def 5
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry z1,z2) /. n));
correctness
coherence
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry z1,z2) /. n)) is Element of BOOLEAN
;
;
end;

:: deftheorem defines Int_add_udfl BINARI_2:def 5 :
for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN holds Int_add_udfl z1,z2 = ((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry z1,z2) /. n));

theorem :: BINARI_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BINARI_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BINARI_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1 being Tuple of 2,BOOLEAN st z1 = <*FALSE *> ^ <*FALSE *> holds
Intval z1 = 0
proof end;

theorem Th4: :: BINARI_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1 being Tuple of 2,BOOLEAN st z1 = <*TRUE *> ^ <*FALSE *> holds
Intval z1 = 1
proof end;

theorem :: BINARI_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1 being Tuple of 2,BOOLEAN st z1 = <*FALSE *> ^ <*TRUE *> holds
Intval z1 = - 2
proof end;

theorem :: BINARI_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1 being Tuple of 2,BOOLEAN st z1 = <*TRUE *> ^ <*TRUE *> holds
Intval z1 = - 1
proof end;

theorem Th7: :: BINARI_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat st i in Seg n & i = 1 holds
(Bin1 n) /. i = TRUE
proof end;

theorem Th8: :: BINARI_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat st i in Seg n & i <> 1 holds
(Bin1 n) /. i = FALSE
proof end;

theorem Th9: :: BINARI_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat holds Bin1 (m + 1) = (Bin1 m) ^ <*FALSE *>
proof end;

theorem Th10: :: BINARI_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat holds Intval ((Bin1 m) ^ <*FALSE *>) = 1
proof end;

theorem Th11: :: BINARI_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>
proof end;

theorem Th12: :: BINARI_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
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))
proof end;

theorem Th13: :: BINARI_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
proof end;

theorem Th14: :: BINARI_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))
proof end;

theorem Th15: :: BINARI_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for x being Tuple of m,BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power m)) - 1
proof end;

theorem Th16: :: BINARI_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*>
proof end;

theorem Th17: :: BINARI_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds (Intval (Neg2 (z ^ <*d*>))) + (IFEQ (Int_add_ovfl ('not' (z ^ <*d*>)),(Bin1 (m + 1))),FALSE ,0,(2 to_power (m + 1))) = - (Intval (z ^ <*d*>))
proof end;

theorem :: BINARI_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
proof end;

definition
let n be non empty Nat;
let x, y be Tuple of n,BOOLEAN ;
func x - y -> Tuple of n,BOOLEAN means :Def6: :: BINARI_2:def 6
for i being Nat st i in Seg n holds
it /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i);
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i)
proof end;
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines - BINARI_2:def 6 :
for n being non empty Nat
for x, y, b4 being Tuple of n,BOOLEAN holds
( b4 = x - y iff for i being Nat st i in Seg n holds
b4 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) );

theorem Th19: :: BINARI_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for x, y being Tuple of m,BOOLEAN holds x - y = x + (Neg2 y)
proof end;

theorem :: BINARI_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl ('not' z2),(Bin1 m))) 'xor' (add_ovfl z1,(Neg2 z2)))*>
proof end;

theorem :: BINARI_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds (((Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0,(2 to_power (m + 1)))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))
proof end;