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 S1[ Nat] means ( 1 <= $1 & $1 <= len Q implies num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. $1)) );
A5: S1[ 0 ] ;
A4: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A10: S1[i] ; :: thesis: S1[i + 1]
thus S1[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 S1[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;