:: BOOLMARK semantic presentation

REAL is set

NAT is non empty V22() V23() V24() V35() V40() V41() Element of K32(REAL)

K32(REAL) is set

NAT is non empty V22() V23() V24() V35() V40() V41() set

K32(NAT) is V35() set

K32(NAT) is V35() set

BOOLEAN is non empty set

{} is set

the empty functional V21() V22() V23() V24() V26() V27() V28() V29() ext-real non positive non negative V35() V40() V42( {} ) FinSequence-membered V48() set is empty functional V21() V22() V23() V24() V26() V27() V28() V29() ext-real non positive non negative V35() V40() V42( {} ) FinSequence-membered V48() set

1 is non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() Element of NAT

2 is non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() Element of NAT

3 is non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() Element of NAT

0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

PTN is non empty set

Sd is non empty set

K33(PTN,Sd) is set

K32(K33(PTN,Sd)) is set

K32(PTN) is set

M0 is Relation-like PTN -defined Sd -valued Function-like quasi_total Element of K32(K33(PTN,Sd))

M0 is Element of K32(PTN)

t is Element of Sd

M0 --> t is Relation-like M0 -defined Sd -valued Function-like quasi_total Element of K32(K33(M0,Sd))

K33(M0,Sd) is set

K32(K33(M0,Sd)) is set

M0 +* (M0 --> t) is Relation-like Function-like set

dom M0 is set

rng M0 is set

rng (M0 --> t) is set

{t} is non empty V5() V42(1) Element of K32(Sd)

K32(Sd) is set

(rng M0) \/ (rng (M0 --> t)) is set

Sd \/ {t} is set

rng (M0 +* (M0 --> t)) is set

dom (M0 +* (M0 --> t)) is set

dom (M0 --> t) is set

(dom M0) \/ (dom (M0 --> t)) is set

[#] PTN is Element of K32(PTN)

([#] PTN) \/ M0 is Element of K32(PTN)

PTN is non empty set

K32(PTN) is set

Sd is non empty set

K33(PTN,Sd) is set

K32(K33(PTN,Sd)) is set

M0 is Element of K32(PTN)

M0 is Element of K32(PTN)

t is Relation-like PTN -defined Sd -valued Function-like quasi_total Element of K32(K33(PTN,Sd))

t .: M0 is set

t .: M0 is set

(t .: M0) /\ (t .: M0) is set

M0 /\ M0 is Element of K32(PTN)

Q is Element of PTN

t . Q is Element of Sd

PTN is set

Sd is set

M0 is Relation-like Function-like set

M0 .: Sd is set

M0 is set

PTN --> M0 is Relation-like PTN -defined {M0} -valued Function-like quasi_total Element of K32(K33(PTN,{M0}))

{M0} is non empty V5() V42(1) set

K33(PTN,{M0}) is set

K32(K33(PTN,{M0})) is set

M0 +* (PTN --> M0) is Relation-like Function-like set

(M0 +* (PTN --> M0)) .: Sd is set

PTN /\ Sd is set

dom (M0 +* (PTN --> M0)) is set

dom M0 is set

dom (PTN --> M0) is set

(dom M0) \/ (dom (PTN --> M0)) is set

t is set

t is set

Q is set

(M0 +* (PTN --> M0)) . Q is set

M0 . Q is set

t is set

t is set

Q is set

M0 . Q is set

(M0 +* (PTN --> M0)) . Q is set

t is set

Q is set

t is set

Q is set

PTN is PT_net_Str

the carrier of PTN is set

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

TRUE is boolean Element of BOOLEAN

{TRUE} is non empty V5() V42(1) Element of K32(BOOLEAN)

K32(BOOLEAN) is set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

Sd is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

M0 is Element of the carrier' of PTN

{M0} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

*' {M0} is Element of K32( the carrier of PTN)

K32( the carrier of PTN) is set

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

FALSE is boolean Element of BOOLEAN

(*' {M0}) --> FALSE is Relation-like *' {M0} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {M0}),BOOLEAN))

K33((*' {M0}),BOOLEAN) is set

K32(K33((*' {M0}),BOOLEAN)) is set

Sd +* ((*' {M0}) --> FALSE) is Relation-like Function-like set

{M0} *' is Element of K32( the carrier of PTN)

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

({M0} *') --> TRUE is Relation-like {M0} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({M0} *'),BOOLEAN))

K33(({M0} *'),BOOLEAN) is set

K32(K33(({M0} *'),BOOLEAN)) is set

(Sd +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE) is Relation-like Function-like set

K33( the carrier of PTN,BOOLEAN) is set

K32(K33( the carrier of PTN,BOOLEAN)) is set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

Sd is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 /. 1 is Element of the carrier' of PTN

(PTN,Sd,(M0 /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

*' {(M0 /. 1)} is Element of K32( the carrier of PTN)

K32( the carrier of PTN) is set

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

(*' {(M0 /. 1)}) --> FALSE is Relation-like *' {(M0 /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. 1)}),BOOLEAN))

K33((*' {(M0 /. 1)}),BOOLEAN) is set

K32(K33((*' {(M0 /. 1)}),BOOLEAN)) is set

Sd +* ((*' {(M0 /. 1)}) --> FALSE) is Relation-like Function-like set

{(M0 /. 1)} *' is Element of K32( the carrier of PTN)

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

({(M0 /. 1)} *') --> TRUE is Relation-like {(M0 /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. 1)} *'),BOOLEAN))

K33(({(M0 /. 1)} *'),BOOLEAN) is set

K32(K33(({(M0 /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {(M0 /. 1)}) --> FALSE)) +* (({(M0 /. 1)} *') --> TRUE) is Relation-like Function-like set

M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

t is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

len t is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

t /. 1 is Element of the carrier' of PTN

(PTN,Sd,(t /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(t /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(t /. 1)} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(t /. 1)}) --> FALSE is Relation-like *' {(t /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(t /. 1)}),BOOLEAN))

K33((*' {(t /. 1)}),BOOLEAN) is set

K32(K33((*' {(t /. 1)}),BOOLEAN)) is set

Sd +* ((*' {(t /. 1)}) --> FALSE) is Relation-like Function-like set

{(t /. 1)} *' is Element of K32( the carrier of PTN)

{ b

( b

({(t /. 1)} *') --> TRUE is Relation-like {(t /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(t /. 1)} *'),BOOLEAN))

K33(({(t /. 1)} *'),BOOLEAN) is set

K32(K33(({(t /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {(t /. 1)}) --> FALSE)) +* (({(t /. 1)} *') --> TRUE) is Relation-like Function-like set

Q is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

s is Element of the carrier' of PTN

<*s*> is non empty V5() Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

Q ^ <*s*> is non empty Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

len Q is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len Q) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(PTN,Sd,s) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{s} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {s} is Element of K32( the carrier of PTN)

{ b

( b

(*' {s}) --> FALSE is Relation-like *' {s} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {s}),BOOLEAN))

K33((*' {s}),BOOLEAN) is set

K32(K33((*' {s}),BOOLEAN)) is set

Sd +* ((*' {s}) --> FALSE) is Relation-like Function-like set

{s} *' is Element of K32( the carrier of PTN)

{ b

( b

({s} *') --> TRUE is Relation-like {s} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({s} *'),BOOLEAN))

K33(({s} *'),BOOLEAN) is set

K32(K33(({s} *'),BOOLEAN)) is set

(Sd +* ((*' {s}) --> FALSE)) +* (({s} *') --> TRUE) is Relation-like Function-like set

M3 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

<*M3*> is non empty V5() Relation-like NAT -defined (PTN) -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of (PTN)

j is non empty V5() Relation-like NAT -defined (PTN) -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of (PTN)

len j is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

j /. (len j) is Element of (PTN)

j /. 1 is Element of (PTN)

len <*s*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len Q) + (len <*s*>) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

0 + (len <*s*>) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

j is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

j + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

j /. (j + 1) is Element of (PTN)

j /. j is Element of (PTN)

t /. (j + 1) is Element of the carrier' of PTN

(PTN,(j /. j),(t /. (j + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(t /. (j + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(t /. (j + 1))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(t /. (j + 1))}) --> FALSE is Relation-like *' {(t /. (j + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(t /. (j + 1))}),BOOLEAN))

K33((*' {(t /. (j + 1))}),BOOLEAN) is set

K32(K33((*' {(t /. (j + 1))}),BOOLEAN)) is set

(j /. j) +* ((*' {(t /. (j + 1))}) --> FALSE) is Relation-like Function-like set

{(t /. (j + 1))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(t /. (j + 1))} *') --> TRUE is Relation-like {(t /. (j + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(t /. (j + 1))} *'),BOOLEAN))

K33(({(t /. (j + 1))} *'),BOOLEAN) is set

K32(K33(({(t /. (j + 1))} *'),BOOLEAN)) is set

((j /. j) +* ((*' {(t /. (j + 1))}) --> FALSE)) +* (({(t /. (j + 1))} *') --> TRUE) is Relation-like Function-like set

0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

dom Q is Element of K32(NAT)

len <*s*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len Q) + (len <*s*>) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. 1 is Element of the carrier' of PTN

(PTN,Sd,(Q /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(Q /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(Q /. 1)} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(Q /. 1)}) --> FALSE is Relation-like *' {(Q /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(Q /. 1)}),BOOLEAN))

K33((*' {(Q /. 1)}),BOOLEAN) is set

K32(K33((*' {(Q /. 1)}),BOOLEAN)) is set

Sd +* ((*' {(Q /. 1)}) --> FALSE) is Relation-like Function-like set

{(Q /. 1)} *' is Element of K32( the carrier of PTN)

{ b

( b

({(Q /. 1)} *') --> TRUE is Relation-like {(Q /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(Q /. 1)} *'),BOOLEAN))

K33(({(Q /. 1)} *'),BOOLEAN) is set

K32(K33(({(Q /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {(Q /. 1)}) --> FALSE)) +* (({(Q /. 1)} *') --> TRUE) is Relation-like Function-like set

j is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len j is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M3 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

j /. (len j) is Element of (PTN)

j /. 1 is Element of (PTN)

(PTN,M3,s) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{s} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {s} is Element of K32( the carrier of PTN)

{ b

( b

(*' {s}) --> FALSE is Relation-like *' {s} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {s}),BOOLEAN))

K33((*' {s}),BOOLEAN) is set

K32(K33((*' {s}),BOOLEAN)) is set

M3 +* ((*' {s}) --> FALSE) is Relation-like Function-like set

{s} *' is Element of K32( the carrier of PTN)

{ b

( b

({s} *') --> TRUE is Relation-like {s} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({s} *'),BOOLEAN))

K33(({s} *'),BOOLEAN) is set

K32(K33(({s} *'),BOOLEAN)) is set

(M3 +* ((*' {s}) --> FALSE)) +* (({s} *') --> TRUE) is Relation-like Function-like set

j is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

<*j*> is non empty V5() Relation-like NAT -defined (PTN) -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of (PTN)

j ^ <*j*> is non empty Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

M is non empty Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len M is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M /. (len M) is Element of (PTN)

M /. 1 is Element of (PTN)

len <*j*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len j) + (len <*j*>) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len j) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

dom j is Element of K32(NAT)

i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

i + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M /. (i + 1) is Element of (PTN)

M /. i is Element of (PTN)

t /. (i + 1) is Element of the carrier' of PTN

(PTN,(M /. i),(t /. (i + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(t /. (i + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(t /. (i + 1))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(t /. (i + 1))}) --> FALSE is Relation-like *' {(t /. (i + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(t /. (i + 1))}),BOOLEAN))

K33((*' {(t /. (i + 1))}),BOOLEAN) is set

K32(K33((*' {(t /. (i + 1))}),BOOLEAN)) is set

(M /. i) +* ((*' {(t /. (i + 1))}) --> FALSE) is Relation-like Function-like set

{(t /. (i + 1))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(t /. (i + 1))} *') --> TRUE is Relation-like {(t /. (i + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(t /. (i + 1))} *'),BOOLEAN))

K33(({(t /. (i + 1))} *'),BOOLEAN) is set

K32(K33(({(t /. (i + 1))} *'),BOOLEAN)) is set

((M /. i) +* ((*' {(t /. (i + 1))}) --> FALSE)) +* (({(t /. (i + 1))} *') --> TRUE) is Relation-like Function-like set

Seg ((len Q) + 1) is V35() V42((len Q) + 1) Element of K32(NAT)

Seg (len Q) is V35() V42( len Q) Element of K32(NAT)

{((len Q) + 1)} is non empty V5() V42(1) Element of K32(NAT)

(Seg (len Q)) \/ {((len Q) + 1)} is Element of K32(NAT)

j /. (i + 1) is Element of (PTN)

j /. i is Element of (PTN)

Q /. (i + 1) is Element of the carrier' of PTN

(PTN,(j /. i),(Q /. (i + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(Q /. (i + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(Q /. (i + 1))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(Q /. (i + 1))}) --> FALSE is Relation-like *' {(Q /. (i + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(Q /. (i + 1))}),BOOLEAN))

K33((*' {(Q /. (i + 1))}),BOOLEAN) is set

K32(K33((*' {(Q /. (i + 1))}),BOOLEAN)) is set

(j /. i) +* ((*' {(Q /. (i + 1))}) --> FALSE) is Relation-like Function-like set

{(Q /. (i + 1))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(Q /. (i + 1))} *') --> TRUE is Relation-like {(Q /. (i + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(Q /. (i + 1))} *'),BOOLEAN))

K33(({(Q /. (i + 1))} *'),BOOLEAN) is set

K32(K33(({(Q /. (i + 1))} *'),BOOLEAN)) is set

((j /. i) +* ((*' {(Q /. (i + 1))}) --> FALSE)) +* (({(Q /. (i + 1))} *') --> TRUE) is Relation-like Function-like set

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 /. 1 is Element of the carrier' of PTN

(PTN,Sd,(M0 /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(M0 /. 1)} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(M0 /. 1)}) --> FALSE is Relation-like *' {(M0 /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. 1)}),BOOLEAN))

K33((*' {(M0 /. 1)}),BOOLEAN) is set

K32(K33((*' {(M0 /. 1)}),BOOLEAN)) is set

Sd +* ((*' {(M0 /. 1)}) --> FALSE) is Relation-like Function-like set

{(M0 /. 1)} *' is Element of K32( the carrier of PTN)

{ b

( b

({(M0 /. 1)} *') --> TRUE is Relation-like {(M0 /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. 1)} *'),BOOLEAN))

K33(({(M0 /. 1)} *'),BOOLEAN) is set

K32(K33(({(M0 /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {(M0 /. 1)}) --> FALSE)) +* (({(M0 /. 1)} *') --> TRUE) is Relation-like Function-like set

M0 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

t is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

Q is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len Q is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (len Q) is Element of (PTN)

Q /. 1 is Element of (PTN)

dom Q is Element of K32(NAT)

Seg (len M0) is V35() V42( len M0) Element of K32(NAT)

s is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len s is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

s /. (len s) is Element of (PTN)

s /. 1 is Element of (PTN)

M3 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. M3 is Element of (PTN)

s /. M3 is Element of (PTN)

M3 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (M3 + 1) is Element of (PTN)

s /. (M3 + 1) is Element of (PTN)

Q /. (M3 + 1) is Element of (PTN)

M0 /. (M3 + 1) is Element of the carrier' of PTN

(PTN,(s /. M3),(M0 /. (M3 + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. (M3 + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(M0 /. (M3 + 1))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(M0 /. (M3 + 1))}) --> FALSE is Relation-like *' {(M0 /. (M3 + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (M3 + 1))}),BOOLEAN))

K33((*' {(M0 /. (M3 + 1))}),BOOLEAN) is set

K32(K33((*' {(M0 /. (M3 + 1))}),BOOLEAN)) is set

(s /. M3) +* ((*' {(M0 /. (M3 + 1))}) --> FALSE) is Relation-like Function-like set

{(M0 /. (M3 + 1))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(M0 /. (M3 + 1))} *') --> TRUE is Relation-like {(M0 /. (M3 + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (M3 + 1))} *'),BOOLEAN))

K33(({(M0 /. (M3 + 1))} *'),BOOLEAN) is set

K32(K33(({(M0 /. (M3 + 1))} *'),BOOLEAN)) is set

((s /. M3) +* ((*' {(M0 /. (M3 + 1))}) --> FALSE)) +* (({(M0 /. (M3 + 1))} *') --> TRUE) is Relation-like Function-like set

s /. (M3 + 1) is Element of (PTN)

Q /. (M3 + 1) is Element of (PTN)

s /. (M3 + 1) is Element of (PTN)

Q /. (M3 + 1) is Element of (PTN)

s /. (M3 + 1) is Element of (PTN)

Q /. 0 is Element of (PTN)

s /. 0 is Element of (PTN)

M3 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() set

dom s is Element of K32(NAT)

Q . M3 is set

Q /. M3 is Element of (PTN)

s /. M3 is Element of (PTN)

s . M3 is set

PTN is non empty set

Sd is set

PTN --> Sd is Relation-like PTN -defined {Sd} -valued Function-like quasi_total Element of K32(K33(PTN,{Sd}))

{Sd} is non empty V5() V42(1) set

K33(PTN,{Sd}) is set

K32(K33(PTN,{Sd})) is set

M0 is Relation-like Function-like set

M0 +* (PTN --> Sd) is Relation-like Function-like set

(M0 +* (PTN --> Sd)) .: PTN is set

M0 is set

dom (M0 +* (PTN --> Sd)) is set

t is set

(M0 +* (PTN --> Sd)) . t is set

dom (PTN --> Sd) is set

(PTN --> Sd) . t is set

t is set

dom (PTN --> Sd) is set

dom (M0 +* (PTN --> Sd)) is set

(PTN --> Sd) . t is set

(M0 +* (PTN --> Sd)) . t is set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

Sd is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

M0 is Element of the carrier' of PTN

{M0} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

{M0} *' is Element of K32( the carrier of PTN)

K32( the carrier of PTN) is set

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

(PTN,Sd,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

*' {M0} is Element of K32( the carrier of PTN)

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

(*' {M0}) --> FALSE is Relation-like *' {M0} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {M0}),BOOLEAN))

K33((*' {M0}),BOOLEAN) is set

K32(K33((*' {M0}),BOOLEAN)) is set

Sd +* ((*' {M0}) --> FALSE) is Relation-like Function-like set

({M0} *') --> TRUE is Relation-like {M0} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({M0} *'),BOOLEAN))

K33(({M0} *'),BOOLEAN) is set

K32(K33(({M0} *'),BOOLEAN)) is set

(Sd +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE) is Relation-like Function-like set

M0 is Element of the carrier of PTN

(PTN,Sd,M0) . M0 is boolean Element of BOOLEAN

[#] the carrier of PTN is Element of K32( the carrier of PTN)

dom Sd is set

dom ((*' {M0}) --> FALSE) is set

dom (({M0} *') --> TRUE) is set

dom ((Sd +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE)) is set

dom (Sd +* ((*' {M0}) --> FALSE)) is set

(dom (Sd +* ((*' {M0}) --> FALSE))) \/ ({M0} *') is set

the carrier of PTN \/ (*' {M0}) is set

( the carrier of PTN \/ (*' {M0})) \/ ({M0} *') is set

(*' {M0}) \/ ({M0} *') is Element of K32( the carrier of PTN)

the carrier of PTN \/ ((*' {M0}) \/ ({M0} *')) is set

((Sd +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE)) .: ({M0} *') is set

((Sd +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE)) . M0 is set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

K32( the carrier of PTN) is set

the carrier of PTN --> TRUE is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33( the carrier of PTN,BOOLEAN))

K33( the carrier of PTN,BOOLEAN) is set

K32(K33( the carrier of PTN,BOOLEAN)) is set

Sd is non empty Element of K32( the carrier of PTN)

Sd --> FALSE is Relation-like Sd -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(Sd,BOOLEAN))

K33(Sd,BOOLEAN) is set

K32(K33(Sd,BOOLEAN)) is set

( the carrier of PTN --> TRUE) +* (Sd --> FALSE) is Relation-like Function-like set

[#] the carrier of PTN is Element of K32( the carrier of PTN)

dom ( the carrier of PTN --> TRUE) is set

dom (Sd --> FALSE) is set

dom (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) is set

the carrier of PTN \/ Sd is set

rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) is set

rng ( the carrier of PTN --> TRUE) is set

rng (Sd --> FALSE) is set

(rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) is set

{FALSE} is non empty V5() V42(1) Element of K32(BOOLEAN)

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

*' Sd is Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

Sd *' is Element of K32( the carrier' of PTN)

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

t is Element of the carrier' of PTN

{t} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

{t} *' is Element of K32( the carrier of PTN)

{ b

( b

({t} *') /\ Sd is Element of K32( the carrier of PTN)

Q is set

M0 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,M0,t) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

*' {t} is Element of K32( the carrier of PTN)

{ b

( b

(*' {t}) --> FALSE is Relation-like *' {t} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {t}),BOOLEAN))

K33((*' {t}),BOOLEAN) is set

K32(K33((*' {t}),BOOLEAN)) is set

M0 +* ((*' {t}) --> FALSE) is Relation-like Function-like set

({t} *') --> TRUE is Relation-like {t} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({t} *'),BOOLEAN))

K33(({t} *'),BOOLEAN) is set

K32(K33(({t} *'),BOOLEAN)) is set

(M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Relation-like Function-like set

(PTN,M0,t) . Q is set

(PTN,M0,t) .: Sd is set

( the carrier of PTN --> TRUE) .: (*' {t}) is set

M0 .: (*' {t}) is set

M0 .: Sd is set

{FALSE} is non empty V5() V42(1) set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

K32( the carrier of PTN) is set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

Sd is non empty Element of K32( the carrier of PTN)

*' Sd is Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

Sd *' is Element of K32( the carrier' of PTN)

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

K32((Sd *')) is set

M0 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

M0 .: Sd is set

M0 is Element of the carrier' of PTN

(PTN,M0,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{M0} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {M0} is Element of K32( the carrier of PTN)

{ b

( b

(*' {M0}) --> FALSE is Relation-like *' {M0} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {M0}),BOOLEAN))

K33((*' {M0}),BOOLEAN) is set

K32(K33((*' {M0}),BOOLEAN)) is set

M0 +* ((*' {M0}) --> FALSE) is Relation-like Function-like set

{M0} *' is Element of K32( the carrier of PTN)

{ b

( b

({M0} *') --> TRUE is Relation-like {M0} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({M0} *'),BOOLEAN))

K33(({M0} *'),BOOLEAN) is set

K32(K33(({M0} *'),BOOLEAN)) is set

(M0 +* ((*' {M0}) --> FALSE)) +* (({M0} *') --> TRUE) is Relation-like Function-like set

(PTN,M0,M0) .: Sd is set

M0 .: (*' {M0}) is set

(M0 +* ((*' {M0}) --> FALSE)) .: Sd is set

PTN is non empty set

Sd is Relation-like NAT -defined PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of PTN

len Sd is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 is Relation-like NAT -defined PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of PTN

Sd ^ M0 is Relation-like NAT -defined PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of PTN

M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(Sd ^ M0) /. M0 is Element of PTN

Sd /. M0 is Element of PTN

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len Sd) + (len M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

dom Sd is Element of K32(NAT)

Seg (len Sd) is V35() V42( len Sd) Element of K32(NAT)

len (Sd ^ M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

dom (Sd ^ M0) is Element of K32(NAT)

Sd . M0 is set

(Sd ^ M0) . M0 is set

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

Sd is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

M0 ^ M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

(PTN,Sd,(M0 ^ M0)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,Sd,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,(PTN,Sd,M0),M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,Sd,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,Sd,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 /. 1 is Element of the carrier' of PTN

(PTN,Sd,(M0 /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

*' {(M0 /. 1)} is Element of K32( the carrier of PTN)

K32( the carrier of PTN) is set

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

(*' {(M0 /. 1)}) --> FALSE is Relation-like *' {(M0 /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. 1)}),BOOLEAN))

K33((*' {(M0 /. 1)}),BOOLEAN) is set

K32(K33((*' {(M0 /. 1)}),BOOLEAN)) is set

Sd +* ((*' {(M0 /. 1)}) --> FALSE) is Relation-like Function-like set

{(M0 /. 1)} *' is Element of K32( the carrier of PTN)

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

({(M0 /. 1)} *') --> TRUE is Relation-like {(M0 /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. 1)} *'),BOOLEAN))

K33(({(M0 /. 1)} *'),BOOLEAN) is set

K32(K33(({(M0 /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {(M0 /. 1)}) --> FALSE)) +* (({(M0 /. 1)} *') --> TRUE) is Relation-like Function-like set

t is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len t is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

t /. (len t) is Element of (PTN)

t /. 1 is Element of (PTN)

len (M0 ^ M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(M0 ^ M0) /. 1 is Element of the carrier' of PTN

(PTN,Sd,((M0 ^ M0) /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{((M0 ^ M0) /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {((M0 ^ M0) /. 1)} is Element of K32( the carrier of PTN)

{ b

( b

(*' {((M0 ^ M0) /. 1)}) --> FALSE is Relation-like *' {((M0 ^ M0) /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {((M0 ^ M0) /. 1)}),BOOLEAN))

K33((*' {((M0 ^ M0) /. 1)}),BOOLEAN) is set

K32(K33((*' {((M0 ^ M0) /. 1)}),BOOLEAN)) is set

Sd +* ((*' {((M0 ^ M0) /. 1)}) --> FALSE) is Relation-like Function-like set

{((M0 ^ M0) /. 1)} *' is Element of K32( the carrier of PTN)

{ b

( b

({((M0 ^ M0) /. 1)} *') --> TRUE is Relation-like {((M0 ^ M0) /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({((M0 ^ M0) /. 1)} *'),BOOLEAN))

K33(({((M0 ^ M0) /. 1)} *'),BOOLEAN) is set

K32(K33(({((M0 ^ M0) /. 1)} *'),BOOLEAN)) is set

(Sd +* ((*' {((M0 ^ M0) /. 1)}) --> FALSE)) +* (({((M0 ^ M0) /. 1)} *') --> TRUE) is Relation-like Function-like set

Q is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len Q is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (len Q) is Element of (PTN)

Q /. 1 is Element of (PTN)

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len M0) + (len M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

0 + (len M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

s is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + s is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (1 + s) is Element of (PTN)

t /. (1 + s) is Element of (PTN)

s + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + (s + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(M0 ^ M0) /. (1 + (s + 1)) is Element of the carrier' of PTN

M0 /. (1 + (s + 1)) is Element of the carrier' of PTN

Q /. (1 + (s + 1)) is Element of (PTN)

(PTN,(t /. (1 + s)),(M0 /. (1 + (s + 1)))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. (1 + (s + 1)))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(M0 /. (1 + (s + 1)))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(M0 /. (1 + (s + 1)))}) --> FALSE is Relation-like *' {(M0 /. (1 + (s + 1)))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (1 + (s + 1)))}),BOOLEAN))

K33((*' {(M0 /. (1 + (s + 1)))}),BOOLEAN) is set

K32(K33((*' {(M0 /. (1 + (s + 1)))}),BOOLEAN)) is set

(t /. (1 + s)) +* ((*' {(M0 /. (1 + (s + 1)))}) --> FALSE) is Relation-like Function-like set

{(M0 /. (1 + (s + 1)))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(M0 /. (1 + (s + 1)))} *') --> TRUE is Relation-like {(M0 /. (1 + (s + 1)))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (1 + (s + 1)))} *'),BOOLEAN))

K33(({(M0 /. (1 + (s + 1)))} *'),BOOLEAN) is set

K32(K33(({(M0 /. (1 + (s + 1)))} *'),BOOLEAN)) is set

((t /. (1 + s)) +* ((*' {(M0 /. (1 + (s + 1)))}) --> FALSE)) +* (({(M0 /. (1 + (s + 1)))} *') --> TRUE) is Relation-like Function-like set

t /. (1 + (s + 1)) is Element of (PTN)

(len M0) - 1 is V21() V29() ext-real set

0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 /. 1 is Element of the carrier' of PTN

(PTN,(PTN,Sd,M0),(M0 /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(M0 /. 1)} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(M0 /. 1)}) --> FALSE is Relation-like *' {(M0 /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. 1)}),BOOLEAN))

K33((*' {(M0 /. 1)}),BOOLEAN) is set

K32(K33((*' {(M0 /. 1)}),BOOLEAN)) is set

(PTN,Sd,M0) +* ((*' {(M0 /. 1)}) --> FALSE) is Relation-like Function-like set

{(M0 /. 1)} *' is Element of K32( the carrier of PTN)

{ b

( b

({(M0 /. 1)} *') --> TRUE is Relation-like {(M0 /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. 1)} *'),BOOLEAN))

K33(({(M0 /. 1)} *'),BOOLEAN) is set

K32(K33(({(M0 /. 1)} *'),BOOLEAN)) is set

((PTN,Sd,M0) +* ((*' {(M0 /. 1)}) --> FALSE)) +* (({(M0 /. 1)} *') --> TRUE) is Relation-like Function-like set

j is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)

len j is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

j /. (len j) is Element of (PTN)

j /. 1 is Element of (PTN)

j is V21() V22() V23() V24() V28() V29() ext-real V35() V40() set

j + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + 0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (1 + 0) is Element of (PTN)

t /. (1 + 0) is Element of (PTN)

(len M0) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

((len M0) + 1) + M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (((len M0) + 1) + M) is Element of (PTN)

j /. (1 + M) is Element of (PTN)

M + (len M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(((len M0) + 1) + M) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

((len M0) + 1) + (M + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len M0) + M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

((len M0) + M) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + (M + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len M0) + (1 + (M + 1)) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(M0 ^ M0) /. ((len M0) + (1 + (M + 1))) is Element of the carrier' of PTN

M0 /. (1 + (M + 1)) is Element of the carrier' of PTN

(len M0) + (1 + M) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (((len M0) + 1) + (M + 1)) is Element of (PTN)

(PTN,(j /. (1 + M)),(M0 /. (1 + (M + 1)))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. (1 + (M + 1)))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {(M0 /. (1 + (M + 1)))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {(M0 /. (1 + (M + 1)))}) --> FALSE is Relation-like *' {(M0 /. (1 + (M + 1)))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (1 + (M + 1)))}),BOOLEAN))

K33((*' {(M0 /. (1 + (M + 1)))}),BOOLEAN) is set

K32(K33((*' {(M0 /. (1 + (M + 1)))}),BOOLEAN)) is set

(j /. (1 + M)) +* ((*' {(M0 /. (1 + (M + 1)))}) --> FALSE) is Relation-like Function-like set

{(M0 /. (1 + (M + 1)))} *' is Element of K32( the carrier of PTN)

{ b

( b

({(M0 /. (1 + (M + 1)))} *') --> TRUE is Relation-like {(M0 /. (1 + (M + 1)))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (1 + (M + 1)))} *'),BOOLEAN))

K33(({(M0 /. (1 + (M + 1)))} *'),BOOLEAN) is set

K32(K33(({(M0 /. (1 + (M + 1)))} *'),BOOLEAN)) is set

((j /. (1 + M)) +* ((*' {(M0 /. (1 + (M + 1)))}) --> FALSE)) +* (({(M0 /. (1 + (M + 1)))} *') --> TRUE) is Relation-like Function-like set

j /. (1 + (M + 1)) is Element of (PTN)

((len M0) + 1) + 0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (((len M0) + 1) + 0) is Element of (PTN)

s is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + s is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (1 + s) is Element of (PTN)

(M0 ^ M0) /. ((len M0) + 1) is Element of the carrier' of PTN

(PTN,(Q /. (1 + s)),((M0 ^ M0) /. ((len M0) + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{((M0 ^ M0) /. ((len M0) + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

*' {((M0 ^ M0) /. ((len M0) + 1))} is Element of K32( the carrier of PTN)

{ b

( b

(*' {((M0 ^ M0) /. ((len M0) + 1))}) --> FALSE is Relation-like *' {((M0 ^ M0) /. ((len M0) + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {((M0 ^ M0) /. ((len M0) + 1))}),BOOLEAN))

K33((*' {((M0 ^ M0) /. ((len M0) + 1))}),BOOLEAN) is set

K32(K33((*' {((M0 ^ M0) /. ((len M0) + 1))}),BOOLEAN)) is set

(Q /. (1 + s)) +* ((*' {((M0 ^ M0) /. ((len M0) + 1))}) --> FALSE) is Relation-like Function-like set

{((M0 ^ M0) /. ((len M0) + 1))} *' is Element of K32( the carrier of PTN)

{ b

( b

({((M0 ^ M0) /. ((len M0) + 1))} *') --> TRUE is Relation-like {((M0 ^ M0) /. ((len M0) + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({((M0 ^ M0) /. ((len M0) + 1))} *'),BOOLEAN))

K33(({((M0 ^ M0) /. ((len M0) + 1))} *'),BOOLEAN) is set

K32(K33(({((M0 ^ M0) /. ((len M0) + 1))} *'),BOOLEAN)) is set

((Q /. (1 + s)) +* ((*' {((M0 ^ M0) /. ((len M0) + 1))}) --> FALSE)) +* (({((M0 ^ M0) /. ((len M0) + 1))} *') --> TRUE) is Relation-like Function-like set

(PTN,(PTN,Sd,M0),((M0 ^ M0) /. ((len M0) + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,Sd,M0) +* ((*' {((M0 ^ M0) /. ((len M0) + 1))}) --> FALSE) is Relation-like Function-like set

((PTN,Sd,M0) +* ((*' {((M0 ^ M0) /. ((len M0) + 1))}) --> FALSE)) +* (({((M0 ^ M0) /. ((len M0) + 1))} *') --> TRUE) is Relation-like Function-like set

j /. (1 + 0) is Element of (PTN)

M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

1 + M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len M0) + (1 + M) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. ((len M0) + (1 + M)) is Element of (PTN)

((len M0) + 1) + M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

Q /. (((len M0) + 1) + M) is Element of (PTN)

PTN is non empty non void V70() with_S-T_arc with_T-S_arc PT_net_Str

the carrier of PTN is non empty set

(PTN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

Funcs ( the carrier of PTN,BOOLEAN) is non empty FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN

the carrier' of PTN is non empty set

Sd is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

M0 ^ M0 is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN

(PTN,Sd,M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

M0 /. 1 is Element of the carrier' of PTN

len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(len M0) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT

(M0 ^ M0) /. ((len M0) + 1) is Element of the carrier' of PTN

(len M0) - 1 is V21() V29() ext-real set

(PTN,(PTN,Sd,M0),M0) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

(PTN,(PTN,Sd,M0),(M0 /. 1)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)

{(M0 /. 1)} is non empty V5() V42(1) Element of K32( the carrier' of PTN)

K32( the carrier' of PTN) is set

*' {(M0 /. 1)} is Element of K32( the carrier of PTN)

K32( the carrier of PTN) is set

the S-T_Arcs of PTN is Relation-like the carrier of PTN -defined the carrier' of PTN -valued Element of K32(K33( the carrier of PTN, the carrier' of PTN))

K33( the carrier of PTN, the carrier' of PTN) is set

K32(K33( the carrier of PTN, the carrier' of PTN)) is set

{ b

( b

(*' {(M0 /. 1)}) --> FALSE is Relation-like *' {(M0 /. 1)} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. 1)}),BOOLEAN))

K33((*' {(M0 /. 1)}),BOOLEAN) is set

K32(K33((*' {(M0 /. 1)}),BOOLEAN)) is set

(PTN,Sd,M0) +* ((*' {(M0 /. 1)}) --> FALSE) is Relation-like Function-like set

{(M0 /. 1)} *' is Element of K32( the carrier of PTN)

the T-S_Arcs of PTN is Relation-like the carrier' of PTN -defined the carrier of PTN -valued Element of K32(K33( the carrier' of PTN, the carrier of PTN))

K33( the carrier' of PTN, the carrier of PTN) is set

K32(K33( the carrier' of PTN, the carrier of PTN)) is set

{ b

( b

({(M0 /. 1)} *') --> TRUE is Relation-like {(M0 /. 1)} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. 1)} *'),BOOLEAN))

K33(({(M0 /. 1)} *'),BOOLEAN) is set

K32(K33((