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

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:47;
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:47;
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:47;
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 Element of 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 Element of NAT st i < len (Q0 ^ Q1) & i > 0 holds
M /. (i + 1) = Firing ((Q0 ^ Q1) /. (i + 1)),(M /. i) by A5, Def5;
defpred S₁[ Element of 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:8;
then A13: len Q0 < len (Q0 ^ Q1) by FINSEQ_1:35;

A14: now

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

now

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 Th8, 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 Element of 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, Th8;
A27: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A26, A14);
defpred S₂[ Element of NAT ] means ( 1 + $1 <= len Q1 implies M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) );

A28: now

let k be Element of 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

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:153;
A34: 1 + k < len Q1 by A32, 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 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:153 ;
then A35: S₂[ 0 ] ;
A36: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A35, A28);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
M /. (len M) = M /. ((len Q0) + (1 + k)) by A9, A21, A25, FINSEQ_1:35
.= 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