let P be set ; :: thesis: 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; :: thesis: for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

let C1, C2 be firing-sequence of N; :: thesis: 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

F . ((len F1) + k) = F2 . k

hence fire (C1 ^ C2) = (fire C2) * (fire C1) by A1, A4, A7, A10, FUNCT_7:48; :: thesis: verum

for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

let N be Petri_net of P; :: thesis: for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

let C1, C2 be firing-sequence of N; :: thesis: 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

for k being Nat st k in dom F2 holds
let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )

assume A13: k in dom F1 ; :: thesis: 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; :: thesis: verum

end;assume A13: k in dom F1 ; :: thesis: 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; :: thesis: verum

F . ((len F1) + k) = F2 . k

proof

then
F = F1 ^ F2
by A11, A12, FINSEQ_1:def 7;
let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )

assume A22: k in dom F2 ; :: thesis: 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; :: thesis: verum

end;assume A22: k in dom F2 ; :: thesis: 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; :: thesis: verum

hence fire (C1 ^ C2) = (fire C2) * (fire C1) by A1, A4, A7, A10, FUNCT_7:48; :: thesis: verum