:: PBOOLE semantic presentation

registration

cluster empty-yielding set ;
existence by RELAT_1:60;

end;

theorem Th1: :: PBOOLE:1

for b₁ being Function st b₁ is non-empty holds
rng b₁ is with_non-empty_elements

proof end;

theorem Th2: :: PBOOLE:2

for b₁ being Function holds
( b₁ is empty-yielding iff ( b₁ = {} or rng b₁ = {{} } ) )

proof end;

definition

let c₁ be set ;
canceled;
canceled;
mode ManySortedSet of c₁ -> Function means :Def3: :: PBOOLE:def 3
dom a₂ = a₁;
existence

proof end;

end;

:: deftheorem Def1 PBOOLE:def 1 :

:: deftheorem Def2 PBOOLE:def 2 :

:: deftheorem Def3 defines ManySortedSet PBOOLE:def 3 :

scheme :: PBOOLE:sch 1
s1{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being set st b₂ in F₁() holds
b₁ . b₂ in F₂(b₂)

provided

E2: for b₁ being set st b₁ in F₁() holds
F₂(b₁) <> {}

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
pred c₂ in c₃ means :Def4: :: PBOOLE:def 4
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ in a₃ . b₁;
pred c₂ c= c₃ means :Def5: :: PBOOLE:def 5
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ c= a₃ . b₁;
reflexivity ;

end;

:: deftheorem Def4 defines in PBOOLE:def 4 :

:: deftheorem Def5 defines c= PBOOLE:def 5 :

definition

let c₁ be non empty set ;
let c₂, c₃ be ManySortedSet of c₁;
redefine pred in as c₂ in c₃;
asymmetry

proof end;

end;

scheme :: PBOOLE:sch 2
s2{ F₁() -> set , F₂() -> ManySortedSet of F₁(), P₁[ set , set ] } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being set st b₂ in F₁() holds
for b₃ being set holds
( b₃ in b₁ . b₂ iff ( b₃ in F₂() . b₂ & P₁[b₂,b₃] ) )

proof end;

theorem Th3: :: PBOOLE:3

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

proof end;

definition

let c₁ be set ;
func [0] c₁ -> ManySortedSet of a₁ equals :: PBOOLE:def 6
a₁ --> {} ;
coherence

proof end;

correctness ;
let c₂, c₃ be ManySortedSet of c₁;
func c₂ \/ c₃ -> ManySortedSet of a₁ means :Def7: :: PBOOLE:def 7
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = (a₂ . b₁) \/ (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func c₂ /\ c₃ -> ManySortedSet of a₁ means :Def8: :: PBOOLE:def 8
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = (a₂ . b₁) /\ (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func c₂ \ c₃ -> ManySortedSet of a₁ means :Def9: :: PBOOLE:def 9
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = (a₂ . b₁) \ (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

pred c₂ overlaps c₃ means :Def10: :: PBOOLE:def 10
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ meets a₃ . b₁;
symmetry ;
pred c₂ misses c₃ means :Def11: :: PBOOLE:def 11
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ misses a₃ . b₁;
symmetry ;

end;

:: deftheorem Def6 defines [0] PBOOLE:def 6 :

:: deftheorem Def7 defines \/ PBOOLE:def 7 :

:: deftheorem Def8 defines /\ PBOOLE:def 8 :

:: deftheorem Def9 defines \ PBOOLE:def 9 :

:: deftheorem Def10 defines overlaps PBOOLE:def 10 :

:: deftheorem Def11 defines misses PBOOLE:def 11 :

notation

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
antonym c₂ does_not_overlap c₃ for c₂ overlaps c₃;
antonym c₂ meets c₃ for c₂ misses c₃;

end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
func c₂ \+\ c₃ -> ManySortedSet of a₁ equals :: PBOOLE:def 12
(a₂ \ a₃) \/ (a₃ \ a₂);
correctness ;
commutativity ;

end;

:: deftheorem Def12 defines \+\ PBOOLE:def 12 :

theorem Th4: :: PBOOLE:4

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

proof end;

theorem Th5: :: PBOOLE:5

for b₁, b₂ being set holds ([0] b₂) . b₁ = {}

proof end;

theorem Th6: :: PBOOLE:6

for b₁ being set
for b₂ being ManySortedSet of b₁ st ( for b₃ being set st b₃ in b₁ holds
b₂ . b₃ = {} ) holds
b₂ = [0] b₁

proof end;

theorem Th7: :: PBOOLE:7

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

proof end;

theorem Th8: :: PBOOLE:8

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ holds
( b₂ in b₃ /\ b₄ iff ( b₂ in b₃ & b₂ in b₄ ) )

proof end;

theorem Th9: :: PBOOLE:9

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

proof end;

theorem Th10: :: PBOOLE:10

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ in b₃ & b₂ in b₄ holds
b₃ overlaps b₄

proof end;

theorem Th11: :: PBOOLE:11

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

proof end;

theorem Th12: :: PBOOLE:12

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

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
redefine pred = as c₂ = c₃ means :: PBOOLE:def 13
( a₂ c= a₃ & a₃ c= a₂ );
compatibility

proof end;

end;

:: deftheorem Def13 defines = PBOOLE:def 13 :

theorem Th13: :: PBOOLE:13

canceled;

theorem Th14: :: PBOOLE:14

canceled;

theorem Th15: :: PBOOLE:15

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

proof end;

theorem Th16: :: PBOOLE:16

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

proof end;

theorem Th17: :: PBOOLE:17

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

proof end;

theorem Th18: :: PBOOLE:18

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 Th19: :: PBOOLE:19

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

proof end;

theorem Th20: :: PBOOLE:20

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

proof end;

theorem Th21: :: PBOOLE:21

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

proof end;

theorem Th22: :: PBOOLE:22

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

proof end;

theorem Th23: :: PBOOLE:23

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

proof end;

theorem Th24: :: PBOOLE:24

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

proof end;

theorem Th25: :: PBOOLE:25

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

proof end;

theorem Th26: :: PBOOLE:26

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

proof end;

theorem Th27: :: PBOOLE:27

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

proof end;

theorem Th28: :: PBOOLE:28

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

proof end;

theorem Th29: :: PBOOLE:29

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

proof end;

theorem Th30: :: PBOOLE:30

canceled;

theorem Th31: :: PBOOLE:31

canceled;

theorem Th32: :: PBOOLE:32

canceled;

theorem Th33: :: PBOOLE:33

canceled;

theorem Th34: :: PBOOLE:34

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

proof end;

theorem Th35: :: PBOOLE:35

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

proof end;

theorem Th36: :: PBOOLE:36

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

proof end;

theorem Th37: :: PBOOLE:37

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

proof end;

theorem Th38: :: PBOOLE:38

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

proof end;

theorem Th39: :: PBOOLE:39

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

proof end;

theorem Th40: :: PBOOLE:40

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

proof end;

theorem Th41: :: PBOOLE:41

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

proof end;

theorem Th42: :: PBOOLE:42

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

proof end;

theorem Th43: :: PBOOLE:43

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

proof end;

theorem Th44: :: PBOOLE:44

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

proof end;

theorem Th45: :: PBOOLE:45

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

proof end;

theorem Th46: :: PBOOLE:46

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

proof end;

theorem Th47: :: PBOOLE:47

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

proof end;

theorem Th48: :: PBOOLE:48

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

proof end;

theorem Th49: :: PBOOLE:49

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

proof end;

theorem Th50: :: PBOOLE:50

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

proof end;

theorem Th51: :: PBOOLE:51

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ & b₂ c= b₄ & b₃ /\ b₄ = [0] b₁ holds
b₂ = [0] b₁

proof end;

theorem Th52: :: PBOOLE:52

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ & b₃ /\ b₄ = [0] b₁ holds
b₂ /\ b₄ = [0] b₁

proof end;

theorem Th53: :: PBOOLE:53

for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( b₂ \/ ([0] b₁) = b₂ & ([0] b₁) \/ b₂ = b₂ )

proof end;

theorem Th54: :: PBOOLE:54

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ \/ b₃ = [0] b₁ holds
( b₂ = [0] b₁ & b₃ = [0] b₁ )

proof end;

theorem Th55: :: PBOOLE:55

for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( b₂ /\ ([0] b₁) = [0] b₁ & ([0] b₁) /\ b₂ = [0] b₁ )

proof end;

theorem Th56: :: PBOOLE:56

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ \/ b₄ & b₂ /\ b₄ = [0] b₁ holds
b₂ c= b₃

proof end;

theorem Th57: :: PBOOLE:57

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ & b₃ /\ b₂ = [0] b₁ holds
b₂ = [0] b₁ by Th25;

theorem Th58: :: PBOOLE:58

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ \ b₃ = [0] b₁ iff b₂ c= b₃ )

proof end;

theorem Th59: :: PBOOLE:59

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

proof end;

theorem Th60: :: PBOOLE:60

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

proof end;

theorem Th61: :: PBOOLE:61

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

proof end;

theorem Th62: :: PBOOLE:62

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

proof end;

theorem Th63: :: PBOOLE:63

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ \ b₂ holds
b₂ = [0] b₁

proof end;

theorem Th64: :: PBOOLE:64

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ \ b₂ = [0] b₁ by Th58;

theorem Th65: :: PBOOLE:65

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ \ ([0] b₁) = b₂

proof end;

theorem Th66: :: PBOOLE:66

for b₁ being set
for b₂ being ManySortedSet of b₁ holds ([0] b₁) \ b₂ = [0] b₁

proof end;

theorem Th67: :: PBOOLE:67

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ \ (b₂ \/ b₃) = [0] b₁ & b₂ \ (b₃ \/ b₂) = [0] b₁ )

proof end;

theorem Th68: :: PBOOLE:68

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

proof end;

theorem Th69: :: PBOOLE:69

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( (b₂ \ b₃) /\ b₃ = [0] b₁ & b₃ /\ (b₂ \ b₃) = [0] b₁ )

proof end;

theorem Th70: :: PBOOLE:70

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

proof end;

theorem Th71: :: PBOOLE:71

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

proof end;

theorem Th72: :: PBOOLE:72

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

proof end;

theorem Th73: :: PBOOLE:73

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

proof end;

theorem Th74: :: PBOOLE:74

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

proof end;

theorem Th75: :: PBOOLE:75

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

proof end;

theorem Th76: :: PBOOLE:76

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

proof end;

theorem Th77: :: PBOOLE:77

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds
( b₂ /\ b₃ = [0] b₁ iff b₂ \ b₃ = b₂ )

proof end;

theorem Th78: :: PBOOLE:78

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

proof end;

theorem Th79: :: PBOOLE:79

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

proof end;

theorem Th80: :: PBOOLE:80

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

proof end;

theorem Th81: :: PBOOLE:81

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

proof end;

theorem Th82: :: PBOOLE:82

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

proof end;

theorem Th83: :: PBOOLE:83

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

proof end;

theorem Th84: :: PBOOLE:84

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

proof end;

theorem Th85: :: PBOOLE:85

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

proof end;

theorem Th86: :: PBOOLE:86

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

proof end;

theorem Th87: :: PBOOLE:87

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

proof end;

theorem Th88: :: PBOOLE:88

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

proof end;

theorem Th89: :: PBOOLE:89

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ \ b₃ c= b₂ \+\ b₃ by Th16;

theorem Th90: :: PBOOLE:90

canceled;

theorem Th91: :: PBOOLE:91

for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( b₂ \+\ ([0] b₁) = b₂ & ([0] b₁) \+\ b₂ = b₂ )

proof end;

theorem Th92: :: PBOOLE:92

for b₁ being set
for b₂ being ManySortedSet of b₁ holds b₂ \+\ b₂ = [0] b₁ by Th58;

theorem Th93: :: PBOOLE:93

canceled;

theorem Th94: :: PBOOLE:94

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

proof end;

theorem Th95: :: PBOOLE:95

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

proof end;

theorem Th96: :: PBOOLE:96

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

proof end;

theorem Th97: :: PBOOLE:97

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

proof end;

theorem Th98: :: PBOOLE:98

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

proof end;

theorem Th99: :: PBOOLE:99

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

theorem Th100: :: PBOOLE:100

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

proof end;

theorem Th101: :: PBOOLE:101

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

proof end;

theorem Th102: :: PBOOLE:102

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

proof end;

theorem Th103: :: PBOOLE:103

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

proof end;

theorem Th104: :: PBOOLE:104

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

proof end;

theorem Th105: :: PBOOLE:105

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

proof end;

theorem Th106: :: PBOOLE:106

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

proof end;

theorem Th107: :: PBOOLE:107

canceled;

theorem Th108: :: PBOOLE:108

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

proof end;

theorem Th109: :: PBOOLE:109

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

proof end;

theorem Th110: :: PBOOLE:110

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

proof end;

theorem Th111: :: PBOOLE:111

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ overlaps b₃ /\ b₄ holds
( b₂ overlaps b₃ & b₂ overlaps b₄ )

proof end;

theorem Th112: :: PBOOLE:112

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

proof end;

theorem Th113: :: PBOOLE:113

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

proof end;

theorem Th114: :: PBOOLE:114

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ does_not_overlap b₃ holds
b₄ /\ b₂ does_not_overlap b₄ /\ b₃

proof end;

theorem Th115: :: PBOOLE:115

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

proof end;

theorem Th116: :: PBOOLE:116

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

proof end;

theorem Th117: :: PBOOLE:117

canceled;

theorem Th118: :: PBOOLE:118

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ misses b₃ \ b₂

proof end;

theorem Th119: :: PBOOLE:119

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ /\ b₃ misses b₂ \ b₃

proof end;

theorem Th120: :: PBOOLE:120

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ /\ b₃ misses b₂ \+\ b₃

proof end;

theorem Th121: :: PBOOLE:121

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ misses b₃ holds
b₂ /\ b₃ = [0] b₁

proof end;

theorem Th122: :: PBOOLE:122

for b₁ being set
for b₂ being ManySortedSet of b₁ st b₂ <> [0] b₁ holds
b₂ meets b₂

proof end;

theorem Th123: :: PBOOLE:123

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ & b₂ c= b₄ & b₃ misses b₄ holds
b₂ = [0] b₁

proof end;

theorem Th124: :: PBOOLE:124

for b₁ being set
for b₂, b₃, b₄, b₅ being ManySortedSet of b₁ st b₂ \/ b₃ = b₄ \/ b₅ & b₄ misses b₂ & b₅ misses b₃ holds
( b₄ = b₃ & b₅ = b₂ )

proof end;

theorem Th125: :: PBOOLE:125

canceled;

theorem Th126: :: PBOOLE:126

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

proof end;

theorem Th127: :: PBOOLE:127

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

proof end;

theorem Th128: :: PBOOLE:128

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

proof end;

theorem Th129: :: PBOOLE:129

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ \ b₃ misses b₃ \ b₂

proof end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
pred c₂ [= c₃ means :Def14: :: PBOOLE:def 14
for b₁ being ManySortedSet of a₁ st b₁ in a₂ holds
b₁ in a₃;
reflexivity ;

end;

:: deftheorem Def14 defines [= PBOOLE:def 14 :

theorem Th130: :: PBOOLE:130

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

proof end;

theorem Th131: :: PBOOLE:131

canceled;

theorem Th132: :: PBOOLE:132

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ [= b₃ & b₃ [= b₄ holds
b₂ [= b₄

proof end;

theorem Th133: :: PBOOLE:133

[0] {} in [0] {}

proof end;

theorem Th134: :: PBOOLE:134

for b₁ being ManySortedSet of {} holds b₁ = {}

proof end;

theorem Th135: :: PBOOLE:135

for b₁ being non empty set
for b₂, b₃ being ManySortedSet of b₁ st b₂ overlaps b₃ holds
b₂ meets b₃

proof end;

theorem Th136: :: PBOOLE:136

for b₁ being non empty set
for b₂ being ManySortedSet of b₁ holds not b₂ in [0] b₁

proof end;

theorem Th137: :: PBOOLE:137

for b₁ being non empty set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ in b₃ & b₂ in b₄ holds
b₃ /\ b₄ <> [0] b₁

proof end;

theorem Th138: :: PBOOLE:138

for b₁ being non empty set
for b₂ being ManySortedSet of b₁ holds
( b₂ does_not_overlap [0] b₁ & [0] b₁ does_not_overlap b₂ )

proof end;

theorem Th139: :: PBOOLE:139

for b₁ being non empty set
for b₂, b₃ being ManySortedSet of b₁ st b₂ /\ b₃ = [0] b₁ holds
b₂ does_not_overlap b₃

proof end;

theorem Th140: :: PBOOLE:140

for b₁ being non empty set
for b₂ being ManySortedSet of b₁ st b₂ overlaps b₂ holds
b₂ <> [0] b₁

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
redefine attr empty-yielding as a₂ is empty-yielding means :Def15: :: PBOOLE:def 15
for b₁ being set st b₁ in a₁ holds
a₂ . b₁ is empty;
compatibility

proof end;

redefine attr non-empty as a₂ is non-empty means :Def16: :: PBOOLE:def 16
for b₁ being set st b₁ in a₁ holds
not a₂ . b₁ is empty;
compatibility

proof end;

end;

:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :

:: deftheorem Def16 defines non-empty PBOOLE:def 16 :

registration

let c₁ be set ;
cluster V4 ManySortedSet of a₁;
existence

proof end;

cluster V3 ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster V3 -> V4 ManySortedSet of a₁;
coherence

proof end;

cluster V4 -> V3 ManySortedSet of a₁;
coherence

proof end;

end;

theorem Th141: :: PBOOLE:141

for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( b₂ is empty-yielding iff b₂ = [0] b₁ )

proof end;

theorem Th142: :: PBOOLE:142

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is empty-yielding & b₃ c= b₂ holds
b₃ is empty-yielding

proof end;

theorem Th143: :: PBOOLE:143

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & b₂ c= b₃ holds
b₃ is non-empty

proof end;

theorem Th144: :: PBOOLE:144

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & b₂ [= b₃ holds
b₂ c= b₃

proof end;

theorem Th145: :: PBOOLE:145

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & b₂ [= b₃ holds
b₃ is non-empty

proof end;

theorem Th146: :: PBOOLE:146

for b₁ being set
for b₂ being V3 ManySortedSet of b₁ ex b₃ being ManySortedSet of b₁ st b₃ in b₂

proof end;

theorem Th147: :: PBOOLE:147

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

proof end;

theorem Th148: :: PBOOLE:148

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being V3 ManySortedSet of b₁ st ( for b₅ being ManySortedSet of b₁ holds
( b₅ in b₄ iff ( b₅ in b₂ & b₅ in b₃ ) ) ) holds
b₄ = b₂ /\ b₃

proof end;

scheme :: PBOOLE:sch 3
s3{ F₁() -> set , P₁[ set , set ] } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being set st b₂ in F₁() holds
P₁[b₂,b₁ . b₂]

provided

E77: for b₁ being set st b₁ in F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

scheme :: PBOOLE:sch 4
s4{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being set st b₂ in F₁() holds
b₁ . b₂ = F₂(b₂)

proof end;

registration

let c₁ be set ;
cluster Function-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode ManySortedFunction of a₁ is Function-yielding ManySortedSet of a₁;

end;

theorem Th149: :: PBOOLE:149

for b₁ being set
for b₂ being V3 ManySortedSet of b₁ holds not {} in rng b₂

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode Component of a₂ is Element of rng a₂;

end;

theorem Th150: :: PBOOLE:150

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Component of b₂ ex b₄ being set st
( b₄ in b₁ & b₃ = b₂ . b₄ )

proof end;

theorem Th151: :: PBOOLE:151

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being set st b₃ in b₁ holds
b₂ . b₃ is Component of b₂

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode Element of c₂ -> ManySortedSet of a₁ means :: PBOOLE:def 17
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ is Element of a₂ . b₁;
existence

proof end;

end;

:: deftheorem Def17 defines Element PBOOLE:def 17 :

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
mode ManySortedFunction of c₂,c₃ -> ManySortedSet of a₁ means :Def18: :: PBOOLE:def 18
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ is Function of a₂ . b₁,a₃ . b₁;
correctness

proof end;

end;

:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :

registration

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
cluster -> Function-yielding ManySortedFunction of a₂,a₃;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func c₂ # -> ManySortedSet of a₁ * means :Def19: :: PBOOLE:def 19
for b₁ being Element of a₁ * holds a₃ . b₁ = product (a₂ * b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines # PBOOLE:def 19 :

registration

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

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be ManySortedSet of c₂;
redefine func * as c₄ * c₃ -> ManySortedSet of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be V3 ManySortedSet of c₂;
redefine func * as c₄ * c₃ -> V3 ManySortedSet of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
func *--> c₁ -> Function of NAT ,{a₁} * means :Def20: :: PBOOLE:def 20
for b₁ being Nat holds a₂ . b₁ = b₁ |-> a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines *--> PBOOLE:def 20 :

theorem Th152: :: PBOOLE:152

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

proof end;

theorem Th153: :: PBOOLE:153

for b₁ being non empty set
for b₂ being Nat
for b₃ being set
for b₄ being ManySortedSet of {b₃} st b₄ = {b₃} --> b₁ holds
((b₄ # ) * (*--> b₃)) . b₂ = Funcs (Seg b₂),b₁

proof end;

definition

let c₁, c₂ be set ;
redefine func --> as c₁ --> c₂ -> Function of a₁,{a₂};
coherence

proof end;

end;

scheme :: PBOOLE:sch 5
s5{ F₁() -> non empty set , F₂( set ) -> set } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being Element of F₁() holds b₁ . b₂ = F₂(b₂)

proof end;

registration

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
let c₃ be Element of c₁;
cluster a₂ . a₃ -> non empty ;
coherence by Def16;

end;

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
func [|c₂,c₃|] -> ManySortedSet of a₁ means :: PBOOLE:def 21
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = [:(a₂ . b₁),(a₃ . b₁):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines [| PBOOLE:def 21 :

definition

let c₁ be set ;
let c₂, c₃ be ManySortedSet of c₁;
deffunc H₁( set ) -> set = Funcs (c₂ . a₁),(c₃ . a₁);
func MSFuncs c₂,c₃ -> ManySortedSet of a₁ means :: PBOOLE:def 22
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = Funcs (a₂ . b₁),(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines MSFuncs PBOOLE:def 22 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode ManySortedSubset of c₂ -> ManySortedSet of a₁ means :Def23: :: PBOOLE:def 23
a₃ c= a₂;
existence ;

end;

:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :

registration

let c₁ be set ;
let c₂ be V3 ManySortedSet of c₁;
cluster V3 ManySortedSubset of a₂;
existence

proof end;

end;

definition

let c₁, c₂ be Function-yielding Function;
func c₂ ** c₁ -> Function-yielding Function means :: PBOOLE:def 24
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₂ . b₁) * (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines ** PBOOLE:def 24 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be ManySortedFunction of c₁;
func c₃ .:.: c₂ -> ManySortedSet of a₁ means :: PBOOLE:def 25
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = (a₃ . b₁) .: (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def25 defines .:.: PBOOLE:def 25 :

registration

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

proof end;

end;