set PLA = {0};

set a = 1;

set b = 2;

set TRA = {1};

set TSA = [:{1},{0}:];

[:{1},{0}:] c= [:{1},{0}:] ;

then reconsider TSA = [:{1},{0}:] as non empty Relation of {1},{0} ;

set STA = [:{0},{1}:];

[:{0},{1}:] c= [:{0},{1}:] ;

then reconsider STA = [:{0},{1}:] as non empty Relation of {0},{1} ;

set CS = {1,2};

set CS0 = {1};

set fa = the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}));

set f = {1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}));

set CPNT = Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #);

A1: Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) is with_S-T_arc ;

Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) is with_T-S_arc ;

then reconsider CPNT = Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) as Colored_Petri_net by A1;

a0: ( 1 in {1,2} & 2 in {1,2} & 1 <> 2 ) by TARSKI:def 2;

then reconsider CPNT = CPNT as strict Colored-PT-net-like Colored_Petri_net by A2, PETRI_2:def 11;

take CPNT ; :: thesis: CPNT is with-nontrivial-ColoredSet

thus CPNT is with-nontrivial-ColoredSet by a0, ZFMISC_1:def 10; :: thesis: verum

set a = 1;

set b = 2;

set TRA = {1};

set TSA = [:{1},{0}:];

[:{1},{0}:] c= [:{1},{0}:] ;

then reconsider TSA = [:{1},{0}:] as non empty Relation of {1},{0} ;

set STA = [:{0},{1}:];

[:{0},{1}:] c= [:{0},{1}:] ;

then reconsider STA = [:{0},{1}:] as non empty Relation of {0},{1} ;

set CS = {1,2};

set CS0 = {1};

set fa = the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}));

set f = {1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}));

set CPNT = Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #);

A1: Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) is with_S-T_arc ;

Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) is with_T-S_arc ;

then reconsider CPNT = Colored_PT_net_Str(# {0},{1},STA,TSA,{1,2},({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) #) 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))

A7:
dom ({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) = {1}
by FUNCOP_1:13;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}

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 {0} by TARSKI:def 1;

then [1,0] in TSA by A4, ZFMISC_1:87;

then reconsider O = {0} as Subset of ({t} *') by ZFMISC_1:31, A3, PETRI:8;

[0,1] in STA by A5, A4, ZFMISC_1:87;

then reconsider I = {0} as Subset of (*' {t}) by ZFMISC_1:31, A3, PETRI:6;

A6: the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0})) is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;

({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) . t = the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0})) 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;proof

then reconsider CS1 = {1} as non empty Subset of the ColoredSet of CPNT ;
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;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

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 {0} by TARSKI:def 1;

then [1,0] in TSA by A4, ZFMISC_1:87;

then reconsider O = {0} as Subset of ({t} *') by ZFMISC_1:31, A3, PETRI:8;

[0,1] in STA by A5, A4, ZFMISC_1:87;

then reconsider I = {0} as Subset of (*' {t}) by ZFMISC_1:31, A3, PETRI:6;

A6: the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0})) is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;

({1} --> the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0}))) . t = the Function of (thin_cylinders ({1},{0})),(thin_cylinders ({1},{0})) 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

now :: thesis: for x being object st x in dom the firing-rule of CPNT holds

x in the carrier' of CPNT \ (Outbds CPNT)

then
dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT)
;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 {0} by TARSKI:def 1;

then a8: [a1,0] in TSA by ZFMISC_1:87;

A9: not a1 in Outbds CPNT

then x = 1 by A7, TARSKI:def 1;

hence x in the carrier' of CPNT \ (Outbds CPNT) by A9, XBOOLE_0:def 5; :: thesis: verum

end;let x be object ; :: thesis: ( x in dom the firing-rule of CPNT implies x in the carrier' of CPNT \ (Outbds CPNT) )

0 in {0} by TARSKI:def 1;

then a8: [a1,0] in TSA by ZFMISC_1:87;

A9: not a1 in Outbds CPNT

proof

assume
x in dom the firing-rule of CPNT
; :: thesis: x in the carrier' of CPNT \ (Outbds CPNT)
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;then ex x being transition of CPNT st

( a1 = x & x is outbound ) ;

hence contradiction by a8, PETRI:8; :: thesis: verum

then x = 1 by A7, TARSKI:def 1;

hence x in the carrier' of CPNT \ (Outbds CPNT) by A9, XBOOLE_0:def 5; :: thesis: verum

then reconsider CPNT = CPNT as strict Colored-PT-net-like Colored_Petri_net by A2, PETRI_2:def 11;

take CPNT ; :: thesis: CPNT is with-nontrivial-ColoredSet

thus CPNT is with-nontrivial-ColoredSet by a0, ZFMISC_1:def 10; :: thesis: verum