let PTN be PT_net_Str ; :: thesis: for M0 being Boolean_marking of PTN
for Q0, Q1 being FinSequence of the Transitions of PTN holds Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)
let M0 be Boolean_marking of PTN; :: thesis: for Q0, Q1 being FinSequence of the Transitions of PTN holds Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)
let Q0, Q1 be FinSequence of the Transitions of PTN; :: thesis: Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)
now per cases
( ( Q0 = {} & Q1 = {} ) or ( Q0 = {} & Q1 <> {} ) or ( Q0 <> {} & Q1 = {} ) or ( Q0 <> {} & Q1 <> {} ) )
;
case A5:
(
Q0 <> {} &
Q1 <> {} )
;
:: thesis: for i being Element of NAT holds Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)let i be
Element of
NAT ;
:: thesis: Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)A6:
len Q0 <> 0
by A5;
A7:
len Q1 <> 0
by A5;
then
(len Q0) + (len Q1) <> 0
by NAT_1:7;
then
len (Q0 ^ Q1) <> 0
by FINSEQ_1:35;
then
Q0 ^ Q1 <> {}
;
then consider M being
FinSequence of
Bool_marks_of PTN such that A8:
len (Q0 ^ Q1) = len M
and A9:
Firing (Q0 ^ Q1),
M0 = M /. (len M)
and A10:
M /. 1
= Firing ((Q0 ^ Q1) /. 1),
M0
and A11:
for
i being
Element of
NAT st
i < len (Q0 ^ Q1) &
i > 0 holds
M /. (i + 1) = Firing ((Q0 ^ Q1) /. (i + 1)),
(M /. i)
by Def5;
consider M3 being
FinSequence of
Bool_marks_of PTN such that A12:
len Q0 = len M3
and A13:
Firing Q0,
M0 = M3 /. (len M3)
and A14:
M3 /. 1
= Firing (Q0 /. 1),
M0
and A15:
for
i being
Element of
NAT st
i < len Q0 &
i > 0 holds
M3 /. (i + 1) = Firing (Q0 /. (i + 1)),
(M3 /. i)
by A5, Def5;
consider M4 being
FinSequence of
Bool_marks_of PTN such that A16:
len Q1 = len M4
and A17:
Firing Q1,
(Firing Q0,M0) = M4 /. (len M4)
and A18:
M4 /. 1
= Firing (Q1 /. 1),
(Firing Q0,M0)
and A19:
for
i being
Element of
NAT st
i < len Q1 &
i > 0 holds
M4 /. (i + 1) = Firing (Q1 /. (i + 1)),
(M4 /. i)
by A5, Def5;
A20:
len Q0 > 0
by A6, NAT_1:3;
A21:
len Q1 > 0
by A7, NAT_1:3;
defpred S1[
Element of
NAT ]
means ( 1
+ $1
<= len Q0 implies
M /. (1 + $1) = M3 /. (1 + $1) );
A22:
S1[
0 ]
by A10, A14, Th8;
0 < len Q1
by A7, NAT_1:3;
then
0 + (len Q0) < (len Q0) + (len Q1)
by XREAL_1:8;
then A23:
len Q0 < len (Q0 ^ Q1)
by FINSEQ_1:35;
A24:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )A25:
0 <= k
by NAT_1:2;
then A26:
0 < 1
+ k
;
assume A27:
S1[
k]
;
:: thesis: S1[k + 1]now assume A28:
1
+ (k + 1) <= len Q0
;
:: thesis: M /. (1 + (k + 1)) = M3 /. (1 + (k + 1))then A29:
(Q0 ^ Q1) /. (1 + (k + 1)) = Q0 /. (1 + (k + 1))
by Th8, NAT_1:11;
A30:
1
+ k < len Q0
by A28, NAT_1:13;
then
(
0 < 1
+ k & 1
+ k < len (Q0 ^ Q1) )
by A23, A25, XXREAL_0:2;
then
M /. (1 + (k + 1)) = Firing (Q0 /. (1 + (k + 1))),
(M3 /. (1 + k))
by A11, A27, A28, A29, NAT_1:13;
hence
M /. (1 + (k + 1)) = M3 /. (1 + (k + 1))
by A15, A26, A30;
:: thesis: verum end; hence
S1[
k + 1]
;
:: thesis: verum end; A31:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A22, A24);
A32:
0 + 1
<= len Q1
by A21, NAT_1:13;
reconsider m =
(len Q0) - 1 as
Element of
NAT by A6, NAT_1:3, NAT_1:20;
defpred S2[
Element of
NAT ]
means ( 1
+ $1
<= len Q1 implies
M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) );
M /. (((len Q0) + 1) + 0 ) =
Firing ((Q0 ^ Q1) /. ((len Q0) + 1)),
(M /. (1 + m))
by A11, A20, A23
.=
Firing ((Q0 ^ Q1) /. ((len Q0) + 1)),
(Firing Q0,M0)
by A12, A13, A31
.=
M4 /. (1 + 0 )
by A18, A32, GOBOARD2:5
;
then A33:
S2[
0 ]
;
A34:
now let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )A35:
(((len Q0) + 1) + k) + 1
= ((len Q0) + 1) + (k + 1)
;
0 <= k
by NAT_1:2;
then A36:
0 < 1
+ k
;
0 <= k + (len Q0)
by NAT_1:2;
then A37:
0 < ((len Q0) + k) + 1
;
assume A38:
S2[
k]
;
:: thesis: S2[k + 1]now assume A39:
1
+ (k + 1) <= len Q1
;
:: thesis: M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1))then A40:
(Q0 ^ Q1) /. ((len Q0) + (1 + (k + 1))) = Q1 /. (1 + (k + 1))
by GOBOARD2:5, NAT_1:11;
A41:
1
+ k < len Q1
by A39, NAT_1:13;
then
(len Q0) + (1 + k) < (len Q0) + (len Q1)
by XREAL_1:8;
then
((len Q0) + 1) + k < len (Q0 ^ Q1)
by FINSEQ_1:35;
then
M /. (((len Q0) + 1) + (k + 1)) = Firing (Q1 /. (1 + (k + 1))),
(M4 /. (1 + k))
by A11, A35, A37, A38, A39, A40, NAT_1:13;
hence
M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1))
by A19, A36, A41;
:: thesis: verum end; hence
S2[
k + 1]
;
:: thesis: verum end; A42:
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A33, A34);
consider k being
Nat such that A43:
len M4 = k + 1
by A7, A16, NAT_1:6;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
M /. (len M) =
M /. ((len Q0) + (1 + k))
by A8, A16, A43, FINSEQ_1:35
.=
M /. (((len Q0) + 1) + k)
.=
M4 /. (len M4)
by A16, A42, A43
;
hence
Firing (Q0 ^ Q1),
M0 = Firing Q1,
(Firing Q0,M0)
by A9, A17;
:: thesis: verum end;
hence
Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)
; :: thesis: verum