:: 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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₃,b₁] ) } is 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
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {s} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {s} & b₂ = [b₃,b₁] ) } is set
({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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. (j + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. (j + 1))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(Q /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(Q /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {s} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {s} & b₂ = [b₃,b₁] ) } is set
({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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. (i + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(t /. (i + 1))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(Q /. (i + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(Q /. (i + 1))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (M3 + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (M3 + 1))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₃,b₁] ) } is set
(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₃,b₁] ) } is set
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
({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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₃,b₁] ) } is set
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₃,b₁] ) } is 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
(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. 1)} & b₂ = [b₃,b₁] ) } is set
({((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (s + 1)))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (s + 1)))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (M + 1)))} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (M + 1)))} & b₂ = [b₃,b₁] ) } is set
({(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. ((len M0) + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. ((len M0) + 1))} & b₂ = [b₃,b₁] ) } is set
({((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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
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)
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. 1)} & b₂ = [b₃,b₁] ) } is set
({(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
M3 is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)
len M3 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M3 /. (len M3) is Element of (PTN)
M3 /. 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
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. 1)} & b₂ = [b₃,b₁] ) } is set
({((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
M is Relation-like NAT -defined (PTN) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (PTN)
len M is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. 1 is Element of (PTN)
(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
i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
1 + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (1 + i) is Element of (PTN)
M3 /. (1 + i) is Element of (PTN)
i + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
1 + (i + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(M0 ^ M0) /. (1 + (i + 1)) is Element of the carrier' of PTN
M0 /. (1 + (i + 1)) is Element of the carrier' of PTN
M /. (1 + (i + 1)) is Element of (PTN)
(PTN,(M3 /. (1 + i)),(M0 /. (1 + (i + 1)))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(M0 /. (1 + (i + 1)))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(M0 /. (1 + (i + 1)))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (i + 1)))} & b₂ = [b₁,b₃] ) } is set
(*' {(M0 /. (1 + (i + 1)))}) --> FALSE is Relation-like *' {(M0 /. (1 + (i + 1)))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN))
K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN) is set
K32(K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN)) is set
(M3 /. (1 + i)) +* ((*' {(M0 /. (1 + (i + 1)))}) --> FALSE) is Relation-like Function-like set
{(M0 /. (1 + (i + 1)))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (i + 1)))} & b₂ = [b₃,b₁] ) } is set
({(M0 /. (1 + (i + 1)))} *') --> TRUE is Relation-like {(M0 /. (1 + (i + 1)))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN))
K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN) is set
K32(K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN)) is set
((M3 /. (1 + i)) +* ((*' {(M0 /. (1 + (i + 1)))}) --> FALSE)) +* (({(M0 /. (1 + (i + 1)))} *') --> TRUE) is Relation-like Function-like set
M3 /. (1 + (i + 1)) is Element of (PTN)
1 + 0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (1 + 0) is Element of (PTN)
M3 /. (1 + 0) is Element of (PTN)
i 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() set
j + 1 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
dom M0 is Element of K32(NAT)
(M0 ^ M0) /. (i + 1) is Element of the carrier' of PTN
M0 /. (i + 1) is Element of the carrier' of PTN
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
M /. i is Element of (PTN)
M3 /. i is Element of (PTN)
M /. (i + 1) is Element of (PTN)
(PTN,(M /. i),((M0 ^ M0) /. (i + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{((M0 ^ M0) /. (i + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {((M0 ^ M0) /. (i + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. (i + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {((M0 ^ M0) /. (i + 1))}) --> FALSE is Relation-like *' {((M0 ^ M0) /. (i + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {((M0 ^ M0) /. (i + 1))}),BOOLEAN))
K33((*' {((M0 ^ M0) /. (i + 1))}),BOOLEAN) is set
K32(K33((*' {((M0 ^ M0) /. (i + 1))}),BOOLEAN)) is set
(M /. i) +* ((*' {((M0 ^ M0) /. (i + 1))}) --> FALSE) is Relation-like Function-like set
{((M0 ^ M0) /. (i + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. (i + 1))} & b₂ = [b₃,b₁] ) } is set
({((M0 ^ M0) /. (i + 1))} *') --> TRUE is Relation-like {((M0 ^ M0) /. (i + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({((M0 ^ M0) /. (i + 1))} *'),BOOLEAN))
K33(({((M0 ^ M0) /. (i + 1))} *'),BOOLEAN) is set
K32(K33(({((M0 ^ M0) /. (i + 1))} *'),BOOLEAN)) is set
((M /. i) +* ((*' {((M0 ^ M0) /. (i + 1))}) --> FALSE)) +* (({((M0 ^ M0) /. (i + 1))} *') --> TRUE) is Relation-like Function-like set
M3 /. (i + 1) is Element of (PTN)
(PTN,(M3 /. i),(M0 /. (i + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(M0 /. (i + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(M0 /. (i + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (i + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(M0 /. (i + 1))}) --> FALSE is Relation-like *' {(M0 /. (i + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (i + 1))}),BOOLEAN))
K33((*' {(M0 /. (i + 1))}),BOOLEAN) is set
K32(K33((*' {(M0 /. (i + 1))}),BOOLEAN)) is set
(M3 /. i) +* ((*' {(M0 /. (i + 1))}) --> FALSE) is Relation-like Function-like set
{(M0 /. (i + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (i + 1))} & b₂ = [b₃,b₁] ) } is set
({(M0 /. (i + 1))} *') --> TRUE is Relation-like {(M0 /. (i + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (i + 1))} *'),BOOLEAN))
K33(({(M0 /. (i + 1))} *'),BOOLEAN) is set
K32(K33(({(M0 /. (i + 1))} *'),BOOLEAN)) is set
((M3 /. i) +* ((*' {(M0 /. (i + 1))}) --> FALSE)) +* (({(M0 /. (i + 1))} *') --> TRUE) is Relation-like Function-like set
i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
1 + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
((len M0) + 1) + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (((len M0) + 1) + i) is Element of (PTN)
s /. (1 + i) is Element of (PTN)
i + (len M0) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(((len M0) + 1) + i) + 1 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
((len M0) + 1) + (i + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(len M0) + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
((len M0) + i) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
1 + (i + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(len M0) + (1 + (i + 1)) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(M0 ^ M0) /. ((len M0) + (1 + (i + 1))) is Element of the carrier' of PTN
M0 /. (1 + (i + 1)) is Element of the carrier' of PTN
(len M0) + (1 + i) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (((len M0) + 1) + (i + 1)) is Element of (PTN)
(PTN,(s /. (1 + i)),(M0 /. (1 + (i + 1)))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(M0 /. (1 + (i + 1)))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(M0 /. (1 + (i + 1)))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (i + 1)))} & b₂ = [b₁,b₃] ) } is set
(*' {(M0 /. (1 + (i + 1)))}) --> FALSE is Relation-like *' {(M0 /. (1 + (i + 1)))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN))
K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN) is set
K32(K33((*' {(M0 /. (1 + (i + 1)))}),BOOLEAN)) is set
(s /. (1 + i)) +* ((*' {(M0 /. (1 + (i + 1)))}) --> FALSE) is Relation-like Function-like set
{(M0 /. (1 + (i + 1)))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (1 + (i + 1)))} & b₂ = [b₃,b₁] ) } is set
({(M0 /. (1 + (i + 1)))} *') --> TRUE is Relation-like {(M0 /. (1 + (i + 1)))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN))
K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN) is set
K32(K33(({(M0 /. (1 + (i + 1)))} *'),BOOLEAN)) is set
((s /. (1 + i)) +* ((*' {(M0 /. (1 + (i + 1)))}) --> FALSE)) +* (({(M0 /. (1 + (i + 1)))} *') --> TRUE) is Relation-like Function-like set
s /. (1 + (i + 1)) is Element of (PTN)
((len M0) + 1) + 0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (((len M0) + 1) + 0) is Element of (PTN)
Q is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
1 + Q is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (1 + Q) is Element of (PTN)
(PTN,(M /. (1 + Q)),((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. ((len M0) + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {((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
(M /. (1 + Q)) +* ((*' {((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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. ((len M0) + 1))} & b₂ = [b₃,b₁] ) } is set
({((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
((M /. (1 + Q)) +* ((*' {((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
s /. (1 + 0) is Element of (PTN)
i 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() set
j + 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
((len M0) + 1) + 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
(len M0) + (j + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(len M0) + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. ((len M0) + i) is Element of (PTN)
s /. i is Element of (PTN)
i + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
dom M0 is Element of K32(NAT)
((len M0) + i) + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(M0 ^ M0) /. (((len M0) + i) + 1) is Element of the carrier' of PTN
(len M0) + (i + 1) is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
(M0 ^ M0) /. ((len M0) + (i + 1)) is Element of the carrier' of PTN
M0 /. (i + 1) is Element of the carrier' of PTN
((len M0) + 1) + i is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M /. (((len M0) + i) + 1) is Element of (PTN)
(PTN,(M /. ((len M0) + i)),((M0 ^ M0) /. (((len M0) + i) + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{((M0 ^ M0) /. (((len M0) + i) + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {((M0 ^ M0) /. (((len M0) + i) + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. (((len M0) + i) + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {((M0 ^ M0) /. (((len M0) + i) + 1))}) --> FALSE is Relation-like *' {((M0 ^ M0) /. (((len M0) + i) + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {((M0 ^ M0) /. (((len M0) + i) + 1))}),BOOLEAN))
K33((*' {((M0 ^ M0) /. (((len M0) + i) + 1))}),BOOLEAN) is set
K32(K33((*' {((M0 ^ M0) /. (((len M0) + i) + 1))}),BOOLEAN)) is set
(M /. ((len M0) + i)) +* ((*' {((M0 ^ M0) /. (((len M0) + i) + 1))}) --> FALSE) is Relation-like Function-like set
{((M0 ^ M0) /. (((len M0) + i) + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {((M0 ^ M0) /. (((len M0) + i) + 1))} & b₂ = [b₃,b₁] ) } is set
({((M0 ^ M0) /. (((len M0) + i) + 1))} *') --> TRUE is Relation-like {((M0 ^ M0) /. (((len M0) + i) + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({((M0 ^ M0) /. (((len M0) + i) + 1))} *'),BOOLEAN))
K33(({((M0 ^ M0) /. (((len M0) + i) + 1))} *'),BOOLEAN) is set
K32(K33(({((M0 ^ M0) /. (((len M0) + i) + 1))} *'),BOOLEAN)) is set
((M /. ((len M0) + i)) +* ((*' {((M0 ^ M0) /. (((len M0) + i) + 1))}) --> FALSE)) +* (({((M0 ^ M0) /. (((len M0) + i) + 1))} *') --> TRUE) is Relation-like Function-like set
s /. (i + 1) is Element of (PTN)
(PTN,(s /. i),(M0 /. (i + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(M0 /. (i + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(M0 /. (i + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (i + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(M0 /. (i + 1))}) --> FALSE is Relation-like *' {(M0 /. (i + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(M0 /. (i + 1))}),BOOLEAN))
K33((*' {(M0 /. (i + 1))}),BOOLEAN) is set
K32(K33((*' {(M0 /. (i + 1))}),BOOLEAN)) is set
(s /. i) +* ((*' {(M0 /. (i + 1))}) --> FALSE) is Relation-like Function-like set
{(M0 /. (i + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(M0 /. (i + 1))} & b₂ = [b₃,b₁] ) } is set
({(M0 /. (i + 1))} *') --> TRUE is Relation-like {(M0 /. (i + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(M0 /. (i + 1))} *'),BOOLEAN))
K33(({(M0 /. (i + 1))} *'),BOOLEAN) is set
K32(K33(({(M0 /. (i + 1))} *'),BOOLEAN)) is set
((s /. i) +* ((*' {(M0 /. (i + 1))}) --> FALSE)) +* (({(M0 /. (i + 1))} *') --> TRUE) is Relation-like Function-like set
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
M /. (len M3) 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 Element of the carrier' of PTN
<*M0*> 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
<*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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(<*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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. 1)} & b₂ = [b₃,b₁] ) } is set
({(<*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
<*(PTN,Sd,(<*M0*> /. 1))*> is non empty V5() Relation-like NAT -defined (PTN) -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of (PTN)
<*(PTN,Sd,(<*M0*> /. 1))*> /. 1 is Element of (PTN)
len <*M0*> is non empty 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
t is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
<*(PTN,Sd,(<*M0*> /. 1))*> /. t is Element of (PTN)
t + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
<*M0*> /. (t + 1) is Element of the carrier' of PTN
<*(PTN,Sd,(<*M0*> /. 1))*> /. (t + 1) is Element of (PTN)
(PTN,(<*(PTN,Sd,(<*M0*> /. 1))*> /. t),(<*M0*> /. (t + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(<*M0*> /. (t + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(<*M0*> /. (t + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. (t + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(<*M0*> /. (t + 1))}) --> FALSE is Relation-like *' {(<*M0*> /. (t + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN))
K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN) is set
K32(K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN)) is set
(<*(PTN,Sd,(<*M0*> /. 1))*> /. t) +* ((*' {(<*M0*> /. (t + 1))}) --> FALSE) is Relation-like Function-like set
{(<*M0*> /. (t + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. (t + 1))} & b₂ = [b₃,b₁] ) } is set
({(<*M0*> /. (t + 1))} *') --> TRUE is Relation-like {(<*M0*> /. (t + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN))
K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN) is set
K32(K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN)) is set
((<*(PTN,Sd,(<*M0*> /. 1))*> /. t) +* ((*' {(<*M0*> /. (t + 1))}) --> FALSE)) +* (({(<*M0*> /. (t + 1))} *') --> TRUE) is Relation-like Function-like set
len <*(PTN,Sd,(<*M0*> /. 1))*> is non empty 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)
len M0 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
M0 /. 1 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 Element 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)
{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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₁,b₃] ) } is set
(*' {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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {M0} & b₂ = [b₃,b₁] ) } is 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 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
(PTN,Sd,<*M0*>) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
<*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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(<*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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. 1)} & b₂ = [b₃,b₁] ) } is set
({(<*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
<*(PTN,Sd,(<*M0*> /. 1))*> is non empty V5() Relation-like NAT -defined (PTN) -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of (PTN)
len <*M0*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
<*(PTN,Sd,(<*M0*> /. 1))*> /. 1 is Element of (PTN)
0 + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
t is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
t + 1 is V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
<*(PTN,Sd,(<*M0*> /. 1))*> /. (t + 1) is Element of (PTN)
<*(PTN,Sd,(<*M0*> /. 1))*> /. t is Element of (PTN)
<*M0*> /. (t + 1) is Element of the carrier' of PTN
(PTN,(<*(PTN,Sd,(<*M0*> /. 1))*> /. t),(<*M0*> /. (t + 1))) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
{(<*M0*> /. (t + 1))} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {(<*M0*> /. (t + 1))} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. (t + 1))} & b₂ = [b₁,b₃] ) } is set
(*' {(<*M0*> /. (t + 1))}) --> FALSE is Relation-like *' {(<*M0*> /. (t + 1))} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN))
K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN) is set
K32(K33((*' {(<*M0*> /. (t + 1))}),BOOLEAN)) is set
(<*(PTN,Sd,(<*M0*> /. 1))*> /. t) +* ((*' {(<*M0*> /. (t + 1))}) --> FALSE) is Relation-like Function-like set
{(<*M0*> /. (t + 1))} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*M0*> /. (t + 1))} & b₂ = [b₃,b₁] ) } is set
({(<*M0*> /. (t + 1))} *') --> TRUE is Relation-like {(<*M0*> /. (t + 1))} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN))
K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN) is set
K32(K33(({(<*M0*> /. (t + 1))} *'),BOOLEAN)) is set
((<*(PTN,Sd,(<*M0*> /. 1))*> /. t) +* ((*' {(<*M0*> /. (t + 1))}) --> FALSE)) +* (({(<*M0*> /. (t + 1))} *') --> TRUE) is Relation-like Function-like set
len <*(PTN,Sd,(<*M0*> /. 1))*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
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)
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 --> 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 (Sd --> FALSE) is set
M0 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
M0 .: Sd is 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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₃,b₁] ) } is set
K32((Sd *')) is set
t is Relation-like NAT -defined the carrier' of PTN -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier' of PTN
(PTN,M0,t) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
(PTN,M0,t) .: Sd is set
Q is Element of the carrier' of PTN
<*Q*> 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
t ^ <*Q*> 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
(PTN,M0,(t ^ <*Q*>)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
(PTN,M0,(t ^ <*Q*>)) .: Sd is set
(PTN,(PTN,M0,t),<*Q*>) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
len <*Q*> is non empty V21() V22() V23() V24() V28() V29() ext-real V35() V40() Element of NAT
<*Q*> /. 1 is Element of the carrier' of PTN
(PTN,(PTN,M0,t),(<*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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*Q*> /. 1)} & b₂ = [b₁,b₃] ) } is set
(*' {(<*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
(PTN,M0,t) +* ((*' {(<*Q*> /. 1)}) --> FALSE) is Relation-like Function-like set
{(<*Q*> /. 1)} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {(<*Q*> /. 1)} & b₂ = [b₃,b₁] ) } is set
({(<*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
((PTN,M0,t) +* ((*' {(<*Q*> /. 1)}) --> FALSE)) +* (({(<*Q*> /. 1)} *') --> TRUE) is Relation-like Function-like set
{Q} is non empty V5() V42(1) Element of K32( the carrier' of PTN)
*' {Q} is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {Q} & b₂ = [b₁,b₃] ) } is set
(*' {Q}) --> FALSE is Relation-like *' {Q} -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33((*' {Q}),BOOLEAN))
K33((*' {Q}),BOOLEAN) is set
K32(K33((*' {Q}),BOOLEAN)) is set
(PTN,M0,t) +* ((*' {Q}) --> FALSE) is Relation-like Function-like set
{Q} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {Q} & b₂ = [b₃,b₁] ) } is set
({Q} *') --> TRUE is Relation-like {Q} *' -defined BOOLEAN -valued Function-like quasi_total boolean-valued Element of K32(K33(({Q} *'),BOOLEAN))
K33(({Q} *'),BOOLEAN) is set
K32(K33(({Q} *'),BOOLEAN)) is set
((PTN,M0,t) +* ((*' {Q}) --> FALSE)) +* (({Q} *') --> TRUE) is Relation-like Function-like set
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)
(PTN,M0,t) .: (*' {Q}) is set
((PTN,M0,t) +* ((*' {Q}) --> FALSE)) .: Sd is set
<*> the carrier' of PTN is empty Relation-like NAT -defined the carrier' of PTN -valued Function-like functional V21() V22() V23() V24() V26() V27() V28() V29() ext-real non positive non negative V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V48() FinSequence of the carrier' of PTN
(PTN,M0,(<*> the carrier' of PTN)) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
(PTN,M0,(<*> 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 ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) is 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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier' of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier of PTN st
( b₃ in Sd & b₂ = [b₃,b₁] ) } is set
K32((Sd *')) is set
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₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the S-T_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₁,b₃] ) } is set
( the carrier of PTN --> TRUE) .: (*' {t}) is set
M0 is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
M0 .: (*' {t}) is set
<*t*> 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
{t} *' is Element of K32( the carrier of PTN)
{ b₁ where b₁ is Element of the carrier of PTN : ex b₂ being Element of the T-S_Arcs of PTN ex b₃ being Element of the carrier' of PTN st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
({t} *') /\ Sd is Element of K32( the carrier of PTN)
s is set
(PTN,M0,t) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
(*' {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) . s is set
(PTN,M0,t) .: Sd is 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
(PTN,M0,Q) is Relation-like the carrier of PTN -defined BOOLEAN -valued Function-like quasi_total Element of (PTN)
(PTN,M0,Q) .: Sd is set
M0 .: Sd is set