let PTN be Petri_net; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )

now :: thesis: ( ( 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 ) ) ) )end;

hence
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
; :: thesis: verum( 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 <> {} ) )
;

end;

case A2:
( Q = {} & Q1 <> {} )
; :: thesis: ( Q is_firable_at M0 & Q1 is_firable_at Firing (Q,M0) )

hence
Q is_firable_at M0
; :: thesis: Q1 is_firable_at Firing (Q,M0)

Q ^ Q1 = Q1 by A2, FINSEQ_1:34;

hence Q1 is_firable_at Firing (Q,M0) by A1, A2, Defb; :: thesis: verum

end;Q ^ Q1 = Q1 by A2, FINSEQ_1:34;

hence Q1 is_firable_at Firing (Q,M0) by A1, A2, Defb; :: thesis: verum

case A3:
( Q <> {} & Q1 = {} )
; :: thesis: ( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )

hence
Q1 is_firable_at Firing (Q,M0)
; :: thesis: Q is_firable_at M0

thus Q is_firable_at M0 by A1, A3, FINSEQ_1:34; :: thesis: verum

end;thus Q is_firable_at M0 by A1, A3, FINSEQ_1:34; :: thesis: verum

case A4:
( Q <> {} & Q1 <> {} )
; :: thesis: for i being Nat holds

( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )

( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )

let i be Nat; :: thesis: ( 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 S_{1}[ 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;

_{1}[ 0 ]
by A16, A12, BOOLMARK:7;

A26: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A25, A19);

_{2}[ Nat] means ( 1 + $1 <= len Q1 implies M /. (((len Q) + 1) + $1) = M4 /. (1 + $1) );

.= Firing (((Q ^ Q1) /. ((len Q) + 1)),(Firing (Q,M0))) by A10, A11, A26

.= M4 /. (1 + 0) by A8, A5, SEQ_4:136 ;

then A43: S_{2}[ 0 ]
;

A44: for k being Nat holds S_{2}[k]
from NAT_1:sch 2(A43, A35);

hence Q1 is_firable_at Firing (Q,M0) by A11, A7, A8, A45, A17, A10, A4, A18, A6; :: thesis: 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; :: thesis: verum

end;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 S

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 :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A25:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A21: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A21: S

now :: thesis: ( 1 + (k + 1) <= len Q implies M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) )

hence
Sassume A22:
1 + (k + 1) <= len Q
; :: thesis: M /. (1 + (k + 1)) = M3 /. (1 + (k + 1))

then A23: (Q ^ Q1) /. (1 + (k + 1)) = Q /. (1 + (k + 1)) by BOOLMARK:7, NAT_1:11;

A24: 1 + k < len Q by A22, NAT_1:13;

then 1 + k < len (Q ^ Q1) by A18, XXREAL_0:2;

then M /. (1 + (k + 1)) = Firing ((Q /. (1 + (k + 1))),(M3 /. (1 + k))) by A17, A21, A22, A23, NAT_1:13;

hence M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) by A13, A24; :: thesis: verum

end;then A23: (Q ^ Q1) /. (1 + (k + 1)) = Q /. (1 + (k + 1)) by BOOLMARK:7, NAT_1:11;

A24: 1 + k < len Q by A22, NAT_1:13;

then 1 + k < len (Q ^ Q1) by A18, XXREAL_0:2;

then M /. (1 + (k + 1)) = Firing ((Q /. (1 + (k + 1))),(M3 /. (1 + k))) by A17, A21, A22, A23, NAT_1:13;

hence M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) by A13, A24; :: thesis: verum

A26: for k being Nat holds S

A27: now :: thesis: 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)) )

defpred S( Q /. (i + 1) is_firable_at M3 /. i & M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) )

let i be Nat; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;assume that

A28: i < len Q and

A29: i > 0 ; :: thesis: ( 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; :: thesis: verum

A35: now :: thesis: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

M /. (((len Q) + 1) + 0) =
Firing (((Q ^ Q1) /. ((len Q) + 1)),(M /. (1 + m)))
by A17, A18
S

let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A36: S_{2}[k]
; :: thesis: S_{2}[k + 1]

A37: ( (((len Q) + 1) + k) + 1 = ((len Q) + 1) + (k + 1) & 0 < ((len Q) + k) + 1 ) ;

_{2}[k + 1]
; :: thesis: verum

end;assume A36: S

A37: ( (((len Q) + 1) + k) + 1 = ((len Q) + 1) + (k + 1) & 0 < ((len Q) + k) + 1 ) ;

now :: thesis: ( 1 + (k + 1) <= len Q1 implies M /. (((len Q) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) )

hence
Sassume A39:
1 + (k + 1) <= len Q1
; :: thesis: M /. (((len Q) + 1) + (k + 1)) = M4 /. (1 + (k + 1))

then A40: (Q ^ Q1) /. ((len Q) + (1 + (k + 1))) = Q1 /. (1 + (k + 1)) by NAT_1:11, SEQ_4:136;

A41: 1 + k < len Q1 by A39, NAT_1:13;

then (len Q) + (1 + k) < (len Q) + (len Q1) by XREAL_1:6;

then ((len Q) + 1) + k < len (Q ^ Q1) by FINSEQ_1:22;

then M /. (((len Q) + 1) + (k + 1)) = Firing ((Q1 /. (1 + (k + 1))),(M4 /. (1 + k))) by A17, A37, A36, A39, A40, NAT_1:13;

hence M /. (((len Q) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) by A9, A41; :: thesis: verum

end;then A40: (Q ^ Q1) /. ((len Q) + (1 + (k + 1))) = Q1 /. (1 + (k + 1)) by NAT_1:11, SEQ_4:136;

A41: 1 + k < len Q1 by A39, NAT_1:13;

then (len Q) + (1 + k) < (len Q) + (len Q1) by XREAL_1:6;

then ((len Q) + 1) + k < len (Q ^ Q1) by FINSEQ_1:22;

then M /. (((len Q) + 1) + (k + 1)) = Firing ((Q1 /. (1 + (k + 1))),(M4 /. (1 + k))) by A17, A37, A36, A39, A40, NAT_1:13;

hence M /. (((len Q) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) by A9, A41; :: thesis: verum

.= Firing (((Q ^ Q1) /. ((len Q) + 1)),(Firing (Q,M0))) by A10, A11, A26

.= M4 /. (1 + 0) by A8, A5, SEQ_4:136 ;

then A43: S

A44: for k being Nat holds S

A45: now :: thesis: 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)) )

M /. (len M3) = M3 /. (len M3)
by A10, A26, A14;( Q1 /. (i + 1) is_firable_at M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) )

let i be Nat; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;assume that

A46: i < len Q1 and

A47: i > 0 ; :: thesis: ( 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; :: thesis: verum

hence Q1 is_firable_at Firing (Q,M0) by A11, A7, A8, A45, A17, A10, A4, A18, A6; :: thesis: 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; :: thesis: verum