:: by Klaus E. Grue and Artur Korni{\l}owicz

::

:: Received August 28, 2007

:: Copyright (c) 2007-2019 Association of Mizar Users

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

field R is Subset of (R1 \/ R2) by RELSET_1:8;

end;
let R be Relation of R1,R2;

:: original: field

redefine func field R -> Subset of (R1 \/ R2);

coherence

field R is Subset of (R1 \/ R2) by RELSET_1:8;

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

R \/ S is Relation of (R1 \/ S1),(R2 \/ S2) by ZFMISC_1:119;

end;
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

R \/ S is Relation of (R1 \/ S1),(R2 \/ S2) by ZFMISC_1:119;

registration

let R1, S1 be set ;

let R be total Relation of R1;

let S be total Relation of S1;

coherence

for b_{1} being Relation of (R1 \/ S1) st b_{1} = R \/ S holds

b_{1} is total

end;
let R be total Relation of R1;

let S be total Relation of S1;

coherence

for b

b

proof end;

registration

let R1, S1 be set ;

let R be reflexive Relation of R1;

let S be reflexive Relation of S1;

coherence

for b_{1} being Relation of (R1 \/ S1) st b_{1} = R \/ S holds

b_{1} is reflexive
;

end;
let R be reflexive Relation of R1;

let S be reflexive Relation of S1;

coherence

for b

b

registration

let R1, S1 be set ;

let R be symmetric Relation of R1;

let S be symmetric Relation of S1;

coherence

for b_{1} being Relation of (R1 \/ S1) st b_{1} = R \/ S holds

b_{1} is symmetric
;

end;
let R be symmetric Relation of R1;

let S be symmetric Relation of S1;

coherence

for b

b

Lm1: now :: thesis: for R1, S1 being set

for R being Relation of R1

for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

for R being Relation of R1

for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let R1, S1 be set ; :: thesis: for R being Relation of R1

for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let R be Relation of R1; :: thesis: for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let S be Relation of S1; :: thesis: ( R1 misses S1 implies for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 ) )

assume A1: R1 misses S1 ; :: thesis: for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let q1, q2 be object ; :: thesis: ( [q1,q2] in R \/ S & q2 in S1 implies ( [q1,q2] in S & q1 in S1 ) )

assume that

A2: [q1,q2] in R \/ S and

A3: q2 in S1 ; :: thesis: ( [q1,q2] in S & q1 in S1 )

A4: ( [q1,q2] in R or [q1,q2] in S ) by A2, XBOOLE_0:def 3;

end;
for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let R be Relation of R1; :: thesis: for S being Relation of S1 st R1 misses S1 holds

for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let S be Relation of S1; :: thesis: ( R1 misses S1 implies for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 ) )

assume A1: R1 misses S1 ; :: thesis: for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds

( [q1,q2] in S & q1 in S1 )

let q1, q2 be object ; :: thesis: ( [q1,q2] in R \/ S & q2 in S1 implies ( [q1,q2] in S & q1 in S1 ) )

assume that

A2: [q1,q2] in R \/ S and

A3: q2 in S1 ; :: thesis: ( [q1,q2] in S & q1 in S1 )

A4: ( [q1,q2] in R or [q1,q2] in S ) by A2, XBOOLE_0:def 3;

now :: thesis: not [q1,q2] in R

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

then q2 in R1 by ZFMISC_1:87;

hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum

end;
then q2 in R1 by ZFMISC_1:87;

hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum

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

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;

for b_{1} being set holds

( b_{1} = Carrier C iff for i being Element of I holds b_{1} . i = the carrier of (C . i) )

end;
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 for i being Element of I holds it . i = the carrier of (C . i);

for b

( b

proof end;

:: deftheorem Def1 defines Carrier PCS_0:def 1 :

for I being non empty set

for C being 1-sorted-yielding ManySortedSet of I

for b_{3} being set holds

( b_{3} = Carrier C iff for i being Element of I holds b_{3} . i = the carrier of (C . i) );

for I being non empty set

for C being 1-sorted-yielding ManySortedSet of I

for b

( b

definition

let R1, R2, S1, S2 be set ;

let R be Relation of R1,R2;

let S be Relation of S1,S2;

defpred S_{1}[ object , object ] 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 ) );

ex b_{1} being Relation of [:R1,S1:],[:R2,S2:] st

for x, y being object holds

( [x,y] in b_{1} 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 ) ) )

for b_{1}, b_{2} being Relation of [:R1,S1:],[:R2,S2:] st ( for x, y being object holds

( [x,y] in b_{1} 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 ) ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} 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 ) ) ) ) holds

b_{1} = b_{2}

end;
let R be Relation of R1,R2;

let S be Relation of S1,S2;

defpred S

( $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 object 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 for x, y being object 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 ) ) );

ex b

for x, y being object holds

( [x,y] in b

( 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 ) ) )

proof end;

uniqueness for b

( [x,y] in b

( 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 ) ) ) ) & ( for x, y being object holds

( [x,y] in b

( 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 ) ) ) ) holds

b

proof end;

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

for R1, R2, S1, S2 being set

for R being Relation of R1,R2

for S being Relation of S1,S2

for b_{7} being Relation of [:R1,S1:],[:R2,S2:] holds

( b_{7} = [^R,S^] iff for x, y being object holds

( [x,y] in b_{7} 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 ) ) ) );

for R1, R2, S1, S2 being set

for R being Relation of R1,R2

for S being Relation of S1,S2

for b

( b

( [x,y] in b

( 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 ) ) ) );

definition

let R1, R2, S1, S2 be non empty set ;

let R be Relation of R1,R2;

let S be Relation of S1,S2;

for b_{1} being Relation of [:R1,S1:],[:R2,S2:] holds

( b_{1} = [^R,S^] iff 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 b_{1} iff ( [r1,r2] in R or [s1,s2] in S ) ) )

end;
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 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 ) );

for b

( b

for r2 being Element of R2

for s1 being Element of S1

for s2 being Element of S2 holds

( [[r1,s1],[r2,s2]] in b

proof end;

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

for R1, R2, S1, S2 being non empty set

for R being Relation of R1,R2

for S being Relation of S1,S2

for b_{7} being Relation of [:R1,S1:],[:R2,S2:] holds

( b_{7} = [^R,S^] iff 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 b_{7} iff ( [r1,r2] in R or [s1,s2] in S ) ) );

for R1, R2, S1, S2 being non empty set

for R being Relation of R1,R2

for S being Relation of S1,S2

for b

( b

for r2 being Element of R2

for s1 being Element of S1

for s2 being Element of S2 holds

( [[r1,s1],[r2,s2]] in b

registration

let R1, S1 be set ;

let R be total Relation of R1;

let S be total Relation of S1;

coherence

[^R,S^] is total

end;
let R be total Relation of R1;

let S be total Relation of S1;

coherence

[^R,S^] is total

proof end;

registration

let R1, S1 be set ;

let R be reflexive Relation of R1;

let S be reflexive Relation of S1;

coherence

[^R,S^] is reflexive

end;
let R be reflexive Relation of R1;

let S be reflexive Relation of S1;

coherence

[^R,S^] is reflexive

proof end;

registration

let R1, S1 be set ;

let R be Relation of R1;

let S be total reflexive Relation of S1;

coherence

[^R,S^] is reflexive

end;
let R be Relation of R1;

let S be total reflexive Relation of S1;

coherence

[^R,S^] is reflexive

proof end;

registration

let R1, S1 be set ;

let R be total reflexive Relation of R1;

let S be Relation of S1;

coherence

[^R,S^] is reflexive

end;
let R be total reflexive Relation of R1;

let S be Relation of S1;

coherence

[^R,S^] is reflexive

proof end;

registration

let R1, S1 be set ;

let R be symmetric Relation of R1;

let S be symmetric Relation of S1;

coherence

[^R,S^] is symmetric

end;
let R be symmetric Relation of R1;

let S be symmetric Relation of S1;

coherence

[^R,S^] is symmetric

proof end;

definition

let R be Relation;

end;
attr R is transitive-yielding means :Def4: :: PCS_0:def 4

for S being RelStr st S in rng R holds

S is transitive ;

for S being RelStr st S in rng R holds

S is transitive ;

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

for R being Relation holds

( R is transitive-yielding iff for S being RelStr st S in rng R holds

S is transitive );

for R being Relation holds

( R is transitive-yielding iff for S being RelStr st S in rng R holds

S is transitive );

registration

coherence

for b_{1} being Relation st b_{1} is Poset-yielding holds

b_{1} is transitive-yielding
by YELLOW16:def 5;

end;
for b

b

registration
end;

definition

let I be set ;

let C be RelStr-yielding ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

ex P being RelStr st

( P = C . i & b_{1} . i = the InternalRel of P )

for b_{1}, b_{2} being ManySortedSet of I st ( for i being set st i in I holds

ex P being RelStr st

( P = C . i & b_{1} . i = the InternalRel of P ) ) & ( for i being set st i in I holds

ex P being RelStr st

( P = C . i & b_{2} . i = the InternalRel of P ) ) holds

b_{1} = b_{2}

end;
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 for i being set st i in I holds

ex P being RelStr st

( P = C . i & it . i = the InternalRel of P );

ex b

for i being set st i in I holds

ex P being RelStr st

( P = C . i & b

proof end;

uniqueness for b

ex P being RelStr st

( P = C . i & b

ex P being RelStr st

( P = C . i & b

b

proof end;

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

for I being set

for C being RelStr-yielding ManySortedSet of I

for b_{3} being ManySortedSet of I holds

( b_{3} = pcs-InternalRels C iff for i being set st i in I holds

ex P being RelStr st

( P = C . i & b_{3} . i = the InternalRel of P ) );

for I being set

for C being RelStr-yielding ManySortedSet of I

for b

( b

ex P being RelStr st

( P = C . i & b

definition

let I be non empty set ;

let C be RelStr-yielding ManySortedSet of I;

for b_{1} being ManySortedSet of I holds

( b_{1} = pcs-InternalRels C iff for i being Element of I holds b_{1} . i = the InternalRel of (C . i) )

end;
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 for i being Element of I holds it . i = the InternalRel of (C . i);

for b

( b

proof end;

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

for I being non empty set

for C being RelStr-yielding ManySortedSet of I

for b_{3} being ManySortedSet of I holds

( b_{3} = pcs-InternalRels C iff for i being Element of I holds b_{3} . i = the InternalRel of (C . i) );

for I being non empty set

for C being RelStr-yielding ManySortedSet of I

for b

( b

registration

let I be set ;

let C be RelStr-yielding ManySortedSet of I;

coherence

pcs-InternalRels C is Relation-yielding

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

coherence

pcs-InternalRels C is Relation-yielding

proof end;

registration

let I be non empty set ;

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

let i be Element of I;

coherence

for b_{1} being RelStr st b_{1} = C . i holds

b_{1} is transitive

end;
let C be RelStr-yielding transitive-yielding ManySortedSet of I;

let i be Element of I;

coherence

for b

b

proof end;

definition

attr c_{1} is strict ;

struct TolStr -> 1-sorted ;

aggr TolStr(# carrier, ToleranceRel #) -> TolStr ;

sel ToleranceRel c_{1} -> Relation of the carrier of c_{1};

end;
struct TolStr -> 1-sorted ;

aggr TolStr(# carrier, ToleranceRel #) -> TolStr ;

sel ToleranceRel c

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

for P being TolStr

for p, q being Element of P holds

( p (--) q iff [p,q] in the ToleranceRel of P );

for P being TolStr

for p, q being Element of P holds

( p (--) q iff [p,q] in the ToleranceRel of P );

definition

let P be TolStr ;

end;
attr P is pcs-tol-reflexive means :Def9: :: PCS_0:def 9

the ToleranceRel of P is_reflexive_in the carrier of P;

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;

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;

the ToleranceRel of P is_symmetric_in the carrier of P;

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

for P being TolStr holds

( P is pcs-tol-total iff the ToleranceRel of P is total );

for P being TolStr holds

( P is pcs-tol-total iff the ToleranceRel of P is total );

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

for P being TolStr holds

( P is pcs-tol-reflexive iff the ToleranceRel of P is_reflexive_in the carrier of P );

for P being TolStr holds

( P is pcs-tol-reflexive iff the ToleranceRel of P is_reflexive_in the carrier of P );

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

for P being TolStr holds

( P is pcs-tol-irreflexive iff the ToleranceRel of P is_irreflexive_in the carrier of P );

for P being TolStr holds

( P is pcs-tol-irreflexive iff the ToleranceRel of P is_irreflexive_in the carrier of P );

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

for P being TolStr holds

( P is pcs-tol-symmetric iff the ToleranceRel of P is_symmetric_in the carrier of P );

for P being TolStr holds

( P is pcs-tol-symmetric iff the ToleranceRel of P is_symmetric_in the carrier of P );

registration
end;

theorem :: PCS_0:2

for P being TolStr st P is empty holds

TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr

TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr

proof end;

registration

coherence

for b_{1} being TolStr st b_{1} is pcs-tol-reflexive holds

b_{1} is pcs-tol-total

end;
for b

b

proof end;

registration

coherence

for b_{1} being TolStr st b_{1} is empty holds

( b_{1} is pcs-tol-reflexive & b_{1} is pcs-tol-irreflexive & b_{1} is pcs-tol-symmetric )

end;
for b

( b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let L be pcs-tol-total TolStr ;

coherence

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

end;
coherence

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

definition

let P be pcs-tol-symmetric TolStr ;

let p, q be Element of P;

:: original: (--)

redefine pred p (--) q;

symmetry

for p, q being Element of P st (P,b_{1},b_{2}) holds

(P,b_{2},b_{1})

end;
let p, q be Element of P;

:: original: (--)

redefine pred p (--) q;

symmetry

for p, q being Element of P st (P,b

(P,b

proof end;

registration

let D be set ;

coherence

( TolStr(# D,(nabla D) #) is pcs-tol-reflexive & TolStr(# D,(nabla D) #) is pcs-tol-symmetric )

end;
coherence

( TolStr(# D,(nabla D) #) is pcs-tol-reflexive & TolStr(# D,(nabla D) #) is pcs-tol-symmetric )

proof end;

registration

let D be set ;

coherence

( TolStr(# D,({} (D,D)) #) is pcs-tol-irreflexive & TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric )

end;
coherence

( TolStr(# D,({} (D,D)) #) is pcs-tol-irreflexive & TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric )

proof end;

registration

existence

ex b_{1} being TolStr st

( b_{1} is strict & not b_{1} is empty & b_{1} is pcs-tol-reflexive & b_{1} is pcs-tol-symmetric )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being TolStr st

( b_{1} is strict & not b_{1} is empty & b_{1} is pcs-tol-irreflexive & b_{1} is pcs-tol-symmetric )

end;
ex b

( b

proof end;

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

for R being Relation holds

( R is TolStr-yielding iff for P being set st P in rng R holds

P is TolStr );

for R being Relation holds

( R is TolStr-yielding iff for P being set st P in rng R holds

P is TolStr );

definition

let f be Function;

( f is TolStr-yielding iff for x being set st x in dom f holds

f . x is TolStr )

end;
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 for x being set st x in dom f holds

f . x is TolStr ;

( f is TolStr-yielding iff for x being set st x in dom f holds

f . x is TolStr )

proof end;

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

for f being Function holds

( f is TolStr-yielding iff for x being set st x in dom f holds

f . x is TolStr );

for f being Function holds

( f is TolStr-yielding iff for x being set st x in dom f holds

f . x is TolStr );

definition

let I be set ;

let f be ManySortedSet of I;

A1: dom f = I by PARTFUN1:def 2;

( f is TolStr-yielding iff for x being set st x in I holds

f . x is TolStr ) by A1;

end;
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 redefine attr f is TolStr-yielding means :: PCS_0:def 15

for x being set st x in I holds

f . x is TolStr ;

( f is TolStr-yielding iff for x being set st x in I holds

f . x is TolStr ) by A1;

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

for I being set

for f being ManySortedSet of I holds

( f is TolStr-yielding iff for x being set st x in I holds

f . x is TolStr );

for I being set

for f being ManySortedSet of I holds

( f is TolStr-yielding iff for x being set st x in I holds

f . x is TolStr );

definition

let R be Relation;

end;
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 ;

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 ;

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 ;

for S being TolStr st S in rng R holds

S is pcs-tol-symmetric ;

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

for R being Relation holds

( R is pcs-tol-reflexive-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-reflexive );

for R being Relation holds

( R is pcs-tol-reflexive-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-reflexive );

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

for R being Relation holds

( R is pcs-tol-irreflexive-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-irreflexive );

for R being Relation holds

( R is pcs-tol-irreflexive-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-irreflexive );

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

for R being Relation holds

( R is pcs-tol-symmetric-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-symmetric );

for R being Relation holds

( R is pcs-tol-symmetric-yielding iff for S being TolStr st S in rng R holds

S is pcs-tol-symmetric );

registration

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is pcs-tol-reflexive-yielding & b_{1} is pcs-tol-irreflexive-yielding & b_{1} is pcs-tol-symmetric-yielding )
;

end;

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

coherence for b

( b

registration

let I be set ;

let P be TolStr ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is TolStr-yielding
by FUNCOP_1:7;

end;
let P be TolStr ;

coherence

for b

b

registration

let I be set ;

let P be pcs-tol-reflexive TolStr ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is pcs-tol-reflexive-yielding

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

coherence

for b

b

proof end;

registration

let I be set ;

let P be pcs-tol-irreflexive TolStr ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is pcs-tol-irreflexive-yielding

end;
let P be pcs-tol-irreflexive TolStr ;

coherence

for b

b

proof end;

registration

let I be set ;

let P be pcs-tol-symmetric TolStr ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is pcs-tol-symmetric-yielding

end;
let P be pcs-tol-symmetric TolStr ;

coherence

for b

b

proof end;

registration

coherence

for b_{1} being Function st b_{1} is TolStr-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration

let I be set ;

ex b_{1} being ManySortedSet of I st

( b_{1} is pcs-tol-reflexive-yielding & b_{1} is pcs-tol-symmetric-yielding & b_{1} is () )

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

existence ex b

( b

proof end;

registration

let I be set ;

ex b_{1} being ManySortedSet of I st

( b_{1} is pcs-tol-irreflexive-yielding & b_{1} is pcs-tol-symmetric-yielding & b_{1} is () )

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

existence ex b

( b

proof end;

registration
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

C . i is TolStr

end;
let C be () ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func C . i -> TolStr ;

coherence

C . i is TolStr

proof end;

definition

let I be set ;

let C be () ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

ex P being TolStr st

( P = C . i & b_{1} . i = the ToleranceRel of P )

for b_{1}, b_{2} being ManySortedSet of I st ( for i being set st i in I holds

ex P being TolStr st

( P = C . i & b_{1} . i = the ToleranceRel of P ) ) & ( for i being set st i in I holds

ex P being TolStr st

( P = C . i & b_{2} . i = the ToleranceRel of P ) ) holds

b_{1} = b_{2}

end;
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 for i being set st i in I holds

ex P being TolStr st

( P = C . i & it . i = the ToleranceRel of P );

ex b

for i being set st i in I holds

ex P being TolStr st

( P = C . i & b

proof end;

uniqueness for b

ex P being TolStr st

( P = C . i & b

ex P being TolStr st

( P = C . i & b

b

proof end;

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

for I being set

for C being () ManySortedSet of I

for b_{3} being ManySortedSet of I holds

( b_{3} = pcs-ToleranceRels C iff for i being set st i in I holds

ex P being TolStr st

( P = C . i & b_{3} . i = the ToleranceRel of P ) );

for I being set

for C being () ManySortedSet of I

for b

( b

ex P being TolStr st

( P = C . i & b

definition

let I be non empty set ;

let C be () ManySortedSet of I;

for b_{1} being ManySortedSet of I holds

( b_{1} = pcs-ToleranceRels C iff for i being Element of I holds b_{1} . i = the ToleranceRel of (C . i) )

end;
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 for i being Element of I holds it . i = the ToleranceRel of (C . i);

for b

( b

proof end;

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

for I being non empty set

for C being () ManySortedSet of I

for b_{3} being ManySortedSet of I holds

( b_{3} = pcs-ToleranceRels C iff for i being Element of I holds b_{3} . i = the ToleranceRel of (C . i) );

for I being non empty set

for C being () ManySortedSet of I

for b

( b

registration

let I be set ;

let C be () ManySortedSet of I;

coherence

pcs-ToleranceRels C is Relation-yielding

end;
let C be () ManySortedSet of I;

coherence

pcs-ToleranceRels C is Relation-yielding

proof end;

registration

let I be non empty set ;

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

let i be Element of I;

coherence

for b_{1} being TolStr st b_{1} = C . i holds

b_{1} is pcs-tol-reflexive

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

let i be Element of I;

coherence

for b

b

proof end;

registration

let I be non empty set ;

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

let i be Element of I;

coherence

for b_{1} being TolStr st b_{1} = C . i holds

b_{1} is pcs-tol-irreflexive

end;
let C be () pcs-tol-irreflexive-yielding ManySortedSet of I;

let i be Element of I;

coherence

for b

b

proof end;

registration

let I be non empty set ;

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

let i be Element of I;

coherence

for b_{1} being TolStr st b_{1} = C . i holds

b_{1} is pcs-tol-symmetric

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

let i be Element of I;

coherence

for b

b

proof 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 ;

Q is pcs-tol-reflexive ;

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 ;

Q is pcs-tol-irreflexive ;

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 ;

Q is pcs-tol-symmetric ;

definition

let P, Q be TolStr ;

TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #) is TolStr ;

end;
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 TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #) is TolStr ;

:: deftheorem defines [^ PCS_0:def 21 :

for P, Q being TolStr holds [^P,Q^] = TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

for P, Q being TolStr holds [^P,Q^] = TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

notation
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

[^,^] is Element of [^P,Q^]

end;
let p be Element of P;

let q be Element of Q;

:: original: [^

redefine func [^p,q^] -> Element of [^P,Q^];

coherence

[^,^] is Element of [^P,Q^]

proof end;

notation
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

^`1 is Element of P by MCART_1:10;

:: original: ^`2

redefine func p ^`2 -> Element of Q;

coherence

^`2 is Element of Q by MCART_1:10;

end;
let p be Element of [^P,Q^];

:: original: ^`1

redefine func p ^`1 -> Element of P;

coherence

^`1 is Element of P by MCART_1:10;

:: original: ^`2

redefine func p ^`2 -> Element of Q;

coherence

^`2 is Element of Q by MCART_1:10;

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 ) )

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 ;

coherence

[^P,Q^] is pcs-tol-reflexive

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

coherence

[^P,Q^] is pcs-tol-reflexive

proof end;

registration

let P be pcs-tol-reflexive TolStr ;

let Q be TolStr ;

coherence

[^P,Q^] is pcs-tol-reflexive

end;
let Q be TolStr ;

coherence

[^P,Q^] is pcs-tol-reflexive

proof end;

registration
end;

definition

attr c_{1} is strict ;

struct pcs-Str -> RelStr , TolStr ;

aggr pcs-Str(# carrier, InternalRel, ToleranceRel #) -> pcs-Str ;

end;
struct pcs-Str -> RelStr , TolStr ;

aggr pcs-Str(# carrier, InternalRel, ToleranceRel #) -> pcs-Str ;

definition

let P be pcs-Str ;

end;
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;

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

p9 (--) q9;

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

for P being pcs-Str holds

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

p9 (--) q9 );

for P being pcs-Str holds

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

p9 (--) q9 );

definition

let P be pcs-Str ;

end;
attr P is pcs-like means :: PCS_0:def 23

( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible );

( 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 :: PCS_0:def 24

( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible );

( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible );

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

for P being pcs-Str holds

( P is pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

for P being pcs-Str holds

( P is pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

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

for P being pcs-Str holds

( P is anti-pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

for P being pcs-Str holds

( P is anti-pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

registration

for b_{1} being pcs-Str st b_{1} is pcs-like holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is pcs-tol-reflexive & b_{1} is pcs-tol-symmetric & b_{1} is pcs-compatible )
;

for b_{1} being pcs-Str st b_{1} is reflexive & b_{1} is transitive & b_{1} is pcs-tol-reflexive & b_{1} is pcs-tol-symmetric & b_{1} is pcs-compatible holds

b_{1} is pcs-like
;

for b_{1} being pcs-Str st b_{1} is anti-pcs-like holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is pcs-tol-irreflexive & b_{1} is pcs-tol-symmetric & b_{1} is pcs-compatible )
;

for b_{1} being pcs-Str st b_{1} is reflexive & b_{1} is transitive & b_{1} is pcs-tol-irreflexive & b_{1} is pcs-tol-symmetric & b_{1} is pcs-compatible holds

b_{1} is anti-pcs-like
;

end;

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

coherence for b

( b

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

coherence for b

b

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

coherence for b

( b

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

coherence for b

b

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

for D being set holds pcs-total D = pcs-Str(# D,(nabla D),(nabla D) #);

for D being set holds pcs-total D = pcs-Str(# D,(nabla D),(nabla D) #);

registration
end;

registration

let D be set ;

coherence

( pcs-total D is reflexive & pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric )

end;
coherence

( pcs-total D is reflexive & pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric )

proof end;

registration
end;

registration
end;

registration

existence

ex b_{1} being pcs-Str st

( b_{1} is strict & not b_{1} is empty & b_{1} is pcs-like )

ex b_{1} being pcs-Str st

( b_{1} is strict & not b_{1} is empty & b_{1} is anti-pcs-like )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

definition
end;

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

for p being set holds pcs-singleton p = pcs-total {p};

for p being set holds pcs-singleton p = pcs-total {p};

registration

let p be set ;

coherence

( pcs-singleton p is strict & not pcs-singleton p is empty & pcs-singleton p is pcs-like ) ;

end;
coherence

( pcs-singleton p is strict & not pcs-singleton p is empty & pcs-singleton p is pcs-like ) ;

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

for R being Relation holds

( R is pcs-Str-yielding iff for P being set st P in rng R holds

P is pcs-Str );

for R being Relation holds

( R is pcs-Str-yielding iff for P being set st P in rng R holds

P is pcs-Str );

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

for R being Relation holds

( R is pcs-yielding iff for P being set st P in rng R holds

P is pcs );

for R being Relation holds

( R is pcs-yielding iff for P being set st P in rng R holds

P is pcs );

definition

let f be Function;

( f is pcs-Str-yielding iff for x being set st x in dom f holds

f . x is pcs-Str )

( f is pcs-yielding iff for x being set st x in dom f holds

f . x is pcs )

end;
redefine attr f is pcs-Str-yielding means :: PCS_0:def 30

for x being set st x in dom f holds

f . x is pcs-Str ;

compatibility for x being set st x in dom f holds

f . x is pcs-Str ;

( f is pcs-Str-yielding iff for x being set st x in dom f holds

f . x is pcs-Str )

proof end;

redefine attr f is pcs-yielding means :: PCS_0:def 31

for x being set st x in dom f holds

f . x is pcs;

compatibility for x being set st x in dom f holds

f . x is pcs;

( f is pcs-yielding iff for x being set st x in dom f holds

f . x is pcs )

proof end;

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

for f being Function holds

( f is pcs-Str-yielding iff for x being set st x in dom f holds

f . x is pcs-Str );

for f being Function holds

( f is pcs-Str-yielding iff for x being set st x in dom f holds

f . x is pcs-Str );

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

for f being Function holds

( f is pcs-yielding iff for x being set st x in dom f holds

f . x is pcs );

for f being Function holds

( f is pcs-yielding iff for x being set st x in dom f holds

f . x is pcs );

definition

let I be set ;

let f be ManySortedSet of I;

A1: dom f = I by PARTFUN1:def 2;

( f is pcs-Str-yielding iff for x being set st x in I holds

f . x is pcs-Str ) by A1;

( f is pcs-yielding iff for x being set st x in I holds

f . x is pcs ) by A1;

end;
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 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 ;

( f is pcs-Str-yielding iff for x being set st x in I holds

f . x is pcs-Str ) by A1;

:: 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 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;

( f is pcs-yielding iff for x being set st x in I holds

f . x is pcs ) by A1;

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

for I being set

for f being ManySortedSet of I holds

( f is pcs-Str-yielding iff for x being set st x in I holds

f . x is pcs-Str );

for I being set

for f being ManySortedSet of I holds

( f is pcs-Str-yielding iff for x being set st x in I holds

f . x is pcs-Str );

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

for I being set

for f being ManySortedSet of I holds

( f is pcs-yielding iff for x being set st x in I holds

f . x is pcs );

for I being set

for f being ManySortedSet of I holds

( f is pcs-yielding iff for x being set st x in I holds

f . x is pcs );

registration

coherence

for b_{1} being Relation st b_{1} is pcs-Str-yielding holds

( b_{1} is TolStr-yielding & b_{1} is RelStr-yielding )

for b_{1} being Relation st b_{1} is pcs-yielding holds

b_{1} is pcs-Str-yielding
;

for b_{1} being Relation st b_{1} is pcs-yielding holds

( b_{1} is reflexive-yielding & b_{1} is transitive-yielding & b_{1} is pcs-tol-reflexive-yielding & b_{1} is pcs-tol-symmetric-yielding )
;

end;
for b

( b

proof end;

coherence for b

b

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

coherence for b

( b

registration

let I be set ;

let P be pcs;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is pcs-yielding
by FUNCOP_1:7;

end;
let P be pcs;

coherence

for b

b

registration
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

C . i is pcs-Str by Def32;

end;
let C be () ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func C . i -> pcs-Str ;

coherence

C . i is pcs-Str by Def32;

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

C . i is pcs by Def33;

end;
let C be () ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func C . i -> pcs;

coherence

C . i is pcs by Def33;

:: Union of PCS's

definition

let P, Q be pcs-Str ;

for P being pcs-Str holds

( the carrier of P c= the carrier of P & the InternalRel of P c= the InternalRel of P & the ToleranceRel of P c= the ToleranceRel of P ) ;

end;
pred P c= Q means :: 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 ( 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 );

for P being pcs-Str holds

( the carrier of P c= the carrier of P & the InternalRel of P c= the InternalRel of P & the ToleranceRel of P c= the ToleranceRel of P ) ;

:: deftheorem defines c= PCS_0:def 34 :

for P, Q being pcs-Str holds

( P c= Q iff ( 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 ) );

for P, Q being pcs-Str holds

( P c= Q iff ( 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 ) );

theorem :: 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 ;

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 ;

theorem :: 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 ;

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 ;

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

;

definition

let C be Relation;

end;
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;

for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds

Q c= P;

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

for C being Relation holds

( C is pcs-chain-like iff for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds

Q c= P );

for C being Relation holds

( C is pcs-chain-like iff for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds

Q c= P );

registration

let I be set ;

let P be pcs-Str ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> P holds

b_{1} is pcs-chain-like

end;
let P be pcs-Str ;

coherence

for b

b

proof end;

registration
end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is pcs-chain-like & b_{1} is () )

end;
existence

ex b

( b

proof end;

definition

let I be set ;

let C be () ManySortedSet of I;

ex b_{1} being strict pcs-Str st

( the carrier of b_{1} = Union (Carrier C) & the InternalRel of b_{1} = Union (pcs-InternalRels C) & the ToleranceRel of b_{1} = Union (pcs-ToleranceRels C) )

for b_{1}, b_{2} being strict pcs-Str st the carrier of b_{1} = Union (Carrier C) & the InternalRel of b_{1} = Union (pcs-InternalRels C) & the ToleranceRel of b_{1} = Union (pcs-ToleranceRels C) & the carrier of b_{2} = Union (Carrier C) & the InternalRel of b_{2} = Union (pcs-InternalRels C) & the ToleranceRel of b_{2} = Union (pcs-ToleranceRels C) holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = Union (Carrier C) & the InternalRel of it = Union (pcs-InternalRels C) & the ToleranceRel of it = Union (pcs-ToleranceRels C) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

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

for I being set

for C being () ManySortedSet of I

for b_{3} being strict pcs-Str holds

( b_{3} = pcs-union C iff ( the carrier of b_{3} = Union (Carrier C) & the InternalRel of b_{3} = Union (pcs-InternalRels C) & the ToleranceRel of b_{3} = Union (pcs-ToleranceRels C) ) );

for I being set

for C being () ManySortedSet of I

for b

( b

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 object 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 ) )

for C being () ManySortedSet of I

for p, q being Element of (pcs-union C) holds

( p <= q iff ex i being object 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 ) )

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 object 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 ) )

for C being () ManySortedSet of I

for p, q being Element of (pcs-union C) holds

( p (--) q iff ex i being object 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 ) )

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;

coherence

pcs-union C is reflexive

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

coherence

pcs-union C is reflexive

proof end;

registration

let I be set ;

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

coherence

pcs-union C is pcs-tol-reflexive

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

coherence

pcs-union C is pcs-tol-reflexive

proof end;

registration

let I be set ;

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

coherence

pcs-union C is pcs-tol-symmetric

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

coherence

pcs-union C is pcs-tol-symmetric

proof end;

registration

let I be set ;

let C be pcs-Chain of I;

coherence

( pcs-union C is transitive & pcs-union C is pcs-compatible )

end;
let C be pcs-Chain of I;

coherence

( pcs-union C is transitive & pcs-union C is pcs-compatible )

proof end;

:: Direct Sum of PCS's

Lm3: now :: thesis: for a, b being object holds rng <%a,b%> = {a,b}

let a, b be object ; :: thesis: rng <%a,b%> = {a,b}

<%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;

hence rng <%a,b%> = {a,b} by FUNCT_4:64; :: thesis: verum

end;
<%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;

hence rng <%a,b%> = {a,b} by FUNCT_4:64; :: thesis: verum

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

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

for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-union <%P,Q%>;

for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-union <%P,Q%>;

deffunc H

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 )

( 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 ) ) )

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 ) ) )

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
end;

registration
end;

:: Extension

definition

let P be pcs-Str ;

let a be set ;

ex b_{1} being strict pcs-Str st

( the carrier of b_{1} = {a} \/ the carrier of P & the InternalRel of b_{1} = [:{a}, the carrier of b_{1}:] \/ the InternalRel of P & the ToleranceRel of b_{1} = ([:{a}, the carrier of b_{1}:] \/ [: the carrier of b_{1},{a}:]) \/ the ToleranceRel of P )

for b_{1}, b_{2} being strict pcs-Str st the carrier of b_{1} = {a} \/ the carrier of P & the InternalRel of b_{1} = [:{a}, the carrier of b_{1}:] \/ the InternalRel of P & the ToleranceRel of b_{1} = ([:{a}, the carrier of b_{1}:] \/ [: the carrier of b_{1},{a}:]) \/ the ToleranceRel of P & the carrier of b_{2} = {a} \/ the carrier of P & the InternalRel of b_{2} = [:{a}, the carrier of b_{2}:] \/ the InternalRel of P & the ToleranceRel of b_{2} = ([:{a}, the carrier of b_{2}:] \/ [: the carrier of b_{2},{a}:]) \/ the ToleranceRel of P holds

b_{1} = b_{2}
;

end;
let a be set ;

func pcs-extension (P,a) -> strict pcs-Str means :Def39: :: PCS_0:def 40

( 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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

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

for P being pcs-Str

for a being set

for b_{3} being strict pcs-Str holds

( b_{3} = pcs-extension (P,a) iff ( the carrier of b_{3} = {a} \/ the carrier of P & the InternalRel of b_{3} = [:{a}, the carrier of b_{3}:] \/ the InternalRel of P & the ToleranceRel of b_{3} = ([:{a}, the carrier of b_{3}:] \/ [: the carrier of b_{3},{a}:]) \/ the ToleranceRel of P ) );

for P being pcs-Str

for a being set

for b

( b

registration
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)) )

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

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

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 )

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

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

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 )

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

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

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
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

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 ;

coherence

pcs-extension (P,a) is pcs-tol-reflexive

end;
let a be set ;

coherence

pcs-extension (P,a) is pcs-tol-reflexive

proof end;

registration

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

let a be set ;

coherence

pcs-extension (P,a) is pcs-tol-symmetric

end;
let a be set ;

coherence

pcs-extension (P,a) is pcs-tol-symmetric

proof 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

for a being set st not a in the carrier of P holds

pcs-extension (P,a) is pcs-compatible

proof end;

:: Reverse

definition

let P be pcs-Str ;

ex b_{1} being strict pcs-Str st

( the carrier of b_{1} = the carrier of P & the InternalRel of b_{1} = the InternalRel of P ~ & the ToleranceRel of b_{1} = the ToleranceRel of P ` )

for b_{1}, b_{2} being strict pcs-Str st the carrier of b_{1} = the carrier of P & the InternalRel of b_{1} = the InternalRel of P ~ & the ToleranceRel of b_{1} = the ToleranceRel of P ` & the carrier of b_{2} = the carrier of P & the InternalRel of b_{2} = the InternalRel of P ~ & the ToleranceRel of b_{2} = the ToleranceRel of P ` holds

b_{1} = b_{2}
;

end;
func pcs-reverse P -> strict pcs-Str means :Def40: :: PCS_0:def 41

( 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 ( the carrier of it = the carrier of P & the InternalRel of it = the InternalRel of P ~ & the ToleranceRel of it = the ToleranceRel of P ` );

ex b

( the carrier of b

proof end;

uniqueness for b

b

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

for P being pcs-Str

for b_{2} being strict pcs-Str holds

( b_{2} = pcs-reverse P iff ( the carrier of b_{2} = the carrier of P & the InternalRel of b_{2} = the InternalRel of P ~ & the ToleranceRel of b_{2} = the ToleranceRel of P ` ) );

for P being pcs-Str

for b

( b

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 )

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

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

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
end;

registration
end;

registration
end;

registration
end;

:: Times

definition

let P, Q be pcs-Str ;

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^] #) is pcs-Str ;

end;
func P pcs-times Q -> pcs-Str equals :: PCS_0:def 42

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 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^] #);

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^] #) is pcs-Str ;

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

for P, Q being pcs-Str holds P pcs-times 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^] #);

for P, Q being pcs-Str holds P pcs-times 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^] #);

registration
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 ) )

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

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;

registration

let P be pcs-Str ;

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

coherence

P pcs-times Q is pcs-tol-reflexive

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

coherence

P pcs-times Q is pcs-tol-reflexive

proof end;

registration

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

let Q be pcs-Str ;

coherence

P pcs-times Q is pcs-tol-reflexive

end;
let Q be pcs-Str ;

coherence

P pcs-times Q is pcs-tol-reflexive

proof end;

registration
end;

registration
end;

:: deftheorem defines --> PCS_0:def 43 :

for P, Q being pcs-Str holds P --> Q = (pcs-reverse P) pcs-times Q;

for P, Q being pcs-Str holds P --> Q = (pcs-reverse P) pcs-times Q;

registration
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 ) )

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

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

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
end;

registration
end;

registration
end;

registration
end;

:: Self-coherence

definition

let P be TolStr ;

let S be Subset of P;

end;
let S be Subset of P;

attr S is pcs-self-coherent means :: PCS_0:def 44

for x, y being Element of P st x in S & y in S holds

x (--) y;

for x, y being Element of P st x in S & y in S holds

x (--) y;

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

for P being TolStr

for S being Subset of P holds

( S is pcs-self-coherent iff for x, y being Element of P st x in S & y in S holds

x (--) y );

for P being TolStr

for S being Subset of P holds

( S is pcs-self-coherent iff for x, y being Element of P st x in S & y in S holds

x (--) y );

registration

let P be TolStr ;

coherence

for b_{1} being Subset of P st b_{1} is empty holds

b_{1} is pcs-self-coherent
;

end;
coherence

for b

b

definition

let P be TolStr ;

let F be Subset-Family of P;

end;
let F be Subset-Family of P;

attr F is pcs-self-coherent-membered means :Def44: :: PCS_0:def 45

for S being Subset of P st S in F holds

S is pcs-self-coherent ;

for S being Subset of P st S in F holds

S is pcs-self-coherent ;

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

for P being TolStr

for F being Subset-Family of P holds

( F is pcs-self-coherent-membered iff for S being Subset of P st S in F holds

S is pcs-self-coherent );

for P being TolStr

for F being Subset-Family of P holds

( F is pcs-self-coherent-membered iff for S being Subset of P st S in F holds

S is pcs-self-coherent );

registration

let P be TolStr ;

existence

ex b_{1} being Subset-Family of P st

( not b_{1} is empty & b_{1} is pcs-self-coherent-membered )

end;
existence

ex b

( not b

proof end;

definition

let P be RelStr ;

let D be set ;

defpred S_{1}[ 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 ) ) );

ex b_{1} being Relation of D st

for A, B being set holds

( [A,B] in b_{1} 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 ) ) ) )

for b_{1}, b_{2} being Relation of D st ( for A, B being set holds

( [A,B] in b_{1} 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 ) ) ) ) ) & ( for A, B being set holds

( [A,B] in b_{2} 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 ) ) ) ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 46

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 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 ) ) ) );

ex b

for A, B being set holds

( [A,B] in b

ex b being set st

( b in B & [a,b] in the InternalRel of P ) ) ) )

proof end;

uniqueness for b

( [A,B] in b

ex b being set st

( b in B & [a,b] in the InternalRel of P ) ) ) ) ) & ( for A, B being set holds

( [A,B] in b

ex b being set st

( b in B & [a,b] in the InternalRel of P ) ) ) ) ) holds

b

proof end;

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

for P being RelStr

for D being set

for b_{3} being Relation of D holds

( b_{3} = pcs-general-power-IR (P,D) iff for A, B being set holds

( [A,B] in b_{3} 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 ) ) ) ) );

for P being RelStr

for D being set

for b

( b

( [A,B] in b

ex b being set st

( b in B & [a,b] in the InternalRel of P ) ) ) ) );

definition

let P be TolStr ;

let D be set ;

defpred S_{1}[ 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 ) );

ex b_{1} being Relation of D st

for A, B being set holds

( [A,B] in b_{1} 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 ) ) )

for b_{1}, b_{2} being Relation of D st ( for A, B being set holds

( [A,B] in b_{1} 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 ) ) ) ) & ( for A, B being set holds

( [A,B] in b_{2} 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 ) ) ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

[a,b] in the ToleranceRel of P ) );

func pcs-general-power-TR (P,D) -> Relation of D means :Def46: :: PCS_0:def 47

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 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 ) ) );

ex b

for A, B being set holds

( [A,B] in b

[a,b] in the ToleranceRel of P ) ) )

proof end;

uniqueness for b

( [A,B] in b

[a,b] in the ToleranceRel of P ) ) ) ) & ( for A, B being set holds

( [A,B] in b

[a,b] in the ToleranceRel of P ) ) ) ) holds

b

proof end;

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

for P being TolStr

for D being set

for b_{3} being Relation of D holds

( b_{3} = pcs-general-power-TR (P,D) iff for A, B being set holds

( [A,B] in b_{3} 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 ) ) ) );

for P being TolStr

for D being set

for b

( b

( [A,B] in b

[a,b] in the ToleranceRel of P ) ) ) );

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 ) ) ) )

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 ) ) )

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 ;

pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #) is pcs-Str ;

end;
let D be set ;

func pcs-general-power (P,D) -> pcs-Str equals :: PCS_0:def 48

pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

coherence pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #) is pcs-Str ;

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

for P being pcs-Str

for D being set holds pcs-general-power (P,D) = pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

for P being pcs-Str

for D being set holds pcs-general-power (P,D) = pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

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;
let D be Subset-Family of P;

synonym pcs-general-power D for pcs-general-power (P,D);

registration
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 )

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

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 :: 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

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 reflexive pcs-Str ;

let D be Subset-Family of P;

coherence

pcs-general-power D is reflexive

end;
let D be Subset-Family of P;

coherence

pcs-general-power D is reflexive

proof end;

registration

let P be transitive pcs-Str ;

let D be set ;

coherence

pcs-general-power (P,D) is transitive

end;
let D be set ;

coherence

pcs-general-power (P,D) is transitive

proof end;

registration

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

let D be pcs-self-coherent-membered Subset-Family of P;

coherence

pcs-general-power D is pcs-tol-reflexive

end;
let D be pcs-self-coherent-membered Subset-Family of P;

coherence

pcs-general-power D is pcs-tol-reflexive

proof end;

registration

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

let D be Subset-Family of P;

coherence

pcs-general-power D is pcs-tol-symmetric

end;
let D be Subset-Family of P;

coherence

pcs-general-power D is pcs-tol-symmetric

proof end;

registration

let P be pcs-compatible pcs-Str ;

let D be Subset-Family of P;

coherence

pcs-general-power D is pcs-compatible

end;
let D be Subset-Family of P;

coherence

pcs-general-power D is pcs-compatible

proof end;

definition

let P be pcs-Str ;

{ X where X is Subset of P : X is pcs-self-coherent } is set ;

end;
func pcs-coherent-power P -> set equals :: PCS_0:def 49

{ X where X is Subset of P : X is pcs-self-coherent } ;

coherence { X where X is Subset of P : X is pcs-self-coherent } ;

{ X where X is Subset of P : X is pcs-self-coherent } is set ;

:: deftheorem defines pcs-coherent-power PCS_0:def 49 :

for P being pcs-Str holds pcs-coherent-power P = { X where X is Subset of P : X is pcs-self-coherent } ;

for P being pcs-Str holds pcs-coherent-power P = { X where X is Subset of P : X is pcs-self-coherent } ;

registration
end;

theorem Th48: :: PCS_0:48

for P being pcs-Str

for X being set st X in pcs-coherent-power P holds

X is pcs-self-coherent Subset of P

for X being set st X in pcs-coherent-power P holds

X is pcs-self-coherent Subset of P

proof end;

definition

let P be pcs-Str ;

:: original: pcs-coherent-power

redefine func pcs-coherent-power P -> Subset-Family of P;

coherence

pcs-coherent-power P is Subset-Family of P

end;
:: original: pcs-coherent-power

redefine func pcs-coherent-power P -> Subset-Family of P;

coherence

pcs-coherent-power P is Subset-Family of P

proof end;

registration

let P be pcs-Str ;

coherence

for b_{1} being Subset-Family of P st b_{1} = pcs-coherent-power P holds

b_{1} is pcs-self-coherent-membered
by Th48;

end;
coherence

for b

b

:: deftheorem defines pcs-power PCS_0:def 50 :

for P being pcs-Str holds pcs-power P = pcs-general-power (pcs-coherent-power P);

for P being pcs-Str holds pcs-power P = pcs-general-power (pcs-coherent-power P);

registration
end;

registration
end;

registration
end;