let P be set ; for N being Petri_net of P
for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
let N be Petri_net of P; for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
let C1, C2 be firing-sequence of N; fire (C1 ^ C2) = (fire C2) * (fire C1)
consider F being Function-yielding FinSequence such that
A1:
fire (C1 ^ C2) = compose (F,(Funcs (P,NAT)))
and
A2:
len F = len (C1 ^ C2)
and
A3:
for i being Element of NAT st i in dom (C1 ^ C2) holds
F . i = fire ((C1 ^ C2) /. i)
by Def10;
consider F1 being Function-yielding FinSequence such that
A4:
fire C1 = compose (F1,(Funcs (P,NAT)))
and
A5:
len F1 = len C1
and
A6:
for i being Element of NAT st i in dom C1 holds
F1 . i = fire (C1 /. i)
by Def10;
consider F2 being Function-yielding FinSequence such that
A7:
fire C2 = compose (F2,(Funcs (P,NAT)))
and
A8:
len F2 = len C2
and
A9:
for i being Element of NAT st i in dom C2 holds
F2 . i = fire (C2 /. i)
by Def10;
A10:
rng (fire C1) c= Funcs (P,NAT)
by Th26;
len F = (len C1) + (len C2)
by A2, FINSEQ_1:22;
then A11:
dom F = Seg ((len F1) + (len F2))
by A5, A8, FINSEQ_1:def 3;
A12:
for k being Nat st k in dom F1 holds
F . k = F1 . k
proof
let k be
Nat;
( k in dom F1 implies F . k = F1 . k )
assume A13:
k in dom F1
;
F . k = F1 . k
A14:
dom F1 = Seg (len F1)
by FINSEQ_1:def 3;
A15:
dom F1 = Seg (len C1)
by A5, FINSEQ_1:def 3;
A16:
dom F1 = dom C1
by A5, A14, FINSEQ_1:def 3;
A17:
k in dom C1
by A13, A15, FINSEQ_1:def 3;
A18:
dom C1 c= dom (C1 ^ C2)
by FINSEQ_1:26;
then A19:
F . k = fire ((C1 ^ C2) /. k)
by A3, A17;
A20:
(C1 ^ C2) /. k = (C1 ^ C2) . k
by A17, A18, PARTFUN1:def 6;
A21:
(C1 ^ C2) . k = C1 . k
by A13, A16, FINSEQ_1:def 7;
C1 . k = C1 /. k
by A13, A16, PARTFUN1:def 6;
hence
F . k = F1 . k
by A6, A13, A16, A19, A20, A21;
verum
end;
for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . k
proof
let k be
Nat;
( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume A22:
k in dom F2
;
F . ((len F1) + k) = F2 . k
dom F2 = Seg (len F2)
by FINSEQ_1:def 3;
then A23:
dom F2 = dom C2
by A8, FINSEQ_1:def 3;
then A24:
(len F1) + k in dom (C1 ^ C2)
by A5, A22, FINSEQ_1:28;
reconsider lFk =
(len F1) + k as
Element of
NAT by ORDINAL1:def 12;
A25:
F . ((len F1) + k) = fire ((C1 ^ C2) /. lFk)
by A3, A5, A22, A23, FINSEQ_1:28;
A26:
(C1 ^ C2) /. ((len F1) + k) = (C1 ^ C2) . ((len F1) + k)
by A24, PARTFUN1:def 6;
A27:
(C1 ^ C2) . ((len F1) + k) = C2 . k
by A5, A22, A23, FINSEQ_1:def 7;
C2 . k = C2 /. k
by A22, A23, PARTFUN1:def 6;
hence
F . ((len F1) + k) = F2 . k
by A9, A22, A23, A25, A26, A27;
verum
end;
then
F = F1 ^ F2
by A11, A12, FINSEQ_1:def 7;
hence
fire (C1 ^ C2) = (fire C2) * (fire C1)
by A1, A4, A7, A10, FUNCT_7:48; verum