let B1, B2 be marking of PTN; ( ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) & ( not Q = {} & 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)) ) ) & ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & B2 = 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)) ) ) implies B1 = B2 ) )
thus
( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 )
; ( not Q = {} & 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)) ) ) & ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & B2 = 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)) ) ) implies B1 = B2 )
assume
Q <> {}
; ( for M being FinSequence of nat_marks_of PTN holds
( not len Q = len M or not B1 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or for M being FinSequence of nat_marks_of PTN holds
( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 )
given M1 being FinSequence of nat_marks_of PTN such that A30:
len Q = len M1
and
A31:
B1 = M1 /. (len M1)
and
A32:
M1 /. 1 = Firing ((Q /. 1),M0)
and
A33:
for i being Nat st i < len Q & i > 0 holds
M1 /. (i + 1) = Firing ((Q /. (i + 1)),(M1 /. i))
; ( for M being FinSequence of nat_marks_of PTN holds
( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Nat st
( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 )
A34:
dom M1 = Seg (len Q)
by A30, FINSEQ_1:def 3;
given M2 being FinSequence of nat_marks_of PTN such that A35:
len Q = len M2
and
A36:
B2 = M2 /. (len M2)
and
A37:
M2 /. 1 = Firing ((Q /. 1),M0)
and
A38:
for i being Nat st i < len Q & i > 0 holds
M2 /. (i + 1) = Firing ((Q /. (i + 1)),(M2 /. i))
; B1 = B2
defpred S1[ Nat] means ( $1 in Seg (len Q) implies M1 /. $1 = M2 /. $1 );
A39:
now for j being Nat st S1[j] holds
S1[j + 1]let j be
Nat;
( S1[j] implies S1[j + 1] )assume A40:
S1[
j]
;
S1[j + 1]now ( j + 1 in Seg (len Q) implies M1 /. (j + 1) = M2 /. (j + 1) )assume A41:
j + 1
in Seg (len Q)
;
M1 /. (j + 1) = M2 /. (j + 1)per cases
( j = 0 or j <> 0 )
;
suppose A42:
j <> 0
;
M1 /. (j + 1) = M2 /. (j + 1)
(
j + 1
<= len Q &
j < j + 1 )
by A41, FINSEQ_1:1, XREAL_1:29;
then A44:
j < len Q
by XXREAL_0:2;
1
<= j
by A42, NAT_1:14;
then B2:
j in dom Q
by A44, FINSEQ_3:25;
thus M1 /. (j + 1) =
Firing (
(Q /. (j + 1)),
(M1 /. j))
by A33, A44, A42
.=
M2 /. (j + 1)
by A38, A44, A42, A40, FINSEQ_1:def 3, B2
;
verum end; end; end; hence
S1[
j + 1]
;
verum end;
A45:
S1[ 0 ]
by FINSEQ_1:1;
A46:
for j being Nat holds S1[j]
from NAT_1:sch 2(A45, A39);
hence
B1 = B2
by A30, A31, A35, A36, FINSEQ_2:9; verum