:: 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

( not b

{ (b

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

( not b

{ (b

{ b

( not b

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

( not b

{ b

( not b

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

( not b

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

( not b

{ b

( not b

{ b

( not b

( not b

( not b

K11( { b

( not b

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

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

( not b

{ (b

{ b

( not b

{ b

( not b

{ b

( not b

T1 is set

{ b

( not b

( not b

( not b

K11( { b

( not b

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

( not b

{ (b

{ b

( not b

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

( not b

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

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

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

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

( not b

{ (b

{ b

( not b

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

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

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

( not b

{ (b

{ b

( not b

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