let P be set ; :: thesis: for N being Petri_net of P

for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let N be Petri_net of P; :: thesis: for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let C be firing-sequence of N; :: thesis: ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

defpred S_{1}[ Nat] means for F being Function-yielding FinSequence st len F = $1 & ( for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ) holds

( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) );

A1: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A2);

consider F being Function-yielding FinSequence such that

A18: fire C = compose (F,(Funcs (P,NAT))) and

A19: len F = len C and

A20: for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) by Def10;

for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t

for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let N be Petri_net of P; :: thesis: for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

let C be firing-sequence of N; :: thesis: ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

defpred S

ex t being transition of P st F . i = fire t ) holds

( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) );

A1: S

proof

A2:
for k being Nat st S
let F be Function-yielding FinSequence; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

assume len F = 0 ; :: thesis: ( ex i being Nat st

( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

then F = {} ;

then compose (F,(Funcs (P,NAT))) = id (Funcs (P,NAT)) by FUNCT_7:39;

hence ( ex i being Nat st

( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ) ; :: thesis: verum

end;ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

assume len F = 0 ; :: thesis: ( ex i being Nat st

( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

then F = {} ;

then compose (F,(Funcs (P,NAT))) = id (Funcs (P,NAT)) by FUNCT_7:39;

hence ( ex i being Nat st

( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ) ; :: thesis: verum

S

proof

A17:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: for G being Function-yielding FinSequence st len G = k & ( for i being Nat st i in dom G holds

ex t being transition of P st G . i = fire t ) holds

( dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ; :: thesis: S_{1}[k + 1]

let F be Function-yielding FinSequence; :: thesis: ( len F = k + 1 & ( for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

assume that

A4: len F = k + 1 and

A5: for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ; :: thesis: ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) )

consider G being FinSequence, x being set such that

A6: F = G ^ <*x*> and

A7: len G = k by A4, TREES_2:3;

reconsider G = G as Function-yielding FinSequence by A6, FUNCT_7:23;

0 + 1 <= k + 1 by XREAL_1:7;

then k + 1 in dom F by A4, FINSEQ_3:25;

then consider t being transition of P such that

A8: F . (k + 1) = fire t by A5;

x = F . (k + 1) by A6, A7, FINSEQ_1:42;

then A9: compose (F,(Funcs (P,NAT))) = (fire t) * (compose (G,(Funcs (P,NAT)))) by A6, A8, FUNCT_7:41;

A10: dom (fire t) = Funcs (P,NAT) by Def8;

A11: rng (fire t) c= Funcs (P,NAT) by Th20;

A12: for i being Nat st i in dom G holds

ex t being transition of P st G . i = fire t

A16: rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) by A3, A7, A12;

rng (compose (F,(Funcs (P,NAT)))) c= rng (fire t) by A9, RELAT_1:26;

hence ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) by A9, A10, A11, A15, A16, RELAT_1:27; :: thesis: verum

end;assume A3: for G being Function-yielding FinSequence st len G = k & ( for i being Nat st i in dom G holds

ex t being transition of P st G . i = fire t ) holds

( dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ; :: thesis: S

let F be Function-yielding FinSequence; :: thesis: ( len F = k + 1 & ( for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )

assume that

A4: len F = k + 1 and

A5: for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t ; :: thesis: ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) )

consider G being FinSequence, x being set such that

A6: F = G ^ <*x*> and

A7: len G = k by A4, TREES_2:3;

reconsider G = G as Function-yielding FinSequence by A6, FUNCT_7:23;

0 + 1 <= k + 1 by XREAL_1:7;

then k + 1 in dom F by A4, FINSEQ_3:25;

then consider t being transition of P such that

A8: F . (k + 1) = fire t by A5;

x = F . (k + 1) by A6, A7, FINSEQ_1:42;

then A9: compose (F,(Funcs (P,NAT))) = (fire t) * (compose (G,(Funcs (P,NAT)))) by A6, A8, FUNCT_7:41;

A10: dom (fire t) = Funcs (P,NAT) by Def8;

A11: rng (fire t) c= Funcs (P,NAT) by Th20;

A12: for i being Nat st i in dom G holds

ex t being transition of P st G . i = fire t

proof

then A15:
dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT)
by A3, A7;
let i be Nat; :: thesis: ( i in dom G implies ex t being transition of P st G . i = fire t )

A13: dom G c= dom F by A6, FINSEQ_1:26;

assume A14: i in dom G ; :: thesis: ex t being transition of P st G . i = fire t

then G . i = F . i by A6, FINSEQ_1:def 7;

hence ex t being transition of P st G . i = fire t by A5, A13, A14; :: thesis: verum

end;A13: dom G c= dom F by A6, FINSEQ_1:26;

assume A14: i in dom G ; :: thesis: ex t being transition of P st G . i = fire t

then G . i = F . i by A6, FINSEQ_1:def 7;

hence ex t being transition of P st G . i = fire t by A5, A13, A14; :: thesis: verum

A16: rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) by A3, A7, A12;

rng (compose (F,(Funcs (P,NAT)))) c= rng (fire t) by A9, RELAT_1:26;

hence ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) by A9, A10, A11, A15, A16, RELAT_1:27; :: thesis: verum

consider F being Function-yielding FinSequence such that

A18: fire C = compose (F,(Funcs (P,NAT))) and

A19: len F = len C and

A20: for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) by Def10;

for i being Nat st i in dom F holds

ex t being transition of P st F . i = fire t

proof

hence
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
by A17, A18, A19; :: thesis: verum
let i be Nat; :: thesis: ( i in dom F implies ex t being transition of P st F . i = fire t )

assume A21: i in dom F ; :: thesis: ex t being transition of P st F . i = fire t

A22: dom F = Seg (len F) by FINSEQ_1:def 3;

A23: dom C = Seg (len C) by FINSEQ_1:def 3;

reconsider t = C /. i as Element of N ;

take t ; :: thesis: F . i = fire t

thus F . i = fire t by A19, A20, A21, A22, A23; :: thesis: verum

end;assume A21: i in dom F ; :: thesis: ex t being transition of P st F . i = fire t

A22: dom F = Seg (len F) by FINSEQ_1:def 3;

A23: dom C = Seg (len C) by FINSEQ_1:def 3;

reconsider t = C /. i as Element of N ;

take t ; :: thesis: F . i = fire t

thus F . i = fire t by A19, A20, A21, A22, A23; :: thesis: verum