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

definition
let f be FinSequence of REAL ;
func max_p f -> Nat means :Def1: :: RFINSEQ2:def 1
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max_p RFINSEQ2:def 1 :
for f being FinSequence of REAL
for b2 being Nat holds
( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of REAL ;
func min_p f -> Nat means :Def2: :: RFINSEQ2:def 2
( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds
it <= j ) ) ) );
existence
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines min_p RFINSEQ2:def 2 :
for f being FinSequence of REAL
for b2 being Nat holds
( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of REAL ;
func max f -> Real equals :: RFINSEQ2:def 3
f . (max_p f);
correctness
coherence
f . (max_p f) is Real
;
;
func min f -> Real equals :: RFINSEQ2:def 4
f . (min_p f);
correctness
coherence
f . (min_p f) is Real
;
;
end;

:: deftheorem defines max RFINSEQ2:def 3 :
for f being FinSequence of REAL holds max f = f . (max_p f);

:: deftheorem defines min RFINSEQ2:def 4 :
for f being FinSequence of REAL holds min f = f . (min_p f);

theorem Th1: :: RFINSEQ2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for i being Nat st 1 <= i & i <= len f holds
( f . i <= f . (max_p f) & f . i <= max f )
proof end;

theorem Th2: :: RFINSEQ2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for i being Nat st 1 <= i & i <= len f holds
( f . i >= f . (min_p f) & f . i >= min f )
proof end;

theorem :: RFINSEQ2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( max_p f = 1 & max f = r )
proof end;

theorem :: RFINSEQ2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for r being Real st f = <*r*> holds
( min_p f = 1 & min f = r )
proof end;

theorem :: RFINSEQ2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for r1, r2 being Real st f = <*r1,r2*> holds
( max f = max r1,r2 & max_p f = IFEQ r1,(max r1,r2),1,2 )
proof end;

theorem :: RFINSEQ2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for r1, r2 being Real st f = <*r1,r2*> holds
( min f = min r1,r2 & min_p f = IFEQ r1,(min r1,r2),1,2 )
proof end;

theorem :: RFINSEQ2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
max (f1 + f2) <= (max f1) + (max f2)
proof end;

theorem :: RFINSEQ2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds
min (f1 + f2) >= (min f1) + (min f2)
proof end;

theorem :: RFINSEQ2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for a being Real st len f > 0 & a > 0 holds
( max (a * f) = a * (max f) & max_p (a * f) = max_p f )
proof end;

theorem :: RFINSEQ2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for a being Real st len f > 0 & a > 0 holds
( min (a * f) = a * (min f) & min_p (a * f) = min_p f )
proof end;

theorem :: RFINSEQ2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st len f > 0 holds
( max (- f) = - (min f) & max_p (- f) = min_p f )
proof end;

theorem :: RFINSEQ2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st len f > 0 holds
( min (- f) = - (max f) & min_p (- f) = max_p f )
proof end;

theorem :: RFINSEQ2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL
for n being Nat st 1 <= n & n < len f holds
( max (f /^ n) <= max f & min (f /^ n) >= min f )
proof end;

Lm1: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g
proof end;

theorem Th14: :: RFINSEQ2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f = max g
proof end;

Lm2: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g
proof end;

theorem Th15: :: RFINSEQ2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f = min g
proof end;

definition
let f be FinSequence of REAL ;
func sort_d f -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent
by RFINSEQ:35;
uniqueness
for b1, b2 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
for f being FinSequence of REAL
for b2 being non-increasing FinSequence of REAL holds
( b2 = sort_d f iff f,b2 are_fiberwise_equipotent );

theorem Th16: :: RFINSEQ2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-decreasing
proof end;

theorem Th17: :: RFINSEQ2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being FinSequence of REAL holds
( R is non-decreasing iff for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n <= R . m )
proof end;

Lm3: for f, g being non-decreasing FinSequence of REAL
for n being Nat st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
proof end;

theorem Th18: :: RFINSEQ2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non-decreasing FinSequence of REAL
for n being Nat holds R | n is non-decreasing FinSequence of REAL
proof end;

Lm4: for n being Nat
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
proof end;

theorem Th19: :: RFINSEQ2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R1, R2 being non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2
proof end;

definition
let f be FinSequence of REAL ;
func sort_a f -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6
f,it are_fiberwise_equipotent ;
existence
ex b1 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent
by INTEGRA2:3;
uniqueness
for b1, b2 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
for f being FinSequence of REAL
for b2 being non-decreasing FinSequence of REAL holds
( b2 = sort_a f iff f,b2 are_fiberwise_equipotent );

theorem :: RFINSEQ2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non-increasing FinSequence of REAL holds sort_d f = f by Def5;

theorem :: RFINSEQ2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non-decreasing FinSequence of REAL holds sort_a f = f by Def6;

theorem :: RFINSEQ2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds sort_d (sort_d f) = sort_d f by Def5;

theorem :: RFINSEQ2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds sort_a (sort_a f) = sort_a f by Def6;

theorem Th24: :: RFINSEQ2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st f is non-increasing holds
- f is non-decreasing
proof end;

theorem Th25: :: RFINSEQ2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st f is non-decreasing holds
- f is non-increasing
proof end;

theorem Th26: :: RFINSEQ2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL
for P being Permutation of dom g st f = g * P & len g >= 1 holds
- f = (- g) * P
proof end;

theorem Th27: :: RFINSEQ2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
- f, - g are_fiberwise_equipotent
proof end;

theorem :: RFINSEQ2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds sort_d (- f) = - (sort_a f)
proof end;

theorem :: RFINSEQ2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds sort_a (- f) = - (sort_d f)
proof end;

theorem Th30: :: RFINSEQ2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds
( dom (sort_d f) = dom f & len (sort_d f) = len f )
proof end;

theorem Th31: :: RFINSEQ2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds
( dom (sort_a f) = dom f & len (sort_a f) = len f )
proof end;

theorem :: RFINSEQ2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st len f >= 1 holds
( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )
proof end;