set N = PetriNet ;

A5: 0 in the carrier of PetriNet by TARSKI:def 1;

1 in the carrier' of PetriNet by TARSKI:def 1;

then reconsider a0 = 0 , a1 = 1 as Element of places_and_trans_of PetriNet by A5, XBOOLE_0:def 3;

reconsider fs = <*a0,a1,a0*> as FinSequence of places_and_trans_of PetriNet ;

( fs is directed_path_like & fs is circular & fs is almost-one-to-one ) by Th12, Th13;

hence PetriNet is With_directed_circuit ; :: thesis: PetriNet is Petri

Flow PetriNet c= [: the carrier of PetriNet, the carrier' of PetriNet:] \/ [: the carrier' of PetriNet, the carrier of PetriNet:] ;

hence PetriNet is Petri by NET_1:def 2, ZFMISC_1:11; :: thesis: verum

now :: thesis: for s being place of PetriNet holds

( ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds

t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

hence
PetriNet is decision_free_like
; :: thesis: ( PetriNet is With_directed_circuit & PetriNet is Petri )( ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds

t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

let s be place of PetriNet; :: thesis: ( ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds

t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

thus ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet :: thesis: ( ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds

t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

t1 = t2 :: thesis: ( ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

t1 = t2

t1 = t2 :: thesis: verum

end;t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

thus ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet :: thesis: ( ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds

t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

proof

thus
for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds
reconsider t = 1 as transition of PetriNet by TARSKI:def 1;

take t ; :: thesis: [t,s] in the T-S_Arcs of PetriNet

thus [t,s] in the T-S_Arcs of PetriNet ; :: thesis: verum

end;take t ; :: thesis: [t,s] in the T-S_Arcs of PetriNet

thus [t,s] in the T-S_Arcs of PetriNet ; :: thesis: verum

t1 = t2 :: thesis: ( ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds

t1 = t2 ) )

proof

thus
ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet
:: thesis: for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
let t1, t2 be transition of PetriNet; :: thesis: ( [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet implies t1 = t2 )

assume ( [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet ) ; :: thesis: t1 = t2

t1 = 1 by TARSKI:def 1;

hence t1 = t2 by TARSKI:def 1; :: thesis: verum

end;assume ( [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet ) ; :: thesis: t1 = t2

t1 = 1 by TARSKI:def 1;

hence t1 = t2 by TARSKI:def 1; :: thesis: verum

t1 = t2

proof

thus
for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
reconsider t = 1 as transition of PetriNet by TARSKI:def 1;

take t ; :: thesis: [s,t] in the S-T_Arcs of PetriNet

thus [s,t] in the S-T_Arcs of PetriNet ; :: thesis: verum

end;take t ; :: thesis: [s,t] in the S-T_Arcs of PetriNet

thus [s,t] in the S-T_Arcs of PetriNet ; :: thesis: verum

t1 = t2 :: thesis: verum

proof

let t1, t2 be transition of PetriNet; :: thesis: ( [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet implies t1 = t2 )

assume ( [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet ) ; :: thesis: t1 = t2

t1 = 1 by TARSKI:def 1;

hence t1 = t2 by TARSKI:def 1; :: thesis: verum

end;assume ( [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet ) ; :: thesis: t1 = t2

t1 = 1 by TARSKI:def 1;

hence t1 = t2 by TARSKI:def 1; :: thesis: verum

A5: 0 in the carrier of PetriNet by TARSKI:def 1;

1 in the carrier' of PetriNet by TARSKI:def 1;

then reconsider a0 = 0 , a1 = 1 as Element of places_and_trans_of PetriNet by A5, XBOOLE_0:def 3;

reconsider fs = <*a0,a1,a0*> as FinSequence of places_and_trans_of PetriNet ;

( fs is directed_path_like & fs is circular & fs is almost-one-to-one ) by Th12, Th13;

hence PetriNet is With_directed_circuit ; :: thesis: PetriNet is Petri

Flow PetriNet c= [: the carrier of PetriNet, the carrier' of PetriNet:] \/ [: the carrier' of PetriNet, the carrier of PetriNet:] ;

hence PetriNet is Petri by NET_1:def 2, ZFMISC_1:11; :: thesis: verum