:: SCM_INST semantic presentation

REAL is set
NAT is non empty V17() V18() V19() V24() cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is non empty V17() V18() V19() V24() cardinal limit_cardinal set
bool NAT is V24() set
bool NAT is V24() set
COMPLEX is set
RAT is set
INT is set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set
the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set
1 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
2 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
3 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
8 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued Element of NAT
4 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
5 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
6 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
7 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
Seg 1 is non empty trivial V24() 1 -element Element of bool NAT
{ b₁ where b₁ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial 1 -element set
Seg 2 is non empty V24() 2 -element Element of bool NAT
{ b₁ where b₁ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty set
9 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT
Segm 9 is Element of bool NAT
{1} is non empty trivial 1 -element Element of bool NAT
[:{1},NAT:] is Relation-like V24() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is set
() is set
() is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued Element of Segm 9
[(),{},{}] is V1() V2() set
[(),{}] is V1() set
{(),{}} is non empty functional set
{()} is non empty trivial functional 1 -element set
{{(),{}},{()}} is non empty set
[[(),{}],{}] is V1() set
{[(),{}],{}} is non empty set
{[(),{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[(),{}],{}},{[(),{}]}} is non empty set
{[(),{},{}]} is non empty trivial Relation-like 1 -element standard-ins homogeneous J/A-independent with_halt set
{ [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : b₁ = 6 } is set
{[(),{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : b₁ = 6 } is non empty set
{7,8} is non empty Element of bool NAT
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT , b₃ is Element of () : b₁ in {7,8} } is set
({[(),{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT , b₃ is Element of () : b₁ in {7,8} } is non empty set
{1,2,3,4,5} is Element of bool NAT
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of () : b₁ in {1,2,3,4,5} } is set
(({[(),{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT , b₃ is Element of () : b₁ in {7,8} } ) \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of () : b₁ in {1,2,3,4,5} } is non empty set
() is non empty set
[0,{},{}] is V1() V2() set
[0,{}] is V1() set
{0,{}} is non empty functional set
{0} is non empty trivial functional 1 -element set
{{0,{}},{0}} is non empty set
[[0,{}],{}] is V1() set
{[0,{}],{}} is non empty set
{[0,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[0,{}],{}},{[0,{}]}} is non empty set
T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*T*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,T] is V1() set
{1,T} is non empty set
{{1,T},{1}} is non empty set
{[1,T]} is non empty trivial Relation-like Function-like constant 1 -element set
[6,<*T*>,{}] is V1() V2() set
[6,<*T*>] is V1() set
{6,<*T*>} is non empty set
{6} is non empty trivial 1 -element set
{{6,<*T*>},{6}} is non empty set
[[6,<*T*>],{}] is V1() set
{[6,<*T*>],{}} is non empty set
{[6,<*T*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[6,<*T*>],{}},{[6,<*T*>]}} is non empty set
f1 is Element of Segm 9
[f1,<*T*>,{}] is V1() V2() set
[f1,<*T*>] is V1() set
{f1,<*T*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*T*>},{f1}} is non empty set
[[f1,<*T*>],{}] is V1() set
{[f1,<*T*>],{}} is non empty set
{[f1,<*T*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*T*>],{}},{[f1,<*T*>]}} is non empty set
T is set
f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
f2 is Element of ()
<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
[T,<*f1*>,<*f2*>] is V1() V2() set
[T,<*f1*>] is V1() set
{T,<*f1*>} is non empty set
{T} is non empty trivial 1 -element set
{{T,<*f1*>},{T}} is non empty set
[[T,<*f1*>],<*f2*>] is V1() set
{[T,<*f1*>],<*f2*>} is non empty set
{[T,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,<*f1*>],<*f2*>},{[T,<*f1*>]}} is non empty set
p is Element of Segm 9
[p,<*f1*>,<*f2*>] is V1() V2() set
[p,<*f1*>] is V1() set
{p,<*f1*>} is non empty set
{p} is non empty trivial 1 -element set
{{p,<*f1*>},{p}} is non empty set
[[p,<*f1*>],<*f2*>] is V1() set
{[p,<*f1*>],<*f2*>} is non empty set
{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set
T is set
f1 is Element of ()
f2 is Element of ()
<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
K183(1,1) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
[T,{},<*f1,f2*>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty trivial 1 -element set
{{T,{}},{T}} is non empty set
[[T,{}],<*f1,f2*>] is V1() set
{[T,{}],<*f1,f2*>} is non empty set
{[T,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,{}],<*f1,f2*>},{[T,{}]}} is non empty set
p is Element of Segm 9
[p,{},<*f1,f2*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty trivial 1 -element set
{{p,{}},{p}} is non empty set
[[p,{}],<*f1,f2*>] is V1() set
{[p,{}],<*f1,f2*>} is non empty set
{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set
T is Element of ()
p is Element of Segm 9
f1 is Element of ()
f2 is Element of ()
<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
K183(1,1) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
[p,{},<*f1,f2*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty trivial 1 -element set
{{p,{}},{p}} is non empty set
[[p,{}],<*f1,f2*>] is V1() set
{[p,{}],<*f1,f2*>} is non empty set
{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set
T `3_3 is set
<*f1,f2*> /. 1 is Element of ()
i1 is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
J is Element of ()
i1 /. 1 is Element of ()
a is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
K is Element of ()
a /. 1 is Element of ()
<*f1,f2*> /. 2 is Element of ()
i1 is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
J is Element of ()
i1 /. 2 is Element of ()
a is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
K is Element of ()
a /. 2 is Element of ()
T is Element of ()
(T) is Element of ()
(T) is Element of ()
f1 is Element of ()
f2 is Element of ()
<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
p is Element of Segm 9
[p,{},<*f1,f2*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty trivial 1 -element set
{{p,{}},{p}} is non empty set
[[p,{}],<*f1,f2*>] is V1() set
{[p,{}],<*f1,f2*>} is non empty set
{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set
T `3_3 is set
J is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
J /. 1 is Element of ()
K is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()
K /. 2 is Element of ()
T is Element of ()
f2 is Element of Segm 9
f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
[f2,<*f1*>,{}] is V1() V2() set
[f2,<*f1*>] is V1() set
{f2,<*f1*>} is non empty set
{f2} is non empty trivial 1 -element set
{{f2,<*f1*>},{f2}} is non empty set
[[f2,<*f1*>],{}] is V1() set
{[f2,<*f1*>],{}} is non empty set
{[f2,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f2,<*f1*>],{}},{[f2,<*f1*>]}} is non empty set
T `2_3 is set
K13(T) is set
K13(T) `3_3 is set
<*f1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
K is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
p is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
K /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
i1 is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
i1 /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
T is Element of ()
(T) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
f2 is Element of Segm 9
[f2,<*f1*>,{}] is V1() V2() set
[f2,<*f1*>] is V1() set
{f2,<*f1*>} is non empty set
{f2} is non empty trivial 1 -element set
{{f2,<*f1*>},{f2}} is non empty set
[[f2,<*f1*>],{}] is V1() set
{[f2,<*f1*>],{}} is non empty set
{[f2,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f2,<*f1*>],{}},{[f2,<*f1*>]}} is non empty set
T `2_3 is set
K13(T) is set
K13(T) `3_3 is set
p is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
p /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
T is Element of ()
p is Element of Segm 9
f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
f2 is Element of ()
<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
[p,<*f1*>,<*f2*>] is V1() V2() set
[p,<*f1*>] is V1() set
{p,<*f1*>} is non empty set
{p} is non empty trivial 1 -element set
{{p,<*f1*>},{p}} is non empty set
[[p,<*f1*>],<*f2*>] is V1() set
{[p,<*f1*>],<*f2*>} is non empty set
{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set
T `2_3 is set
K13(T) is set
K13(T) `3_3 is set
<*f1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,i1] is V1() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set
J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*i1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
a is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*a*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,a] is V1() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set
K is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*a*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
T `3_3 is set
<*f2*> /. 1 is Element of ()
i1 is Element of ()
<*i1*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,i1] is V1() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set
J is Element of ()
<*i1*> /. 1 is Element of ()
a is Element of ()
<*a*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,a] is V1() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set
K is Element of ()
<*a*> /. 1 is Element of ()
T is Element of ()
(T) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
(T) is Element of ()
f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f1] is V1() set
{1,f1} is non empty set
{{1,f1},{1}} is non empty set
{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
f2 is Element of ()
<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
p is Element of Segm 9
[p,<*f1*>,<*f2*>] is V1() V2() set
[p,<*f1*>] is V1() set
{p,<*f1*>} is non empty set
{p} is non empty trivial 1 -element set
{{p,<*f1*>},{p}} is non empty set
[[p,<*f1*>],<*f2*>] is V1() set
{[p,<*f1*>],<*f2*>} is non empty set
{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set
T `2_3 is set
K13(T) is set
K13(T) `3_3 is set
J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,J] is V1() set
{1,J} is non empty set
{{1,J},{1}} is non empty set
{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set
<*J*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
T `3_3 is set
K is Element of ()
<*K*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,K] is V1() set
{1,K} is non empty set
{{1,K},{1}} is non empty set
{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set
<*K*> /. 1 is Element of ()
NAT * is non empty functional FinSequence-membered set
proj2 () is set
[:NAT,(NAT *),(proj2 ()):] is set
T is set
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,{}] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],{}] is V1() set
{[f1,<*f2*>],{}} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
p is Element of ()
<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,<*p*>] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],<*p*>] is V1() set
{[f1,<*f2*>],<*p*>} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set
f1 is Element of Segm 9
f2 is Element of ()
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
T is set
f1 is set
[f1,T] is V1() set
{f1,T} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,T},{f1}} is non empty set
p is Element of Segm 9
J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,J] is V1() set
{1,J} is non empty set
{{1,J},{1}} is non empty set
{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set
[p,<*J*>,{}] is V1() V2() set
[p,<*J*>] is V1() set
{p,<*J*>} is non empty set
{p} is non empty trivial 1 -element set
{{p,<*J*>},{p}} is non empty set
[[p,<*J*>],{}] is V1() set
{[p,<*J*>],{}} is non empty set
{[p,<*J*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,<*J*>],{}},{[p,<*J*>]}} is non empty set
p is Element of Segm 9
J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,J] is V1() set
{1,J} is non empty set
{{1,J},{1}} is non empty set
{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set
K is Element of ()
<*K*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,K] is V1() set
{1,K} is non empty set
{{1,K},{1}} is non empty set
{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set
[p,<*J*>,<*K*>] is V1() V2() set
[p,<*J*>] is V1() set
{p,<*J*>} is non empty set
{p} is non empty trivial 1 -element set
{{p,<*J*>},{p}} is non empty set
[[p,<*J*>],<*K*>] is V1() set
{[p,<*J*>],<*K*>} is non empty set
{[p,<*J*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,<*J*>],<*K*>},{[p,<*J*>]}} is non empty set
p is Element of Segm 9
J is Element of ()
K is Element of ()
<*J,K*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*J*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,J] is V1() set
{1,J} is non empty set
{{1,J},{1}} is non empty set
{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set
<*K*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,K] is V1() set
{1,K} is non empty set
{{1,K},{1}} is non empty set
{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*J*>,<*K*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},<*J,K*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty trivial 1 -element set
{{p,{}},{p}} is non empty set
[[p,{}],<*J,K*>] is V1() set
{[p,{}],<*J,K*>} is non empty set
{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,{}],<*J,K*>},{[p,{}]}} is non empty set
T is Element of ()
T `1_3 is set
K13(T) is set
K13(K13(T)) is set
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,{}] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],{}] is V1() set
{[f1,<*f2*>],{}} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
p is Element of ()
<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,<*p*>] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],<*p*>] is V1() set
{[f1,<*f2*>],<*p*>} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set
f1 is Element of Segm 9
f2 is Element of ()
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
T is non empty set
T * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(T *):] is set
T is Element of ()
InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K13(T) is set
K13(K13(T)) is set
T is Element of ()
InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K13(T) is set
K13(K13(T)) is set
T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(T) `3_3 is set
f1 is Element of Segm 9
f2 is Element of ()
p is Element of ()
<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[f1,{},<*f2,p*>] is V1() V2() set
[f1,{}] is V1() set
{f1,{}} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,{}},{f1}} is non empty set
[[f1,{}],<*f2,p*>] is V1() set
{[f1,{}],<*f2,p*>} is non empty set
{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K13(T) is set
K13(K13(T)) is set
T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(T) `3_3 is set
dom (T `2_3) is Element of bool NAT
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
p is Element of ()
<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,p] is V1() set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,<*p*>] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],<*p*>] is V1() set
{[f1,<*f2*>],<*p*>} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K13(T) is set
K13(K13(T)) is set
T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(T) `3_3 is set
dom (T `2_3) is Element of bool NAT
f1 is Element of Segm 9
f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,f2] is V1() set
{1,f2} is non empty set
{{1,f2},{1}} is non empty set
{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
[f1,<*f2*>,{}] is V1() V2() set
[f1,<*f2*>] is V1() set
{f1,<*f2*>} is non empty set
{f1} is non empty trivial 1 -element set
{{f1,<*f2*>},{f1}} is non empty set
[[f1,<*f2*>],{}] is V1() set
{[f1,<*f2*>],{}} is non empty set
{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set
T is Element of ()
InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
K13(T) is set
K13(K13(T)) is set
f1 is Element of ()
InsCode f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(f1) is set
K13(K13(f1)) is set
T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(T) `3_3 is set
dom (T `2_3) is Element of bool NAT
f1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(f1) `3_3 is set
dom (f1 `2_3) is Element of bool NAT
InsCodes () is non empty set
K23(()) is set
proj1 () is non empty set
proj1 (proj1 ()) is set
T is Element of InsCodes ()
f1 is set
[T,f1] is V1() set
{T,f1} is non empty set
{T} is non empty trivial 1 -element set
{{T,f1},{T}} is non empty set
f2 is set
[[T,f1],f2] is V1() set
{[T,f1],f2} is non empty set
{[T,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,f1],f2},{[T,f1]}} is non empty set
[T,f1,f2] is V1() V2() set
p is Element of ()
InsCode p is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(p) is set
K13(K13(p)) is set
{0} is non empty trivial functional 1 -element Element of bool NAT
T is Element of InsCodes ()
JumpParts T is non empty functional set
{ (b<sub>1</sub> `2_3) where b₁ is Element of () : InsCode b₁ = T } is set
f1 is set
f2 is Element of ()
f2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(f2) is set
K13(f2) `3_3 is set
InsCode f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(K13(f2)) is set
f1 is set
[(),{},{}] `2_3 is set
K13([(),{},{}]) is set
K13([(),{},{}]) `3_3 is set
[(),{},{}] `1_3 is set
K13(K13([(),{},{}])) is set
{{}} is non empty trivial functional 1 -element set
T is Element of InsCodes ()
JumpParts T is non empty functional set
{ (b<sub>1</sub> `2_3) where b₁ is Element of () : InsCode b₁ = T } is set
f1 is set
f2 is Element of ()
f2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(f2) is set
K13(f2) `3_3 is set
InsCode f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(K13(f2)) is set
p is Element of Segm 9
J is Element of ()
K is Element of ()
<*J,K*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<*J*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,J] is V1() set
{1,J} is non empty set
{{1,J},{1}} is non empty set
{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set
<*K*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1,K] is V1() set
{1,K} is non empty set
{{1,K},{1}} is non empty set
{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<*J*>,<*K*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[p,{},<*J,K*>] is V1() V2() set
[p,{}] is V1() set
{p,{}} is non empty set
{p} is non empty trivial 1 -element set
{{p,{}},{p}} is non empty set
[[p,{}],<*J,K*>] is V1() set
{[p,{}],<*J,K*>} is non empty set
{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[p,{}],<*J,K*>},{[p,{}]}} is non empty set
the Element of () is Element of ()
f2 is set
<* the Element of (), the Element of ()*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()
<* the Element of ()*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set
[1, the Element of ()] is V1() set
{1, the Element of ()} is non empty set
{{1, the Element of ()},{1}} is non empty set
{[1, the Element of ()]} is non empty trivial Relation-like Function-like constant 1 -element set
K116(<* the Element of ()*>,<* the Element of ()*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set
[T,{},<* the Element of (), the Element of ()*>] is V1() V2() set
[T,{}] is V1() set
{T,{}} is non empty set
{T} is non empty trivial 1 -element set
{{T,{}},{T}} is non empty set
[[T,{}],<* the Element of (), the Element of ()*>] is V1() set
{[T,{}],<* the Element of (), the Element of ()*>} is non empty set
{[T,{}]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,{}],<* the Element of (), the Element of ()*>},{[T,{}]}} is non empty set
[T,{},<* the Element of (), the Element of ()*>] `2_3 is set
K13([T,{},<* the Element of (), the Element of ()*>]) is set
K13([T,{},<* the Element of (), the Element of ()*>]) `3_3 is set
[T,{},<* the Element of (), the Element of ()*>] `1_3 is set
K13(K13([T,{},<* the Element of (), the Element of ()*>])) is set
T is Element of InsCodes ()
JumpParts T is non empty functional set
{ (b<sub>1</sub> `2_3) where b₁ is Element of () : InsCode b₁ = T } is set
f1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 f1 is set
f2 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 f2 is set
p is set
[T,f1,p] is V1() V2() set
[T,f1] is V1() set
{T,f1} is non empty set
{T} is non empty trivial 1 -element set
{{T,f1},{T}} is non empty set
[[T,f1],p] is V1() set
{[T,f1],p} is non empty set
{[T,f1]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,f1],p},{[T,f1]}} is non empty set
[T,f2,p] is V1() V2() set
[T,f2] is V1() set
{T,f2} is non empty set
{{T,f2},{T}} is non empty set
[[T,f2],p] is V1() set
{[T,f2],p} is non empty set
{[T,f2]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,f2],p},{[T,f2]}} is non empty set
J is Element of ()
InsCode J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(J) is set
K13(K13(J)) is set
K is Element of Segm 9
i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,i1] is V1() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set
[K,<*i1*>,{}] is V1() V2() set
[K,<*i1*>] is V1() set
{K,<*i1*>} is non empty set
{K} is non empty trivial 1 -element set
{{K,<*i1*>},{K}} is non empty set
[[K,<*i1*>],{}] is V1() set
{[K,<*i1*>],{}} is non empty set
{[K,<*i1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[K,<*i1*>],{}},{[K,<*i1*>]}} is non empty set
f2 . 1 is V17() V18() V19() V23() V24() cardinal V39() V41() V42() ext-real set
[T,f2,{}] is V1() V2() set
[[T,f2],{}] is V1() set
{[T,f2],{}} is non empty set
{{[T,f2],{}},{[T,f2]}} is non empty set
a is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*a*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,a] is V1() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set
[6,<*a*>,{}] is V1() V2() set
[6,<*a*>] is V1() set
{6,<*a*>} is non empty set
{6} is non empty trivial 1 -element set
{{6,<*a*>},{6}} is non empty set
[[6,<*a*>],{}] is V1() set
{[6,<*a*>],{}} is non empty set
{[6,<*a*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[6,<*a*>],{}},{[6,<*a*>]}} is non empty set
I is Element of ()
I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set
K13(I) is set
K13(I) `3_3 is set
J is Element of ()
InsCode J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(J) is set
K13(K13(J)) is set
K is Element of Segm 9
i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,i1] is V1() set
{1,i1} is non empty set
{{1,i1},{1}} is non empty set
{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set
a is Element of ()
<*a*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,a] is V1() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set
[K,<*i1*>,<*a*>] is V1() V2() set
[K,<*i1*>] is V1() set
{K,<*i1*>} is non empty set
{K} is non empty trivial 1 -element set
{{K,<*i1*>},{K}} is non empty set
[[K,<*i1*>],<*a*>] is V1() set
{[K,<*i1*>],<*a*>} is non empty set
{[K,<*i1*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[K,<*i1*>],<*a*>},{[K,<*i1*>]}} is non empty set
f2 . 1 is V17() V18() V19() V23() V24() cardinal V39() V41() V42() ext-real set
l is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*l*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,l] is V1() set
{1,l} is non empty set
{{1,l},{1}} is non empty set
{[1,l]} is non empty trivial Relation-like Function-like constant 1 -element set
[T,<*l*>,<*a*>] is V1() V2() set
[T,<*l*>] is V1() set
{T,<*l*>} is non empty set
{{T,<*l*>},{T}} is non empty set
[[T,<*l*>],<*a*>] is V1() set
{[T,<*l*>],<*a*>} is non empty set
{[T,<*l*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,<*l*>],<*a*>},{[T,<*l*>]}} is non empty set
I is Element of ()
InsCode I is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()
K13(I) is set
K13(K13(I)) is set
L is Element of Segm 9
i2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT
<*i2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT
[1,i2] is V1() set
{1,i2} is non empty set
{{1,i2},{1}} is non empty set
{[1,i2]} is non empty trivial Relation-like Function-like constant 1 -element set
b is Element of ()
<*b*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()
[1,b] is V1() set
{1,b} is non empty set
{{1,b},{1}} is non empty set
{[1,b]} is non empty trivial Relation-like Function-like constant 1 -element set
[L,<*i2*>,<*b*>] is V1() V2() set
[L,<*i2*>] is V1() set
{L,<*i2*>} is non empty set
{L} is non empty trivial 1 -element set
{{L,<*i2*>},{L}} is non empty set
[[L,<*i2*>],<*b*>] is V1() set
{[L,<*i2*>],<*b*>} is non empty set
{[L,<*i2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[L,<*i2*>],<*b*>},{[L,<*i2*>]}} is non empty set
[T,<*i2*>,<*b*>] is V1() V2() set
[T,<*i2*>] is V1() set
{T,<*i2*>} is non empty set
{{T,<*i2*>},{T}} is non empty set
[[T,<*i2*>],<*b*>] is V1() set
{[T,<*i2*>],<*b*>} is non empty set
{[T,<*i2*>]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[T,<*i2*>],<*b*>},{[T,<*i2*>]}} is non empty set