defpred S1[ 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 S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
thus S1[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 ;
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) + () by
.= 0 + 1 by ;
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 ; :: 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 ;
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 ; :: 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) + () by
.= (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 ; :: 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 ; :: 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 ;
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 ;
:: 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 ;
then A20: ( Seg ((len Q1) + 1) = (Seg (len Q1)) \/ {((len Q1) + 1)} & i + 1 in Seg ((len Q1) + 1) ) by ;
per cases ( i + 1 in Seg (len Q1) or i + 1 in {((len Q1) + 1)} ) by ;
suppose A21: i + 1 in Seg (len Q1) ; :: thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i))
then i + 1 <= len B by ;
then i + 1 <= (len B) + 1 by NAT_1:12;
then A22: i <= len B by XREAL_1:6;
0 + 1 < i + 1 by ;
then 1 <= i by NAT_1:13;
then A23: i in dom B by ;
i + 1 <= len Q1 by ;
then i < len Q1 by NAT_1:13;
then A24: B /. (i + 1) = Firing ((Q1 /. (i + 1)),(B /. i)) by ;
i + 1 in dom Q1 by ;
then A25: Q1 /. (i + 1) = Q /. (i + 1) by ;
i + 1 in dom B by ;
then B /. (i + 1) = M /. (i + 1) by FINSEQ_4:68;
hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by ; :: 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 ;
A28: i + 1 = (len Q1) + 1 by ;
then ( M /. (i + 1) = M2 & Q /. (i + 1) = t ) by ;
hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
A29: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A29, A1);
hence ( ( Q = {} implies ex b1 being marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b1 = 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