:: HALLMAR1 semantic presentation

theorem Th1: :: HALLMAR1:1

for X, Y being finite set holds (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)

proof end;

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

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

provided

A1: ( P₁[F₁()] & F₁() >= 2 ) and
A2: for k being Nat st 1 <= k & k < F₁() & P₁[k + 1] holds
P₁[k]

proof end;

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

P₁[1]

provided

A1: ex n being Nat st
( n > 1 & P₁[n] ) and
A2: for k being Nat st k >= 1 & P₁[k + 1] holds
P₁[k]

proof end;

registration

let F be non empty set ;
cluster non empty non-empty FinSequence of bool F;
existence

proof end;

end;

theorem Th2: :: HALLMAR1:2

for F being non empty set
for f being non-empty FinSequence of bool F
for i being Nat st i in dom f holds
f . i <> {}

proof end;

registration

let F be finite set ;
let A be FinSequence of bool F;
let i be Nat;
cluster A . i -> finite ;
coherence

proof end;

end;

definition

let F be set ;
let A be FinSequence of bool F;
let J be set ;
func union A,J -> set means :Def1: :: HALLMAR1:def 1
for x being set holds
( x in it iff ex j being set st
( j in J & j in dom A & x in A . j ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines union HALLMAR1:def 1 :

theorem Th3: :: HALLMAR1:3

for F being set
for A being FinSequence of bool F
for J being set holds union A,J c= F

proof end;

theorem :: HALLMAR1:4

for F being finite set
for A being FinSequence of bool F
for J, K being set st J c= K holds
union A,J c= union A,K

proof end;

registration

let F be finite set ;
let A be FinSequence of bool F;
let J be set ;
cluster union A,J -> finite ;
coherence

proof end;

end;

theorem Th5: :: HALLMAR1:5

for F being finite set
for A being FinSequence of bool F
for i being Nat st i in dom A holds
union A,{i} = A . i

proof end;

theorem Th6: :: HALLMAR1:6

for F being finite set
for A being FinSequence of bool F
for i, j being Nat st i in dom A & j in dom A holds
union A,{i,j} = (A . i) \/ (A . j)

proof end;

theorem Th7: :: HALLMAR1:7

for J being set
for F being finite set
for A being FinSequence of bool F
for i being Nat st i in J & i in dom A holds
A . i c= union A,J

proof end;

theorem Th8: :: HALLMAR1:8

for J being set
for F being finite set
for i being Nat
for A being FinSequence of bool F st i in J & i in dom A holds
union A,J = (union A,(J \ {i})) \/ (A . i)

proof end;

theorem Th9: :: HALLMAR1:9

for J1, J2 being set
for F being finite set
for i being Nat
for A being FinSequence of bool F st i in dom A holds
union A,(({i} \/ J1) \/ J2) = (A . i) \/ (union A,(J1 \/ J2))

proof end;

theorem Th10: :: HALLMAR1:10

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i

proof end;

definition

let F be finite set ;
let A be FinSequence of bool F;
let i be Nat;
let x be set ;
func Cut A,i,x -> FinSequence of bool F means :Def2: :: HALLMAR1:def 2
( dom it = dom A & ( for k being Nat st k in dom it holds
( ( i = k implies it . k = (A . k) \ {x} ) & ( i <> k implies it . k = A . k ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Cut HALLMAR1:def 2 :

theorem Th11: :: HALLMAR1:11

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x being set st i in dom A & x in A . i holds
card ((Cut A,i,x) . i) = (card (A . i)) - 1

proof end;

theorem Th12: :: HALLMAR1:12

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x, J being set holds union (Cut A,i,x),(J \ {i}) = union A,(J \ {i})

proof end;

theorem Th13: :: HALLMAR1:13

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x, J being set st not i in J holds
union A,J = union (Cut A,i,x),J

proof end;

theorem Th14: :: HALLMAR1:14

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x, J being set st i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) & i in J holds
union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x})

proof end;

definition

let F be finite set ;
let X be FinSequence of bool F;
let A be set ;
pred A is_a_system_of_different_representatives_of X means :Def3: :: HALLMAR1:def 3
ex f being FinSequence of F st
( f = A & dom X = dom f & ( for i being Nat st i in dom f holds
f . i in X . i ) & f is one-to-one );

end;

:: deftheorem Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def 3 :

definition

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

end;

:: deftheorem Def4 defines Hall HALLMAR1:def 4 :

theorem Th15: :: HALLMAR1:15

for F being finite set
for A being non empty FinSequence of bool F st A is Hall holds
A is non-empty

proof end;

theorem Th16: :: HALLMAR1:16

for F being finite set
for A being FinSequence of bool F
for i being Nat st i in dom A & A is Hall holds
card (A . i) >= 1

proof end;

theorem Th17: :: HALLMAR1:17

for F being non empty finite set
for A being non empty FinSequence of bool F st ( for i being Nat st i in dom A holds
card (A . i) = 1 ) & A is Hall holds
ex X being set st X is_a_system_of_different_representatives_of A

proof end;

theorem Th18: :: HALLMAR1:18

for F being finite set
for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds
A is Hall

proof end;

definition

let F be set ;
let A be FinSequence of bool F;
let i be Nat;
mode Reduction of A,i -> FinSequence of bool F means :Def5: :: HALLMAR1:def 5
( dom it = dom A & ( for j being Nat st j in dom A & j <> i holds
A . j = it . j ) & it . i c= A . i );
existence

proof end;

end;

:: deftheorem Def5 defines Reduction HALLMAR1:def 5 :

definition

let F be set ;
let A be FinSequence of bool F;
mode Reduction of A -> FinSequence of bool F means :Def6: :: HALLMAR1:def 6
( dom it = dom A & ( for i being Nat st i in dom A holds
it . i c= A . i ) );
existence

proof end;

end;

:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :

definition

let F be set ;
let A be FinSequence of bool F;
let i be Nat;
assume A1: ( i in dom A & A . i <> {} ) ;
mode Singlification of A,i -> Reduction of A means :Def7: :: HALLMAR1:def 7
Card (it . i) = 1;
existence

proof end;

end;

:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :

theorem Th19: :: HALLMAR1:19

for F being finite set
for A being FinSequence of bool F
for i being Nat
for C being Reduction of A,i holds C is Reduction of A

proof end;

theorem Th20: :: HALLMAR1:20

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x being set st i in dom A & x in A . i holds
Cut A,i,x is Reduction of A,i

proof end;

theorem Th21: :: HALLMAR1:21

for F being finite set
for A being FinSequence of bool F
for i being Nat
for x being set st i in dom A & x in A . i holds
Cut A,i,x is Reduction of A

proof end;

theorem Th22: :: HALLMAR1:22

for F being finite set
for A being FinSequence of bool F
for B being Reduction of A
for C being Reduction of B holds C is Reduction of A

proof end;

theorem :: HALLMAR1:23

for F being non empty finite set
for A being non-empty FinSequence of bool F
for i being Nat
for B being Singlification of A,i st i in dom A holds
B . i <> {}

proof end;

theorem Th24: :: HALLMAR1:24

for F being non empty finite set
for A being non-empty FinSequence of bool F
for i, j being Nat
for B being Singlification of A,i
for C being Singlification of B,j st i in dom A & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )

proof end;

theorem :: HALLMAR1:25

for F being set
for A being FinSequence of bool F
for i being Nat holds A is Reduction of A,i

proof end;

theorem Th26: :: HALLMAR1:26

for F being set
for A being FinSequence of bool F holds A is Reduction of A

proof end;

definition

let F be non empty set ;
let A be FinSequence of bool F;
assume A1: A is non-empty ;
mode Singlification of A -> Reduction of A means :Def8: :: HALLMAR1:def 8
for i being Nat st i in dom A holds
Card (it . i) = 1;
existence

proof end;

end;

:: deftheorem Def8 defines Singlification HALLMAR1:def 8 :

theorem Th27: :: HALLMAR1:27

for F being non empty finite set
for A being non empty non-empty FinSequence of bool F
for f being Function holds
( f is Singlification of A iff ( dom f = dom A & ( for i being Nat st i in dom A holds
f is Singlification of A,i ) ) )

proof end;

registration

let F be non empty finite set ;
let A be non empty FinSequence of bool F;
let k be Nat;
cluster -> non empty Singlification of A,k;
coherence

proof end;

end;

registration

let F be non empty finite set ;
let A be non empty FinSequence of bool F;
cluster -> non empty Singlification of A;
coherence

proof end;

end;

theorem Th28: :: HALLMAR1:28

for F being non empty finite set
for A being non empty FinSequence of bool F
for X being set
for B being Reduction of A st X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A

proof end;

theorem Th29: :: HALLMAR1:29

for F being finite set
for A being FinSequence of bool F st A is Hall holds
for i being Nat st card (A . i) >= 2 holds
ex x being set st
( x in A . i & Cut A,i,x is Hall )

proof end;

theorem Th30: :: HALLMAR1:30

for F being finite set
for A being FinSequence of bool F
for i being Nat st i in dom A & A is Hall holds
ex G being Singlification of A,i st G is Hall

proof end;

theorem Th31: :: HALLMAR1:31

for F being non empty finite set
for A being non empty FinSequence of bool F st A is Hall holds
ex G being Singlification of A st G is Hall

proof end;

theorem :: HALLMAR1:32

for F being non empty finite set
for A being non empty FinSequence of bool F holds
( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )

proof end;