defpred S_{1}[ 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)) ) ) ) );

_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A29, A1);

hence ( ( Q = {} implies ex b_{1} being marking of PTN st b_{1} = M0 ) & ( not Q = {} implies ex b_{1} being marking of PTN ex M being FinSequence of nat_marks_of PTN st

( len Q = len M & b_{1} = 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

( ( 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_{1}[n] holds

S_{1}[n + 1]

A29:
SS

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

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

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

end;assume A2: S

thus S

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

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

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

end;

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

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

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

( 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

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

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

end;

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

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

for n being Nat holds S

hence ( ( Q = {} implies ex b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) ; :: thesis: verum