let PTN be Petri_net; for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
let M0 be marking of PTN; for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
let Q, Q1 be FinSequence of the carrier' of PTN; Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
now ( ( Q = {} & Q1 = {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q = {} & Q1 <> {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q <> {} & Q1 = {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q <> {} & Q1 <> {} & ( for i being Element of NAT holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) ) )per cases
( ( Q = {} & Q1 = {} ) or ( Q = {} & Q1 <> {} ) or ( Q <> {} & Q1 = {} ) or ( Q <> {} & Q1 <> {} ) )
;
case A5:
(
Q <> {} &
Q1 <> {} )
;
for i being Element of NAT holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))then consider M3 being
FinSequence of
nat_marks_of PTN such that A6:
(
len Q = len M3 &
Firing (
Q,
M0)
= M3 /. (len M3) )
and A7:
M3 /. 1
= Firing (
(Q /. 1),
M0)
and A8:
for
i being
Nat st
i < len Q &
i > 0 holds
M3 /. (i + 1) = Firing (
(Q /. (i + 1)),
(M3 /. i))
by Defb;
consider M being
FinSequence of
nat_marks_of PTN such that A9:
len (Q ^ Q1) = len M
and A10:
Firing (
(Q ^ Q1),
M0)
= M /. (len M)
and A11:
M /. 1
= Firing (
((Q ^ Q1) /. 1),
M0)
and A12:
for
i being
Nat st
i < len (Q ^ Q1) &
i > 0 holds
M /. (i + 1) = Firing (
((Q ^ Q1) /. (i + 1)),
(M /. i))
by A5, Defb;
defpred S1[
Nat]
means ( 1
+ $1
<= len Q implies
M /. (1 + $1) = M3 /. (1 + $1) );
0 + (len Q) < (len Q) + (len Q1)
by XREAL_1:6, A5;
then A13:
len Q < len (Q ^ Q1)
by FINSEQ_1:22;
A14:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A16:
S1[
k]
;
S1[k + 1]hence
S1[
k + 1]
;
verum end; reconsider m =
(len Q) - 1 as
Element of
NAT by A5, NAT_1:20;
let i be
Element of
NAT ;
Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))A20:
0 + 1
<= len Q1
by NAT_1:13, A5;
consider M4 being
FinSequence of
nat_marks_of PTN such that A21:
len Q1 = len M4
and A22:
Firing (
Q1,
(Firing (Q,M0)))
= M4 /. (len M4)
and A23:
M4 /. 1
= Firing (
(Q1 /. 1),
(Firing (Q,M0)))
and A24:
for
i being
Nat st
i < len Q1 &
i > 0 holds
M4 /. (i + 1) = Firing (
(Q1 /. (i + 1)),
(M4 /. i))
by A5, Defb;
consider k being
Nat such that A25:
len M4 = k + 1
by A5, A21, NAT_1:6;
A26:
S1[
0 ]
by A11, A7, BOOLMARK:7;
A27:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A26, A14);
defpred S2[
Nat]
means ( 1
+ $1
<= len Q1 implies
M /. (((len Q) + 1) + $1) = M4 /. (1 + $1) );
A28:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A29:
S2[
k]
;
S2[k + 1]A30:
(
(((len Q) + 1) + k) + 1
= ((len Q) + 1) + (k + 1) &
0 < ((len Q) + k) + 1 )
;
hence
S2[
k + 1]
;
verum end; M /. (((len Q) + 1) + 0) =
Firing (
((Q ^ Q1) /. ((len Q) + 1)),
(M /. (1 + m)))
by A12, A13
.=
Firing (
((Q ^ Q1) /. ((len Q) + 1)),
(Firing (Q,M0)))
by A6, A27
.=
M4 /. (1 + 0)
by A23, A20, SEQ_4:136
;
then A35:
S2[
0 ]
;
A36:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A35, A28);
M /. (len M) =
M /. ((len Q) + (1 + k))
by A9, A21, A25, FINSEQ_1:22
.=
M /. (((len Q) + 1) + k)
.=
M4 /. (len M4)
by A21, A36, A25
;
hence
Firing (
(Q ^ Q1),
M0)
= Firing (
Q1,
(Firing (Q,M0)))
by A10, A22;
verum end; end; end;
hence
Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
; verum