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 )

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 ) ) ) )

per cases ( ( Q = {} & Q1 = {} ) or ( Q = {} & Q1 <> {} ) or ( Q <> {} & Q1 = {} ) or ( Q <> {} & Q1 <> {} ) ) ;

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

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

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;

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;

case A4: ( Q <> {} & Q1 <> {} ) ; :: thesis: for i being Nat holds
( 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₁[ 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;

A19: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A21: S₁[k] ; :: thesis: S₁[k + 1]

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

assume 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;

hence S₁[k + 1] ; :: thesis: verum

end;

A25: S₁[ 0 ] by A16, A12, BOOLMARK:7;
A26: for k being Nat holds S₁[k] from NAT_1:sch 2(A25, A19);

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)) )

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;

defpred S₂[ Nat] means ( 1 + $1 <= len Q1 implies M /. (((len Q) + 1) + $1) = M4 /. (1 + $1) );

A35: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A36: S₂[k] ; :: thesis: S₂[k + 1]
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)) )

assume 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;

hence S₂[k + 1] ; :: thesis: verum

end;

M /. (((len Q) + 1) + 0) = Firing (((Q ^ Q1) /. ((len Q) + 1)),(M /. (1 + m))) by A17, A18
.= 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₂[ 0 ] ;
A44: for k being Nat holds S₂[k] from NAT_1:sch 2(A43, A35);

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)) )

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;

M /. (len M3) = M3 /. (len M3) by A10, A26, A14;
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;

end;

end;

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