set PLA = ;
set a = 1;
set b = 2;
set TRA = {1};
set TSA = ;
[:{1},:] c= ;
then reconsider TSA = as non empty Relation of {1}, ;
set STA = ;
[:,{1}:] c= ;
then reconsider STA = as non empty Relation of ,{1} ;
set CS = {1,2};
set CS0 = {1};
set fa = the Function of (),();
set f = {1} --> the Function of (),();
set CPNT = Colored_PT_net_Str(# ,{1},STA,TSA,{1,2},({1} --> the Function of (),()) #);
A1: Colored_PT_net_Str(# ,{1},STA,TSA,{1,2},({1} --> the Function of (),()) #) is with_S-T_arc ;
Colored_PT_net_Str(# ,{1},STA,TSA,{1,2},({1} --> the Function of (),()) #) is with_T-S_arc ;
then reconsider CPNT = Colored_PT_net_Str(# ,{1},STA,TSA,{1,2},({1} --> the Function of (),()) #) as Colored_Petri_net by A1;
a0: ( 1 in {1,2} & 2 in {1,2} & 1 <> 2 ) by TARSKI:def 2;
A2: now :: thesis: for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O))
{1} c= {1,2}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in {1,2} )
assume x in {1} ; :: thesis: x in {1,2}
then x = 1 by TARSKI:def 1;
hence x in {1,2} by TARSKI:def 2; :: thesis: verum
end;
then reconsider CS1 = {1} as non empty Subset of the ColoredSet of CPNT ;
let t be transition of CPNT; :: thesis: ( t in dom the firing-rule of CPNT implies ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) )
assume t in dom the firing-rule of CPNT ; :: thesis: ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O))
A3: t = 1 by TARSKI:def 1;
A4: 1 in {1} by TARSKI:def 1;
A5: 0 in by TARSKI:def 1;
then [1,0] in TSA by ;
then reconsider O = as Subset of ({t} *') by ;
[0,1] in STA by ;
then reconsider I = as Subset of (*' {t}) by ;
A6: the Function of (),() is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;
({1} --> the Function of (),()) . t = the Function of (),() by FUNCOP_1:7;
hence ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) by A6; :: thesis: verum
end;
A7: dom ({1} --> the Function of (),()) = {1} by FUNCOP_1:13;
now :: thesis: for x being object st x in dom the firing-rule of CPNT holds
x in the carrier' of CPNT \ (Outbds CPNT)
reconsider a1 = 1 as transition of CPNT by TARSKI:def 1;
let x be object ; :: thesis: ( x in dom the firing-rule of CPNT implies x in the carrier' of CPNT \ (Outbds CPNT) )
0 in by TARSKI:def 1;
then a8: [a1,0] in TSA by ZFMISC_1:87;
A9: not a1 in Outbds CPNT
proof
assume a1 in Outbds CPNT ; :: thesis: contradiction
then ex x being transition of CPNT st
( a1 = x & x is outbound ) ;
hence contradiction by a8, PETRI:8; :: thesis: verum
end;
assume x in dom the firing-rule of CPNT ; :: thesis: x in the carrier' of CPNT \ (Outbds CPNT)
then x = 1 by ;
hence x in the carrier' of CPNT \ (Outbds CPNT) by ; :: thesis: verum
end;
then dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) ;
then reconsider CPNT = CPNT as strict Colored-PT-net-like Colored_Petri_net by ;
take CPNT ; :: thesis:
thus CPNT is with-nontrivial-ColoredSet by ; :: thesis: verum