let P be set ; 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; 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; ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
defpred S1[ 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:
S1[ 0 ]
proof
let F be
Function-yielding FinSequence;
( 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
;
( 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) ) )
;
verum
end;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[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) )
;
S1[k + 1]
let F be
Function-yielding FinSequence;
( 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
;
( 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
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;
verum
end;
A17:
for k being Nat holds S1[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
hence
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
by A17, A18, A19; verum