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

definition
let R be Relation;
let X be set ;
pred R is_reflexive_in X means :Def1: :: RELAT_2:def 1
for x being set st x in X holds
[x,x] in R;
pred R is_irreflexive_in X means :Def2: :: RELAT_2:def 2
for x being set st x in X holds
not [x,x] in R;
pred R is_symmetric_in X means :Def3: :: RELAT_2:def 3
for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R;
pred R is_antisymmetric_in X means :Def4: :: RELAT_2:def 4
for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y;
pred R is_asymmetric_in X means :Def5: :: RELAT_2:def 5
for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R;
pred R is_connected_in X means :Def6: :: RELAT_2:def 6
for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R;
pred R is_strongly_connected_in X means :Def7: :: RELAT_2:def 7
for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R;
pred R is_transitive_in X means :Def8: :: RELAT_2:def 8
for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R;
end;

:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
for R being Relation
for X being set holds
( R is_reflexive_in X iff for x being set st x in X holds
[x,x] in R );

:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def 2 :
for R being Relation
for X being set holds
( R is_irreflexive_in X iff for x being set st x in X holds
not [x,x] in R );

:: deftheorem Def3 defines is_symmetric_in RELAT_2:def 3 :
for R being Relation
for X being set holds
( R is_symmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
[y,x] in R );

:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def 4 :
for R being Relation
for X being set holds
( R is_antisymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y );

:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def 5 :
for R being Relation
for X being set holds
( R is_asymmetric_in X iff for x, y being set st x in X & y in X & [x,y] in R holds
not [y,x] in R );

:: deftheorem Def6 defines is_connected_in RELAT_2:def 6 :
for R being Relation
for X being set holds
( R is_connected_in X iff for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def 7 :
for R being Relation
for X being set holds
( R is_strongly_connected_in X iff for x, y being set st x in X & y in X & not [x,y] in R holds
[y,x] in R );

:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
for R being Relation
for X being set holds
( R is_transitive_in X iff for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R );

definition
let R be Relation;
attr R is reflexive means :Def9: :: RELAT_2:def 9
R is_reflexive_in field R;
attr R is irreflexive means :Def10: :: RELAT_2:def 10
R is_irreflexive_in field R;
attr R is symmetric means :Def11: :: RELAT_2:def 11
R is_symmetric_in field R;
attr R is antisymmetric means :Def12: :: RELAT_2:def 12
R is_antisymmetric_in field R;
attr R is asymmetric means :Def13: :: RELAT_2:def 13
R is_asymmetric_in field R;
attr R is connected means :Def14: :: RELAT_2:def 14
R is_connected_in field R;
attr R is strongly_connected means :Def15: :: RELAT_2:def 15
R is_strongly_connected_in field R;
attr R is transitive means :Def16: :: RELAT_2:def 16
R is_transitive_in field R;
end;

:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
for R being Relation holds
( R is reflexive iff R is_reflexive_in field R );

:: deftheorem Def10 defines irreflexive RELAT_2:def 10 :
for R being Relation holds
( R is irreflexive iff R is_irreflexive_in field R );

:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
for R being Relation holds
( R is symmetric iff R is_symmetric_in field R );

:: deftheorem Def12 defines antisymmetric RELAT_2:def 12 :
for R being Relation holds
( R is antisymmetric iff R is_antisymmetric_in field R );

:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
for R being Relation holds
( R is asymmetric iff R is_asymmetric_in field R );

:: deftheorem Def14 defines connected RELAT_2:def 14 :
for R being Relation holds
( R is connected iff R is_connected_in field R );

:: deftheorem Def15 defines strongly_connected RELAT_2:def 15 :
for R being Relation holds
( R is strongly_connected iff R is_strongly_connected_in field R );

:: deftheorem Def16 defines transitive RELAT_2:def 16 :
for R being Relation holds
( R is transitive iff R is_transitive_in field R );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: RELAT_2:17  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 is reflexive iff id (field R) c= R )
proof end;

theorem :: RELAT_2:18  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 is irreflexive iff id (field R) misses R )
proof end;

theorem :: RELAT_2:19  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 is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
proof end;

theorem :: RELAT_2:20  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 is_asymmetric_in X holds
R \/ (id X) is_antisymmetric_in X
proof end;

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

theorem Th22: :: RELAT_2:22  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 is symmetric & R is transitive holds
R is reflexive
proof end;

theorem Th23: :: RELAT_2:23  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 is symmetric & id X is transitive )
proof end;

theorem :: RELAT_2:24  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 is antisymmetric & id X is reflexive )
proof end;

theorem :: RELAT_2:25  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 is irreflexive & R is transitive holds
R is asymmetric
proof end;

theorem :: RELAT_2:26  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 is asymmetric holds
( R is irreflexive & R is antisymmetric )
proof end;

theorem Th27: :: RELAT_2:27  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 is reflexive holds
R ~ is reflexive
proof end;

theorem :: RELAT_2:28  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 is irreflexive holds
R ~ is irreflexive
proof end;

theorem :: RELAT_2:29  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 is reflexive holds
( dom R = dom (R ~ ) & rng R = rng (R ~ ) )
proof end;

theorem Th30: :: RELAT_2:30  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 is symmetric iff R = R ~ )
proof end;

theorem :: RELAT_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is reflexive & R is reflexive holds
( P \/ R is reflexive & P /\ R is reflexive )
proof end;

theorem :: RELAT_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is irreflexive & R is irreflexive holds
( P \/ R is irreflexive & P /\ R is irreflexive )
proof end;

theorem :: RELAT_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is irreflexive holds
P \ R is irreflexive
proof end;

theorem :: RELAT_2:34  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 is symmetric holds
R ~ is symmetric by Th30;

theorem :: RELAT_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is symmetric & R is symmetric holds
( P \/ R is symmetric & P /\ R is symmetric & P \ R is symmetric )
proof end;

theorem :: RELAT_2:36  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 is asymmetric holds
R ~ is asymmetric
proof end;

theorem :: RELAT_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is asymmetric & R is asymmetric holds
P /\ R is asymmetric
proof end;

theorem :: RELAT_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is asymmetric holds
P \ R is asymmetric
proof end;

theorem :: RELAT_2:39  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 is antisymmetric iff R /\ (R ~ ) c= id (dom R) )
proof end;

theorem :: RELAT_2: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 st R is antisymmetric holds
R ~ is antisymmetric
proof end;

theorem :: RELAT_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is antisymmetric holds
( P /\ R is antisymmetric & P \ R is antisymmetric )
proof end;

theorem :: RELAT_2:42  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 is transitive holds
R ~ is transitive
proof end;

theorem :: RELAT_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st P is transitive & R is transitive holds
P /\ R is transitive
proof end;

theorem :: RELAT_2:44  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 is transitive iff R * R c= R )
proof end;

theorem :: RELAT_2: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
( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ ) )
proof end;

theorem :: RELAT_2:46  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 is strongly_connected holds
( R is connected & R is reflexive )
proof end;

theorem :: RELAT_2: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
( R is strongly_connected iff [:(field R),(field R):] = R \/ (R ~ ) )
proof end;