:: SYSREL semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let X, Y be set ;
cluster [:X,Y:] -> Relation-like ;
correctness
coherence
[:X,Y:] is Relation-like
;
by RELAT_1:6;
end;

theorem :: SYSREL:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: SYSREL:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
proof end;

theorem Th13: :: SYSREL:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
proof end;

theorem :: SYSREL:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation st X misses Y holds
( dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) & dom ((R ~ ) /\ [:X,Y:]) misses rng ((R ~ ) /\ [:X,Y:]) )
proof end;

theorem Th15: :: SYSREL:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
proof end;

theorem :: SYSREL:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
proof end;

theorem :: SYSREL:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds [:X,Y:] ~ = [:Y,X:]
proof end;

theorem :: SYSREL:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th20: :: SYSREL:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S, T being Relation holds
( (R \/ S) * T = (R * T) \/ (S * T) & R * (S \/ T) = (R * S) \/ (R * T) )
proof end;

theorem :: SYSREL:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SYSREL:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, x, y being set
for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
proof end;

theorem :: SYSREL:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: SYSREL:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being set
for R being Relation holds
( ( R c= [:X,Y:] & Z c= X implies R | Z = R /\ [:Z,Y:] ) & ( R c= [:X,Y:] & Z c= Y implies Z | R = R /\ [:X,Z:] ) )
proof end;

theorem :: SYSREL:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z, W being set
for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
proof end;

theorem :: SYSREL:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
proof end;

theorem :: SYSREL:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being Relation st R c= S holds
R ~ c= S ~
proof end;

Lm1: for X being set holds id X c= [:X,X:]
proof end;

theorem :: SYSREL:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th29: :: SYSREL:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds (id X) * (id X) = id X
proof end;

theorem :: SYSREL:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds id {x} = {[x,x]}
proof end;

theorem :: SYSREL:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, X being set holds
( [x,y] in id X iff [y,x] in id X ) by RELAT_1:def 10;

theorem Th32: :: SYSREL:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof end;

theorem Th33: :: SYSREL:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
id X c= id Y
proof end;

theorem :: SYSREL:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds (id (X \ Y)) \ (id X) = {}
proof end;

theorem :: SYSREL:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation st R c= id (dom R) holds
R = id (dom R)
proof end;

theorem :: SYSREL:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation st id X c= R \/ (R ~ ) holds
( id X c= R & id X c= R ~ )
proof end;

theorem :: SYSREL:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation st id X c= R holds
id X c= R ~
proof end;

theorem :: SYSREL:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
proof end;

theorem :: SYSREL:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation holds
( ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ (dom (id X)) ) & ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ (rng (id X)) ) )
proof end;

theorem Th40: :: SYSREL:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R ) )
proof end;

theorem :: SYSREL:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( ( R c= R * R & R * (R \ (id (rng R))) = {} implies R /\ (id (rng R)) = id (rng R) ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies R /\ (id (dom R)) = id (dom R) ) )
proof end;

theorem :: SYSREL:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation holds
( ( R * (R \ (id X)) = {} & rng R c= X implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} & dom R c= X implies (R \ (id (dom R))) * R = {} ) )
proof end;

definition
let R be Relation;
func CL R -> Relation equals :: SYSREL:def 1
R /\ (id (dom R));
correctness
coherence
R /\ (id (dom R)) is Relation
;
;
end;

:: deftheorem defines CL SYSREL:def 1 :
for R being Relation holds CL R = R /\ (id (dom R));

theorem Th43: :: SYSREL:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( CL R c= R & CL R c= id (dom R) ) by XBOOLE_1:17;

theorem Th44: :: SYSREL:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
proof end;

theorem Th45: :: SYSREL:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds dom (CL R) = rng (CL R)
proof end;

theorem Th46: :: SYSREL:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
proof end;

theorem Th47: :: SYSREL:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds CL R = id (dom (CL R))
proof end;

theorem Th48: :: SYSREL:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for R being Relation holds
( ( R * R = R & R * (R \ (CL R)) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (CL R)) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
proof end;

theorem :: SYSREL:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )
proof end;

theorem :: SYSREL:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) )
proof end;

theorem Th51: :: SYSREL:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R )
proof end;

theorem :: SYSREL:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
proof end;

theorem Th53: :: SYSREL:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
proof end;

theorem Th54: :: SYSREL:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation holds
( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X | R = id X ) )
proof end;

theorem :: SYSREL:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) & ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) | R = id (dom (CL R)) & (rng (CL R)) | R = id (rng (CL R)) ) ) )
proof end;

theorem :: SYSREL:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) & ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} ) )
proof end;

theorem Th57: :: SYSREL:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} ) )
proof end;

theorem Th58: :: SYSREL:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} implies CL S c= CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} implies CL S c= CL R ) )
proof end;

theorem :: SYSREL:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, R being Relation holds
( ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R ) )
proof end;