let B1, B2 be marking of PTN; :: thesis: ( ( 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 ) ; :: thesis: ( 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 <> {} ; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: B1 = B2

defpred S_{1}[ Nat] means ( $1 in Seg (len Q) implies M1 /. $1 = M2 /. $1 );

_{1}[ 0 ]
by FINSEQ_1:1;

A46: for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A45, A39);

( 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 ) ; :: thesis: ( 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 <> {} ; :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: B1 = B2

defpred S

A39: now :: thesis: for j being Nat st S_{1}[j] holds

S_{1}[j + 1]

A45:
SS

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

assume A40: S_{1}[j]
; :: thesis: S_{1}[j + 1]

_{1}[j + 1]
; :: thesis: verum

end;assume A40: S

now :: thesis: ( j + 1 in Seg (len Q) implies M1 /. (j + 1) = M2 /. (j + 1) )

hence
Sassume A41:
j + 1 in Seg (len Q)
; :: thesis: M1 /. (j + 1) = M2 /. (j + 1)

end;per cases
( j = 0 or j <> 0 )
;

end;

suppose A42:
j <> 0
; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum

A46: for j being Nat holds S

now :: thesis: for j being Nat st j in dom M1 holds

M1 . j = M2 . j

hence
B1 = B2
by A30, A31, A35, A36, FINSEQ_2:9; :: thesis: verumM1 . j = M2 . j

let j be Nat; :: thesis: ( j in dom M1 implies M1 . j = M2 . j )

assume A47: j in dom M1 ; :: thesis: M1 . j = M2 . j

then A48: j in dom M2 by A35, A34, FINSEQ_1:def 3;

thus M1 . j = M1 /. j by A47, PARTFUN1:def 6

.= M2 /. j by A46, A34, A47

.= M2 . j by A48, PARTFUN1:def 6 ; :: thesis: verum

end;assume A47: j in dom M1 ; :: thesis: M1 . j = M2 . j

then A48: j in dom M2 by A35, A34, FINSEQ_1:def 3;

thus M1 . j = M1 /. j by A47, PARTFUN1:def 6

.= M2 /. j by A46, A34, A47

.= M2 . j by A48, PARTFUN1:def 6 ; :: thesis: verum