:: MBOOLEAN semantic presentation

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func bool c₂ -> ManySortedSet of a₁ means :Def1: :: MBOOLEAN:def 1
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = bool (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines bool MBOOLEAN:def 1 :

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster bool a₂ -> V3 ;
coherence

proof end;

end;

Lemma2: for b₁, b₂, b₃ being set
for b₄ being ManySortedSet of b₂ st b₁ in b₂ holds
dom (b₄ +* (b₁ .--> b₃)) = b₂

proof end;

Lemma3: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(bool (b₂ \/ b₃)) . b₄ = bool ((b₂ . b₄) \/ (b₃ . b₄))

proof end;

Lemma4: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(bool (b₂ /\ b₃)) . b₄ = bool ((b₂ . b₄) /\ (b₃ . b₄))

proof end;

Lemma5: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(bool (b₂ \ b₃)) . b₄ = bool ((b₂ . b₄) \ (b₃ . b₄))

proof end;

Lemma6: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(bool (b₂ \+\ b₃)) . b₄ = bool ((b₂ . b₄) \+\ (b₃ . b₄))

proof end;

theorem Th1: :: MBOOLEAN:1

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ = bool b₃ iff for b₄ being ManySortedSet of b₁ holds
( b₄ in b₂ iff b₄ c= b₃ ) )

proof end;

theorem Th2: :: MBOOLEAN:2

for b₁ being set holds bool ([0] b₁) = b₁ --> {{} }

proof end;

theorem Th3: :: MBOOLEAN:3

for b₁, b₂ being set holds bool (b₁ --> b₂) = b₁ --> (bool b₂)

proof end;

theorem Th4: :: MBOOLEAN:4

for b₁, b₂ being set holds bool (b₁ --> {b₂}) = b₁ --> {{} ,{b₂}}

proof end;

theorem Th5: :: MBOOLEAN:5

for b₁ being set
for b₂ being ManySortedSet of b₁ holds [0] b₁ c= b₂

proof end;

theorem Th6: :: MBOOLEAN:6

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ holds
bool b₂ c= bool b₃

proof end;

theorem Th7: :: MBOOLEAN:7

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds (bool b₂) \/ (bool b₃) c= bool (b₂ \/ b₃)

proof end;

theorem Th8: :: MBOOLEAN:8

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st (bool b₂) \/ (bool b₃) = bool (b₂ \/ b₃) holds
for b₄ being set st b₄ in b₁ holds
b₂ . b₄,b₃ . b₄ are_c=-comparable

proof end;

theorem Th9: :: MBOOLEAN:9

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds bool (b₂ /\ b₃) = (bool b₂) /\ (bool b₃)

proof end;

theorem Th10: :: MBOOLEAN:10

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds bool (b₂ \ b₃) c= (b₁ --> {{} }) \/ ((bool b₂) \ (bool b₃))

proof end;

theorem Th11: :: MBOOLEAN:11

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( b₂ c= b₃ \ b₄ iff ( b₂ c= b₃ & b₂ misses b₄ ) )

proof end;

theorem Th12: :: MBOOLEAN:12

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds (bool (b₂ \ b₃)) \/ (bool (b₃ \ b₂)) c= bool (b₂ \+\ b₃)

proof end;

theorem Th13: :: MBOOLEAN:13

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( b₂ c= b₃ \+\ b₄ iff ( b₂ c= b₃ \/ b₄ & b₂ misses b₃ /\ b₄ ) )

proof end;

theorem Th14: :: MBOOLEAN:14

canceled;

theorem Th15: :: MBOOLEAN:15

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st ( b₂ c= b₃ or b₄ c= b₃ ) holds
b₂ /\ b₄ c= b₃

proof end;

theorem Th16: :: MBOOLEAN:16

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ holds
b₂ \ b₄ c= b₃

proof end;

theorem Th17: :: MBOOLEAN:17

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ & b₄ c= b₃ holds
b₂ \+\ b₄ c= b₃

proof end;

theorem Th18: :: MBOOLEAN:18

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds [|b₂,b₃|] c= bool (bool (b₂ \/ b₃))

proof end;

theorem Th19: :: MBOOLEAN:19

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ c= b₃ iff b₂ in bool b₃ )

proof end;

theorem Th20: :: MBOOLEAN:20

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds MSFuncs b₂,b₃ c= bool [|b₂,b₃|]

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func union c₂ -> ManySortedSet of a₁ means :Def2: :: MBOOLEAN:def 2
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = union (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines union MBOOLEAN:def 2 :

registration

let c₁ be set ;
cluster union ([0] a₁) -> V4 ;
coherence

proof end;

end;

Lemma9: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(union (b₂ \/ b₃)) . b₄ = union ((b₂ . b₄) \/ (b₃ . b₄))

proof end;

Lemma10: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being set st b₄ in b₁ holds
(union (b₂ /\ b₃)) . b₄ = union ((b₂ . b₄) /\ (b₃ . b₄))

proof end;

theorem Th21: :: MBOOLEAN:21

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ in union b₃ iff ex b₄ being ManySortedSet of b₁ st
( b₂ in b₄ & b₄ in b₃ ) )

proof end;

theorem Th22: :: MBOOLEAN:22

for b₁ being set holds union ([0] b₁) = [0] b₁

proof end;

theorem Th23: :: MBOOLEAN:23

for b₁, b₂ being set holds union (b₁ --> b₂) = b₁ --> (union b₂)

proof end;

theorem Th24: :: MBOOLEAN:24

for b₁, b₂ being set holds union (b₁ --> {b₂}) = b₁ --> b₂

proof end;

theorem Th25: :: MBOOLEAN:25

for b₁, b₂, b₃ being set holds union (b₁ --> {{b₂},{b₃}}) = b₁ --> {b₂,b₃}

proof end;

theorem Th26: :: MBOOLEAN:26

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ in b₃ holds
b₂ c= union b₃

proof end;

theorem Th27: :: MBOOLEAN:27

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ holds
union b₂ c= union b₃

proof end;

theorem Th28: :: MBOOLEAN:28

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds union (b₂ \/ b₃) = (union b₂) \/ (union b₃)

proof end;

theorem Th29: :: MBOOLEAN:29

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds union (b₂ /\ b₃) c= (union b₂) /\ (union b₃)

proof end;

theorem Th30: :: MBOOLEAN:30

for b₁ being set
for b₂ being ManySortedSet of b₁ holds union (bool b₂) = b₂

proof end;

theorem Th31: :: MBOOLEAN:31

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ c= bool (union b₂)

proof end;

theorem Th32: :: MBOOLEAN:32

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st union b₂ c= b₃ & b₄ in b₂ holds
b₄ c= b₃

proof end;

theorem Th33: :: MBOOLEAN:33

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being V3 ManySortedSet of b₁ st ( for b₄ being ManySortedSet of b₁ st b₄ in b₃ holds
b₄ c= b₂ ) holds
union b₃ c= b₂

proof end;

theorem Th34: :: MBOOLEAN:34

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being V3 ManySortedSet of b₁ st ( for b₄ being ManySortedSet of b₁ st b₄ in b₃ holds
b₄ /\ b₂ = [0] b₁ ) holds
(union b₃) /\ b₂ = [0] b₁

proof end;

theorem Th35: :: MBOOLEAN:35

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ \/ b₃ is non-empty & ( for b₄, b₅ being ManySortedSet of b₁ st b₄ <> b₅ & b₄ in b₂ \/ b₃ & b₅ in b₂ \/ b₃ holds
b₄ /\ b₅ = [0] b₁ ) holds
union (b₂ /\ b₃) = (union b₂) /\ (union b₃)

proof end;

theorem Th36: :: MBOOLEAN:36

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being V3 ManySortedSet of b₁ st b₃ c= union (b₂ \/ b₄) & ( for b₅ being ManySortedSet of b₁ st b₅ in b₄ holds
b₅ /\ b₃ = [0] b₁ ) holds
b₃ c= union b₂

proof end;

theorem Th37: :: MBOOLEAN:37

for b₁ being set
for b₂ being V3 locally-finite ManySortedSet of b₁ st ( for b₃, b₄ being ManySortedSet of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ c= b₄ holds
b₄ c= b₃ ) holds
union b₂ in b₂

proof end;