let PTN be Petri_net; for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN st Q ^ Q1 is_firable_at M0 holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
let M0 be marking of PTN; for Q, Q1 being FinSequence of the carrier' of PTN st Q ^ Q1 is_firable_at M0 holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
let Q, Q1 be FinSequence of the carrier' of PTN; ( Q ^ Q1 is_firable_at M0 implies ( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 ) )
assume A1:
Q ^ Q1 is_firable_at M0
; ( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
now ( ( Q = {} & Q1 = {} & Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 ) or ( Q = {} & Q1 <> {} & Q is_firable_at M0 & Q1 is_firable_at Firing (Q,M0) ) or ( Q <> {} & Q1 = {} & Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 ) or ( Q <> {} & Q1 <> {} & ( for i being Nat holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 ) ) ) )per cases
( ( Q = {} & Q1 = {} ) or ( Q = {} & Q1 <> {} ) or ( Q <> {} & Q1 = {} ) or ( Q <> {} & Q1 <> {} ) )
;
case A4:
(
Q <> {} &
Q1 <> {} )
;
for i being Nat holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )let i be
Nat;
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )A5:
0 + 1
<= len Q1
by NAT_1:13, A4;
then A6:
Q1 /. 1
= (Q ^ Q1) /. ((len Q) + 1)
by SEQ_4:136;
reconsider m =
(len Q) - 1 as
Element of
NAT by A4, NAT_1:20;
consider M4 being
FinSequence of
nat_marks_of PTN such that A7:
len Q1 = len M4
and
Firing (
Q1,
(Firing (Q,M0)))
= M4 /. (len M4)
and A8:
M4 /. 1
= Firing (
(Q1 /. 1),
(Firing (Q,M0)))
and A9:
for
i being
Nat st
i < len Q1 &
i > 0 holds
M4 /. (i + 1) = Firing (
(Q1 /. (i + 1)),
(M4 /. i))
by A4, Defb;
consider M3 being
FinSequence of
nat_marks_of PTN such that A10:
len Q = len M3
and A11:
Firing (
Q,
M0)
= M3 /. (len M3)
and A12:
M3 /. 1
= Firing (
(Q /. 1),
M0)
and A13:
for
i being
Nat st
i < len Q &
i > 0 holds
M3 /. (i + 1) = Firing (
(Q /. (i + 1)),
(M3 /. i))
by A4, Defb;
consider j being
Nat such that A14:
len M3 = j + 1
by A4, A10, NAT_1:6;
consider M being
FinSequence of
nat_marks_of PTN such that
len (Q ^ Q1) = len M
and A15:
(Q ^ Q1) /. 1
is_firable_at M0
and A16:
M /. 1
= Firing (
((Q ^ Q1) /. 1),
M0)
and A17:
for
i being
Nat st
i < len (Q ^ Q1) &
i > 0 holds
(
(Q ^ Q1) /. (i + 1) is_firable_at M /. i &
M /. (i + 1) = Firing (
((Q ^ Q1) /. (i + 1)),
(M /. i)) )
by A1, A4;
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, A4;
then A18:
len Q < len (Q ^ Q1)
by FINSEQ_1:22;
A19:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A21:
S1[
k]
;
S1[k + 1]hence
S1[
k + 1]
;
verum end; A25:
S1[
0 ]
by A16, A12, BOOLMARK:7;
A26:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A25, A19);
A27:
now for i being Nat st i < len Q & i > 0 holds
( Q /. (i + 1) is_firable_at M3 /. i & M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) )let i be
Nat;
( i < len Q & i > 0 implies ( Q /. (i + 1) is_firable_at M3 /. i & M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) ) )assume that A28:
i < len Q
and A29:
i > 0
;
( Q /. (i + 1) is_firable_at M3 /. i & M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) )consider j being
Nat such that A30:
i = j + 1
by A29, NAT_1:6;
A33:
(
i + 1
>= 1 &
i + 1
<= len Q )
by A28, NAT_1:11, NAT_1:13;
then
i + 1
in dom Q
by FINSEQ_3:25;
then A31:
(Q ^ Q1) /. (i + 1) = Q /. (i + 1)
by FINSEQ_4:68;
A32:
M /. i = M3 /. i
by A26, A28, A30;
A34:
i < len (Q ^ Q1)
by A18, A28, XXREAL_0:2;
then
M /. (i + 1) = Firing (
((Q ^ Q1) /. (i + 1)),
(M /. i))
by A17, A29;
hence
(
Q /. (i + 1) is_firable_at M3 /. i &
M3 /. (i + 1) = Firing (
(Q /. (i + 1)),
(M3 /. i)) )
by A17, A26, A29, A34, A31, A32, A33;
verum end; defpred S2[
Nat]
means ( 1
+ $1
<= len Q1 implies
M /. (((len Q) + 1) + $1) = M4 /. (1 + $1) );
A35:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A36:
S2[
k]
;
S2[k + 1]A37:
(
(((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 A17, A18
.=
Firing (
((Q ^ Q1) /. ((len Q) + 1)),
(Firing (Q,M0)))
by A10, A11, A26
.=
M4 /. (1 + 0)
by A8, A5, SEQ_4:136
;
then A43:
S2[
0 ]
;
A44:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A43, A35);
A45:
now for i being Nat st i < len Q1 & i > 0 holds
( Q1 /. (i + 1) is_firable_at M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) )let i be
Nat;
( i < len Q1 & i > 0 implies ( Q1 /. (i + 1) is_firable_at M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) ) )assume that A46:
i < len Q1
and A47:
i > 0
;
( Q1 /. (i + 1) is_firable_at M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) )consider j being
Nat such that A48:
i = j + 1
by A47, NAT_1:6;
((len Q) + 1) + j = (len Q) + (j + 1)
;
then A49:
M /. ((len Q) + i) = M4 /. i
by A44, A46, A48;
a52:
(
i + 1
>= 1 &
i + 1
<= len Q1 )
by A46, NAT_1:11, NAT_1:13;
then A50:
i + 1
in dom Q1
by FINSEQ_3:25;
A51:
(Q ^ Q1) /. (((len Q) + i) + 1) =
(Q ^ Q1) /. ((len Q) + (i + 1))
.=
Q1 /. (i + 1)
by A50, FINSEQ_4:69
;
A52:
((len Q) + 1) + i = ((len Q) + i) + 1
;
len (Q ^ Q1) = (len Q) + (len Q1)
by FINSEQ_1:22;
then A53:
(len Q) + i < len (Q ^ Q1)
by A46, XREAL_1:6;
M /. (((len Q) + i) + 1) = Firing (
((Q ^ Q1) /. (((len Q) + i) + 1)),
(M /. ((len Q) + i)))
by A17, A53, A4;
hence
(
Q1 /. (i + 1) is_firable_at M4 /. i &
M4 /. (i + 1) = Firing (
(Q1 /. (i + 1)),
(M4 /. i)) )
by A17, A44, A53, A51, A49, A52, A47, a52;
verum end;
M /. (len M3) = M3 /. (len M3)
by A10, A26, A14;
hence
Q1 is_firable_at Firing (
Q,
M0)
by A11, A7, A8, A45, A17, A10, A4, A18, A6;
Q is_firable_at M0
0 + 1
<= len Q
by A4, NAT_1:13;
then
Q /. 1
is_firable_at M0
by A15, BOOLMARK:7;
hence
Q is_firable_at M0
by A10, A12, A27;
verum end; end; end;
hence
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
; verum