PCS_0: Basic Operations on Preordered Coherent Spaces

:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users

begin

reconsider z = 0 , j = 1 as Element of {0,1} by TARSKI:def 2;

definition

let R1, R2 be set ;
let R be Relation of R1,R2;
:: original: field
redefine func field R -> Subset of (R1 \/ R2);
coherence by RELSET_1:8;

end;

definition

let R1, R2, S1, S2 be set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
:: original: \/
redefine func R \/ S -> Relation of (R1 \/ S1),(R2 \/ S2);
coherence by ZFMISC_1:119;

end;

registration

let R1, S1 be set ;
let R be total Relation of R1;
let S be total Relation of S1;

cluster R \/ S -> total for Relation of (R1 \/ S1);

coherence

proof end;

end;

registration

let R1, S1 be set ;
let R be reflexive Relation of R1;
let S be reflexive Relation of S1;

cluster R \/ S -> reflexive for Relation of (R1 \/ S1);

coherence ;

end;

registration

let R1, S1 be set ;
let R be symmetric Relation of R1;
let S be symmetric Relation of S1;

cluster R \/ S -> symmetric for Relation of (R1 \/ S1);

coherence ;

end;

Lm1: now :: thesis:

let R1, S1 be set ; :: thesis:
let R be Relation of R1; :: thesis:
let S be Relation of S1; :: thesis:
assume A1: R1 misses S1 ; :: thesis:
let q1, q2 be set ; :: thesis:
assume that
A2: [q1,q2] in R \/ S and
A3: q2 in S1 ; :: thesis:
A4: ( [q1,q2] in R or [q1,q2] in S ) by A2, XBOOLE_0:def 3;

now :: thesis:

assume [q1,q2] in R ; :: thesis:
then q2 in R1 by ZFMISC_1:87;
hence contradiction by A1, A3, XBOOLE_0:3; :: thesis:

end;

hence ( [q1,q2] in S & q1 in S1 ) by A4, ZFMISC_1:87; :: thesis:

end;

theorem Th1: :: PCS_0:1

for R1, S1 being set
for R being transitive Relation of R1
for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive

proof end;

definition

let I be non empty set ;
let C be 1-sorted-yielding ManySortedSet of I;

redefine func Carrier C means :Def1: :: PCS_0:def 1
for i being Element of I holds it . i = the carrier of (C . i);

compatibility

proof end;

end;

:: deftheorem Def1 defines Carrier PCS_0:def 1 :

definition

let R1, R2, S1, S2 be set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
defpred S₁[ set , set ] means ex r1, s1, r2, s2 being set st
( $1 = [r1,s1] & $2 = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) );

func [^R,S^] -> Relation of [:R1,S1:],[:R2,S2:] means :Def2: :: PCS_0:def 2
for x, y being set holds
( [x,y] in it iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines [^ PCS_0:def 2 :

definition

let R1, R2, S1, S2 be non empty set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;

redefine func [^R,S^] means :Def3: :: PCS_0:def 3
for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in it iff ( [r1,r2] in R or [s1,s2] in S ) );

compatibility

proof end;

end;

:: deftheorem Def3 defines [^ PCS_0:def 3 :

registration

let R1, S1 be set ;
let R be total Relation of R1;
let S be total Relation of S1;

cluster [^R,S^] -> total ;

coherence

proof end;

end;

registration

let R1, S1 be set ;
let R be reflexive Relation of R1;
let S be reflexive Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence

proof end;

end;

registration

let R1, S1 be set ;
let R be Relation of R1;
let S be total reflexive Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence

proof end;

end;

registration

let R1, S1 be set ;
let R be total reflexive Relation of R1;
let S be Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence

proof end;

end;

registration

let R1, S1 be set ;
let R be symmetric Relation of R1;
let S be symmetric Relation of S1;

cluster [^R,S^] -> symmetric ;

coherence

proof end;

end;

begin

registration

cluster empty -> total for RelStr ;

coherence

proof end;

end;

definition

let R be Relation;

attr R is transitive-yielding means :Def4: :: PCS_0:def 4
for S being RelStr st S in rng R holds
S is transitive ;

end;

:: deftheorem Def4 defines transitive-yielding PCS_0:def 4 :

registration

cluster Relation-like Poset-yielding -> transitive-yielding for set ;

coherence

proof end;

end;

registration

cluster Relation-like Function-like Poset-yielding for set ;

existence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total Poset-yielding for set ;

existence

proof end;

end;

definition

let I be set ;
let C be RelStr-yielding ManySortedSet of I;

func pcs-InternalRels C -> ManySortedSet of I means :Def5: :: PCS_0:def 5
for i being set st i in I holds
ex P being RelStr st
( P = C . i & it . i = the InternalRel of P );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines pcs-InternalRels PCS_0:def 5 :

definition

let I be non empty set ;
let C be RelStr-yielding ManySortedSet of I;

redefine func pcs-InternalRels C means :Def6: :: PCS_0:def 6
for i being Element of I holds it . i = the InternalRel of (C . i);

compatibility

proof end;

end;

:: deftheorem Def6 defines pcs-InternalRels PCS_0:def 6 :

registration

let I be set ;
let C be RelStr-yielding ManySortedSet of I;

cluster pcs-InternalRels C -> Relation-yielding ;

coherence

proof end;

end;

registration

let I be non empty set ;
let C be RelStr-yielding transitive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> transitive for RelStr ;

coherence

proof end;

end;

begin

definition

attr c₁ is strict ;
struct TolStr -> 1-sorted ;
aggr TolStr(# carrier, ToleranceRel #) -> TolStr ;
sel ToleranceRel c₁ -> Relation of the carrier of c₁;

end;

definition

let P be TolStr ;
let p, q be Element of P;

pred p (--) q means :Def7: :: PCS_0:def 7
[p,q] in the ToleranceRel of P;

end;

:: deftheorem Def7 defines (--) PCS_0:def 7 :

definition

let P be TolStr ;

attr P is pcs-tol-total means :Def8: :: PCS_0:def 8
the ToleranceRel of P is total ;

attr P is pcs-tol-reflexive means :Def9: :: PCS_0:def 9
the ToleranceRel of P is_reflexive_in the carrier of P;

attr P is pcs-tol-irreflexive means :Def10: :: PCS_0:def 10
the ToleranceRel of P is_irreflexive_in the carrier of P;

attr P is pcs-tol-symmetric means :Def11: :: PCS_0:def 11
the ToleranceRel of P is_symmetric_in the carrier of P;

end;

:: deftheorem Def8 defines pcs-tol-total PCS_0:def 8 :

:: deftheorem Def9 defines pcs-tol-reflexive PCS_0:def 9 :

:: deftheorem Def10 defines pcs-tol-irreflexive PCS_0:def 10 :

:: deftheorem Def11 defines pcs-tol-symmetric PCS_0:def 11 :

definition

func emptyTolStr -> TolStr equals :: PCS_0:def 12
TolStr(# {},({} ({},{})) #);

coherence ;

end;

:: deftheorem defines emptyTolStr PCS_0:def 12 :

registration

cluster emptyTolStr -> empty strict ;

coherence ;

end;

theorem Th2: :: PCS_0:2

for P being TolStr st P is empty holds
TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr

proof end;

registration

cluster pcs-tol-reflexive -> pcs-tol-total for TolStr ;

coherence

proof end;

end;

registration

cluster empty -> pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;

coherence

proof end;

end;

registration

cluster empty strict for TolStr ;

existence

proof end;

end;

registration

let P be pcs-tol-total TolStr ;

cluster the ToleranceRel of P -> total ;

coherence by Def8;

end;

registration

let P be pcs-tol-reflexive TolStr ;

cluster the ToleranceRel of P -> reflexive ;

coherence

proof end;

end;

registration

let P be pcs-tol-irreflexive TolStr ;

cluster the ToleranceRel of P -> irreflexive ;

coherence

proof end;

end;

registration

let P be pcs-tol-symmetric TolStr ;

cluster the ToleranceRel of P -> symmetric ;

coherence

proof end;

end;

registration

let L be pcs-tol-total TolStr ;

cluster TolStr(# the carrier of L, the ToleranceRel of L #) -> pcs-tol-total ;

coherence by Def8;

end;

definition

let P be pcs-tol-symmetric TolStr ;
let p, q be Element of P;
:: original: (--)
redefine pred p (--) q;
symmetry

proof end;

end;

registration

let D be set ;

cluster TolStr(# D,(nabla D) #) -> pcs-tol-reflexive pcs-tol-symmetric ;

coherence

proof end;

end;

registration

let D be set ;

cluster TolStr(# D,({} (D,D)) #) -> pcs-tol-irreflexive pcs-tol-symmetric ;

coherence

proof end;

end;

registration

cluster non empty strict pcs-tol-reflexive pcs-tol-symmetric for TolStr ;

existence

proof end;

end;

registration

cluster non empty strict pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;

existence

proof end;

end;

definition

let R be Relation;

attr R is TolStr-yielding means :Def13: :: PCS_0:def 13
for P being set st P in rng R holds
P is TolStr ;

end;

:: deftheorem Def13 defines TolStr-yielding PCS_0:def 13 :

definition

let f be Function;

redefine attr f is TolStr-yielding means :Def14: :: PCS_0:def 14
for x being set st x in dom f holds
f . x is TolStr ;

compatibility

proof end;

end;

:: deftheorem Def14 defines TolStr-yielding PCS_0:def 14 :

definition

let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;

:: original: TolStr-yielding
redefine attr f is TolStr-yielding means :: PCS_0:def 15
for x being set st x in I holds
f . x is TolStr ;

compatibility by A1, Def14;

end;

:: deftheorem defines TolStr-yielding PCS_0:def 15 :

definition

let R be Relation;

attr R is pcs-tol-reflexive-yielding means :Def16: :: PCS_0:def 16
for S being TolStr st S in rng R holds
S is pcs-tol-reflexive ;

attr R is pcs-tol-irreflexive-yielding means :Def17: :: PCS_0:def 17
for S being TolStr st S in rng R holds
S is pcs-tol-irreflexive ;

attr R is pcs-tol-symmetric-yielding means :Def18: :: PCS_0:def 18
for S being TolStr st S in rng R holds
S is pcs-tol-symmetric ;

end;

:: deftheorem Def16 defines pcs-tol-reflexive-yielding PCS_0:def 16 :

:: deftheorem Def17 defines pcs-tol-irreflexive-yielding PCS_0:def 17 :

:: deftheorem Def18 defines pcs-tol-symmetric-yielding PCS_0:def 18 :

registration

cluster Relation-like empty -> pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;

coherence

proof end;

end;

registration

let I be set ;
let P be TolStr ;

cluster I --> P -> () for ManySortedSet of I;

coherence

proof end;

end;

registration

let I be set ;
let P be pcs-tol-reflexive TolStr ;

cluster I --> P -> pcs-tol-reflexive-yielding for ManySortedSet of I;

coherence

proof end;

end;

registration

let I be set ;
let P be pcs-tol-irreflexive TolStr ;

cluster I --> P -> pcs-tol-irreflexive-yielding for ManySortedSet of I;

coherence

proof end;

end;

registration

let I be set ;
let P be pcs-tol-symmetric TolStr ;

cluster I --> P -> pcs-tol-symmetric-yielding for ManySortedSet of I;

coherence

proof end;

end;

registration

cluster Relation-like Function-like TolStr-yielding -> 1-sorted-yielding for set ;

coherence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;

existence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;

existence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () for set ;

existence

proof end;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> TolStr ;
coherence

proof end;

end;

definition

let I be set ;
let C be () ManySortedSet of I;

func pcs-ToleranceRels C -> ManySortedSet of I means :Def19: :: PCS_0:def 19
for i being set st i in I holds
ex P being TolStr st
( P = C . i & it . i = the ToleranceRel of P );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines pcs-ToleranceRels PCS_0:def 19 :

definition

let I be non empty set ;
let C be () ManySortedSet of I;

redefine func pcs-ToleranceRels C means :Def20: :: PCS_0:def 20
for i being Element of I holds it . i = the ToleranceRel of (C . i);

compatibility

proof end;

end;

:: deftheorem Def20 defines pcs-ToleranceRels PCS_0:def 20 :

registration

let I be set ;
let C be () ManySortedSet of I;

cluster pcs-ToleranceRels C -> Relation-yielding ;

coherence

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-reflexive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-reflexive for TolStr ;

coherence

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-irreflexive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-irreflexive for TolStr ;

coherence

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-symmetric-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-symmetric for TolStr ;

coherence

proof end;

end;

theorem Th3: :: PCS_0:3

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-reflexive holds
Q is pcs-tol-reflexive

proof end;

theorem Th4: :: PCS_0:4

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-irreflexive holds
Q is pcs-tol-irreflexive

proof end;

theorem Th5: :: PCS_0:5

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-symmetric holds
Q is pcs-tol-symmetric

proof end;

definition

let P, Q be TolStr ;

func [^P,Q^] -> TolStr equals :: PCS_0:def 21
TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

coherence ;

end;

:: deftheorem defines [^ PCS_0:def 21 :

notation

let P, Q be TolStr ;
let p be Element of P;
let q be Element of Q;
synonym [^p,q^] for [P,Q];

end;

definition

let P, Q be non empty TolStr ;
let p be Element of P;
let q be Element of Q;
:: original: [^
redefine func [^p,q^] -> Element of [^P,Q^];
coherence

proof end;

end;

notation

let P, Q be TolStr ;
let p be Element of [^P,Q^];
synonym p ^`1 for P `1 ;
synonym p ^`2 for P `2 ;

end;

definition

let P, Q be non empty TolStr ;
let p be Element of [^P,Q^];
:: original: ^`1
redefine func p ^`1 -> Element of P;
coherence by MCART_1:10;
:: original: ^`2
redefine func p ^`2 -> Element of Q;
coherence by MCART_1:10;

end;

theorem Th6: :: PCS_0:6

for S1, S2 being non empty TolStr
for a, c being Element of S1
for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) )

proof end;

theorem :: PCS_0:7

for S1, S2 being non empty TolStr
for x, y being Element of [^S1,S2^] holds
( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) )

proof end;

registration

let P be TolStr ;
let Q be pcs-tol-reflexive TolStr ;

cluster [^P,Q^] -> pcs-tol-reflexive ;

coherence

proof end;

end;

registration

let P be pcs-tol-reflexive TolStr ;
let Q be TolStr ;

cluster [^P,Q^] -> pcs-tol-reflexive ;

coherence

proof end;

end;

registration

let P, Q be pcs-tol-symmetric TolStr ;

cluster [^P,Q^] -> pcs-tol-symmetric ;

coherence

proof end;

end;

begin

definition

attr c₁ is strict ;
struct pcs-Str -> RelStr , TolStr ;
aggr pcs-Str(# carrier, InternalRel, ToleranceRel #) -> pcs-Str ;

end;

definition

let P be pcs-Str ;

attr P is pcs-compatible means :Def22: :: PCS_0:def 22
for p, p9, q, q9 being Element of P st p (--) q & p9 <= p & q9 <= q holds
p9 (--) q9;

end;

:: deftheorem Def22 defines pcs-compatible PCS_0:def 22 :

definition

let P be pcs-Str ;

attr P is pcs-like means :Def23: :: PCS_0:def 23
( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible );

attr P is anti-pcs-like means :Def24: :: PCS_0:def 24
( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible );

end;

:: deftheorem Def23 defines pcs-like PCS_0:def 23 :

:: deftheorem Def24 defines anti-pcs-like PCS_0:def 24 :

registration

cluster pcs-like -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;

coherence by Def23;

cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible -> pcs-like for pcs-Str ;

coherence by Def23;

cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;

coherence by Def24;

cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible -> anti-pcs-like for pcs-Str ;

coherence by Def24;

end;

definition

let D be set ;

func pcs-total D -> pcs-Str equals :: PCS_0:def 25
pcs-Str(# D,(nabla D),(nabla D) #);

coherence ;

end;

:: deftheorem defines pcs-total PCS_0:def 25 :

registration

let D be set ;

cluster pcs-total D -> strict ;

coherence ;

end;

registration

let D be non empty set ;

cluster pcs-total D -> non empty ;

coherence ;

end;

registration

let D be set ;

cluster pcs-total D -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric ;

coherence

proof end;

end;

registration

let D be set ;

cluster pcs-total D -> pcs-like ;

coherence

proof end;

end;

registration

let D be set ;

cluster pcs-Str(# D,(nabla D),({} (D,D)) #) -> anti-pcs-like ;

coherence

proof end;

end;

registration

cluster non empty strict pcs-like for pcs-Str ;

existence

proof end;

cluster non empty strict anti-pcs-like for pcs-Str ;

existence

proof end;

end;

definition

mode pcs is pcs-like pcs-Str ;
mode anti-pcs is anti-pcs-like pcs-Str ;

end;

definition

func pcs-empty -> pcs-Str equals :: PCS_0:def 26
pcs-total 0;

coherence ;

end;

:: deftheorem defines pcs-empty PCS_0:def 26 :

registration

cluster pcs-empty -> empty strict pcs-like ;

coherence ;

end;

definition

let p be set ;

func pcs-singleton p -> pcs-Str equals :: PCS_0:def 27
pcs-total {p};

coherence ;

end;

:: deftheorem defines pcs-singleton PCS_0:def 27 :

registration

let p be set ;

cluster pcs-singleton p -> non empty strict pcs-like ;

coherence ;

end;

definition

let R be Relation;

attr R is pcs-Str-yielding means :Def28: :: PCS_0:def 28
for P being set st P in rng R holds
P is pcs-Str ;

attr R is pcs-yielding means :Def29: :: PCS_0:def 29
for P being set st P in rng R holds
P is pcs;

end;

:: deftheorem Def28 defines pcs-Str-yielding PCS_0:def 28 :

:: deftheorem Def29 defines pcs-yielding PCS_0:def 29 :

definition

let f be Function;

redefine attr f is pcs-Str-yielding means :Def30: :: PCS_0:def 30
for x being set st x in dom f holds
f . x is pcs-Str ;

compatibility

proof end;

redefine attr f is pcs-yielding means :Def31: :: PCS_0:def 31
for x being set st x in dom f holds
f . x is pcs;

compatibility

proof end;

end;

:: deftheorem Def30 defines pcs-Str-yielding PCS_0:def 30 :

:: deftheorem Def31 defines pcs-yielding PCS_0:def 31 :

definition

let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;

:: original: pcs-Str-yielding
redefine attr f is pcs-Str-yielding means :Def32: :: PCS_0:def 32
for x being set st x in I holds
f . x is pcs-Str ;

compatibility by A1, Def30;

:: original: pcs-yielding
redefine attr f is pcs-yielding means :Def33: :: PCS_0:def 33
for x being set st x in I holds
f . x is pcs;

compatibility by A1, Def31;

end;

:: deftheorem Def32 defines pcs-Str-yielding PCS_0:def 32 :

:: deftheorem Def33 defines pcs-yielding PCS_0:def 33 :

registration

cluster Relation-like pcs-Str-yielding -> RelStr-yielding TolStr-yielding for set ;

coherence

proof end;

cluster Relation-like pcs-yielding -> pcs-Str-yielding for set ;

coherence

proof end;

cluster Relation-like pcs-yielding -> reflexive-yielding transitive-yielding pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;

coherence

proof end;

end;

registration

let I be set ;
let P be pcs;

cluster I --> P -> () for ManySortedSet of I;

coherence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () for set ;

existence

proof end;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> pcs-Str ;
coherence by Def32;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> pcs;
coherence by Def33;

end;

:: Union of PCS's

definition

let P, Q be pcs-Str ;

pred P c= Q means :Def34: :: PCS_0:def 34
( the carrier of P c= the carrier of Q & the InternalRel of P c= the InternalRel of Q & the ToleranceRel of P c= the ToleranceRel of Q );

reflexivity ;

end;

:: deftheorem Def34 defines c= PCS_0:def 34 :

theorem Th8: :: PCS_0:8

for P, Q being RelStr
for p, q being Element of P
for p1, q1 being Element of Q st the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q holds
p1 <= q1

proof end;

theorem Th9: :: PCS_0:9

for P, Q being TolStr
for p, q being Element of P
for p1, q1 being Element of Q st the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q holds
p1 (--) q1

proof end;

Lm2: for P, Q being pcs-Str
for p being set st p in the carrier of P & P c= Q holds
p is Element of Q

proof end;

definition

let C be Relation;

attr C is pcs-chain-like means :Def35: :: PCS_0:def 35
for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds
Q c= P;

end;

:: deftheorem Def35 defines pcs-chain-like PCS_0:def 35 :

registration

let I be set ;
let P be pcs-Str ;

cluster I --> P -> pcs-chain-like for ManySortedSet of I;

coherence

proof end;

end;

registration

cluster Relation-like Function-like pcs-yielding pcs-chain-like for set ;

existence

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-chain-like for set ;

existence

proof end;

end;

definition

let I be set ;
mode pcs-Chain of I is () pcs-chain-like ManySortedSet of I;

end;

definition

let I be set ;
let C be () ManySortedSet of I;

func pcs-union C -> strict pcs-Str means :Def36: :: PCS_0:def 36
( the carrier of it = Union (Carrier C) & the InternalRel of it = Union (pcs-InternalRels C) & the ToleranceRel of it = Union (pcs-ToleranceRels C) );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def36 defines pcs-union PCS_0:def 36 :

theorem Th10: :: PCS_0:10

for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being set ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 ) )

proof end;

theorem :: PCS_0:11

for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) )

proof end;

theorem Th12: :: PCS_0:12

for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being set ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )

proof end;

theorem :: PCS_0:13

for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 (--) q9 ) )

proof end;

registration

let I be set ;
let C be reflexive-yielding () ManySortedSet of I;

cluster pcs-union C -> reflexive strict ;

coherence

proof end;

end;

registration

let I be set ;
let C be pcs-tol-reflexive-yielding () ManySortedSet of I;

cluster pcs-union C -> pcs-tol-reflexive strict ;

coherence

proof end;

end;

registration

let I be set ;
let C be pcs-tol-symmetric-yielding () ManySortedSet of I;

cluster pcs-union C -> pcs-tol-symmetric strict ;

coherence

proof end;

end;

registration

let I be set ;
let C be pcs-Chain of I;

cluster pcs-union C -> transitive strict pcs-compatible ;

coherence

proof end;

end;

:: Direct Sum of PCS's

registration

let p, q be set ;

cluster <%p,q%> -> {0,1} -defined ;

coherence

proof end;

cluster <%p,q%> -> total ;

coherence

proof end;

end;

registration

let P, Q be 1-sorted ;

cluster <%P,Q%> -> 1-sorted-yielding ;

coherence

proof end;

end;

Lm3: now :: thesis:

let a, b be set ; :: thesis:
<%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;
hence rng <%a,b%> = {a,b} by FUNCT_4:64; :: thesis:

end;

registration

let P, Q be RelStr ;

cluster <%P,Q%> -> RelStr-yielding ;

coherence

proof end;

end;

registration

let P, Q be TolStr ;

cluster <%P,Q%> -> () ;

coherence

proof end;

end;

registration

let P, Q be pcs-Str ;

cluster <%P,Q%> -> () ;

coherence

proof end;

end;

registration

let P, Q be reflexive pcs-Str ;

cluster <%P,Q%> -> reflexive-yielding ;

coherence

proof end;

end;

registration

let P, Q be transitive pcs-Str ;

cluster <%P,Q%> -> transitive-yielding ;

coherence

proof end;

end;

registration

let P, Q be pcs-tol-reflexive pcs-Str ;

cluster <%P,Q%> -> pcs-tol-reflexive-yielding ;

coherence

proof end;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster <%P,Q%> -> pcs-tol-symmetric-yielding ;

coherence

proof end;

end;

registration

let P, Q be pcs;

cluster <%P,Q%> -> () ;

coherence

proof end;

end;

definition

canceled;
let P, Q be pcs-Str ;

func pcs-sum (P,Q) -> pcs-Str equals :: PCS_0:def 38
pcs-union <%P,Q%>;

coherence ;

end;

:: deftheorem PCS_0:def 37 :

:: deftheorem defines pcs-sum PCS_0:def 38 :

deffunc H₁( pcs-Str , pcs-Str ) -> pcs-Str = pcs-Str(# ( the carrier of $1 \/ the carrier of $2),( the InternalRel of $1 \/ the InternalRel of $2),( the ToleranceRel of $1 \/ the ToleranceRel of $2) #);

theorem Th14: :: PCS_0:14

for P, Q being pcs-Str holds
( the carrier of (pcs-sum (P,Q)) = the carrier of P \/ the carrier of Q & the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q )

proof end;

theorem Th15: :: PCS_0:15

for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-Str(# ( the carrier of P \/ the carrier of Q),( the InternalRel of P \/ the InternalRel of Q),( the ToleranceRel of P \/ the ToleranceRel of Q) #)

proof end;

theorem :: PCS_0:16

for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p <= q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 <= q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 <= q9 ) ) )

proof end;

theorem :: PCS_0:17

for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )

proof end;

registration

let P, Q be reflexive pcs-Str ;

cluster pcs-sum (P,Q) -> reflexive ;

coherence ;

end;

registration

let P, Q be pcs-tol-reflexive pcs-Str ;

cluster pcs-sum (P,Q) -> pcs-tol-reflexive ;

coherence ;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster pcs-sum (P,Q) -> pcs-tol-symmetric ;

coherence ;

end;

theorem Th18: :: PCS_0:18

for P, Q being pcs st P misses Q holds
the InternalRel of (pcs-sum (P,Q)) is transitive

proof end;

theorem Th19: :: PCS_0:19

for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs-compatible

proof end;

theorem :: PCS_0:20

for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs

proof end;

:: Extension

definition

let P be pcs-Str ;
let a be set ;

func pcs-extension (P,a) -> strict pcs-Str means :Def39: :: PCS_0:def 39
( the carrier of it = {a} \/ the carrier of P & the InternalRel of it = [:{a}, the carrier of it:] \/ the InternalRel of P & the ToleranceRel of it = ([:{a}, the carrier of it:] \/ [: the carrier of it,{a}:]) \/ the ToleranceRel of P );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def39 defines pcs-extension PCS_0:def 39 :

registration

let P be pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> non empty strict ;

coherence

proof end;

end;

theorem Th21: :: PCS_0:21

for P being pcs-Str
for a being set holds
( the carrier of P c= the carrier of (pcs-extension (P,a)) & the InternalRel of P c= the InternalRel of (pcs-extension (P,a)) & the ToleranceRel of P c= the ToleranceRel of (pcs-extension (P,a)) )

proof end;

theorem :: PCS_0:22

for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
p <= q

proof end;

theorem Th23: :: PCS_0:23

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <= q holds
p1 <= q1

proof end;

theorem Th24: :: PCS_0:24

for P being pcs-Str
for a being set
for p being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )

proof end;

theorem Th25: :: PCS_0:25

for P being pcs-Str
for a being set
for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P

proof end;

theorem Th26: :: PCS_0:26

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & p1 <= q1 holds
p <= q

proof end;

theorem Th27: :: PCS_0:27

for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
( p (--) q & q (--) p )

proof end;

theorem Th28: :: PCS_0:28

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p (--) q holds
p1 (--) q1

proof end;

theorem Th29: :: PCS_0:29

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q

proof end;

registration

let P be reflexive pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> reflexive strict ;

coherence

proof end;

end;

theorem Th30: :: PCS_0:30

for P being transitive pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is transitive

proof end;

registration

let P be pcs-tol-reflexive pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> pcs-tol-reflexive strict ;

coherence

proof end;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> pcs-tol-symmetric strict ;

coherence

proof end;

end;

theorem Th31: :: PCS_0:31

for P being pcs-compatible pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible

proof end;

theorem :: PCS_0:32

for P being pcs
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs

proof end;

:: Reverse

definition

let P be pcs-Str ;

func pcs-reverse P -> strict pcs-Str means :Def40: :: PCS_0:def 40
( the carrier of it = the carrier of P & the InternalRel of it = the InternalRel of P ~ & the ToleranceRel of it = the ToleranceRel of P ` );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def40 defines pcs-reverse PCS_0:def 40 :

registration

let P be non empty pcs-Str ;

cluster pcs-reverse P -> non empty strict ;

coherence

proof end;

end;

theorem Th33: :: PCS_0:33

for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds
( p <= q iff q9 <= p9 )

proof end;

theorem Th34: :: PCS_0:34

for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds
not p9 (--) q9

proof end;

theorem Th35: :: PCS_0:35

for P being non empty pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds
p (--) q

proof end;

registration

let P be reflexive pcs-Str ;

cluster pcs-reverse P -> reflexive strict ;

coherence

proof end;

end;

registration

let P be transitive pcs-Str ;

cluster pcs-reverse P -> transitive strict ;

coherence

proof end;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;

cluster pcs-reverse P -> pcs-tol-irreflexive strict ;

coherence

proof end;

end;

registration

let P be pcs-tol-irreflexive pcs-Str ;

cluster pcs-reverse P -> pcs-tol-reflexive strict ;

coherence

proof end;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;

cluster pcs-reverse P -> pcs-tol-symmetric strict ;

coherence

proof end;

end;

registration

let P be pcs-compatible pcs-Str ;

cluster pcs-reverse P -> strict pcs-compatible ;

coherence

proof end;

end;

:: Times

definition

let P, Q be pcs-Str ;

func P pcs-times Q -> pcs-Str equals :: PCS_0:def 41
pcs-Str(# [: the carrier of P, the carrier of Q:],[" the InternalRel of P, the InternalRel of Q"],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

coherence ;

end;

:: deftheorem defines pcs-times PCS_0:def 41 :

registration

let P, Q be pcs-Str ;

cluster P pcs-times Q -> strict ;

coherence ;

end;

registration

let P, Q be non empty pcs-Str ;

cluster P pcs-times Q -> non empty ;

coherence ;

end;

theorem :: PCS_0:36

for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p1 <= p2 & q1 <= q2 ) )

proof end;

theorem :: PCS_0:37

for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds
q1 (--) q2

proof end;

theorem Th38: :: PCS_0:38

for P, Q being non empty pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q

proof end;

registration

let P, Q be reflexive pcs-Str ;

cluster P pcs-times Q -> reflexive ;

coherence

proof end;

end;

registration

let P, Q be transitive pcs-Str ;

cluster P pcs-times Q -> transitive ;

coherence

proof end;

end;

registration

let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;

cluster P pcs-times Q -> pcs-tol-reflexive ;

coherence

proof end;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;
let Q be pcs-Str ;

cluster P pcs-times Q -> pcs-tol-reflexive ;

coherence

proof end;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster P pcs-times Q -> pcs-tol-symmetric ;

coherence

proof end;

end;

registration

let P, Q be pcs-compatible pcs-Str ;

cluster P pcs-times Q -> pcs-compatible ;

coherence

proof end;

end;

definition

let P, Q be pcs-Str ;

func P --> Q -> pcs-Str equals :: PCS_0:def 42
(pcs-reverse P) pcs-times Q;

coherence ;

end;

:: deftheorem defines --> PCS_0:def 42 :

registration

let P, Q be pcs-Str ;

cluster P --> Q -> strict ;

coherence ;

end;

registration

let P, Q be non empty pcs-Str ;

cluster P --> Q -> non empty ;

coherence ;

end;

theorem :: PCS_0:39

for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )

proof end;

theorem :: PCS_0:40

for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2

proof end;

theorem :: PCS_0:41

for P, Q being non empty pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q

proof end;

registration

let P, Q be reflexive pcs-Str ;

cluster P --> Q -> reflexive ;

coherence ;

end;

registration

let P, Q be transitive pcs-Str ;

cluster P --> Q -> transitive ;

coherence ;

end;

registration

let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;

cluster P --> Q -> pcs-tol-reflexive ;

coherence ;

end;

registration

let P be pcs-tol-irreflexive pcs-Str ;
let Q be pcs-Str ;

cluster P --> Q -> pcs-tol-reflexive ;

coherence ;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster P --> Q -> pcs-tol-symmetric ;

coherence ;

end;

registration

let P, Q be pcs-compatible pcs-Str ;

cluster P --> Q -> pcs-compatible ;

coherence ;

end;

registration

let P, Q be pcs;

cluster P --> Q -> pcs-like ;

coherence ;

end;

:: Self-coherence

definition

let P be TolStr ;
let S be Subset of P;

attr S is pcs-self-coherent means :Def43: :: PCS_0:def 43
for x, y being Element of P st x in S & y in S holds
x (--) y;

end;

:: deftheorem Def43 defines pcs-self-coherent PCS_0:def 43 :

registration

let P be TolStr ;

cluster empty -> pcs-self-coherent for Element of bool the carrier of P;

coherence

proof end;

end;

definition

let P be TolStr ;
let F be Subset-Family of P;

attr F is pcs-self-coherent-membered means :Def44: :: PCS_0:def 44
for S being Subset of P st S in F holds
S is pcs-self-coherent ;

end;

:: deftheorem Def44 defines pcs-self-coherent-membered PCS_0:def 44 :

registration

let P be TolStr ;

cluster non empty pcs-self-coherent-membered for Element of bool (bool the carrier of P);

existence

proof end;

end;

definition

let P be RelStr ;
let D be set ;
defpred S₁[ set , set ] means ( $1 in D & $2 in D & ( for a being set st a in $1 holds
ex b being set st
( b in $2 & [a,b] in the InternalRel of P ) ) );

func pcs-general-power-IR (P,D) -> Relation of D means :Def45: :: PCS_0:def 45
for A, B being set holds
( [A,B] in it iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 45 :

definition

let P be TolStr ;
let D be set ;
defpred S₁[ set , set ] means ( $1 in D & $2 in D & ( for a, b being set st a in $1 & b in $2 holds
[a,b] in the ToleranceRel of P ) );

func pcs-general-power-TR (P,D) -> Relation of D means :Def46: :: PCS_0:def 46
for A, B being set holds
( [A,B] in it iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def 46 :

theorem :: PCS_0:42

for P being RelStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-IR (P,D) iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )

proof end;

theorem :: PCS_0:43

for P being TolStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-TR (P,D) iff ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds
a (--) b ) ) )

proof end;

definition

let P be pcs-Str ;
let D be set ;

func pcs-general-power (P,D) -> pcs-Str equals :: PCS_0:def 47
pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

coherence ;

end;

:: deftheorem defines pcs-general-power PCS_0:def 47 :

notation

let P be pcs-Str ;
let D be Subset-Family of P;
synonym pcs-general-power D for pcs-general-power (P,D);

end;

registration

let P be pcs-Str ;
let D be non empty set ;

cluster pcs-general-power (P,D) -> non empty ;

coherence ;

end;

theorem Th44: :: PCS_0:44

for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p <= q holds
for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 )

proof end;

theorem :: PCS_0:45

for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 ) ) holds
p <= q

proof end;

theorem Th46: :: PCS_0:46

for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p (--) q holds
for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9

proof end;

theorem :: PCS_0:47

for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ) holds
p (--) q

proof end;

registration

let P be pcs-Str ;
let D be set ;

cluster pcs-general-power (P,D) -> strict ;

coherence ;

end;

registration

let P be reflexive pcs-Str ;
let D be Subset-Family of P;

cluster pcs-general-power (P,D) -> reflexive ;

coherence

proof end;

end;