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

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 = {} )
;

end;

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_{1}[ Nat] means ( 1 <= $1 & $1 <= len Q implies num_marks ((places_of dct),(M /. 1)) = num_marks ((places_of dct),(M /. $1)) );

A5: S_{1}[ 0 ]
;

_{1}[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;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

A5: S

A4: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A6:
for i being Nat holds SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A10: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A10: S

thus S

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;

end;then X1: i < len Q by NAT_1:13;

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

end;

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

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