:: TREES_A semantic presentation

REAL is V32() V33() V34() V38() set
NAT is V32() V33() V34() V35() V36() V37() V38() Element of K11(REAL)
K11(REAL) is set
NAT is V32() V33() V34() V35() V36() V37() V38() set
K11(NAT) is set
K11(NAT) is set
1 is ext-real non empty V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
2 is ext-real non empty V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
3 is ext-real non empty V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
{} is empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered set
the empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered set is empty functional V32() V33() V34() V35() V36() V37() V38() FinSequence-membered set
K168(NAT) is non empty functional FinSequence-membered M14( NAT )
<*> NAT is empty Relation-like NAT -defined NAT -valued Function-like functional V32() V33() V34() V35() V36() V37() V38() V39() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
D is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
T is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
D ^ T is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
T1 is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
T1 ^ P is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
D is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
T is non empty Tree-like set
K11(D) is set
T2 is set
T1 is Element of K11(D)
y is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
y is set
T2 is non empty set
T2 \/ y is non empty set
NAT * is non empty functional FinSequence-membered set
q is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
x is non empty set
q is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
p2 ^ r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes q is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
p2 is set
r2 is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
p2 ^ r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is set
s is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
s ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
len p2 is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
len s is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
p2 ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
p2 ^ (r ^ r) is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
dom r is V32() V33() V34() V35() V36() V37() Element of K11(NAT)
r2 | (dom r) is Relation-like FinSubsequence-like set
len r is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
Seg (len r) is V32() V33() V34() V35() V36() V37() V39() V46( len r) Element of K11(NAT)
r2 | (Seg (len r)) is Relation-like FinSubsequence-like set
t is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p9 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
p2 ^ p9 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
dom s is V32() V33() V34() V35() V36() V37() Element of K11(NAT)
p2 | (dom s) is Relation-like FinSubsequence-like set
r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
s ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
Seg (len s) is V32() V33() V34() V35() V36() V37() V39() V46( len s) Element of K11(NAT)
p2 | (Seg (len s)) is Relation-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
t is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
p9 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
<*p2*> is non empty Relation-like NAT -defined NAT -valued Function-like V39() V46(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ <*p2*> is non empty Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
<*r2*> is non empty Relation-like NAT -defined NAT -valued Function-like V39() V46(1) FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ <*r2*> is non empty Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
<*p2*> is non empty Relation-like NAT -defined Function-like V39() V46(1) FinSequence-like FinSubsequence-like set
q ^ <*p2*> is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
<*r2*> is non empty Relation-like NAT -defined Function-like V39() V46(1) FinSequence-like FinSubsequence-like set
q ^ <*r2*> is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
r ^ s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
len q is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
len r is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
q ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r ^ s is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
q ^ (r ^ s) is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
t is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
len <*p2*> is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
(len q) + (len <*p2*>) is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
(len q) + 1 is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
len <*r2*> is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
(len q) + (len <*r2*>) is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
len r is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
(<*> NAT) ^ s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*> NAT) ^ <*r2*> is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
r ^ r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r ^ r is Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r ^ <*p2*> is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
r ^ (r ^ <*p2*>) is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
dom r is V32() V33() V34() V35() V36() V37() Element of K11(NAT)
s | (dom r) is Relation-like FinSubsequence-like set
len r is ext-real V13() V14() V32() V33() V34() V35() V36() V37() Element of NAT
Seg (len r) is V32() V33() V34() V35() V36() V37() V39() V46( len r) Element of K11(NAT)
s | (Seg (len r)) is Relation-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ <*r2*> is non empty Relation-like NAT -defined Function-like V39() FinSequence-like FinSubsequence-like set
t is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
r ^ t is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is non empty Tree-like set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
r2 ^ r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 ^ r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 ^ r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is non empty Tree-like set
T2 is non empty Tree-like set
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is non empty Tree-like set
T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
(D,T,P) is non empty Tree-like set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
D is non empty Tree-like set
T is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c= b₁ ) } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } is set
P is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is non empty Tree-like set
T is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } is set
P is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
D is non empty Tree-like set
T is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c= b₁ ) } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } \ { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c= b₁ ) } is Element of K11( { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } )
K11( { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c< b₁ ) } ) is set
P is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
P is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
D is non empty Tree-like set
T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is non empty Tree-like set
T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
(D,T,P) is non empty Tree-like set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of T : b₁ in P } is set
T1 is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } \ { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } is Element of K11( { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } )
K11( { b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c< b₁ ) } ) is set
D is non empty Tree-like set
T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of T
(T,D,P) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T,D,P) | T1 is non empty Tree-like set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is non empty Tree-like set
the Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
{ the Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D} is non empty set
P is set
T1 is set
T1 is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
D is non empty Tree-like set
T is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
{T} is non empty set
D is non empty Tree-like set
T is non empty Tree-like set
P is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of D
(D,P) is non empty AntiChain_of_Prefixes-like AntiChain_of_Prefixes of D
(D,T,(D,P)) is non empty Tree-like set
D with-replacement (P,T) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like Function-like DecoratedTree-like set
dom D is non empty Tree-like set
T is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom D
P is Relation-like Function-like DecoratedTree-like set
dom P is non empty Tree-like set
((dom D),(dom P),T) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D . T1 is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c= b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom P : b₁ in T } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in T or not b₂ c= b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom P : b₁ in T } is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
D . T2 is set
y is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom P
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . y is set
x is set
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . p2 is set
T2 is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
P . q is set
p2 is set
r is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ s is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is set
P . s is set
T1 is Relation-like Function-like DecoratedTree-like set
dom T1 is non empty Tree-like set
T2 is Relation-like Function-like DecoratedTree-like set
dom T2 is non empty Tree-like set
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 . y is set
T2 . y is set
D . y is set
x is set
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . q is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . q is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . q is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . q is set
D . y is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 ^ r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . r2 is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
p2 ^ r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . r2 is set
D . y is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D . y is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like Function-like DecoratedTree-like set
dom D is non empty Tree-like set
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom D
(D,P,T) is Relation-like Function-like DecoratedTree-like set
dom (D,P,T) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(D,P,T) . T1 is set
D . T1 is set
((dom D),(dom T),P) is non empty Tree-like set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
P is Relation-like Function-like DecoratedTree-like set
T with-replacement (D,P) is Relation-like Function-like DecoratedTree-like set
dom (T with-replacement (D,P)) is non empty Tree-like set
dom P is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T with-replacement (D,P)) . T1 is set
T . T1 is set
(dom T) with-replacement (D,(dom P)) is non empty Tree-like set
D is Relation-like Function-like DecoratedTree-like set
dom D is non empty Tree-like set
T is Relation-like Function-like DecoratedTree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom D
(D,P,T) is Relation-like Function-like DecoratedTree-like set
dom (D,P,T) is non empty Tree-like set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(D,P,T) . T1 is set
D . T1 is set
T2 is set
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
dom T is non empty Tree-like set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . y is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . y is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
dom T is non empty Tree-like set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : not D c= b₁ } is set
P is Relation-like Function-like DecoratedTree-like set
T with-replacement (D,P) is Relation-like Function-like DecoratedTree-like set
dom (T with-replacement (D,P)) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T with-replacement (D,P)) . T1 is set
T . T1 is set
dom P is non empty Tree-like set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . y is set
dom P is non empty Tree-like set
D is Relation-like Function-like DecoratedTree-like set
dom D is non empty Tree-like set
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom D
(D,P,T) is Relation-like Function-like DecoratedTree-like set
dom (D,P,T) is non empty Tree-like set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : b₁ in P } is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(D,P,T) . T1 is set
D . T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . y is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . y is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . y is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D . T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like Function-like DecoratedTree-like set
dom T is non empty Tree-like set
P is Relation-like Function-like DecoratedTree-like set
T with-replacement (D,P) is Relation-like Function-like DecoratedTree-like set
dom (T with-replacement (D,P)) is non empty Tree-like set
dom P is non empty Tree-like set
{ (D ^ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom P : b₁ = b₁ } is set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T with-replacement (D,P)) . T1 is set
T . T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom P
D ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
P . T2 is set
T . T1 is set
D is Relation-like Function-like DecoratedTree-like set
dom D is non empty Tree-like set
T is Relation-like Function-like DecoratedTree-like set
P is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
((dom D),P) is non empty AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom D
(D,((dom D),P),T) is Relation-like Function-like DecoratedTree-like set
D with-replacement (P,T) is Relation-like Function-like DecoratedTree-like set
dom (D,((dom D),P),T) is non empty Tree-like set
dom T is non empty Tree-like set
((dom D),(dom T),((dom D),P)) is non empty Tree-like set
(dom D) with-replacement (P,(dom T)) is non empty Tree-like set
dom (D with-replacement (P,T)) is non empty Tree-like set
T1 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(D,((dom D),P),T) . T1 is set
(D with-replacement (P,T)) . T1 is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in ((dom D),P) or not b₂ c= b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : b₁ in ((dom D),P) } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in ((dom D),P) or not b₂ c= b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : b₁ in ((dom D),P) } is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D : not y c= b₁ } is set
D . T1 is set
T2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
T2 ^ y is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
{ (T2 ^ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : b₁ = b₁ } is set
x is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom D
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
x ^ q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . q is set
D with-replacement (T2,T) is Relation-like Function-like DecoratedTree-like set
(D with-replacement (T2,T)) . T1 is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
T2 ^ p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T . p2 is set
D is non empty set
T is Relation-like D -valued Function-like DecoratedTree-like set
dom T is non empty Tree-like set
P is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of dom T
T1 is Relation-like D -valued Function-like DecoratedTree-like set
(T,P,T1) is Relation-like Function-like DecoratedTree-like set
y is set
rng (T,P,T1) is set
dom (T,P,T1) is non empty Tree-like set
x is set
(T,P,T1) . x is set
dom T1 is non empty Tree-like set
((dom T),(dom T1),P) is non empty Tree-like set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T1 : b₁ in P } is set
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T : for b₂ being Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT holds
( not b₂ in P or not b₂ c= b₁ ) } \/ { (b₁ ^ b₂) where b₁ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T, b₂ is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T1 : b₁ in P } is set
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T,P,T1) . q is set
T . q is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
rng T is set
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
(T,P,T1) . q is set
p2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T
r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like Element of dom T1
p2 ^ r2 is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT
T1 . r2 is Element of D
q is Relation-like NAT -defined NAT -valued Function-like V39() FinSequence-like FinSubsequence-like FinSequence of NAT