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

definition
let N be Net ;
canceled;
func chaos N -> set equals :: FF_SIEC:def 2
(Elements N) \/ {(Elements N)};
correctness
coherence
(Elements N) \/ {(Elements N)} is set
;
;
end;

:: deftheorem FF_SIEC:def 1 :
canceled;

:: deftheorem defines chaos FF_SIEC:def 2 :
for N being Net holds chaos N = (Elements N) \/ {(Elements N)};

definition
let X, Y be set ;
assume A1: X misses Y ;
canceled;
func PTempty_f_net X,Y -> strict Pnet equals :Def4: :: FF_SIEC:def 4
Net(# X,Y,{} #);
correctness
coherence
Net(# X,Y,{} #) is strict Pnet
;
proof end;
end;

:: deftheorem FF_SIEC:def 3 :
canceled;

:: deftheorem Def4 defines PTempty_f_net FF_SIEC:def 4 :
for X, Y being set st X misses Y holds
PTempty_f_net X,Y = Net(# X,Y,{} #);

definition
let X be set ;
func Tempty_f_net X -> strict Pnet equals :: FF_SIEC:def 5
PTempty_f_net X,{} ;
correctness
coherence
PTempty_f_net X,{} is strict Pnet
;
;
func Pempty_f_net X -> strict Pnet equals :: FF_SIEC:def 6
PTempty_f_net {} ,X;
correctness
coherence
PTempty_f_net {} ,X is strict Pnet
;
;
end;

:: deftheorem defines Tempty_f_net FF_SIEC:def 5 :
for X being set holds Tempty_f_net X = PTempty_f_net X,{} ;

:: deftheorem defines Pempty_f_net FF_SIEC:def 6 :
for X being set holds Pempty_f_net X = PTempty_f_net {} ,X;

definition
let x be set ;
func Tsingle_f_net x -> strict Pnet equals :: FF_SIEC:def 7
PTempty_f_net {} ,{x};
correctness
coherence
PTempty_f_net {} ,{x} is strict Pnet
;
;
func Psingle_f_net x -> strict Pnet equals :: FF_SIEC:def 8
PTempty_f_net {x},{} ;
correctness
coherence
PTempty_f_net {x},{} is strict Pnet
;
;
end;

:: deftheorem defines Tsingle_f_net FF_SIEC:def 7 :
for x being set holds Tsingle_f_net x = PTempty_f_net {} ,{x};

:: deftheorem defines Psingle_f_net FF_SIEC:def 8 :
for x being set holds Psingle_f_net x = PTempty_f_net {x},{} ;

definition
func empty_f_net -> strict Pnet equals :: FF_SIEC:def 9
PTempty_f_net {} ,{} ;
correctness
coherence
PTempty_f_net {} ,{} is strict Pnet
;
;
end;

:: deftheorem defines empty_f_net FF_SIEC:def 9 :
empty_f_net = PTempty_f_net {} ,{} ;

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

theorem :: FF_SIEC:2  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 misses Y holds
( the Places of (PTempty_f_net X,Y) = X & the Transitions of (PTempty_f_net X,Y) = Y & the Flow of (PTempty_f_net X,Y) = {} )
proof end;

theorem :: FF_SIEC:3  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
( the Places of (Tempty_f_net X) = X & the Transitions of (Tempty_f_net X) = {} & the Flow of (Tempty_f_net X) = {} )
proof end;

theorem :: FF_SIEC:4  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
( the Places of (Pempty_f_net X) = {} & the Transitions of (Pempty_f_net X) = X & the Flow of (Pempty_f_net X) = {} )
proof end;

theorem :: FF_SIEC:5  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
( the Places of (Tsingle_f_net x) = {} & the Transitions of (Tsingle_f_net x) = {x} & the Flow of (Tsingle_f_net x) = {} )
proof end;

theorem :: FF_SIEC:6  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
( the Places of (Psingle_f_net x) = {x} & the Transitions of (Psingle_f_net x) = {} & the Flow of (Psingle_f_net x) = {} )
proof end;

theorem :: FF_SIEC:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the Places of empty_f_net = {} & the Transitions of empty_f_net = {} & the Flow of empty_f_net = {} )
proof end;

theorem :: FF_SIEC:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( the Places of M c= Elements M & the Transitions of M c= Elements M ) by NET_1:4, NET_1:5;

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

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

theorem Th11: :: FF_SIEC:11  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 M being Pnet holds
( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) )
proof end;

theorem :: FF_SIEC:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds chaos M <> {}
proof end;

theorem Th13: :: FF_SIEC:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( the Flow of M c= [:(Elements M),(Elements M):] & the Flow of M ~ c= [:(Elements M),(Elements M):] )
proof end;

theorem Th14: :: FF_SIEC:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( rng (the Flow of M | the Transitions of M) c= the Places of M & rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M & dom (the Flow of M | the Transitions of M) c= the Transitions of M & dom ((the Flow of M ~ ) | the Transitions of M) c= the Transitions of M & rng (the Flow of M | the Places of M) c= the Transitions of M & rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M & dom (the Flow of M | the Places of M) c= the Places of M & dom ((the Flow of M ~ ) | the Places of M) c= the Places of M & rng (id the Transitions of M) c= the Transitions of M & dom (id the Transitions of M) c= the Transitions of M & rng (id the Places of M) c= the Places of M & dom (id the Places of M) c= the Places of M )
proof end;

Lm1: for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C
proof end;

theorem Th15: :: FF_SIEC:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (id the Places of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (id the Places of M) & rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M) & rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng (the Flow of M | the Places of M) misses dom (id the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) & dom (the Flow of M | the Places of M) misses rng (the Flow of M | the Places of M) & dom (the Flow of M | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (the Flow of M | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) )
proof end;

theorem Th16: :: FF_SIEC:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & (the Flow of M | the Places of M) * (the Flow of M | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M) = {} )
proof end;

theorem Th17: :: FF_SIEC:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} )
proof end;

theorem Th18: :: FF_SIEC:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (the Flow of M ~ ) | the Transitions of M misses id (Elements M) & the Flow of M | the Transitions of M misses id (Elements M) & (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )
proof end;

theorem Th19: :: FF_SIEC:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M )
proof end;

theorem Th20: :: FF_SIEC:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (the Flow of M | the Places of M) ~ = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Transitions of M) ~ = (the Flow of M ~ ) | the Places of M )
proof end;

theorem Th21: :: FF_SIEC:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M & (the Flow of M | the Transitions of M) \/ (the Flow of M | the Places of M) = the Flow of M & ((the Flow of M | the Places of M) ~ ) \/ ((the Flow of M | the Transitions of M) ~ ) = the Flow of M ~ & ((the Flow of M | the Transitions of M) ~ ) \/ ((the Flow of M | the Places of M) ~ ) = the Flow of M ~ )
proof end;

definition
let M be Pnet;
func f_enter M -> Relation equals :: FF_SIEC:def 10
((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M);
correctness
coherence
((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M) is Relation
;
;
func f_exit M -> Relation equals :: FF_SIEC:def 11
(the Flow of M | the Transitions of M) \/ (id the Places of M);
correctness
coherence
(the Flow of M | the Transitions of M) \/ (id the Places of M) is Relation
;
;
end;

:: deftheorem defines f_enter FF_SIEC:def 10 :
for M being Pnet holds f_enter M = ((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M);

:: deftheorem defines f_exit FF_SIEC:def 11 :
for M being Pnet holds f_exit M = (the Flow of M | the Transitions of M) \/ (id the Places of M);

theorem :: FF_SIEC:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
proof end;

theorem :: FF_SIEC:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )
proof end;

theorem :: FF_SIEC:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )
proof end;

theorem :: FF_SIEC:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )
proof end;

definition
let M be Pnet;
func f_prox M -> Relation equals :: FF_SIEC:def 12
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M);
correctness
coherence
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M) is Relation
;
;
func f_flow M -> Relation equals :: FF_SIEC:def 13
the Flow of M \/ (id (Elements M));
correctness
coherence
the Flow of M \/ (id (Elements M)) is Relation
;
;
end;

:: deftheorem defines f_prox FF_SIEC:def 12 :
for M being Pnet holds f_prox M = ((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M);

:: deftheorem defines f_flow FF_SIEC:def 13 :
for M being Pnet holds f_flow M = the Flow of M \/ (id (Elements M));

theorem :: FF_SIEC:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~ ) )
proof end;

definition
let M be Pnet;
func f_places M -> set equals :: FF_SIEC:def 14
the Places of M;
correctness
coherence
the Places of M is set
;
;
func f_transitions M -> set equals :: FF_SIEC:def 15
the Transitions of M;
correctness
coherence
the Transitions of M is set
;
;
func f_pre M -> Relation equals :: FF_SIEC:def 16
the Flow of M | the Transitions of M;
correctness
coherence
the Flow of M | the Transitions of M is Relation
;
;
func f_post M -> Relation equals :: FF_SIEC:def 17
(the Flow of M ~ ) | the Transitions of M;
correctness
coherence
(the Flow of M ~ ) | the Transitions of M is Relation
;
;
end;

:: deftheorem defines f_places FF_SIEC:def 14 :
for M being Pnet holds f_places M = the Places of M;

:: deftheorem defines f_transitions FF_SIEC:def 15 :
for M being Pnet holds f_transitions M = the Transitions of M;

:: deftheorem defines f_pre FF_SIEC:def 16 :
for M being Pnet holds f_pre M = the Flow of M | the Transitions of M;

:: deftheorem defines f_post FF_SIEC:def 17 :
for M being Pnet holds f_post M = (the Flow of M ~ ) | the Transitions of M;

theorem :: FF_SIEC:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )
proof end;

theorem :: FF_SIEC:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds f_places M misses f_transitions M by NET_1:def 1;

theorem :: FF_SIEC:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
proof end;

definition
let M be Pnet;
func f_entrance M -> Relation equals :: FF_SIEC:def 18
((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M);
correctness
coherence
((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M) is Relation
;
;
func f_escape M -> Relation equals :: FF_SIEC:def 19
(the Flow of M | the Places of M) \/ (id the Transitions of M);
correctness
coherence
(the Flow of M | the Places of M) \/ (id the Transitions of M) is Relation
;
;
end;

:: deftheorem defines f_entrance FF_SIEC:def 18 :
for M being Pnet holds f_entrance M = ((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M);

:: deftheorem defines f_escape FF_SIEC:def 19 :
for M being Pnet holds f_escape M = (the Flow of M | the Places of M) \/ (id the Transitions of M);

theorem :: FF_SIEC:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )
proof end;

theorem :: FF_SIEC:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )
proof end;

theorem :: FF_SIEC:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )
proof end;

theorem :: FF_SIEC:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )
proof end;

notation
let M be Pnet;
synonym f_circulation M for f_flow M;
end;

definition
let M be Pnet;
func f_adjac M -> Relation equals :: FF_SIEC:def 20
((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M);
correctness
coherence
((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M) is Relation
;
;
end;

:: deftheorem defines f_adjac FF_SIEC:def 20 :
for M being Pnet holds f_adjac M = ((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M);

theorem :: FF_SIEC:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Pnet holds
( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~ )) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~ ) )
proof end;