environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XXREAL_0, CARD_1, FINSEQ_1, RELAT_1, TARSKI, XBOOLE_0, NAT_1, ARYTM_3, FUNCT_1, FUNCOP_1, ARYTM_1, PETRI, NET_1, MCART_1, FUNCT_2, FUNCT_7, PARTFUN1, ORDINAL4, VALUED_1, PNPROC_1;
notations HIDDEN, TARSKI, XBOOLE_0, DOMAIN_1, XTUPLE_0, RELAT_1, FUNCT_1, SUBSET_1, PARTFUN1, CARD_1, FINSEQ_1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, MCART_1, FINSEQ_2, FUNCT_7, INT_1, XXREAL_0, PRE_POLY, VALUED_1;
definitions TARSKI, XBOOLE_0, FUNCOP_1;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, RELSET_1, FUNCOP_1, XBOOLE_1, RELAT_1, INT_1, FINSEQ_1, FUNCT_7, XBOOLE_0, TREES_2, FINSEQ_3, ENUMSET1, ZFMISC_1, GRFUNC_1, GRAPH_2, FINSEQ_6, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_1, XTUPLE_0;
schemes NAT_1, FUNCT_1, FINSEQ_1, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, FUNCT_7, GRAPH_2, VALUED_0, VALUED_1, FUNCT_2, MEMBERED, CARD_1, NAT_1, XTUPLE_0;
constructors HIDDEN, WELLORD2, DOMAIN_1, REAL_1, FUNCT_7, NAT_D, RELSET_1, PRE_POLY, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
equalities TARSKI;
expansions TARSKI, XBOOLE_0;
Lm1:
for P, p being set st p in P holds
({$} P) . p = 0
by FUNCOP_1:7;
theorem Th2:
for
P being
set for
m1,
m2,
m3 being
marking of
P st
m1 c= m2 &
m2 c= m3 holds
m1 c= m3
theorem Th4:
for
P being
set for
m1,
m2 being
marking of
P holds
m1 c= m1 + m2
theorem
for
P being
set for
m1,
m2,
m3 being
marking of
P st
m1 c= m2 &
m2 c= m3 holds
m3 - m2 c= m3 - m1
theorem Th7:
for
P being
set for
m1,
m2 being
marking of
P holds
(m1 + m2) - m2 = m1
theorem Th8:
for
P being
set for
m1,
m2,
m being
marking of
P st
m c= m1 &
m1 c= m2 holds
m1 - m c= m2 - m
theorem Th9:
for
P being
set for
m1,
m2,
m3 being
marking of
P st
m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3
theorem
for
P being
set for
m1,
m2 being
marking of
P st
m1 c= m2 &
m2 c= m1 holds
m1 = m2
theorem Th11:
for
P being
set for
m1,
m2,
m3 being
marking of
P holds
(m1 + m2) + m3 = m1 + (m2 + m3)
theorem
for
P being
set for
m1,
m2,
m3,
m4 being
marking of
P st
m1 c= m2 &
m3 c= m4 holds
m1 + m3 c= m2 + m4
theorem
for
P being
set for
m1,
m2 being
marking of
P st
m1 c= m2 holds
m2 - m1 c= m2
theorem Th14:
for
P being
set for
m1,
m2,
m3,
m4 being
marking of
P st
m1 c= m2 &
m3 c= m4 &
m4 c= m1 holds
m1 - m4 c= m2 - m3
theorem Th15:
for
P being
set for
m1,
m2 being
marking of
P st
m1 c= m2 holds
m2 = (m2 - m1) + m1
theorem Th16:
for
P being
set for
m1,
m2 being
marking of
P holds
(m1 + m2) - m1 = m2
theorem Th17:
for
P being
set for
m1,
m2,
m3 being
marking of
P st
m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)
theorem
for
P being
set for
m1,
m2,
m3 being
marking of
P st
m3 c= m2 &
m2 c= m1 holds
m1 - (m2 - m3) = (m1 - m2) + m3
theorem
for
P being
set for
N being
Petri_net of
P for
e,
e1,
e2 being
Element of
N holds
{<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
Lm2:
for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
Lm3:
for p1 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 holds
q1 misses (len p1) Shift q2
by VALUED_1:50, XBOOLE_1:63;