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

theorem Th1: :: BINARI_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat st m > 0 holds
m * 2 >= m + 1
proof end;

theorem Th2: :: BINARI_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat holds 2 to_power m >= m
proof end;

theorem :: BINARI_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat holds (0* m) + (0* m) = 0* m
proof end;

theorem Th4: :: BINARI_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, k being Nat st k <= l & l <= m & not k = l holds
( k + 1 <= l & l <= m )
proof end;

theorem Th5: :: BINARI_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for x, y being Tuple of n,BOOLEAN st x = 0* n & y = 0* n holds
carry x,y = 0* n
proof end;

theorem :: BINARI_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for x, y being Tuple of n,BOOLEAN st x = 0* n & y = 0* n holds
x + y = 0* n
proof end;

theorem :: BINARI_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for F being Tuple of n,BOOLEAN st F = 0* n holds
Intval F = 0
proof end;

theorem Th8: :: BINARI_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, k being Nat st l + m <= k - 1 holds
( l < k & m < k )
proof end;

theorem Th9: :: BINARI_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g, h, i being Integer st g <= h + i & h < 0 & i < 0 holds
( g < h & g < i )
proof end;

theorem Th10: :: BINARI_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE
proof end;

theorem Th11: :: BINARI_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
proof end;

theorem Th12: :: BINARI_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for z being Tuple of n,BOOLEAN st z /. n = TRUE holds
Absval z >= 2 to_power (n -' 1)
proof end;

theorem Th13: :: BINARI_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry (n -BinarySequence l),(n -BinarySequence m)) /. n = FALSE
proof end;

theorem Th14: :: BINARI_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m being Nat
for n being non empty Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
proof end;

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

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

theorem Th17: :: BINARI_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being boolean set holds TRUE 'or' x = TRUE
proof end;

theorem :: BINARI_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat holds
( 0 <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= 0 )
proof end;

theorem :: BINARI_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for x, y being Tuple of n,BOOLEAN st x = 0* n & y = 0* n holds
x,y are_summable
proof end;

theorem Th20: :: BINARI_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for i being Integer holds (i * n) mod n = 0
proof end;

definition
let m, j be Nat;
func MajP m,j -> Nat means :Def1: :: BINARI_4:def 1
( 2 to_power it >= j & it >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= it ) );
existence
ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) & 2 to_power b2 >= j & b2 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines MajP BINARI_4:def 1 :
for m, j, b3 being Nat holds
( b3 = MajP m,j iff ( 2 to_power b3 >= j & b3 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b3 ) ) );

theorem :: BINARI_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, k, m being Nat st j >= k holds
MajP m,j >= MajP m,k
proof end;

theorem Th22: :: BINARI_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, j being Nat st l >= m holds
MajP l,j >= MajP m,j
proof end;

theorem :: BINARI_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat st m >= 1 holds
MajP m,1 = m
proof end;

theorem Th24: :: BINARI_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, m being Nat st j <= 2 to_power m holds
MajP m,j = m
proof end;

theorem :: BINARI_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, m being Nat st j > 2 to_power m holds
MajP m,j > m
proof end;

definition
let m be Nat;
let i be Integer;
func 2sComplement m,i -> Tuple of m,BOOLEAN equals :Def2: :: BINARI_4:def 2
m -BinarySequence (abs ((2 to_power (MajP m,(abs i))) + i)) if i < 0
otherwise m -BinarySequence (abs i);
correctness
coherence
( ( i < 0 implies m -BinarySequence (abs ((2 to_power (MajP m,(abs i))) + i)) is Tuple of m,BOOLEAN ) & ( not i < 0 implies m -BinarySequence (abs i) is Tuple of m,BOOLEAN ) )
;
consistency
for b1 being Tuple of m,BOOLEAN holds verum
;
;
end;

:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :
for m being Nat
for i being Integer holds
( ( i < 0 implies 2sComplement m,i = m -BinarySequence (abs ((2 to_power (MajP m,(abs i))) + i)) ) & ( not i < 0 implies 2sComplement m,i = m -BinarySequence (abs i) ) );

theorem :: BINARI_4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat holds 2sComplement m,0 = 0* m
proof end;

theorem :: BINARI_4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds
Intval (2sComplement n,i) = i
proof end;

Lm1: for n being non empty Nat
for k, l being Nat st k mod n = l mod n & k > l holds
ex s being Integer st k = l + (s * n)
proof end;

Lm2: for n being non empty Nat
for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
proof end;

Lm3: for n being non empty Nat
for k, l, m being Nat st m < n & k mod (2 to_power n) = l mod (2 to_power n) holds
(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
proof end;

Lm4: for n being non empty Nat
for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds
((2 to_power (MajP n,(abs h))) + h) mod (2 to_power n) = ((2 to_power (MajP n,(abs i))) + i) mod (2 to_power n)
proof end;

Lm5: for n being non empty Nat
for h, i being Integer st h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
proof end;

Lm6: for n being non empty Nat
for h, i being Integer st h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
proof end;

theorem :: BINARI_4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i by Lm5, Lm6;

theorem :: BINARI_4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds
2sComplement n,h = 2sComplement n,i
proof end;

theorem Th30: :: BINARI_4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
proof end;

theorem :: BINARI_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for l, m being Nat st l,m are_congruent_mod 2 to_power n holds
n -BinarySequence l = n -BinarySequence m
proof end;

theorem Th32: :: BINARI_4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for i being Integer
for j being Nat st 1 <= j & j <= n holds
(2sComplement (n + 1),i) /. j = (2sComplement n,i) /. j
proof end;

theorem Th33: :: BINARI_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for i being Integer ex x being Element of BOOLEAN st 2sComplement (m + 1),i = (2sComplement m,i) ^ <*x*>
proof end;

theorem :: BINARI_4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, l being Nat ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>
proof end;

theorem Th35: :: BINARI_4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h, i being Integer
for n being non empty Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
(carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1) = TRUE
proof end;

theorem :: BINARI_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h, i being Integer
for n being non empty Nat st - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds
Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i
proof end;

theorem :: BINARI_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h, i being Integer
for n being non empty Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h + i <= (2 to_power ((n + 1) -' 1)) - 1 & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i
proof end;

theorem :: BINARI_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h, i being Integer
for n being non empty Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds
Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i
proof end;