begin
reconsider z = 0 , j = 1 as Element of {0 ,1} by TARSKI:def 2;
Lm1:
now
let R1,
S1 be
set ;
for R being Relation of
for S being Relation of st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let R be
Relation of ;
for S being Relation of st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let S be
Relation of ;
( R1 misses S1 implies for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 ) )assume A1:
R1 misses S1
;
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let q1,
q2 be
set ;
( [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
;
( [q1,q2] in S & q1 in S1 )A4:
(
[q1,q2] in R or
[q1,q2] in S )
by A2, XBOOLE_0:def 3;
hence
(
[q1,q2] in S &
q1 in S1 )
by A4, ZFMISC_1:106;
verum
end;
theorem Th1:
:: deftheorem Def1 defines Carrier PCS_0:def 1 :
definition
let R1,
R2,
S1,
S2 be
set ;
let R be
Relation of ,;
let S be
Relation of ,;
defpred S1[
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 ,
means :
Def2:
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
ex b1 being Relation of , st
for x, y being set holds
( [x,y] in b1 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 ) ) )
uniqueness
for b1, b2 being Relation of , st ( for x, y being set holds
( [x,y] in b1 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 set holds
( [x,y] in b2 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
b1 = b2
end;
:: deftheorem Def2 defines [^ PCS_0:def 2 :
for
R1,
R2,
S1,
S2 being
set for
R being
Relation of ,
for
S being
Relation of ,
for
b7 being
Relation of , holds
(
b7 = [^R,S^] iff for
x,
y being
set holds
(
[x,y] in b7 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 ) ) ) );
definition
let R1,
R2,
S1,
S2 be non
empty set ;
let R be
Relation of ,;
let S be
Relation of ,;
redefine func [^R,S^] means :
Def3:
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 b1 being Relation of , holds
( b1 = [^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 b1 iff ( [r1,r2] in R or [s1,s2] in S ) ) )
end;
:: deftheorem Def3 defines [^ PCS_0:def 3 :
for
R1,
R2,
S1,
S2 being non
empty set for
R being
Relation of ,
for
S being
Relation of ,
for
b7 being
Relation of , holds
(
b7 = [^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 b7 iff (
[r1,r2] in R or
[s1,s2] in S ) ) );
begin
:: deftheorem Def4 defines transitive-yielding PCS_0:def 4 :
:: deftheorem Def5 defines pcs-InternalRels PCS_0:def 5 :
:: deftheorem Def6 defines pcs-InternalRels PCS_0:def 6 :
begin
:: deftheorem Def7 defines (--) PCS_0:def 7 :
:: 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 :
:: deftheorem defines emptyTolStr PCS_0:def 12 :
theorem Th2:
:: deftheorem Def13 defines TolStr-yielding PCS_0:def 13 :
:: deftheorem Def14 defines TolStr-yielding PCS_0:def 14 :
:: deftheorem defines TolStr-yielding PCS_0:def 15 :
:: 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 :
:: deftheorem Def19 defines pcs-ToleranceRels PCS_0:def 19 :
:: deftheorem Def20 defines pcs-ToleranceRels PCS_0:def 20 :
theorem Th3:
theorem Th4:
theorem Th5:
:: deftheorem defines [^ PCS_0:def 21 :
Lm2:
for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds
( (x `1 ) `1 = a1 & (x `1 ) `2 = a2 & (x `2 ) `1 = b1 & (x `2 ) `2 = b2 )
theorem Th6:
theorem
begin
:: deftheorem Def22 defines pcs-compatible PCS_0:def 22 :
:: deftheorem Def23 defines pcs-like PCS_0:def 23 :
:: deftheorem Def24 defines anti-pcs-like PCS_0:def 24 :
:: deftheorem defines pcs-total PCS_0:def 25 :
:: deftheorem defines pcs-empty PCS_0:def 26 :
:: deftheorem defines pcs-singleton PCS_0:def 27 :
:: deftheorem Def28 defines pcs-Str-yielding PCS_0:def 28 :
:: deftheorem Def29 defines pcs-yielding PCS_0:def 29 :
:: deftheorem Def30 defines pcs-Str-yielding PCS_0:def 30 :
:: deftheorem Def31 defines pcs-yielding PCS_0:def 31 :
:: deftheorem Def32 defines pcs-Str-yielding PCS_0:def 32 :
:: deftheorem Def33 defines pcs-yielding PCS_0:def 33 :
:: deftheorem Def34 defines c= PCS_0:def 34 :
theorem Th8:
theorem Th9:
Lm3:
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
:: deftheorem Def35 defines pcs-chain-like PCS_0:def 35 :
:: deftheorem Def36 defines pcs-union PCS_0:def 36 :
theorem Th10:
theorem
theorem Th12:
theorem
:: deftheorem defines MSSet PCS_0:def 37 :
:: deftheorem defines pcs-sum PCS_0:def 38 :
deffunc H1( 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:
theorem Th15:
theorem
for
P,
Q being
pcs-Str for
p,
q being
Element of holds
(
p <= q iff ( ex
p',
q' being
Element of st
(
p' = p &
q' = q &
p' <= q' ) or ex
p',
q' being
Element of st
(
p' = p &
q' = q &
p' <= q' ) ) )
theorem
theorem Th18:
theorem Th19:
theorem
definition
let P be
pcs-Str ;
let a be
set ;
func pcs-extension P,
a -> strict pcs-Str means :
Def39:
( 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
ex b1 being strict pcs-Str st
( the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a},the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a},the carrier of b1:] \/ [:the carrier of b1,{a}:]) \/ the ToleranceRel of P )
uniqueness
for b1, b2 being strict pcs-Str st the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a},the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a},the carrier of b1:] \/ [:the carrier of b1,{a}:]) \/ the ToleranceRel of P & the carrier of b2 = {a} \/ the carrier of P & the InternalRel of b2 = [:{a},the carrier of b2:] \/ the InternalRel of P & the ToleranceRel of b2 = ([:{a},the carrier of b2:] \/ [:the carrier of b2,{a}:]) \/ the ToleranceRel of P holds
b1 = b2
;
end;
:: deftheorem Def39 defines pcs-extension PCS_0:def 39 :
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
:: deftheorem Def40 defines pcs-reverse PCS_0:def 40 :
theorem Th33:
theorem Th34:
theorem Th35:
definition
let P,
Q be
pcs-Str ;
func P pcs-times Q -> pcs-Str equals
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^] #) is pcs-Str
;
end;
:: deftheorem defines pcs-times PCS_0:def 41 :
theorem
theorem
theorem Th38:
:: deftheorem defines --> PCS_0:def 42 :
theorem
theorem
theorem
:: deftheorem Def43 defines pcs-self-coherent PCS_0:def 43 :
:: deftheorem Def44 defines pcs-self-coherent-membered PCS_0:def 44 :
definition
let P be
RelStr ;
let D be
set ;
defpred S1[
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
means :
Def45:
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
ex b1 being Relation of st
for A, B being set holds
( [A,B] in b1 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 ) ) ) )
uniqueness
for b1, b2 being Relation of st ( for A, B being set holds
( [A,B] in b1 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 b2 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
b1 = b2
end;
:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 45 :
definition
let P be
TolStr ;
let D be
set ;
defpred S1[
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
means :
Def46:
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
ex b1 being Relation of st
for A, B being set holds
( [A,B] in b1 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 ) ) )
uniqueness
for b1, b2 being Relation of st ( for A, B being set holds
( [A,B] in b1 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 b2 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
b1 = b2
end;
:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def 46 :
theorem
theorem
:: deftheorem defines pcs-general-power PCS_0:def 47 :
theorem Th44:
theorem
theorem Th46:
theorem
:: deftheorem defines pcs-coherent-power PCS_0:def 48 :
theorem Th48:
:: deftheorem defines pcs-power PCS_0:def 49 :