:: PRELAMB semantic presentation

REAL is non empty non trivial V48() V49() V50() V54() non finite set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

RAT is non empty non trivial V48() V49() V50() V51() V54() non finite set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

{{},1} is non empty V48() V49() V50() V51() V52() V53() finite V59() set

COMPLEX is non empty non trivial V48() V54() non finite set

INT is non empty non trivial V48() V49() V50() V51() V52() V54() non finite set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

[:REAL,REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:1,1:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set

bool [:1,1:] is non empty finite V59() set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set

bool [:[:1,1:],1:] is non empty finite V59() set

[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial V38() non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial V38() non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

Seg 1 is non empty trivial V48() V49() V50() V51() V52() V53() finite 1 -element Element of bool NAT

card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

NAT * is functional non empty FinSequence-membered M10( NAT )

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT

{{}} is functional non empty trivial V48() V49() V50() V51() V52() V53() finite V59() 1 -element set

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() V35() V36() V37() V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL

[:NAT,REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set

Sum (<*> REAL) is ext-real V34() V35() Element of REAL

[:{{}},{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set

[:[:{{}},{{}}:],{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set

bool [:[:{{}},{{}}:],{{}}:] is non empty finite V59() set

the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:] is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]

({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]) is () ()

the carrier of ({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]) is set

s is non empty ()

the carrier of s is non empty set

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

[: the carrier of s, the carrier of s:] is Relation-like non empty set

[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set

bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set

x is Element of the carrier of s

y is Element of the carrier of s

the of s . (x,y) is Element of the carrier of s

[x,y] is V15() set

{x,y} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,y},{x}} is non empty finite V59() set

the of s . [x,y] is set

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

the of s . (x,y) is Element of the carrier of s

the of s . [x,y] is set

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

the of s . (x,y) is Element of the carrier of s

the of s . [x,y] is set

s is non empty ()

the carrier of s is non empty set

the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)

[:( the carrier of s *), the carrier of s:] is Relation-like non empty set

[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set

x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like set

proj1 x is non empty finite V70() set

y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x

x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]

(x . y) `2 is set

branchdeg y is set

(x . y) `1 is set

<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT

x . (y ^ <*0*>) is set

(x . (y ^ <*0*>)) `1 is set

<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT

x . (y ^ <*1*>) is set

(x . (y ^ <*1*>)) `1 is set

4 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

5 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

6 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

7 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT

z is Element of the carrier of s

<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s

[<*z*>,z] is V15() set

{<*z*>,z} is non empty finite set

{<*z*>} is functional non empty trivial finite V59() 1 -element set

{{<*z*>,z},{<*z*>}} is non empty finite V59() set

z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

z is Element of the carrier of s

a is Element of the carrier of s

(s,z,a) is Element of the carrier of s

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

[: the carrier of s, the carrier of s:] is Relation-like non empty set

[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set

bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set

the of s . (z,a) is Element of the carrier of s

[z,a] is V15() set

{z,a} is non empty finite set

{z} is non empty trivial finite 1 -element set

{{z,a},{z}} is non empty finite V59() set

the of s . [z,a] is set

[z,(s,z,a)] is V15() set

{z,(s,z,a)} is non empty finite set

{z} is functional non empty trivial finite V59() 1 -element set

{{z,(s,z,a)},{z}} is non empty finite V59() set

<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s

z ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

[(z ^ <*a*>),z] is V15() set

{(z ^ <*a*>),z} is non empty finite set

{(z ^ <*a*>)} is functional non empty trivial finite V59() 1 -element set

{{(z ^ <*a*>),z},{(z ^ <*a*>)}} is non empty finite V59() set

b is Element of the carrier of s

<*b*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s

[<*b*>,b] is V15() set

{<*b*>,b} is non empty finite set

{<*b*>} is functional non empty trivial finite V59() 1 -element set

{{<*b*>,b},{<*b*>}} is non empty finite V59() set

z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

X9 is Element of the carrier of s

T9 is Element of the carrier of s

(s,X9,T9) is Element of the carrier of s

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

the of s . (X9,T9) is Element of the carrier of s

[X9,T9] is V15() set

{X9,T9} is non empty finite set

{X9} is non empty trivial finite 1 -element set

{{X9,T9},{X9}} is non empty finite V59() set

the of s . [X9,T9] is set

[z,(s,X9,T9)] is V15() set

{z,(s,X9,T9)} is non empty finite set

{z} is functional non empty trivial finite V59() 1 -element set

{{z,(s,X9,T9)},{z}} is non empty finite V59() set

<*X9*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s

<*X9*> ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

[(<*X9*> ^ z),T9] is V15() set

{(<*X9*> ^ z),T9} is non empty finite set

{(<*X9*> ^ z)} is functional non empty trivial finite V59() 1 -element set

{{(<*X9*> ^ z),T9},{(<*X9*> ^ z)}} is non empty finite V59() set

Y9 is Element of the carrier of s

<*Y9*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s

[<*Y9*>,Y9] is V15() set

{<*Y9*>,Y9} is non empty finite set

{<*Y9*>} is functional non empty trivial finite V59() 1 -element set

{{<*Y9*>,Y9},{<*Y9*>}} is non empty finite V59() set

z9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

z9 ^ <*(s,c

y9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s

(z9 ^ <*(s,c

c

((z9 ^ <*(s,c

c

[(((z9 ^ <*(s,c

{(((z9 ^ <*(s,c

{(((z9 ^ <*(s,c

{{(((z9 ^ <*(s,c

[y9,c

{y9,c

{y9} is functional non empty trivial finite V59() 1 -element set

{{y9,c

<*c

z9 ^ <*c

(z9 ^ <*c

[((z9 ^ <*c

{((z9 ^ <*c

{((z9 ^ <*c

{{((z9 ^ <*c

c

<*c

[<*c

{<*c

{<*c

{{<*c

c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

(c

c

((c

c

[(((c

{(((c

{(((c

{{(((c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

<*c

[<*c

{<*c

{<*c

{{<*c

c

c

<*c

[<*c

{<*c

{<*c

{{<*c

c

c

c

c

c

(s,c

the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]

the of s . (c

[c

{c

{c

{{c

the of s . [c

[(c

{(c

{(c

{{(c

[c

{c

{c

{{c

[c

{c

{c

{{c

c

<*c

[<*c

{<*c

{<*c

{{<*c

c

c

c

c

(c

c

[((c

{((c

{((c

{{((c

c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

<*c

[(<*c

{(<*c

{(<*c

{{(<*c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

c

c

(c

c

((c

c

[(((c

{(((c

{(((c

{{(((c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

(c

c

((c

c

[(((c

{(((c

{(((c

{{(((c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[(c

{(c

{(c

{{(c

[c

{c

{c

{{c

[c

{c

{c

{{c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

c

[(c

{(c

{(c

{{(c

c

c

c

c

(c

c

[((c

{((c

{((c

{{((c

c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

<*c

[(<*c

{(<*c

{(<*c

{{(<*c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

c

c

(c

c

((c

c

[(((c

{(((c

{(((c

{{(((c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

<*c

[(<*c

{(<*c

{(<*c

{{(<*c

c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

<*(s,c

(c

c

((c

c

[(((c

{(((c

{(((c

{{(((c

[c

{c

{c

{{c

<*c

c

(c

[((c

{((c

{((c

{{((c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

<*c

[(<*c

{(<*c

{(<*c

{{(<*c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[c

{c

{c

{{c

<*c

<*c

[(<*c

{(<*c

{(<*c

{{(<*c

c

c

c

c

c

(s,c

the of s . (c

[c

{c

{c

{{c

the of s . [c

[(c

{(c

{(c

{{(c

[c

{c

{c

{{c

[c

{c

{c

{{c

c