let PTN be Petri_net; for M0 being Boolean_marking of PTN
for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))
let M0 be Boolean_marking of PTN; for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))
let Q0, Q1 be FinSequence of the carrier' of PTN; Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))
now ( ( Q0 = {} & Q1 = {} & Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ) or ( Q0 = {} & Q1 <> {} & Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ) or ( Q0 <> {} & Q1 = {} & Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ) or ( Q0 <> {} & Q1 <> {} & ( for i being Element of NAT holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ) ) )per cases
( ( Q0 = {} & Q1 = {} ) or ( Q0 = {} & Q1 <> {} ) or ( Q0 <> {} & Q1 = {} ) or ( Q0 <> {} & Q1 <> {} ) )
;
case A5:
(
Q0 <> {} &
Q1 <> {} )
;
for i being Element of NAT holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))then consider M3 being
FinSequence of
Bool_marks_of PTN such that A6:
(
len Q0 = len M3 &
Firing (
Q0,
M0)
= M3 /. (len M3) )
and A7:
M3 /. 1
= Firing (
(Q0 /. 1),
M0)
and A8:
for
i being
Nat st
i < len Q0 &
i > 0 holds
M3 /. (i + 1) = Firing (
(Q0 /. (i + 1)),
(M3 /. i))
by Def5;
consider M being
FinSequence of
Bool_marks_of PTN such that A9:
len (Q0 ^ Q1) = len M
and A10:
Firing (
(Q0 ^ Q1),
M0)
= M /. (len M)
and A11:
M /. 1
= Firing (
((Q0 ^ Q1) /. 1),
M0)
and A12:
for
i being
Nat st
i < len (Q0 ^ Q1) &
i > 0 holds
M /. (i + 1) = Firing (
((Q0 ^ Q1) /. (i + 1)),
(M /. i))
by A5, Def5;
defpred S1[
Nat]
means ( 1
+ $1
<= len Q0 implies
M /. (1 + $1) = M3 /. (1 + $1) );
0 < len Q1
by A5, NAT_1:3;
then
0 + (len Q0) < (len Q0) + (len Q1)
by XREAL_1:6;
then A13:
len Q0 < len (Q0 ^ 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] )A15:
0 <= k
by NAT_1:2;
assume A16:
S1[
k]
;
S1[k + 1]now ( 1 + (k + 1) <= len Q0 implies M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) )assume A17:
1
+ (k + 1) <= len Q0
;
M /. (1 + (k + 1)) = M3 /. (1 + (k + 1))then A18:
(Q0 ^ Q1) /. (1 + (k + 1)) = Q0 /. (1 + (k + 1))
by Th7, NAT_1:11;
A19:
1
+ k < len Q0
by A17, NAT_1:13;
then
1
+ k < len (Q0 ^ Q1)
by A13, XXREAL_0:2;
then
M /. (1 + (k + 1)) = Firing (
(Q0 /. (1 + (k + 1))),
(M3 /. (1 + k)))
by A12, A15, A16, A17, A18, NAT_1:13;
hence
M /. (1 + (k + 1)) = M3 /. (1 + (k + 1))
by A8, A15, A19;
verum end; hence
S1[
k + 1]
;
verum end; reconsider m =
(len Q0) - 1 as
Element of
NAT by A5, NAT_1:3, NAT_1:20;
let i be
Element of
NAT ;
Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))
len Q1 > 0
by A5, NAT_1:3;
then A20:
0 + 1
<= len Q1
by NAT_1:13;
consider M4 being
FinSequence of
Bool_marks_of PTN such that A21:
len Q1 = len M4
and A22:
Firing (
Q1,
(Firing (Q0,M0)))
= M4 /. (len M4)
and A23:
M4 /. 1
= Firing (
(Q1 /. 1),
(Firing (Q0,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, Def5;
consider k being
Nat such that A25:
len M4 = k + 1
by A5, A21, NAT_1:6;
A26:
S1[
0 ]
by A11, A7, Th7;
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 Q0) + 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]
0 <= k + (len Q0)
by NAT_1:2;
then A30:
(
(((len Q0) + 1) + k) + 1
= ((len Q0) + 1) + (k + 1) &
0 < ((len Q0) + k) + 1 )
;
A31:
0 <= k
by NAT_1:2;
now ( 1 + (k + 1) <= len Q1 implies M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) )assume A32:
1
+ (k + 1) <= len Q1
;
M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1))then A33:
(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;
A34:
1
+ k < len Q1
by A32, 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 A12, A30, A29, A32, A33, NAT_1:13;
hence
M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1))
by A24, A31, A34;
verum end; hence
S2[
k + 1]
;
verum end;
len Q0 > 0
by A5, NAT_1:3;
then M /. (((len Q0) + 1) + 0) =
Firing (
((Q0 ^ Q1) /. ((len Q0) + 1)),
(M /. (1 + m)))
by A12, A13
.=
Firing (
((Q0 ^ Q1) /. ((len Q0) + 1)),
(Firing (Q0,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);
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
M /. (len M) =
M /. ((len Q0) + (1 + k))
by A9, A21, A25, FINSEQ_1:22
.=
M /. (((len Q0) + 1) + k)
.=
M4 /. (len M4)
by A21, A36, A25
;
hence
Firing (
(Q0 ^ Q1),
M0)
= Firing (
Q1,
(Firing (Q0,M0)))
by A10, A22;
verum end; end; end;
hence
Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))
; verum