:: COHSP_1 semantic presentation

Lemma1: for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁
for b₅ being set st b₅ in b₃ . b₄ holds
b₅ in union b₂
by TARSKI:def 4;

definition

let c₁ be set ;
redefine attr a₁ is binary_complete means :Def1: :: COHSP_1:def 1
for b₁ being set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
b₂ \/ b₃ in a₁ ) holds
union b₁ in a₁;
compatibility

proof end;

end;

:: deftheorem Def1 defines binary_complete COHSP_1:def 1 :

registration

cluster finite set ;
existence by COH_SP:3;

end;

definition

let c₁ be set ;
func FlatCoh c₁ -> set equals :: COHSP_1:def 2
CohSp (id a₁);
correctness ;
func Sub_of_Fin c₁ -> Subset of a₁ means :Def3: :: COHSP_1:def 3
for b₁ being set holds
( b₁ in a₂ iff ( b₁ in a₁ & b₁ is finite ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def2 defines FlatCoh COHSP_1:def 2 :

:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def 3 :

theorem Th1: :: COHSP_1:1

for b₁, b₂ being set holds
( b₂ in FlatCoh b₁ iff ( b₂ = {} or ex b₃ being set st
( b₂ = {b₃} & b₃ in b₁ ) ) )

proof end;

theorem Th2: :: COHSP_1:2

for b₁ being set holds union (FlatCoh b₁) = b₁

proof end;

theorem Th3: :: COHSP_1:3

for b₁ being subset-closed finite set holds Sub_of_Fin b₁ = b₁

proof end;

registration

cluster {{} } -> subset-closed binary_complete ;
coherence by COH_SP:3;
let c₁ be set ;
cluster bool a₁ -> subset-closed binary_complete ;
coherence by COH_SP:2;
cluster FlatCoh a₁ -> non empty subset-closed binary_complete ;
coherence ;

end;

registration

let c₁ be non empty subset-closed set ;
cluster Sub_of_Fin a₁ -> non empty subset-closed ;
coherence

proof end;

end;

theorem Th4: :: COHSP_1:4

Web {{} } = {}

proof end;

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

ex b₁ being set st
( b₁ in F₂() & P₁[b₁] & ( for b₂ being set st b₂ in F₂() & P₁[b₂] & b₂ c= b₁ holds
b₂ = b₁ ) )

provided

E6: F₁() in F₂() and
E7: P₁[F₁()] and
E8: F₁() is finite

proof end;

registration

let c₁ be Coherence_Space;
cluster finite Element of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is c=directed means :: COHSP_1:def 4
for b₁ being finite Subset of a₁ ex b₂ being set st
( union b₁ c= b₂ & b₂ in a₁ );
attr a₁ is c=filtered means :: COHSP_1:def 5
for b₁ being finite Subset of a₁ ex b₂ being set st
( ( for b₃ being set st b₃ in b₁ holds
b₂ c= b₃ ) & b₂ in a₁ );

end;

:: deftheorem Def4 defines c=directed COHSP_1:def 4 :

:: deftheorem Def5 defines c=filtered COHSP_1:def 5 :

registration

cluster c=directed -> non empty set ;
coherence

proof end;

cluster c=filtered -> non empty set ;
coherence

proof end;

end;

theorem Th5: :: COHSP_1:5

for b₁ being set st b₁ is c=directed holds
for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
ex b₄ being set st
( b₂ \/ b₃ c= b₄ & b₄ in b₁ )

proof end;

theorem Th6: :: COHSP_1:6

for b₁ being non empty set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
ex b₄ being set st
( b₂ \/ b₃ c= b₄ & b₄ in b₁ ) ) holds
b₁ is c=directed

proof end;

theorem Th7: :: COHSP_1:7

for b₁ being set st b₁ is c=filtered holds
for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
ex b₄ being set st
( b₄ c= b₂ /\ b₃ & b₄ in b₁ )

proof end;

theorem Th8: :: COHSP_1:8

for b₁ being non empty set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
ex b₄ being set st
( b₄ c= b₂ /\ b₃ & b₄ in b₁ ) ) holds
b₁ is c=filtered

proof end;

theorem Th9: :: COHSP_1:9

for b₁ being set holds
( {b₁} is c=directed & {b₁} is c=filtered )

proof end;

E10: now

let c₁, c₂ be set ;
thus union {c₁,c₂,(c₁ \/ c₂)} = union ({c₁,c₂} \/ {(c₁ \/ c₂)}) by ENUMSET1:43
.= (union {c₁,c₂}) \/ (union {(c₁ \/ c₂)}) by ZFMISC_1:96
.= (c₁ \/ c₂) \/ (union {(c₁ \/ c₂)}) by ZFMISC_1:93
.= (c₁ \/ c₂) \/ (c₁ \/ c₂) by ZFMISC_1:31
.= c₁ \/ c₂ ;

end;

theorem Th10: :: COHSP_1:10

for b₁, b₂ being set holds {b₁,b₂,(b₁ \/ b₂)} is c=directed

proof end;

theorem Th11: :: COHSP_1:11

for b₁, b₂ being set holds {b₁,b₂,(b₁ /\ b₂)} is c=filtered

proof end;

registration

cluster non empty finite c=directed c=filtered set ;
existence

proof end;

end;

registration

let c₁ be non empty set ;
cluster non empty finite c=directed c=filtered Element of bool a₁;
existence

proof end;

end;

theorem Th12: :: COHSP_1:12

for b₁ being set holds
( Fin b₁ is c=directed & Fin b₁ is c=filtered )

proof end;

registration

let c₁ be set ;
cluster Fin a₁ -> c=directed c=filtered ;
coherence by Th12;

end;

E12: now

let c₁ be non empty subset-closed set ;
let c₂ be Element of c₁;
thus Fin c₂ c= c₁

proof

let c₃ be set ; :: according to TARSKI:def 3
assume c₃ in Fin c₂ ;
then c₃ c= c₂ by FINSUB_1:def 5;
hence c₃ in c₁ by CLASSES1:def 1;

end;

registration

let c₁ be non empty subset-closed set ;
cluster non empty preBoolean Element of bool a₁;
existence

proof end;

end;

definition

let c₁ be non empty subset-closed set ;
let c₂ be Element of c₁;
redefine func Fin as Fin c₂ -> non empty preBoolean Subset of a₁;
coherence

proof end;

end;

theorem Th13: :: COHSP_1:13

for b₁ being non empty set
for b₂ being set st b₁ is c=directed & b₂ c= union b₁ & b₂ is finite holds
ex b₃ being set st
( b₃ in b₁ & b₂ c= b₃ )

proof end;

notation

let c₁ be set ;
synonym multiplicative c₁ for cap-closed c₁;

end;

definition

let c₁ be set ;
canceled;
attr a₁ is d.union-closed means :Def7: :: COHSP_1:def 7
for b₁ being Subset of a₁ st b₁ is c=directed holds
union b₁ in a₁;

end;

:: deftheorem Def6 COHSP_1:def 6 :

:: deftheorem Def7 defines d.union-closed COHSP_1:def 7 :

registration

cluster subset-closed -> multiplicative set ;
coherence

proof end;

end;

theorem Th14: :: COHSP_1:14

canceled;

theorem Th15: :: COHSP_1:15

for b₁ being Coherence_Space
for b₂ being c=directed Subset of b₁ holds union b₂ in b₁

proof end;

registration

cluster -> multiplicative d.union-closed set ;
coherence

proof end;

end;

registration

cluster multiplicative d.union-closed set ;
existence

proof end;

end;

definition

let c₁ be non empty d.union-closed set ;
let c₂ be c=directed Subset of c₁;
redefine func union as union c₂ -> Element of a₁;
coherence by Def7;

end;

definition

let c₁, c₂ be set ;
pred c₁ includes_lattice_of c₂ means :: COHSP_1:def 8
for b₁, b₂ being set st b₁ in a₂ & b₂ in a₂ holds
( b₁ /\ b₂ in a₁ & b₁ \/ b₂ in a₁ );

end;

:: deftheorem Def8 defines includes_lattice_of COHSP_1:def 8 :

theorem Th16: :: COHSP_1:16

for b₁ being non empty set st b₁ includes_lattice_of b₁ holds
( b₁ is c=directed & b₁ is c=filtered )

proof end;

definition

let c₁, c₂, c₃ be set ;
pred c₁ includes_lattice_of c₂,c₃ means :: COHSP_1:def 9
a₁ includes_lattice_of {a₂,a₃};

end;

:: deftheorem Def9 defines includes_lattice_of COHSP_1:def 9 :

theorem Th17: :: COHSP_1:17

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

proof end;

definition

let c₁ be Function;
attr a₁ is union-distributive means :Def10: :: COHSP_1:def 10
for b₁ being Subset of (dom a₁) st union b₁ in dom a₁ holds
a₁ . (union b₁) = union (a₁ .: b₁);
attr a₁ is d.union-distributive means :Def11: :: COHSP_1:def 11
for b₁ being Subset of (dom a₁) st b₁ is c=directed & union b₁ in dom a₁ holds
a₁ . (union b₁) = union (a₁ .: b₁);

end;

:: deftheorem Def10 defines union-distributive COHSP_1:def 10 :

:: deftheorem Def11 defines d.union-distributive COHSP_1:def 11 :

definition

let c₁ be Function;
attr a₁ is c=-monotone means :Def12: :: COHSP_1:def 12
for b₁, b₂ being set st b₁ in dom a₁ & b₂ in dom a₁ & b₁ c= b₂ holds
a₁ . b₁ c= a₁ . b₂;
attr a₁ is cap-distributive means :Def13: :: COHSP_1:def 13
for b₁, b₂ being set st dom a₁ includes_lattice_of b₁,b₂ holds
a₁ . (b₁ /\ b₂) = (a₁ . b₁) /\ (a₁ . b₂);

end;

:: deftheorem Def12 defines c=-monotone COHSP_1:def 12 :

:: deftheorem Def13 defines cap-distributive COHSP_1:def 13 :

registration

cluster d.union-distributive -> c=-monotone set ;
coherence

proof end;

cluster union-distributive -> d.union-distributive set ;
coherence

proof end;

end;

theorem Th18: :: COHSP_1:18

for b₁ being Function st b₁ is union-distributive holds
for b₂, b₃ being set st b₂ in dom b₁ & b₃ in dom b₁ & b₂ \/ b₃ in dom b₁ holds
b₁ . (b₂ \/ b₃) = (b₁ . b₂) \/ (b₁ . b₃)

proof end;

theorem Th19: :: COHSP_1:19

for b₁ being Function st b₁ is union-distributive holds
b₁ . {} = {}

proof end;

registration

let c₁, c₂ be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive M5(a₁,a₂);
existence

proof end;

end;

registration

let c₁ be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be Function;
attr a₁ is U-continuous means :Def14: :: COHSP_1:def 14
( dom a₁ is d.union-closed & a₁ is d.union-distributive );

end;

:: deftheorem Def14 defines U-continuous COHSP_1:def 14 :

definition

let c₁ be Function;
attr a₁ is U-stable means :Def15: :: COHSP_1:def 15
( dom a₁ is multiplicative & a₁ is U-continuous & a₁ is cap-distributive );

end;

:: deftheorem Def15 defines U-stable COHSP_1:def 15 :

definition

let c₁ be Function;
attr a₁ is U-linear means :Def16: :: COHSP_1:def 16
( a₁ is U-stable & a₁ is union-distributive );

end;

:: deftheorem Def16 defines U-linear COHSP_1:def 16 :

registration

cluster U-continuous -> d.union-distributive c=-monotone set ;
coherence by Def14;
cluster U-stable -> cap-distributive U-continuous set ;
coherence by Def15;
cluster U-linear -> union-distributive d.union-distributive c=-monotone U-stable set ;
coherence by Def16;

end;

registration

let c₁ be d.union-closed set ;
cluster d.union-distributive -> U-continuous ManySortedSet of a₁;
coherence

proof end;

end;

registration

let c₁ be multiplicative set ;
cluster cap-distributive U-continuous -> U-stable ManySortedSet of a₁;
coherence

proof end;

end;

registration

cluster union-distributive U-stable -> union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear set ;
coherence by Def16;

end;

registration

cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear set ;
existence

proof end;

let c₁ be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear ManySortedSet of a₁;
existence

proof end;

let c₂ be Coherence_Space;
cluster union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear M5(a₂,a₁);
existence

proof end;

end;

registration

let c₁ be U-continuous Function;
cluster dom a₁ -> d.union-closed ;
coherence by Def14;

end;

registration

let c₁ be U-stable Function;
cluster dom a₁ -> multiplicative d.union-closed ;
coherence by Def15;

end;

theorem Th20: :: COHSP_1:20

for b₁ being set holds union (Fin b₁) = b₁

proof end;

theorem Th21: :: COHSP_1:21

for b₁ being U-continuous Function st dom b₁ is subset-closed holds
for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ = union (b₁ .: (Fin b₂))

proof end;

theorem Th22: :: COHSP_1:22

for b₁ being Function st dom b₁ is subset-closed holds
( b₁ is U-continuous iff ( dom b₁ is d.union-closed & b₁ is c=-monotone & ( for b₂, b₃ being set st b₂ in dom b₁ & b₃ in b₁ . b₂ holds
ex b₄ being set st
( b₄ is finite & b₄ c= b₂ & b₃ in b₁ . b₄ ) ) ) )

proof end;

theorem Th23: :: COHSP_1:23

for b₁ being Function st dom b₁ is subset-closed & dom b₁ is d.union-closed holds
( b₁ is U-stable iff ( b₁ is c=-monotone & ( for b₂, b₃ being set st b₂ in dom b₁ & b₃ in b₁ . b₂ holds
ex b₄ being set st
( b₄ is finite & b₄ c= b₂ & b₃ in b₁ . b₄ & ( for b₅ being set st b₅ c= b₂ & b₃ in b₁ . b₅ holds
b₄ c= b₅ ) ) ) ) )

proof end;

theorem Th24: :: COHSP_1:24

for b₁ being Function st dom b₁ is subset-closed & dom b₁ is d.union-closed holds
( b₁ is U-linear iff ( b₁ is c=-monotone & ( for b₂, b₃ being set st b₂ in dom b₁ & b₃ in b₁ . b₂ holds
ex b₄ being set st
( b₄ in b₂ & b₃ in b₁ . {b₄} & ( for b₅ being set st b₅ c= b₂ & b₃ in b₁ . b₅ holds
b₄ in b₅ ) ) ) ) )

proof end;

definition

let c₁ be Function;
func graph c₁ -> set means :Def17: :: COHSP_1:def 17
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being finite set ex b₃ being set st
( b₁ = [b₂,b₃] & b₂ in dom a₁ & b₃ in a₁ . b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines graph COHSP_1:def 17 :

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
redefine func graph as graph c₃ -> Subset of [:a₁,(union a₂):];
coherence

proof end;

end;

registration

let c₁ be Function;
cluster graph a₁ -> Relation-like ;
coherence

proof end;

end;

theorem Th25: :: COHSP_1:25

for b₁ being Function
for b₂, b₃ being set holds
( [b₂,b₃] in graph b₁ iff ( b₂ is finite & b₂ in dom b₁ & b₃ in b₁ . b₂ ) )

proof end;

theorem Th26: :: COHSP_1:26

for b₁ being c=-monotone Function
for b₂, b₃ being set st b₃ in dom b₁ & b₂ c= b₃ & b₃ is finite holds
for b₄ being set st [b₂,b₄] in graph b₁ holds
[b₃,b₄] in graph b₁

proof end;

theorem Th27: :: COHSP_1:27

for b₁, b₂ being Coherence_Space
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁
for b₅, b₆ being set st [b₄,b₅] in graph b₃ & [b₄,b₆] in graph b₃ holds
{b₅,b₆} in b₂

proof end;

theorem Th28: :: COHSP_1:28

for b₁, b₂ being Coherence_Space
for b₃ being c=-monotone Function of b₁,b₂
for b₄, b₅ being Element of b₁ st b₄ \/ b₅ in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in graph b₃ & [b₅,b₇] in graph b₃ holds
{b₆,b₇} in b₂

proof end;

theorem Th29: :: COHSP_1:29

for b₁, b₂ being Coherence_Space
for b₃, b₄ being U-continuous Function of b₁,b₂ st graph b₃ = graph b₄ holds
b₃ = b₄

proof end;

Lemma35: for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:b₁,(union b₂):] st ( for b₄ being set st b₄ in b₃ holds
b₄ `1 is finite ) & ( for b₄, b₅ being finite Element of b₁ st b₄ c= b₅ holds
for b₆ being set st [b₄,b₆] in b₃ holds
[b₅,b₆] in b₃ ) & ( for b₄ being finite Element of b₁
for b₅, b₆ being set st [b₄,b₅] in b₃ & [b₄,b₆] in b₃ holds
{b₅,b₆} in b₂ ) holds
ex b₄ being U-continuous Function of b₁,b₂ st
( b₃ = graph b₄ & ( for b₅ being Element of b₁ holds b₄ . b₅ = b₃ .: (Fin b₅) ) )

proof end;

theorem Th30: :: COHSP_1:30

for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:b₁,(union b₂):] st ( for b₄ being set st b₄ in b₃ holds
b₄ `1 is finite ) & ( for b₄, b₅ being finite Element of b₁ st b₄ c= b₅ holds
for b₆ being set st [b₄,b₆] in b₃ holds
[b₅,b₆] in b₃ ) & ( for b₄ being finite Element of b₁
for b₅, b₆ being set st [b₄,b₅] in b₃ & [b₄,b₆] in b₃ holds
{b₅,b₆} in b₂ ) holds
ex b₄ being U-continuous Function of b₁,b₂ st b₃ = graph b₄

proof end;

theorem Th31: :: COHSP_1:31

for b₁, b₂ being Coherence_Space
for b₃ being U-continuous Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ . b₄ = (graph b₃) .: (Fin b₄)

proof end;

definition

let c₁ be Function;
func Trace c₁ -> set means :Def18: :: COHSP_1:def 18
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being set st
( b₁ = [b₂,b₃] & b₂ in dom a₁ & b₃ in a₁ . b₂ & ( for b₄ being set st b₄ in dom a₁ & b₄ c= b₂ & b₃ in a₁ . b₄ holds
b₂ = b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Trace COHSP_1:def 18 :

theorem Th32: :: COHSP_1:32

for b₁ being Function
for b₂, b₃ being set holds
( [b₂,b₃] in Trace b₁ iff ( b₂ in dom b₁ & b₃ in b₁ . b₂ & ( for b₄ being set st b₄ in dom b₁ & b₄ c= b₂ & b₃ in b₁ . b₄ holds
b₂ = b₄ ) ) )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
redefine func Trace as Trace c₃ -> Subset of [:a₁,(union a₂):];
coherence

proof end;

end;

registration

let c₁ be Function;
cluster Trace a₁ -> Relation-like ;
coherence

proof end;

end;

theorem Th33: :: COHSP_1:33

for b₁ being U-continuous Function st dom b₁ is subset-closed holds
Trace b₁ c= graph b₁

proof end;

theorem Th34: :: COHSP_1:34

for b₁ being U-continuous Function st dom b₁ is subset-closed holds
for b₂, b₃ being set st [b₂,b₃] in Trace b₁ holds
b₂ is finite

proof end;

theorem Th35: :: COHSP_1:35

for b₁, b₂ being Coherence_Space
for b₃ being c=-monotone Function of b₁,b₂
for b₄, b₅ being set st b₄ \/ b₅ in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in Trace b₃ & [b₅,b₇] in Trace b₃ holds
{b₆,b₇} in b₂

proof end;

theorem Th36: :: COHSP_1:36

for b₁, b₂ being Coherence_Space
for b₃ being cap-distributive Function of b₁,b₂
for b₄, b₅ being set st b₄ \/ b₅ in b₁ holds
for b₆ being set st [b₄,b₆] in Trace b₃ & [b₅,b₆] in Trace b₃ holds
b₄ = b₅

proof end;

theorem Th37: :: COHSP_1:37

for b₁, b₂ being Coherence_Space
for b₃, b₄ being U-stable Function of b₁,b₂ st Trace b₃ c= Trace b₄ holds
for b₅ being Element of b₁ holds b₃ . b₅ c= b₄ . b₅

proof end;

theorem Th38: :: COHSP_1:38

for b₁, b₂ being Coherence_Space
for b₃, b₄ being U-stable Function of b₁,b₂ st Trace b₃ = Trace b₄ holds
b₃ = b₄

proof end;

Lemma43: for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:b₁,(union b₂):] st ( for b₄ being set st b₄ in b₃ holds
b₄ `1 is finite ) & ( for b₄, b₅ being Element of b₁ st b₄ \/ b₅ in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in b₃ & [b₅,b₇] in b₃ holds
{b₆,b₇} in b₂ ) & ( for b₄, b₅ being Element of b₁ st b₄ \/ b₅ in b₁ holds
for b₆ being set st [b₄,b₆] in b₃ & [b₅,b₆] in b₃ holds
b₄ = b₅ ) holds
ex b₄ being U-stable Function of b₁,b₂ st
( b₃ = Trace b₄ & ( for b₅ being Element of b₁ holds b₄ . b₅ = b₃ .: (Fin b₅) ) )

proof end;

theorem Th39: :: COHSP_1:39

for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:b₁,(union b₂):] st ( for b₄ being set st b₄ in b₃ holds
b₄ `1 is finite ) & ( for b₄, b₅ being Element of b₁ st b₄ \/ b₅ in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in b₃ & [b₅,b₇] in b₃ holds
{b₆,b₇} in b₂ ) & ( for b₄, b₅ being Element of b₁ st b₄ \/ b₅ in b₁ holds
for b₆ being set st [b₄,b₆] in b₃ & [b₅,b₆] in b₃ holds
b₄ = b₅ ) holds
ex b₄ being U-stable Function of b₁,b₂ st b₃ = Trace b₄

proof end;

theorem Th40: :: COHSP_1:40

for b₁, b₂ being Coherence_Space
for b₃ being U-stable Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ . b₄ = (Trace b₃) .: (Fin b₄)

proof end;

theorem Th41: :: COHSP_1:41

for b₁, b₂ being Coherence_Space
for b₃ being U-stable Function of b₁,b₂
for b₄ being Element of b₁
for b₅ being set holds
( b₅ in b₃ . b₄ iff ex b₆ being Element of b₁ st
( [b₆,b₅] in Trace b₃ & b₆ c= b₄ ) )

proof end;

theorem Th42: :: COHSP_1:42

for b₁, b₂ being Coherence_Space ex b₃ being U-stable Function of b₁,b₂ st Trace b₃ = {}

proof end;

theorem Th43: :: COHSP_1:43

for b₁, b₂ being Coherence_Space
for b₃ being finite Element of b₁
for b₄ being set st b₄ in union b₂ holds
ex b₅ being U-stable Function of b₁,b₂ st Trace b₅ = {[b₃,b₄]}

proof end;

theorem Th44: :: COHSP_1:44

for b₁, b₂ being Coherence_Space
for b₃ being Element of b₁
for b₄ being set
for b₅ being U-stable Function of b₁,b₂ st Trace b₅ = {[b₃,b₄]} holds
for b₆ being Element of b₁ holds
( ( b₃ c= b₆ implies b₅ . b₆ = {b₄} ) & ( not b₃ c= b₆ implies b₅ . b₆ = {} ) )

proof end;

theorem Th45: :: COHSP_1:45

for b₁, b₂ being Coherence_Space
for b₃ being U-stable Function of b₁,b₂
for b₄ being Subset of (Trace b₃) ex b₅ being U-stable Function of b₁,b₂ st Trace b₅ = b₄

proof end;

theorem Th46: :: COHSP_1:46

for b₁, b₂ being Coherence_Space
for b₃ being set st ( for b₄, b₅ being set st b₄ in b₃ & b₅ in b₃ holds
ex b₆ being U-stable Function of b₁,b₂ st b₄ \/ b₅ = Trace b₆ ) holds
ex b₄ being U-stable Function of b₁,b₂ st union b₃ = Trace b₄

proof end;

definition

let c₁, c₂ be Coherence_Space;
func StabCoh c₁,c₂ -> set means :Def19: :: COHSP_1:def 19
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being U-stable Function of a₁,a₂ st b₁ = Trace b₂ );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def19 defines StabCoh COHSP_1:def 19 :

registration

let c₁, c₂ be Coherence_Space;
cluster StabCoh a₁,a₂ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th47: :: COHSP_1:47

for b₁, b₂ being Coherence_Space
for b₃ being U-stable Function of b₁,b₂ holds Trace b₃ c= [:(Sub_of_Fin b₁),(union b₂):]

proof end;

theorem Th48: :: COHSP_1:48

for b₁, b₂ being Coherence_Space holds union (StabCoh b₁,b₂) = [:(Sub_of_Fin b₁),(union b₂):]

proof end;

theorem Th49: :: COHSP_1:49

for b₁, b₂ being Coherence_Space
for b₃, b₄ being finite Element of b₁
for b₅, b₆ being set holds
( [[b₃,b₅],[b₄,b₆]] in Web (StabCoh b₁,b₂) iff ( ( not b₃ \/ b₄ in b₁ & b₅ in union b₂ & b₆ in union b₂ ) or ( [b₅,b₆] in Web b₂ & ( b₅ = b₆ implies b₃ = b₄ ) ) ) )

proof end;

theorem Th50: :: COHSP_1:50

for b₁, b₂ being Coherence_Space
for b₃ being U-stable Function of b₁,b₂ holds
( b₃ is U-linear iff for b₄, b₅ being set st [b₄,b₅] in Trace b₃ holds
ex b₆ being set st b₄ = {b₆} )

proof end;

definition

let c₁ be Function;
func LinTrace c₁ -> set means :Def20: :: COHSP_1:def 20
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being set st
( b₁ = [b₂,b₃] & [{b₂},b₃] in Trace a₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def20 defines LinTrace COHSP_1:def 20 :

theorem Th51: :: COHSP_1:51

for b₁ being Function
for b₂, b₃ being set holds
( [b₂,b₃] in LinTrace b₁ iff [{b₂},b₃] in Trace b₁ )

proof end;

theorem Th52: :: COHSP_1:52

for b₁ being Function st b₁ . {} = {} holds
for b₂, b₃ being set st {b₂} in dom b₁ & b₃ in b₁ . {b₂} holds
[b₂,b₃] in LinTrace b₁

proof end;

theorem Th53: :: COHSP_1:53

for b₁ being Function
for b₂, b₃ being set st [b₂,b₃] in LinTrace b₁ holds
( {b₂} in dom b₁ & b₃ in b₁ . {b₂} )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
redefine func LinTrace as LinTrace c₃ -> Subset of [:(union a₁),(union a₂):];
coherence

proof end;

end;

registration

let c₁ be Function;
cluster LinTrace a₁ -> Relation-like ;
coherence

proof end;

end;

definition

let c₁, c₂ be Coherence_Space;
func LinCoh c₁,c₂ -> set means :Def21: :: COHSP_1:def 21
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being U-linear Function of a₁,a₂ st b₁ = LinTrace b₂ );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def21 defines LinCoh COHSP_1:def 21 :

theorem Th54: :: COHSP_1:54

for b₁, b₂ being Coherence_Space
for b₃ being c=-monotone Function of b₁,b₂
for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in LinTrace b₃ & [b₅,b₇] in LinTrace b₃ holds
{b₆,b₇} in b₂

proof end;

theorem Th55: :: COHSP_1:55

for b₁, b₂ being Coherence_Space
for b₃ being cap-distributive Function of b₁,b₂
for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆ being set st [b₄,b₆] in LinTrace b₃ & [b₅,b₆] in LinTrace b₃ holds
b₄ = b₅

proof end;

theorem Th56: :: COHSP_1:56

for b₁, b₂ being Coherence_Space
for b₃, b₄ being U-linear Function of b₁,b₂ st LinTrace b₃ = LinTrace b₄ holds
b₃ = b₄

proof end;

Lemma61: for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:(union b₁),(union b₂):] st ( for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in b₃ & [b₅,b₇] in b₃ holds
{b₆,b₇} in b₂ ) & ( for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆ being set st [b₄,b₆] in b₃ & [b₅,b₆] in b₃ holds
b₄ = b₅ ) holds
ex b₄ being U-linear Function of b₁,b₂ st
( b₃ = LinTrace b₄ & ( for b₅ being Element of b₁ holds b₄ . b₅ = b₃ .: b₅ ) )

proof end;

theorem Th57: :: COHSP_1:57

for b₁, b₂ being Coherence_Space
for b₃ being Subset of [:(union b₁),(union b₂):] st ( for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆, b₇ being set st [b₄,b₆] in b₃ & [b₅,b₇] in b₃ holds
{b₆,b₇} in b₂ ) & ( for b₄, b₅ being set st {b₄,b₅} in b₁ holds
for b₆ being set st [b₄,b₆] in b₃ & [b₅,b₆] in b₃ holds
b₄ = b₅ ) holds
ex b₄ being U-linear Function of b₁,b₂ st b₃ = LinTrace b₄

proof end;

theorem Th58: :: COHSP_1:58

for b₁, b₂ being Coherence_Space
for b₃ being U-linear Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ . b₄ = (LinTrace b₃) .: b₄

proof end;

theorem Th59: :: COHSP_1:59

for b₁, b₂ being Coherence_Space ex b₃ being U-linear Function of b₁,b₂ st LinTrace b₃ = {}

proof end;

theorem Th60: :: COHSP_1:60

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set st b₃ in union b₁ & b₄ in union b₂ holds
ex b₅ being U-linear Function of b₁,b₂ st LinTrace b₅ = {[b₃,b₄]}

proof end;

theorem Th61: :: COHSP_1:61

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set st b₃ in union b₁ & b₄ in union b₂ holds
for b₅ being U-linear Function of b₁,b₂ st LinTrace b₅ = {[b₃,b₄]} holds
for b₆ being Element of b₁ holds
( ( b₃ in b₆ implies b₅ . b₆ = {b₄} ) & ( not b₃ in b₆ implies b₅ . b₆ = {} ) )

proof end;

theorem Th62: :: COHSP_1:62

for b₁, b₂ being Coherence_Space
for b₃ being U-linear Function of b₁,b₂
for b₄ being Subset of (LinTrace b₃) ex b₅ being U-linear Function of b₁,b₂ st LinTrace b₅ = b₄

proof end;

theorem Th63: :: COHSP_1:63

for b₁, b₂ being Coherence_Space
for b₃ being set st ( for b₄, b₅ being set st b₄ in b₃ & b₅ in b₃ holds
ex b₆ being U-linear Function of b₁,b₂ st b₄ \/ b₅ = LinTrace b₆ ) holds
ex b₄ being U-linear Function of b₁,b₂ st union b₃ = LinTrace b₄

proof end;

registration

let c₁, c₂ be Coherence_Space;
cluster LinCoh a₁,a₂ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th64: :: COHSP_1:64

for b₁, b₂ being Coherence_Space holds union (LinCoh b₁,b₂) = [:(union b₁),(union b₂):]

proof end;

theorem Th65: :: COHSP_1:65

for b₁, b₂ being Coherence_Space
for b₃, b₄, b₅, b₆ being set holds
( [[b₃,b₅],[b₄,b₆]] in Web (LinCoh b₁,b₂) iff ( b₃ in union b₁ & b₄ in union b₁ & ( ( not [b₃,b₄] in Web b₁ & b₅ in union b₂ & b₆ in union b₂ ) or ( [b₅,b₆] in Web b₂ & ( b₅ = b₆ implies b₃ = b₄ ) ) ) ) )

proof end;

definition

let c₁ be Coherence_Space;
func 'not' c₁ -> set equals :: COHSP_1:def 22
{ b₁ where B is Subset of (union a₁) : for b₁ being Element of a₁ ex b₂ being set st b₁ /\ b₂ c= {b₃} } ;
correctness ;

end;

:: deftheorem Def22 defines 'not' COHSP_1:def 22 :

theorem Th66: :: COHSP_1:66

for b₁ being Coherence_Space
for b₂ being set holds
( b₂ in 'not' b₁ iff ( b₂ c= union b₁ & ( for b₃ being Element of b₁ ex b₄ being set st b₂ /\ b₃ c= {b₄} ) ) )

proof end;

registration

let c₁ be Coherence_Space;
cluster 'not' a₁ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th67: :: COHSP_1:67

for b₁ being Coherence_Space holds union ('not' b₁) = union b₁

proof end;

theorem Th68: :: COHSP_1:68

for b₁ being Coherence_Space
for b₂, b₃ being set st b₂ <> b₃ & {b₂,b₃} in b₁ holds
not {b₂,b₃} in 'not' b₁

proof end;

theorem Th69: :: COHSP_1:69

for b₁ being Coherence_Space
for b₂, b₃ being set st {b₂,b₃} c= union b₁ & not {b₂,b₃} in b₁ holds
{b₂,b₃} in 'not' b₁

proof end;

theorem Th70: :: COHSP_1:70

for b₁ being Coherence_Space
for b₂, b₃ being set holds
( [b₂,b₃] in Web ('not' b₁) iff ( b₂ in union b₁ & b₃ in union b₁ & ( b₂ = b₃ or not [b₂,b₃] in Web b₁ ) ) )

proof end;

Lemma70: for b₁ being Coherence_Space holds 'not' ('not' b₁) c= b₁

proof end;

theorem Th71: :: COHSP_1:71

for b₁ being Coherence_Space holds 'not' ('not' b₁) = b₁

proof end;

theorem Th72: :: COHSP_1:72

'not' {{} } = {{} }

proof end;

theorem Th73: :: COHSP_1:73

for b₁ being set holds
( 'not' (FlatCoh b₁) = bool b₁ & 'not' (bool b₁) = FlatCoh b₁ )

proof end;

definition

let c₁, c₂ be set ;
func c₁ U+ c₂ -> set equals :: COHSP_1:def 23
Union (disjoin <*a₁,a₂*>);
correctness ;

end;

:: deftheorem Def23 defines U+ COHSP_1:def 23 :

theorem Th74: :: COHSP_1:74

for b₁, b₂ being set holds b₁ U+ b₂ = [:b₁,{1}:] \/ [:b₂,{2}:]

proof end;

theorem Th75: :: COHSP_1:75

for b₁ being set holds
( b₁ U+ {} = [:b₁,{1}:] & {} U+ b₁ = [:b₁,{2}:] )

proof end;

theorem Th76: :: COHSP_1:76

for b₁, b₂, b₃ being set st b₃ in b₁ U+ b₂ holds
( b₃ = [(b₃ `1 ),(b₃ `2 )] & ( ( b₃ `2 = 1 & b₃ `1 in b₁ ) or ( b₃ `2 = 2 & b₃ `1 in b₂ ) ) )

proof end;

theorem Th77: :: COHSP_1:77

for b₁, b₂, b₃ being set holds
( [b₃,1] in b₁ U+ b₂ iff b₃ in b₁ )

proof end;

theorem Th78: :: COHSP_1:78

for b₁, b₂, b₃ being set holds
( [b₃,2] in b₁ U+ b₂ iff b₃ in b₂ )

proof end;

theorem Th79: :: COHSP_1:79

for b₁, b₂, b₃, b₄ being set holds
( b₁ U+ b₂ c= b₃ U+ b₄ iff ( b₁ c= b₃ & b₂ c= b₄ ) )

proof end;

theorem Th80: :: COHSP_1:80

for b₁, b₂, b₃ being set st b₃ c= b₁ U+ b₂ holds
ex b₄, b₅ being set st
( b₃ = b₄ U+ b₅ & b₄ c= b₁ & b₅ c= b₂ )

proof end;

theorem Th81: :: COHSP_1:81

for b₁, b₂, b₃, b₄ being set holds
( b₁ U+ b₂ = b₃ U+ b₄ iff ( b₁ = b₃ & b₂ = b₄ ) )

proof end;

theorem Th82: :: COHSP_1:82

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

proof end;

theorem Th83: :: COHSP_1:83

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

proof end;

definition

let c₁, c₂ be Coherence_Space;
func c₁ "/\" c₂ -> set equals :: COHSP_1:def 24
{ (b₁ U+ b₂) where B is Element of a₁, B is Element of a₂ : verum } ;
correctness ;
func c₁ "\/" c₂ -> set equals :: COHSP_1:def 25
{ (b₁ U+ {} ) where B is Element of a₁ : verum } \/ { ({} U+ b₁) where B is Element of a₂ : verum } ;
correctness ;

end;

:: deftheorem Def24 defines "/\" COHSP_1:def 24 :

:: deftheorem Def25 defines "\/" COHSP_1:def 25 :

theorem Th84: :: COHSP_1:84

for b₁, b₂ being Coherence_Space
for b₃ being set holds
( b₃ in b₁ "/\" b₂ iff ex b₄ being Element of b₁ex b₅ being Element of b₂ st b₃ = b₄ U+ b₅ ) ;

theorem Th85: :: COHSP_1:85

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( b₃ U+ b₄ in b₁ "/\" b₂ iff ( b₃ in b₁ & b₄ in b₂ ) )

proof end;

theorem Th86: :: COHSP_1:86

for b₁, b₂ being Coherence_Space holds union (b₁ "/\" b₂) = (union b₁) U+ (union b₂)

proof end;

theorem Th87: :: COHSP_1:87

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( b₃ U+ b₄ in b₁ "\/" b₂ iff ( ( b₃ in b₁ & b₄ = {} ) or ( b₃ = {} & b₄ in b₂ ) ) )

proof end;

theorem Th88: :: COHSP_1:88

for b₁, b₂ being Coherence_Space
for b₃ being set st b₃ in b₁ "\/" b₂ holds
ex b₄ being Element of b₁ex b₅ being Element of b₂ st
( b₃ = b₄ U+ b₅ & ( b₄ = {} or b₅ = {} ) )

proof end;

theorem Th89: :: COHSP_1:89

for b₁, b₂ being Coherence_Space holds union (b₁ "\/" b₂) = (union b₁) U+ (union b₂)

proof end;

registration

let c₁, c₂ be Coherence_Space;
cluster a₁ "/\" a₂ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

cluster a₁ "\/" a₂ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th90: :: COHSP_1:90

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( [[b₃,1],[b₄,1]] in Web (b₁ "/\" b₂) iff [b₃,b₄] in Web b₁ )

proof end;

theorem Th91: :: COHSP_1:91

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( [[b₃,2],[b₄,2]] in Web (b₁ "/\" b₂) iff [b₃,b₄] in Web b₂ )

proof end;

theorem Th92: :: COHSP_1:92

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set st b₃ in union b₁ & b₄ in union b₂ holds
( [[b₃,1],[b₄,2]] in Web (b₁ "/\" b₂) & [[b₄,2],[b₃,1]] in Web (b₁ "/\" b₂) )

proof end;

theorem Th93: :: COHSP_1:93

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( [[b₃,1],[b₄,1]] in Web (b₁ "\/" b₂) iff [b₃,b₄] in Web b₁ )

proof end;

theorem Th94: :: COHSP_1:94

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( [[b₃,2],[b₄,2]] in Web (b₁ "\/" b₂) iff [b₃,b₄] in Web b₂ )

proof end;

theorem Th95: :: COHSP_1:95

for b₁, b₂ being Coherence_Space
for b₃, b₄ being set holds
( not [[b₃,1],[b₄,2]] in Web (b₁ "\/" b₂) & not [[b₄,2],[b₃,1]] in Web (b₁ "\/" b₂) )

proof end;

theorem Th96: :: COHSP_1:96

for b₁, b₂ being Coherence_Space holds 'not' (b₁ "/\" b₂) = ('not' b₁) "\/" ('not' b₂)

proof end;

definition

let c₁, c₂ be Coherence_Space;
func c₁ [*] c₂ -> set equals :: COHSP_1:def 26
union { (bool [:b₁,b₂:]) where B is Element of a₁, B is Element of a₂ : verum } ;
correctness ;

end;

:: deftheorem Def26 defines [*] COHSP_1:def 26 :

theorem Th97: :: COHSP_1:97

for b₁, b₂ being Coherence_Space
for b₃ being set holds
( b₃ in b₁ [*] b₂ iff ex b₄ being Element of b₁ex b₅ being Element of b₂ st b₃ c= [:b₄,b₅:] )

proof end;

registration

let c₁, c₂ be Coherence_Space;
cluster a₁ [*] a₂ -> non empty ;
coherence

proof end;

end;

theorem Th98: :: COHSP_1:98

for b₁, b₂ being Coherence_Space
for b₃ being Element of b₁ [*] b₂ holds
( proj1 b₃ in b₁ & proj2 b₃ in b₂ & b₃ c= [:(proj1 b₃),(proj2 b₃):] )

proof end;

registration

let c₁, c₂ be Coherence_Space;
cluster a₁ [*] a₂ -> non empty multiplicative subset-closed binary_complete d.union-closed ;
coherence

proof end;

end;

theorem Th99: :: COHSP_1:99

for b₁, b₂ being Coherence_Space holds union (b₁ [*] b₂) = [:(union b₁),(union b₂):]

proof end;

theorem Th100: :: COHSP_1:100

for b₁, b₂ being Coherence_Space
for b₃, b₄, b₅, b₆ being set holds
( [[b₃,b₅],[b₄,b₆]] in Web (b₁ [*] b₂) iff ( [b₃,b₄] in Web b₁ & [b₅,b₆] in Web b₂ ) )

proof end;