:: REARRAN1 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be real-membered set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be Real;
redefine func (#) as c₄ (#) c₃ -> Element of PFuncs a₁,REAL ;
coherence

proof end;

end;

Lemma1: for b₁ being Function
for b₂ being set st not b₂ in rng b₁ holds
b₁ " {b₂} = {}

proof end;

definition

let c₁ be FinSequence;
attr a₁ is terms've_same_card_as_number means :Def1: :: REARRAN1:def 1
for b₁ being Nat st 1 <= b₁ & b₁ <= len a₁ holds
for b₂ being finite set st b₂ = a₁ . b₁ holds
card b₂ = b₁;
attr a₁ is ascending means :Def2: :: REARRAN1:def 2
for b₁ being Nat st 1 <= b₁ & b₁ <= (len a₁) - 1 holds
a₁ . b₁ c= a₁ . (b₁ + 1);

end;

:: deftheorem Def1 defines terms've_same_card_as_number REARRAN1:def 1 :

:: deftheorem Def2 defines ascending REARRAN1:def 2 :

Lemma4: for b₁ being non empty finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
b₂ . b₃ is finite

proof end;

Lemma5: for b₁ being non empty finite set
for b₂ being FinSequence of bool b₁ st len b₂ = card b₁ & b₂ is terms've_same_card_as_number holds
for b₃ being finite set st b₃ = b₂ . (len b₂) holds
b₃ = b₁

proof end;

Lemma6: for b₁ being non empty finite set ex b₂ being FinSequence of bool b₁ st
( len b₂ = card b₁ & b₂ is ascending & b₂ is terms've_same_card_as_number )

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
attr a₂ is lenght_equal_card_of_set means :Def3: :: REARRAN1:def 3
ex b₁ being finite set st
( b₁ = union a₁ & len a₂ = card b₁ );

end;

:: deftheorem Def3 defines lenght_equal_card_of_set REARRAN1:def 3 :

registration

let c₁ be non empty finite set ;
cluster terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool a₁;
existence

proof end;

end;

definition

let c₁ be non empty finite set ;
mode RearrangmentGen of a₁ is terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool a₁;

end;

theorem Th1: :: REARRAN1:1

for b₁ being non empty finite set
for b₂ being FinSequence of bool b₁ holds
( b₂ is lenght_equal_card_of_set iff len b₂ = card b₁ )

proof end;

theorem Th2: :: REARRAN1:2

for b₁ being FinSequence holds
( b₁ is ascending iff for b₂, b₃ being Nat st b₂ <= b₃ & b₂ in dom b₁ & b₃ in dom b₁ holds
b₁ . b₂ c= b₁ . b₃ )

proof end;

theorem Th3: :: REARRAN1:3

for b₁ being non empty finite set
for b₂ being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool b₁ holds b₂ . (len b₂) = b₁

proof end;

theorem Th4: :: REARRAN1:4

for b₁ being non empty finite set
for b₂ being lenght_equal_card_of_set FinSequence of bool b₁ holds len b₂ <> 0

proof end;

theorem Th5: :: REARRAN1:5

for b₁ being non empty finite set
for b₂ being terms've_same_card_as_number ascending FinSequence of bool b₁
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ & b₃ <> b₄ holds
b₂ . b₃ <> b₂ . b₄

proof end;

theorem Th6: :: REARRAN1:6

for b₁ being non empty finite set
for b₂ being terms've_same_card_as_number ascending FinSequence of bool b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= (len b₂) - 1 holds
b₂ . b₃ <> b₂ . (b₃ + 1)

proof end;

Lemma14: for b₁ being Nat
for b₂ being non empty finite set
for b₃ being FinSequence of bool b₂ st b₁ in dom b₃ holds
b₃ . b₁ c= b₂

proof end;

theorem Th7: :: REARRAN1:7

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being terms've_same_card_as_number FinSequence of bool b₂ st b₁ in dom b₃ holds
b₃ . b₁ <> {}

proof end;

theorem Th8: :: REARRAN1:8

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being terms've_same_card_as_number FinSequence of bool b₂ st 1 <= b₁ & b₁ <= (len b₃) - 1 holds
(b₃ . (b₁ + 1)) \ (b₃ . b₁) <> {}

proof end;

theorem Th9: :: REARRAN1:9

for b₁ being non empty finite set
for b₂ being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool b₁ ex b₃ being Element of b₁ st b₂ . 1 = {b₃}

proof end;

theorem Th10: :: REARRAN1:10

for b₁ being Nat
for b₂ being non empty finite set
for b₃ being terms've_same_card_as_number ascending FinSequence of bool b₂ st 1 <= b₁ & b₁ <= (len b₃) - 1 holds
ex b₄ being Element of b₂ st
( (b₃ . (b₁ + 1)) \ (b₃ . b₁) = {b₄} & b₃ . (b₁ + 1) = (b₃ . b₁) \/ {b₄} & (b₃ . (b₁ + 1)) \ {b₄} = b₃ . b₁ )

proof end;

definition

let c₁ be non empty finite set ;
let c₂ be RearrangmentGen of c₁;
func Co_Gen c₂ -> RearrangmentGen of a₁ means :Def4: :: REARRAN1:def 4
for b₁ being Nat st 1 <= b₁ & b₁ <= (len a₃) - 1 holds
a₃ . b₁ = a₁ \ (a₂ . ((len a₂) - b₁));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Co_Gen REARRAN1:def 4 :

theorem Th11: :: REARRAN1:11

for b₁ being non empty finite set
for b₂ being RearrangmentGen of b₁ holds Co_Gen (Co_Gen b₂) = b₂

proof end;

theorem Th12: :: REARRAN1:12

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
len (MIM (FinS b₃,b₁)) = len (CHI b₄,b₂)

proof end;

definition

let c₁, c₂ be non empty finite set ;
let c₃ be RearrangmentGen of c₂;
let c₄ be PartFunc of c₁, REAL ;
func Rland c₄,c₃ -> PartFunc of a₂, REAL equals :: REARRAN1:def 5
Sum ((MIM (FinS a₄,a₁)) (#) (CHI a₃,a₂));
correctness ;
func Rlor c₄,c₃ -> PartFunc of a₂, REAL equals :: REARRAN1:def 6
Sum ((MIM (FinS a₄,a₁)) (#) (CHI (Co_Gen a₃),a₂));
correctness ;

end;

:: deftheorem Def5 defines Rland REARRAN1:def 5 :

:: deftheorem Def6 defines Rlor REARRAN1:def 6 :

theorem Th13: :: REARRAN1:13

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
dom (Rland b₃,b₄) = b₂

proof end;

theorem Th14: :: REARRAN1:14

for b₁, b₂ being non empty finite set
for b₃ being Element of b₁
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₁ st b₄ is total & card b₁ = card b₂ holds
( ( b₃ in b₅ . 1 implies ((MIM (FinS b₄,b₂)) (#) (CHI b₅,b₁)) # b₃ = MIM (FinS b₄,b₂) ) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₅ & b₃ in (b₅ . (b₆ + 1)) \ (b₅ . b₆) holds
((MIM (FinS b₄,b₂)) (#) (CHI b₅,b₁)) # b₃ = (b₆ |-> 0) ^ (MIM ((FinS b₄,b₂) /^ b₆)) ) )

proof end;

theorem Th15: :: REARRAN1:15

for b₁, b₂ being non empty finite set
for b₃ being Element of b₁
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₁ st b₄ is total & card b₁ = card b₂ holds
( ( b₃ in b₅ . 1 implies (Rland b₄,b₅) . b₃ = (FinS b₄,b₂) . 1 ) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₅ & b₃ in (b₅ . (b₆ + 1)) \ (b₅ . b₆) holds
(Rland b₄,b₅) . b₃ = (FinS b₄,b₂) . (b₆ + 1) ) )

proof end;

theorem Th16: :: REARRAN1:16

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
rng (Rland b₃,b₄) = rng (FinS b₃,b₁)

proof end;

theorem Th17: :: REARRAN1:17

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
Rland b₃,b₄, FinS b₃,b₁ are_fiberwise_equipotent

proof end;

theorem Th18: :: REARRAN1:18

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
FinS (Rland b₃,b₄),b₂ = FinS b₃,b₁

proof end;

theorem Th19: :: REARRAN1:19

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
Sum (Rland b₃,b₄),b₂ = Sum b₃,b₁

proof end;

theorem Th20: :: REARRAN1:20

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( FinS ((Rland b₄,b₅) - b₁),b₃ = FinS (b₄ - b₁),b₂ & Sum ((Rland b₄,b₅) - b₁),b₃ = Sum (b₄ - b₁),b₂ )

proof end;

theorem Th21: :: REARRAN1:21

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
dom (Rlor b₃,b₄) = b₂

proof end;

theorem Th22: :: REARRAN1:22

for b₁, b₂ being non empty finite set
for b₃ being Element of b₁
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₁ st b₄ is total & card b₁ = card b₂ holds
( ( b₃ in (Co_Gen b₅) . 1 implies (Rlor b₄,b₅) . b₃ = (FinS b₄,b₂) . 1 ) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len (Co_Gen b₅) & b₃ in ((Co_Gen b₅) . (b₆ + 1)) \ ((Co_Gen b₅) . b₆) holds
(Rlor b₄,b₅) . b₃ = (FinS b₄,b₂) . (b₆ + 1) ) )

proof end;

theorem Th23: :: REARRAN1:23

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
rng (Rlor b₃,b₄) = rng (FinS b₃,b₁)

proof end;

theorem Th24: :: REARRAN1:24

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
Rlor b₃,b₄, FinS b₃,b₁ are_fiberwise_equipotent

proof end;

theorem Th25: :: REARRAN1:25

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
FinS (Rlor b₃,b₄),b₂ = FinS b₃,b₁

proof end;

theorem Th26: :: REARRAN1:26

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
Sum (Rlor b₃,b₄),b₂ = Sum b₃,b₁

proof end;

theorem Th27: :: REARRAN1:27

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( FinS ((Rlor b₄,b₅) - b₁),b₃ = FinS (b₄ - b₁),b₂ & Sum ((Rlor b₄,b₅) - b₁),b₃ = Sum (b₄ - b₁),b₂ )

proof end;

theorem Th28: :: REARRAN1:28

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₂ = card b₁ holds
( Rlor b₃,b₄, Rland b₃,b₄ are_fiberwise_equipotent & FinS (Rlor b₃,b₄),b₂ = FinS (Rland b₃,b₄),b₂ & Sum (Rlor b₃,b₄),b₂ = Sum (Rland b₃,b₄),b₂ )

proof end;

theorem Th29: :: REARRAN1:29

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( max+ ((Rland b₄,b₅) - b₁), max+ (b₄ - b₁) are_fiberwise_equipotent & FinS (max+ ((Rland b₄,b₅) - b₁)),b₃ = FinS (max+ (b₄ - b₁)),b₂ & Sum (max+ ((Rland b₄,b₅) - b₁)),b₃ = Sum (max+ (b₄ - b₁)),b₂ )

proof end;

theorem Th30: :: REARRAN1:30

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( max- ((Rland b₄,b₅) - b₁), max- (b₄ - b₁) are_fiberwise_equipotent & FinS (max- ((Rland b₄,b₅) - b₁)),b₃ = FinS (max- (b₄ - b₁)),b₂ & Sum (max- ((Rland b₄,b₅) - b₁)),b₃ = Sum (max- (b₄ - b₁)),b₂ )

proof end;

theorem Th31: :: REARRAN1:31

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₁ = card b₂ holds
( len (FinS (Rland b₃,b₄),b₂) = card b₂ & 1 <= len (FinS (Rland b₃,b₄),b₂) )

proof end;

theorem Th32: :: REARRAN1:32

for b₁ being Nat
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₂ = card b₃ & b₁ in dom b₅ holds
(FinS (Rland b₄,b₅),b₃) | b₁ = FinS (Rland b₄,b₅),(b₅ . b₁)

proof end;

theorem Th33: :: REARRAN1:33

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₂ = card b₃ holds
Rland (b₄ - b₁),b₅ = (Rland b₄,b₅) - b₁

proof end;

theorem Th34: :: REARRAN1:34

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( max+ ((Rlor b₄,b₅) - b₁), max+ (b₄ - b₁) are_fiberwise_equipotent & FinS (max+ ((Rlor b₄,b₅) - b₁)),b₃ = FinS (max+ (b₄ - b₁)),b₂ & Sum (max+ ((Rlor b₄,b₅) - b₁)),b₃ = Sum (max+ (b₄ - b₁)),b₂ )

proof end;

theorem Th35: :: REARRAN1:35

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₃ = card b₂ holds
( max- ((Rlor b₄,b₅) - b₁), max- (b₄ - b₁) are_fiberwise_equipotent & FinS (max- ((Rlor b₄,b₅) - b₁)),b₃ = FinS (max- (b₄ - b₁)),b₂ & Sum (max- ((Rlor b₄,b₅) - b₁)),b₃ = Sum (max- (b₄ - b₁)),b₂ )

proof end;

theorem Th36: :: REARRAN1:36

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₁ = card b₂ holds
( len (FinS (Rlor b₃,b₄),b₂) = card b₂ & 1 <= len (FinS (Rlor b₃,b₄),b₂) )

proof end;

theorem Th37: :: REARRAN1:37

for b₁ being Nat
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₂ = card b₃ & b₁ in dom b₅ holds
(FinS (Rlor b₄,b₅),b₃) | b₁ = FinS (Rlor b₄,b₅),((Co_Gen b₅) . b₁)

proof end;

theorem Th38: :: REARRAN1:38

for b₁ being Real
for b₂, b₃ being non empty finite set
for b₄ being PartFunc of b₂, REAL
for b₅ being RearrangmentGen of b₃ st b₄ is total & card b₂ = card b₃ holds
Rlor (b₄ - b₁),b₅ = (Rlor b₄,b₅) - b₁

proof end;

theorem Th39: :: REARRAN1:39

for b₁, b₂ being non empty finite set
for b₃ being PartFunc of b₁, REAL
for b₄ being RearrangmentGen of b₂ st b₃ is total & card b₁ = card b₂ holds
( Rland b₃,b₄,b₃ are_fiberwise_equipotent & Rlor b₃,b₄,b₃ are_fiberwise_equipotent & rng (Rland b₃,b₄) = rng b₃ & rng (Rlor b₃,b₄) = rng b₃ )

proof end;