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₁[ 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₁[ 0 ]

proof

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;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[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₁[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

proof

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;

then A15: dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) by A3, A7;
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;

A17: for k being Nat holds S₁[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

proof

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;

hence ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) ) by A17, A18, A19; :: thesis: verum