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