defpred S₁[ Element of NAT ] means for Q being FinSequence of the Transitions of PTN st $1 = len Q holds
( ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of NAT st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) );
A1: S₁[ 0 ] ;

A2: now

let n be Element of NAT ; :: thesis:
assume A3: S₁[n] ; :: thesis:
thus S₁[n + 1] :: thesis:

let Q be FinSequence of the Transitions of PTN; :: thesis:
assume A4: n + 1 = len Q ; :: thesis:
thus ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) ; :: thesis:
thus ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of NAT st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) :: thesis:

assume Q <> {} ; :: thesis:
then len Q <> 0 ;
then consider Q1 being FinSequence of the Transitions of PTN, t being transition of PTN such that
A5: Q = Q1 ^ <*t*> by FINSEQ_2:22;
A6: n + 1 = (len Q1) + 1 by A4, A5, FINSEQ_2:19;

per cases ;

suppose A7: Q1 = {} ; :: thesis:

take M2 = Firing t,M0; :: thesis:
take M = <*M2*>; :: thesis:
A8: len Q = (len Q1) + (len <*t*>) by A5, FINSEQ_1:35
.= 0 + (len <*t*>) by A7
.= 0 + 1 by FINSEQ_1:56 ;
hence len Q = len M by FINSEQ_1:56; :: thesis:
hence M2 = M /. (len M) by A8, FINSEQ_4:25; :: thesis:
Q = <*t*> by A5, A7, FINSEQ_1:47;
then Q /. 1 = t by FINSEQ_4:25;
hence M /. 1 = Firing (Q /. 1),M0 by FINSEQ_4:25; :: thesis:
let i be Element of NAT ; :: thesis:
assume ( i < len Q & i > 0 ) ; :: thesis:
hence M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) by A8, NAT_1:13; :: thesis:

end;

suppose A9: Q1 <> {} ; :: thesis:

then consider B2 being Boolean_marking of PTN, B being FinSequence of Bool_marks_of PTN such that
A10: len Q1 = len B and
A11: B2 = B /. (len B) and
A12: B /. 1 = Firing (Q1 /. 1),M0 and
A13: for i being Element of NAT st i < len Q1 & i > 0 holds
B /. (i + 1) = Firing (Q1 /. (i + 1)),(B /. i) by A3, A6;
take M2 = Firing t,B2; :: thesis:
take M = B ^ <*M2*>; :: thesis:
A14: len M = (len B) + (len <*M2*>) by FINSEQ_1:35
.= (len B) + 1 by FINSEQ_1:57 ;
A15: len Q = (len Q1) + (len <*t*>) by A5, FINSEQ_1:35
.= (len Q1) + 1 by FINSEQ_1:57 ;
hence len Q = len M by A10, A14; :: thesis:
thus M2 = M /. (len M) by A14, FINSEQ_4:82; :: thesis:
len Q1 <> 0 by A9;
then A16: len Q1 > 0 by NAT_1:3;
then 0 + 1 < (len B) + 1 by A10, XREAL_1:8;
then A17: 1 <= len B by NAT_1:13;
then A18: 1 in dom B by FINSEQ_3:27;
0 + 1 < (len Q1) + 1 by A16, XREAL_1:8;
then 1 <= len Q1 by NAT_1:13;
then A19: 1 in dom Q1 by FINSEQ_3:27;
thus M /. 1 = B /. 1 by A18, FINSEQ_4:83
.= Firing (Q /. 1),M0 by A5, A12, A19, FINSEQ_4:83 ; :: thesis:
let i be Element of NAT ; :: thesis:
assume that
A20: i < len Q and
A21: i > 0 ; :: thesis:
thus M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) :: thesis:

A22: Seg ((len Q1) + 1) = (Seg (len Q1)) \/ {((len Q1) + 1)} by FINSEQ_1:11;
A23: 1 <= i + 1 by NAT_1:12;
i + 1 <= (len Q1) + 1 by A15, A20, NAT_1:13;
then A24: i + 1 in Seg ((len Q1) + 1) by A23, FINSEQ_1:3;

per cases by A22, A24, XBOOLE_0:def 3;

suppose A25: i + 1 in Seg (len Q1) ; :: thesis:

then i + 1 <= len Q1 by FINSEQ_1:3;
then i < len Q1 by NAT_1:13;
then A26: B /. (i + 1) = Firing (Q1 /. (i + 1)),(B /. i) by A13, A21;
0 + 1 < i + 1 by A21, XREAL_1:8;
then A27: 1 <= i by NAT_1:13;
i + 1 in dom B by A10, A25, FINSEQ_1:def 3;
then A28: B /. (i + 1) = M /. (i + 1) by FINSEQ_4:83;
A29: i + 1 <= len B by A10, A25, FINSEQ_1:3;
i + 1 in dom Q1 by A25, FINSEQ_1:def 3;
then A30: Q1 /. (i + 1) = Q /. (i + 1) by A5, FINSEQ_4:83;
i + 1 <= (len B) + 1 by A29, NAT_1:12;
then i <= len B by XREAL_1:8;
then i in dom B by A27, FINSEQ_3:27;
hence M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) by A26, A28, A30, FINSEQ_4:83; :: thesis:

end;

suppose i + 1 in {((len Q1) + 1)} ; :: thesis:

then A31: i + 1 = (len Q1) + 1 by TARSKI:def 1;
then A32: M /. (i + 1) = M2 by A10, FINSEQ_4:82;
A33: Q /. (i + 1) = t by A5, A31, FINSEQ_4:82;
len B in dom B by A17, FINSEQ_3:27;
hence M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) by A10, A11, A31, A32, A33, FINSEQ_4:83; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence ( ( Q = {} implies ex b₁ being Boolean_marking of PTN st b₁ = M0 ) & ( not Q = {} implies ex b₁ being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b₁ = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of NAT st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) ) ; :: thesis: