let PTN be Petri_net; :: thesis: 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; :: thesis: 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; :: thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))

now :: thesis: ( ( 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 A1: ( Q0 = {} & Q1 = {} ) ; :: thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))

then A2: Q0 ^ Q1 = {} by FINSEQ_1:34;
Firing (Q1,(Firing (Q0,M0))) = Firing (Q1,M0) by A1, Def5
.= M0 by A1, Def5 ;
hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A2, Def5; :: thesis: verum

end;

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

then Firing ((Q0 ^ Q1),M0) = Firing (Q1,M0) by FINSEQ_1:34;
hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A3, Def5; :: thesis: verum

end;

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

then Firing ((Q0 ^ Q1),M0) = Firing (Q0,M0) by FINSEQ_1:34;
hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A4, Def5; :: thesis: verum

end;

case A5: ( Q0 <> {} & Q1 <> {} ) ; :: thesis: 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 S₁[ 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 :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A15: 0 <= k by NAT_1:2;
assume A16: S₁[k] ; :: thesis: S₁[k + 1]

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

assume A17: 1 + (k + 1) <= len Q0 ; :: thesis: 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; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: 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 ; :: thesis: 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: S₁[ 0 ] by A11, A7, Th7;
A27: for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A14);
defpred S₂[ Nat] means ( 1 + $1 <= len Q1 implies M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) );

A28: 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 A29: S₂[k] ; :: thesis: S₂[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 :: thesis: ( 1 + (k + 1) <= len Q1 implies M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) )

assume A32: 1 + (k + 1) <= len Q1 ; :: thesis: 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; :: thesis: verum

end;

hence S₂[k + 1] ; :: thesis: 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: S₂[ 0 ] ;
A36: for k being Nat holds S₂[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; :: thesis: verum

end;

end;

end;

hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ; :: thesis: verum