let Dftn be Decision_free_PT; :: thesis: for dct being Circuit_of_places_and_trans of Dftn
for M0 being marking of Dftn
for Q being FinSequence of the carrier' of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))
let dct be Circuit_of_places_and_trans of Dftn; :: thesis: for M0 being marking of Dftn
for Q being FinSequence of the carrier' of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))
let M0 be marking of Dftn; :: thesis: for Q being FinSequence of the carrier' of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))
let Q be FinSequence of the carrier' of Dftn; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))
set P = places_of dct;
set F = Firing (Q,M0);

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

suppose C1: Q <> {} ; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))

then consider M being FinSequence of nat_marks_of Dftn such that
A2: len Q = len M and
A2a: Firing (Q,M0) = M /. (len M) and
A2b: M /. 1 = Firing ((Q /. 1),M0) and
A2c: for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by Defb;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len Q implies num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. $1)) );
A5: S₁[ 0 ] ;

A4: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A10: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A9: ( 1 <= i + 1 & i + 1 <= len Q ) ; :: thesis: num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. (i + 1)))
then X1: i < len Q by NAT_1:13;

per cases ( 0 = i or 0 < i ) ;

suppose 0 = i ; :: thesis: num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. (i + 1)))

hence num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. (i + 1))) ; :: thesis: verum

end;

suppose S2: 0 < i ; :: thesis: num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. (i + 1)))

then 0 + 1 <= i by NAT_1:13;
hence num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(Firing ((Q /. (i + 1)),(M /. i)))) by Th7, A10, NAT_1:13, A9
.= num_marks ((places_of dct),(M /. (i + 1))) by A2c, S2, X1 ;
:: thesis: verum

end;

end;

end;

end;

A6: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A4);
0 + 1 <= len Q by NAT_1:13, C1;
then num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. (len M))) by A2, A6;
hence num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0))) by A2a, A2b, Th7; :: thesis: verum

end;

suppose Q = {} ; :: thesis: num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))

hence num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0))) by Defb; :: thesis: verum

end;

end;