let PTN be Petri_net; :: thesis: for M0 being marking of PTN

for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

let M0 be marking of PTN; :: thesis: for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

let Q, Q1 be FinSequence of the carrier' of PTN; :: thesis: Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

let M0 be marking of PTN; :: thesis: for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

let Q, Q1 be FinSequence of the carrier' of PTN; :: thesis: Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

now :: thesis: ( ( Q = {} & Q1 = {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q = {} & Q1 <> {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q <> {} & Q1 = {} & Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) or ( Q <> {} & Q1 <> {} & ( for i being Element of NAT holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) ) ) )end;

hence
Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
; :: thesis: verumper cases
( ( Q = {} & Q1 = {} ) or ( Q = {} & Q1 <> {} ) or ( Q <> {} & Q1 = {} ) or ( Q <> {} & Q1 <> {} ) )
;

end;

case A1:
( Q = {} & Q1 = {} )
; :: thesis: Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

then A2:
Q ^ Q1 = {}
by FINSEQ_1:34;

Firing (Q1,(Firing (Q,M0))) = Firing (Q1,M0) by A1, Defb

.= M0 by A1, Defb ;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A2, Defb; :: thesis: verum

end;Firing (Q1,(Firing (Q,M0))) = Firing (Q1,M0) by A1, Defb

.= M0 by A1, Defb ;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A2, Defb; :: thesis: verum

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

then
Firing ((Q ^ Q1),M0) = Firing (Q1,M0)
by FINSEQ_1:34;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A3, Defb; :: thesis: verum

end;hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A3, Defb; :: thesis: verum

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

then
Firing ((Q ^ Q1),M0) = Firing (Q,M0)
by FINSEQ_1:34;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A4, Defb; :: thesis: verum

end;hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A4, Defb; :: thesis: verum

case A5:
( Q <> {} & Q1 <> {} )
; :: thesis: for i being Element of NAT holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

then consider M3 being FinSequence of nat_marks_of PTN such that

A6: ( len Q = len M3 & Firing (Q,M0) = M3 /. (len M3) ) and

A7: M3 /. 1 = Firing ((Q /. 1),M0) and

A8: for i being Nat st i < len Q & i > 0 holds

M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) by Defb;

consider M being FinSequence of nat_marks_of PTN such that

A9: len (Q ^ Q1) = len M and

A10: Firing ((Q ^ Q1),M0) = M /. (len M) and

A11: M /. 1 = Firing (((Q ^ Q1) /. 1),M0) and

A12: for i being Nat st i < len (Q ^ Q1) & i > 0 holds

M /. (i + 1) = Firing (((Q ^ Q1) /. (i + 1)),(M /. i)) by A5, Defb;

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, A5;

then A13: len Q < len (Q ^ Q1) by FINSEQ_1:22;

let i be Element of NAT ; :: thesis: Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

A20: 0 + 1 <= len Q1 by NAT_1:13, A5;

consider M4 being FinSequence of nat_marks_of PTN such that

A21: len Q1 = len M4 and

A22: Firing (Q1,(Firing (Q,M0))) = M4 /. (len M4) and

A23: M4 /. 1 = Firing ((Q1 /. 1),(Firing (Q,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, Defb;

consider k being Nat such that

A25: len M4 = k + 1 by A5, A21, NAT_1:6;

A26: S_{1}[ 0 ]
by A11, A7, BOOLMARK:7;

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

defpred S_{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 A6, A27

.= M4 /. (1 + 0) by A23, A20, SEQ_4:136 ;

then A35: S_{2}[ 0 ]
;

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

M /. (len M) = M /. ((len Q) + (1 + k)) by A9, A21, A25, FINSEQ_1:22

.= M /. (((len Q) + 1) + k)

.= M4 /. (len M4) by A21, A36, A25 ;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A10, A22; :: thesis: verum

end;A6: ( len Q = len M3 & Firing (Q,M0) = M3 /. (len M3) ) and

A7: M3 /. 1 = Firing ((Q /. 1),M0) and

A8: for i being Nat st i < len Q & i > 0 holds

M3 /. (i + 1) = Firing ((Q /. (i + 1)),(M3 /. i)) by Defb;

consider M being FinSequence of nat_marks_of PTN such that

A9: len (Q ^ Q1) = len M and

A10: Firing ((Q ^ Q1),M0) = M /. (len M) and

A11: M /. 1 = Firing (((Q ^ Q1) /. 1),M0) and

A12: for i being Nat st i < len (Q ^ Q1) & i > 0 holds

M /. (i + 1) = Firing (((Q ^ Q1) /. (i + 1)),(M /. i)) by A5, Defb;

defpred S

0 + (len Q) < (len Q) + (len Q1) by XREAL_1:6, A5;

then A13: len Q < len (Q ^ Q1) by FINSEQ_1:22;

A14: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

reconsider m = (len Q) - 1 as Element of NAT by A5, NAT_1:20;S

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

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

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

end;assume A16: S

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

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

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

A19: 1 + k < len Q by A17, NAT_1:13;

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

then M /. (1 + (k + 1)) = Firing ((Q /. (1 + (k + 1))),(M3 /. (1 + k))) by A12, A16, A17, A18, NAT_1:13;

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

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

A19: 1 + k < len Q by A17, NAT_1:13;

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

then M /. (1 + (k + 1)) = Firing ((Q /. (1 + (k + 1))),(M3 /. (1 + k))) by A12, A16, A17, A18, NAT_1:13;

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

let i be Element of NAT ; :: thesis: Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))

A20: 0 + 1 <= len Q1 by NAT_1:13, A5;

consider M4 being FinSequence of nat_marks_of PTN such that

A21: len Q1 = len M4 and

A22: Firing (Q1,(Firing (Q,M0))) = M4 /. (len M4) and

A23: M4 /. 1 = Firing ((Q1 /. 1),(Firing (Q,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, Defb;

consider k being Nat such that

A25: len M4 = k + 1 by A5, A21, NAT_1:6;

A26: S

A27: for k being Nat holds S

defpred S

A28: 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 A12, A13
S

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

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

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

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

end;assume A29: S

A30: ( (((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 A32:
1 + (k + 1) <= len Q1
; :: thesis: M /. (((len Q) + 1) + (k + 1)) = M4 /. (1 + (k + 1))

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

A34: 1 + k < len Q1 by A32, 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 A12, A30, A29, A32, A33, NAT_1:13;

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

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

A34: 1 + k < len Q1 by A32, 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 A12, A30, A29, A32, A33, NAT_1:13;

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

.= Firing (((Q ^ Q1) /. ((len Q) + 1)),(Firing (Q,M0))) by A6, A27

.= M4 /. (1 + 0) by A23, A20, SEQ_4:136 ;

then A35: S

A36: for k being Nat holds S

M /. (len M) = M /. ((len Q) + (1 + k)) by A9, A21, A25, FINSEQ_1:22

.= M /. (((len Q) + 1) + k)

.= M4 /. (len M4) by A21, A36, A25 ;

hence Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0))) by A10, A22; :: thesis: verum