:: HALLMAR1 semantic presentation

theorem Th1: :: HALLMAR1:1

for b₁, b₂ being finite set holds (card (b₁ \/ b₂)) + (card (b₁ /\ b₂)) = (card b₁) + (card b₂)

proof end;

scheme :: HALLMAR1:sch 1
s1{ F₁() -> Nat, P₁[ set ] } :

for b₁ being Nat st 1 <= b₁ & b₁ <= F₁() holds
P₁[b₁]

provided

E2: ( P₁[F₁()] & F₁() >= 2 ) and
E3: for b₁ being Nat st 1 <= b₁ & b₁ < F₁() & P₁[b₁ + 1] holds
P₁[b₁]

proof end;

scheme :: HALLMAR1:sch 2
s2{ P₁[ Nat] } :

P₁[1]

provided

E2: ex b₁ being Nat st
( b₁ > 1 & P₁[b₁] ) and
E3: for b₁ being Nat st b₁ >= 1 & P₁[b₁ + 1] holds
P₁[b₁]

proof end;

registration

let c₁ be non empty set ;
cluster non empty non-empty FinSequence of bool a₁;
existence

proof end;

end;

theorem Th2: :: HALLMAR1:2

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

proof end;

registration

let c₁ be finite set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
cluster a₂ . a₃ -> finite ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
let c₃ be set ;
func union c₂,c₃ -> set means :Def1: :: HALLMAR1:def 1
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being set st
( b₂ in a₃ & b₂ in dom a₂ & b₁ in a₂ . b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines union HALLMAR1:def 1 :

theorem Th3: :: HALLMAR1:3

for b₁ being set
for b₂ being FinSequence of bool b₁
for b₃ being set holds union b₂,b₃ c= b₁

proof end;

theorem Th4: :: HALLMAR1:4

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃, b₄ being set st b₃ c= b₄ holds
union b₂,b₃ c= union b₂,b₄

proof end;

registration

let c₁ be finite set ;
let c₂ be FinSequence of bool c₁;
let c₃ be set ;
cluster union a₂,a₃ -> finite ;
coherence

proof end;

end;

theorem Th5: :: HALLMAR1:5

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat st b₃ in dom b₂ holds
union b₂,{b₃} = b₂ . b₃

proof end;

theorem Th6: :: HALLMAR1:6

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ holds
union b₂,{b₃,b₄} = (b₂ . b₃) \/ (b₂ . b₄)

proof end;

theorem Th7: :: HALLMAR1:7

for b₁ being set
for b₂ being finite set
for b₃ being FinSequence of bool b₂
for b₄ being Nat st b₄ in b₁ & b₄ in dom b₃ holds
b₃ . b₄ c= union b₃,b₁

proof end;

theorem Th8: :: HALLMAR1:8

for b₁ being set
for b₂ being finite set
for b₃ being Nat
for b₄ being FinSequence of bool b₂ st b₃ in b₁ & b₃ in dom b₄ holds
union b₄,b₁ = (union b₄,(b₁ \ {b₃})) \/ (b₄ . b₃)

proof end;

theorem Th9: :: HALLMAR1:9

for b₁, b₂ being set
for b₃ being finite set
for b₄ being Nat
for b₅ being FinSequence of bool b₃ st b₄ in dom b₅ holds
union b₅,(({b₄} \/ b₁) \/ b₂) = (b₅ . b₄) \/ (union b₅,(b₁ \/ b₂))

proof end;

theorem Th10: :: HALLMAR1:10

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄, b₅ being set st b₄ <> b₅ & b₄ in b₂ . b₃ & b₅ in b₂ . b₃ holds
((b₂ . b₃) \ {b₄}) \/ ((b₂ . b₃) \ {b₅}) = b₂ . b₃

proof end;

definition

let c₁ be finite set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
let c₄ be set ;
func Cut c₂,c₃,c₄ -> FinSequence of bool a₁ means :Def2: :: HALLMAR1:def 2
( dom a₅ = dom a₂ & ( for b₁ being Nat st b₁ in dom a₅ holds
( ( a₃ = b₁ implies a₅ . b₁ = (a₂ . b₁) \ {a₄} ) & ( a₃ <> b₁ implies a₅ . b₁ = a₂ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Cut HALLMAR1:def 2 :

theorem Th11: :: HALLMAR1:11

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄ being set st b₃ in dom b₂ & b₄ in b₂ . b₃ holds
card ((Cut b₂,b₃,b₄) . b₃) = (card (b₂ . b₃)) - 1

proof end;

theorem Th12: :: HALLMAR1:12

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄, b₅ being set holds union (Cut b₂,b₃,b₄),(b₅ \ {b₃}) = union b₂,(b₅ \ {b₃})

proof end;

theorem Th13: :: HALLMAR1:13

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄, b₅ being set st not b₃ in b₅ holds
union b₂,b₅ = union (Cut b₂,b₃,b₄),b₅

proof end;

theorem Th14: :: HALLMAR1:14

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄, b₅ being set st b₃ in dom (Cut b₂,b₃,b₄) & b₅ c= dom (Cut b₂,b₃,b₄) & b₃ in b₅ holds
union (Cut b₂,b₃,b₄),b₅ = (union b₂,(b₅ \ {b₃})) \/ ((b₂ . b₃) \ {b₄})

proof end;

definition

let c₁ be finite set ;
let c₂ be FinSequence of bool c₁;
let c₃ be set ;
pred c₃ is_a_system_of_different_representatives_of c₂ means :Def3: :: HALLMAR1:def 3
ex b₁ being FinSequence of a₁ st
( b₁ = a₃ & dom a₂ = dom b₁ & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ in a₂ . b₂ ) & b₁ is one-to-one );

end;

:: deftheorem Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def 3 :

definition

let c₁ be finite set ;
let c₂ be FinSequence of bool c₁;
attr a₂ is Hall means :Def4: :: HALLMAR1:def 4
for b₁ being finite set st b₁ c= dom a₂ holds
card b₁ <= card (union a₂,b₁);

end;

:: deftheorem Def4 defines Hall HALLMAR1:def 4 :

theorem Th15: :: HALLMAR1:15

for b₁ being finite set
for b₂ being non empty FinSequence of bool b₁ st b₂ is Hall holds
b₂ is non-empty

proof end;

theorem Th16: :: HALLMAR1:16

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat st b₃ in dom b₂ & b₂ is Hall holds
card (b₂ . b₃) >= 1

proof end;

theorem Th17: :: HALLMAR1:17

for b₁ being non empty finite set
for b₂ being non empty FinSequence of bool b₁ st ( for b₃ being Nat st b₃ in dom b₂ holds
card (b₂ . b₃) = 1 ) & b₂ is Hall holds
ex b₃ being set st b₃ is_a_system_of_different_representatives_of b₂

proof end;

theorem Th18: :: HALLMAR1:18

for b₁ being finite set
for b₂ being FinSequence of bool b₁ st ex b₃ being set st b₃ is_a_system_of_different_representatives_of b₂ holds
b₂ is Hall

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
mode Reduction of c₂,c₃ -> FinSequence of bool a₁ means :Def5: :: HALLMAR1:def 5
( dom a₄ = dom a₂ & ( for b₁ being Nat st b₁ in dom a₂ & b₁ <> a₃ holds
a₂ . b₁ = a₄ . b₁ ) & a₄ . a₃ c= a₂ . a₃ );
existence

proof end;

end;

:: deftheorem Def5 defines Reduction HALLMAR1:def 5 :

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
mode Reduction of c₂ -> FinSequence of bool a₁ means :Def6: :: HALLMAR1:def 6
( dom a₃ = dom a₂ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₃ . b₁ c= a₂ . b₁ ) );
existence

proof end;

end;

:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :

definition

let c₁ be set ;
let c₂ be FinSequence of bool c₁;
let c₃ be Nat;
assume E24: ( c₃ in dom c₂ & c₂ . c₃ <> {} ) ;
mode Singlification of c₂,c₃ -> Reduction of a₂ means :Def7: :: HALLMAR1:def 7
Card (a₄ . a₃) = 1;
existence

proof end;

end;

:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :

theorem Th19: :: HALLMAR1:19

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄ being Reduction of b₂,b₃ holds b₄ is Reduction of b₂

proof end;

theorem Th20: :: HALLMAR1:20

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄ being set st b₃ in dom b₂ & b₄ in b₂ . b₃ holds
Cut b₂,b₃,b₄ is Reduction of b₂,b₃

proof end;

theorem Th21: :: HALLMAR1:21

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat
for b₄ being set st b₃ in dom b₂ & b₄ in b₂ . b₃ holds
Cut b₂,b₃,b₄ is Reduction of b₂

proof end;

theorem Th22: :: HALLMAR1:22

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Reduction of b₂
for b₄ being Reduction of b₃ holds b₄ is Reduction of b₂

proof end;

theorem Th23: :: HALLMAR1:23

for b₁ being non empty finite set
for b₂ being non-empty FinSequence of bool b₁
for b₃ being Nat
for b₄ being Singlification of b₂,b₃ st b₃ in dom b₂ holds
b₄ . b₃ <> {}

proof end;

theorem Th24: :: HALLMAR1:24

for b₁ being non empty finite set
for b₂ being non-empty FinSequence of bool b₁
for b₃, b₄ being Nat
for b₅ being Singlification of b₂,b₃
for b₆ being Singlification of b₅,b₄ st b₃ in dom b₂ & b₄ in dom b₂ & b₆ . b₃ <> {} & b₅ . b₄ <> {} holds
( b₆ is Singlification of b₂,b₄ & b₆ is Singlification of b₂,b₃ )

proof end;

theorem Th25: :: HALLMAR1:25

for b₁ being set
for b₂ being FinSequence of bool b₁
for b₃ being Nat holds b₂ is Reduction of b₂,b₃

proof end;

theorem Th26: :: HALLMAR1:26

for b₁ being set
for b₂ being FinSequence of bool b₁ holds b₂ is Reduction of b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of bool c₁;
assume E31: c₂ is non-empty ;
mode Singlification of c₂ -> Reduction of a₂ means :Def8: :: HALLMAR1:def 8
for b₁ being Nat st b₁ in dom a₂ holds
Card (a₃ . b₁) = 1;
existence

proof end;

end;

:: deftheorem Def8 defines Singlification HALLMAR1:def 8 :

theorem Th27: :: HALLMAR1:27

for b₁ being non empty finite set
for b₂ being non empty non-empty FinSequence of bool b₁
for b₃ being Function holds
( b₃ is Singlification of b₂ iff ( dom b₃ = dom b₂ & ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ is Singlification of b₂,b₄ ) ) )

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be non empty FinSequence of bool c₁;
let c₃ be Nat;
cluster -> non empty Singlification of a₂,a₃;
coherence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂ be non empty FinSequence of bool c₁;
cluster -> non empty Singlification of a₂;
coherence

proof end;

end;

theorem Th28: :: HALLMAR1:28

for b₁ being non empty finite set
for b₂ being non empty FinSequence of bool b₁
for b₃ being set
for b₄ being Reduction of b₂ st b₃ is_a_system_of_different_representatives_of b₄ holds
b₃ is_a_system_of_different_representatives_of b₂

proof end;

theorem Th29: :: HALLMAR1:29

for b₁ being finite set
for b₂ being FinSequence of bool b₁ st b₂ is Hall holds
for b₃ being Nat st card (b₂ . b₃) >= 2 holds
ex b₄ being set st
( b₄ in b₂ . b₃ & Cut b₂,b₃,b₄ is Hall )

proof end;

theorem Th30: :: HALLMAR1:30

for b₁ being finite set
for b₂ being FinSequence of bool b₁
for b₃ being Nat st b₃ in dom b₂ & b₂ is Hall holds
ex b₄ being Singlification of b₂,b₃ st b₄ is Hall

proof end;

theorem Th31: :: HALLMAR1:31

for b₁ being non empty finite set
for b₂ being non empty FinSequence of bool b₁ st b₂ is Hall holds
ex b₃ being Singlification of b₂ st b₃ is Hall

proof end;

theorem Th32: :: HALLMAR1:32

for b₁ being non empty finite set
for b₂ being non empty FinSequence of bool b₁ holds
( ex b₃ being set st b₃ is_a_system_of_different_representatives_of b₂ iff b₂ is Hall )

proof end;