defpred S₁[ Nat] means for Q being FinSequence of the carrier' of PTN st $1 = len Q holds
( ( Q = {} implies ex M1 being marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) );

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

proof

let Q be FinSequence of the carrier' of PTN; :: thesis: ( n + 1 = len Q implies ( ( Q = {} implies ex M1 being marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) )
assume A3: n + 1 = len Q ; :: thesis: ( ( Q = {} implies ex M1 being marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )
thus ( Q = {} implies ex M1 being marking of PTN st M1 = M0 ) ; :: thesis: ( Q <> {} implies ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) )
thus ( Q <> {} implies ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) :: thesis: verum

proof

assume Q <> {} ; :: thesis: ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
then len Q <> 0 ;
then consider Q1 being FinSequence of the carrier' of PTN, t being transition of PTN such that
A4: Q = Q1 ^ <*t*> by FINSEQ_2:19;
A5: n + 1 = (len Q1) + 1 by A3, A4, FINSEQ_2:16;

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

suppose A6: Q1 = {} ; :: thesis: ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )

take M2 = Firing (t,M0); :: thesis: ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
take M = <*M2*>; :: thesis: ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
A7: len Q = (len Q1) + (len <*t*>) by A4, FINSEQ_1:22
.= 0 + 1 by FINSEQ_1:39, A6 ;
hence len Q = len M by FINSEQ_1:39; :: thesis: ( M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
hence M2 = M /. (len M) by A7, FINSEQ_4:16; :: thesis: ( M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
Q = <*t*> by A4, A6, FINSEQ_1:34;
then Q /. 1 = t by FINSEQ_4:16;
hence M /. 1 = Firing ((Q /. 1),M0) by FINSEQ_4:16; :: thesis: for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))
let i be Nat; :: thesis: ( i < len Q & i > 0 implies M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) )
assume ( i < len Q & i > 0 ) ; :: thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))
hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A7, NAT_1:13; :: thesis: verum

end;

suppose A8: Q1 <> {} ; :: thesis: ex M2 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )

then 0 + 1 < (len Q1) + 1 by XREAL_1:6;
then 1 <= len Q1 by NAT_1:13;
then A10: 1 in dom Q1 by FINSEQ_3:25;
A11: len Q = (len Q1) + (len <*t*>) by A4, FINSEQ_1:22
.= (len Q1) + 1 by FINSEQ_1:40 ;
consider B2 being marking of PTN, B being FinSequence of nat_marks_of PTN such that
A12: len Q1 = len B and
A13: B2 = B /. (len B) and
A14: B /. 1 = Firing ((Q1 /. 1),M0) and
A15: for i being Nat st i < len Q1 & i > 0 holds
B /. (i + 1) = Firing ((Q1 /. (i + 1)),(B /. i)) by A2, A5, A8;
take M2 = Firing (t,B2); :: thesis: ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
take M = B ^ <*M2*>; :: thesis: ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
A16: len M = (len B) + (len <*M2*>) by FINSEQ_1:22
.= (len B) + 1 by FINSEQ_1:40 ;
hence len Q = len M by A12, A11; :: thesis: ( M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
thus M2 = M /. (len M) by A16, FINSEQ_4:67; :: thesis: ( M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) )
0 + 1 < (len B) + 1 by A12, A8, XREAL_1:6;
then A17: 1 <= len B by NAT_1:13;
then 1 in dom B by FINSEQ_3:25;
hence M /. 1 = B /. 1 by FINSEQ_4:68
.= Firing ((Q /. 1),M0) by A4, A14, A10, FINSEQ_4:68 ;
:: thesis: for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))
let i be Nat; :: thesis: ( i < len Q & i > 0 implies M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) )
assume that
A18: i < len Q and
A19: i > 0 ; :: thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))
thus M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) :: thesis: verum

proof

( 1 <= i + 1 & i + 1 <= (len Q1) + 1 ) by A11, A18, NAT_1:12, NAT_1:13;
then A20: ( Seg ((len Q1) + 1) = (Seg (len Q1)) \/ {((len Q1) + 1)} & i + 1 in Seg ((len Q1) + 1) ) by FINSEQ_1:9, FINSEQ_1:1;

per cases ( i + 1 in Seg (len Q1) or i + 1 in {((len Q1) + 1)} ) by A20, XBOOLE_0:def 3;

suppose A21: i + 1 in Seg (len Q1) ; :: thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))

then i + 1 <= len B by A12, FINSEQ_1:1;
then i + 1 <= (len B) + 1 by NAT_1:12;
then A22: i <= len B by XREAL_1:6;
0 + 1 < i + 1 by A19, XREAL_1:6;
then 1 <= i by NAT_1:13;
then A23: i in dom B by A22, FINSEQ_3:25;
i + 1 <= len Q1 by A21, FINSEQ_1:1;
then i < len Q1 by NAT_1:13;
then A24: B /. (i + 1) = Firing ((Q1 /. (i + 1)),(B /. i)) by A15, A19;
i + 1 in dom Q1 by A21, FINSEQ_1:def 3;
then A25: Q1 /. (i + 1) = Q /. (i + 1) by A4, FINSEQ_4:68;
i + 1 in dom B by A12, A21, FINSEQ_1:def 3;
then B /. (i + 1) = M /. (i + 1) by FINSEQ_4:68;
hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A24, A25, A23, FINSEQ_4:68; :: thesis: verum

end;

suppose A26: i + 1 in {((len Q1) + 1)} ; :: thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))

A27: len B in dom B by A17, FINSEQ_3:25;
A28: i + 1 = (len Q1) + 1 by A26, TARSKI:def 1;
then ( M /. (i + 1) = M2 & Q /. (i + 1) = t ) by A4, A12, FINSEQ_4:67;
hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A12, A13, A28, A27, FINSEQ_4:68; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

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