:: SCM_COMP semantic presentation

REAL is non empty V28() set
NAT is non empty V21() V22() V23() Element of bool REAL
bool REAL is non empty set
NAT is non empty V21() V22() V23() set
bool NAT is non empty set
bool NAT is non empty set
{} is Function-like functional empty V21() V22() V23() V25() V26() V27() FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees V86() V87() ext-real integer set
the Function-like functional empty V21() V22() V23() V25() V26() V27() FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees V86() V87() ext-real integer set is Function-like functional empty V21() V22() V23() V25() V26() V27() FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees V86() V87() ext-real integer set
1 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is non empty set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of PeanoNat is non empty set
FinTrees the carrier of PeanoNat is functional non empty constituted-DTrees DTree-set of the carrier of PeanoNat
TS PeanoNat is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)
bool (FinTrees the carrier of PeanoNat) is non empty set
[:(TS PeanoNat),NAT:] is non empty set
bool [:(TS PeanoNat),NAT:] is non empty set
[:NAT,(TS PeanoNat):] is non empty set
bool [:NAT,(TS PeanoNat):] is non empty set
COMPLEX is non empty V28() set
RAT is non empty V28() set
INT is non empty V28() set
2 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
9 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
Segm 9 is Element of bool NAT
K434() is set
K267(NAT,1) is non empty V127() V128() Element of bool NAT
[:K267(NAT,1),NAT:] is V1() V4( NAT ) V5( REAL ) non empty Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty set
bool [:NAT,REAL:] is non empty set
SCM-Memory is set
bool SCM-Memory is non empty set
[:SCM-Memory,2:] is set
bool [:SCM-Memory,2:] is non empty set
SCM-OK is V1() V4( SCM-Memory ) V5(2) Function-like V14( SCM-Memory ) quasi_total Element of bool [:SCM-Memory,2:]
SCM-VAL is V1() V4(2) Function-like V14(2) set
SCM-VAL * SCM-OK is V1() Function-like set
K287((SCM-VAL * SCM-OK)) is set
K435() is non empty set
Funcs (K287((SCM-VAL * SCM-OK)),K287((SCM-VAL * SCM-OK))) is functional non empty set
[:K435(),(Funcs (K287((SCM-VAL * SCM-OK)),K287((SCM-VAL * SCM-OK)))):] is non empty set
bool [:K435(),(Funcs (K287((SCM-VAL * SCM-OK)),K287((SCM-VAL * SCM-OK)))):] is non empty set
SCM is non empty V146(2) IC-Ins-separated strict strict V154(2) AMI-Struct over 2
the InstructionsF of SCM is V1() non empty V135() V136() V137() V139() set
the carrier of SCM is non empty set
K529(2,SCM) is V1() non-empty V4( the carrier of SCM) Function-like V14( the carrier of SCM) set
3 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
0 is Function-like functional empty V21() V22() V23() V25() V26() V27() FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees V86() V87() ext-real integer Element of NAT
4 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
Seg 1 is non empty V28() 1 -element Element of bool NAT
{1} is non empty V127() V128() set
Seg 2 is non empty V28() 2 -element Element of bool NAT
{1,2} is non empty V127() V128() set
NonZero SCM is Element of bool the carrier of SCM
bool the carrier of SCM is non empty set
SCM-Data-Loc is Element of bool SCM-Memory
K165(0) is non empty V41() finite-order binary set
{{}} is non empty set
{ b₁ where b₁ is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT : not 1 <= b₁ } is set
5 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT
{ b₁ where b₁ is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT : not 5 <= b₁ } is set
[:1,5:] is non empty set
SCM-Data-Loc \/ [:1,5:] is non empty set
nt0 is non empty strict binary DTConstrStr
the carrier of nt0 is non empty set
NonTerminals nt0 is set
{ b₁ where b₁ is Element of the carrier of nt0 : ex b₂ being V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
nt1 is set
nt2 is Element of the carrier of nt0
nt3 is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
nt3 is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
nt4 is Element of the carrier of nt0
i2i is Element of the carrier of nt0
<*nt4,i2i*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
nt1 is set
nt2 is Element of the carrier of nt0
<*nt2,nt2*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
Terminals nt0 is set
{ b₁ where b₁ is Element of the carrier of nt0 : for b₂ being V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
nt1 is set
nt2 is Element of the carrier of nt0
<*nt2,nt2*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
nt1 is set
nt2 is Element of the carrier of nt0
nt3 is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
nt4 is Element of the carrier of nt0
i2i is Element of the carrier of nt0
<*nt4,i2i*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
nt4 is set
i2i is set
[nt4,i2i] is V15() set
{nt4,i2i} is non empty set
{nt4} is non empty set
{{nt4,i2i},{nt4}} is non empty V127() V128() set
[0,i2i] is V15() set
{0,i2i} is non empty set
{0} is non empty set
{{0,i2i},{0}} is non empty V127() V128() set
Term is set
f is set
[Term,f] is V15() set
{Term,f} is non empty set
{Term} is non empty set
{{Term,f},{Term}} is non empty V127() V128() set
dl. 1 is Int-like Element of the carrier of SCM
[1,1] is V15() set
{1,1} is non empty V127() V128() set
{{1,1},{1}} is non empty V127() V128() set
dl. 0 is Int-like Element of the carrier of SCM
[1,0] is V15() set
{1,0} is non empty set
{{1,0},{1}} is non empty V127() V128() set
nt2 is Element of the carrier of nt0
root-tree nt2 is V1() V5( the carrier of nt0) Function-like DecoratedTree-like Element of FinTrees the carrier of nt0
FinTrees the carrier of nt0 is functional non empty constituted-DTrees DTree-set of the carrier of nt0
TS nt0 is functional constituted-DTrees Element of bool (FinTrees the carrier of nt0)
bool (FinTrees the carrier of nt0) is non empty set
nt1 is Element of the carrier of nt0
root-tree nt1 is V1() V5( the carrier of nt0) Function-like DecoratedTree-like Element of FinTrees the carrier of nt0
<*(root-tree nt1),(root-tree nt2)*> is V1() V4( NAT ) V5( FinTrees the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like DTree-yielding M20( FinTrees the carrier of nt0,K205((FinTrees the carrier of nt0)))
K205((FinTrees the carrier of nt0)) is functional non empty FinSequence-membered M19( FinTrees the carrier of nt0)
nt4 is Element of the carrier of nt0
nt3 is V1() V4( NAT ) V5( TS nt0) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of TS nt0
i2i is V1() V4( NAT ) V5( TS nt0) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of TS nt0
roots i2i is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
(root-tree nt1) . {} is set
(root-tree nt2) . {} is set
<*((root-tree nt1) . {}),((root-tree nt2) . {})*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
<*((root-tree nt1) . {}),nt2*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
<*nt1,nt2*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
nt0 is non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr
Terminals nt0 is non empty Element of bool the carrier of nt0
the carrier of nt0 is non empty set
bool the carrier of nt0 is non empty set
NonTerminals nt0 is non empty Element of bool the carrier of nt0
nt1 is non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr
Terminals nt1 is non empty Element of bool the carrier of nt1
the carrier of nt1 is non empty set
bool the carrier of nt1 is non empty set
NonTerminals nt1 is non empty Element of bool the carrier of nt1
(Terminals nt0) \/ (NonTerminals nt0) is non empty Element of bool the carrier of nt0
the Rules of nt0 is V1() V4( the carrier of nt0) V5(K205( the carrier of nt0)) Element of bool [: the carrier of nt0,K205( the carrier of nt0):]
K205( the carrier of nt0) is functional non empty FinSequence-membered M19( the carrier of nt0)
[: the carrier of nt0,K205( the carrier of nt0):] is non empty set
bool [: the carrier of nt0,K205( the carrier of nt0):] is non empty set
the Rules of nt1 is V1() V4( the carrier of nt1) V5(K205( the carrier of nt1)) Element of bool [: the carrier of nt1,K205( the carrier of nt1):]
K205( the carrier of nt1) is functional non empty FinSequence-membered M19( the carrier of nt1)
[: the carrier of nt1,K205( the carrier of nt1):] is non empty set
bool [: the carrier of nt1,K205( the carrier of nt1):] is non empty set
nt4 is set
i2i is set
[nt4,i2i] is V15() set
{nt4,i2i} is non empty set
{nt4} is non empty set
{{nt4,i2i},{nt4}} is non empty V127() V128() set
the carrier of nt0 * is functional non empty FinSequence-membered set
Term is Element of the carrier of nt0
f is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of nt0 *
F is Element of the carrier of nt0
term is Element of the carrier of nt0
<*F,term*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
aux is Element of the carrier of nt1
n is Element of the carrier of nt1
s is Element of the carrier of nt1
<*n,s*> is V1() V4( NAT ) V5( the carrier of nt1) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt1,K205( the carrier of nt1))
the carrier of nt1 * is functional non empty FinSequence-membered set
Term is Element of the carrier of nt1
f is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of nt1 *
F is Element of the carrier of nt1
term is Element of the carrier of nt1
<*F,term*> is V1() V4( NAT ) V5( the carrier of nt1) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt1,K205( the carrier of nt1))
aux is Element of the carrier of nt0
n is Element of the carrier of nt0
s is Element of the carrier of nt0
<*n,s*> is V1() V4( NAT ) V5( the carrier of nt0) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of nt0,K205( the carrier of nt0))
() is non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr
NonTerminals () is non empty Element of bool the carrier of ()
the carrier of () is non empty set
bool the carrier of () is non empty set
FinTrees the carrier of () is functional non empty constituted-DTrees DTree-set of the carrier of ()
TS () is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of ())
bool (FinTrees the carrier of ()) is non empty set
nt0 is Element of NonTerminals ()
nt1 is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
nt2 is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
nt0 -tree (nt1,nt2) is V1() Function-like DecoratedTree-like set
root-label nt1 is Element of the carrier of ()
root-label nt2 is Element of the carrier of ()
<*(root-label nt1),(root-label nt2)*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
<*nt1,nt2*> is V1() V4( NAT ) V5( TS ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like DTree-yielding M20( TS (),K205((TS ())))
K205((TS ())) is functional non empty FinSequence-membered M19( TS ())
roots <*nt1,nt2*> is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
nt0 -tree <*nt1,nt2*> is V1() Function-like DecoratedTree-like set
Terminals () is non empty Element of bool the carrier of ()
nt0 is Element of Terminals ()
root-tree nt0 is V1() Function-like DecoratedTree-like set
nt0 is Element of Terminals ()
nt1 is Element of SCM-Data-Loc
nt2 is Element of the carrier of SCM
[0,0] is V15() set
{0,0} is non empty set
{0} is non empty set
{{0,0},{0}} is non empty V127() V128() set
[0,1] is V15() set
{0,1} is non empty set
{{0,1},{0}} is non empty V127() V128() set
[0,2] is V15() set
{0,2} is non empty set
{{0,2},{0}} is non empty V127() V128() set
[0,3] is V15() set
{0,3} is non empty set
{{0,3},{0}} is non empty V127() V128() set
[0,4] is V15() set
{0,4} is non empty set
{{0,4},{0}} is non empty V127() V128() set
nt0 is Element of NonTerminals ()
nt1 is set
nt2 is set
[nt1,nt2] is V15() set
{nt1,nt2} is non empty set
{nt1} is non empty set
{{nt1,nt2},{nt1}} is non empty V127() V128() set
nt3 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
4 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i2i is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,0] -tree (i2i,Term) is V1() Function-like DecoratedTree-like set
nt0 is Element of NonTerminals ()
(nt0,i2i,Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,1] -tree (i2i,Term) is V1() Function-like DecoratedTree-like set
nt1 is Element of NonTerminals ()
(nt1,i2i,Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,2] -tree (i2i,Term) is V1() Function-like DecoratedTree-like set
nt2 is Element of NonTerminals ()
(nt2,i2i,Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,3] -tree (i2i,Term) is V1() Function-like DecoratedTree-like set
nt3 is Element of NonTerminals ()
(nt3,i2i,Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,4] -tree (i2i,Term) is V1() Function-like DecoratedTree-like set
nt4 is Element of NonTerminals ()
(nt4,i2i,Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
i2i is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label i2i is Element of the carrier of ()
i2i . {} is set
(Terminals ()) \/ (NonTerminals ()) is non empty Element of bool the carrier of ()
Term is Element of Terminals ()
(Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term is Element of NonTerminals ()
f is V1() V4( NAT ) V5( TS ()) Function-like V28() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS ()
Term -tree f is V1() Function-like DecoratedTree-like set
roots f is V1() V4( NAT ) Function-like V28() FinSequence-like FinSubsequence-like set
len (roots f) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is Element of the carrier of ()
term is Element of the carrier of ()
<*F,term*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
dom (roots f) is Element of bool NAT
dom f is Element of bool NAT
f . 2 is V1() Function-like set
(roots f) . 2 is set
F is V1() Function-like DecoratedTree-like set
F . {} is set
f . 1 is V1() Function-like set
(roots f) . 1 is set
term is V1() Function-like DecoratedTree-like set
term . {} is set
len f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
n is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
<*aux,n*> is V1() V4( NAT ) V5( TS ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like DTree-yielding M20( TS (),K205((TS ())))
K205((TS ())) is functional non empty FinSequence-membered M19( TS ())
(Term,aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,0] -tree (aux,n) is V1() Function-like DecoratedTree-like set
(aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,1] -tree (aux,n) is V1() Function-like DecoratedTree-like set
(aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,2] -tree (aux,n) is V1() Function-like DecoratedTree-like set
(aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,3] -tree (aux,n) is V1() Function-like DecoratedTree-like set
(aux,n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,4] -tree (aux,n) is V1() Function-like DecoratedTree-like set
i2i is Element of NonTerminals ()
Term is V86() V87() ext-real integer set
f is V86() V87() ext-real integer set
Term + f is V86() V87() ext-real integer set
Term - f is V86() V87() ext-real integer set
Term * f is V86() V87() ext-real integer set
Term div f is V86() V87() ext-real integer set
Term mod f is V86() V87() ext-real integer set
[0,2] `2 is set
[0,3] `2 is set
[0,0] `2 is set
[0,1] `2 is set
F is V86() V87() ext-real integer set
term is V86() V87() ext-real integer set
aux is V86() V87() ext-real integer set
n is V86() V87() ext-real integer set
s is V86() V87() ext-real integer set
i is V86() V87() ext-real integer set
u is V86() V87() ext-real integer set
dn is V86() V87() ext-real integer set
u1 is V86() V87() ext-real integer set
i2 is V86() V87() ext-real integer set
i2i is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Term is Element of Terminals ()
i2i . Term is set
(Term) is Int-like Element of the carrier of SCM
i2i . (Term) is V86() V87() ext-real integer set
i2i is non empty set
[:INT,i2i:] is non empty set
bool [:INT,i2i:] is non empty set
Term is V1() V4( INT ) V5(i2i) Function-like non empty V14( INT ) quasi_total Element of bool [:INT,i2i:]
f is V86() V87() ext-real integer set
Term . f is set
F is V86() V87() ext-real integer Element of INT
Term . F is Element of i2i
id INT is V1() V4( INT ) V5( INT ) Function-like one-to-one non empty V14( INT ) quasi_total Element of bool [:INT,INT:]
[:INT,INT:] is non empty set
bool [:INT,INT:] is non empty set
[:(TS ()),INT:] is non empty set
bool [:(TS ()),INT:] is non empty set
f is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
F is V1() V4( TS ()) V5( INT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),INT:]
F . f is V86() V87() ext-real integer Element of INT
term is V86() V87() ext-real integer Element of INT
aux is Element of Terminals ()
Term . aux is V86() V87() ext-real integer set
(INT,(id INT),(Term . aux)) is V86() V87() ext-real integer Element of INT
(aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
F . (aux) is V86() V87() ext-real integer Element of INT
aux is Element of NonTerminals ()
n is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label n is Element of the carrier of ()
s is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label s is Element of the carrier of ()
F . n is V86() V87() ext-real integer Element of INT
F . s is V86() V87() ext-real integer Element of INT
(aux,n,s) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
F . (aux,n,s) is V86() V87() ext-real integer Element of INT
i is Element of the carrier of ()
u is Element of the carrier of ()
<*i,u*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
dn is V86() V87() ext-real integer Element of INT
u1 is V86() V87() ext-real integer Element of INT
(aux,dn,u1) is V86() V87() ext-real integer set
(INT,(id INT),(aux,dn,u1)) is V86() V87() ext-real integer Element of INT
F is V86() V87() ext-real integer set
term is V86() V87() ext-real integer set
aux is V1() V4( TS ()) V5( INT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),INT:]
aux . f is V86() V87() ext-real integer Element of INT
n is Element of Terminals ()
Term . n is V86() V87() ext-real integer set
(INT,(id INT),(Term . n)) is V86() V87() ext-real integer Element of INT
(n) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
aux . (n) is V86() V87() ext-real integer Element of INT
u is Element of the carrier of ()
s is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label s is Element of the carrier of ()
dn is Element of the carrier of ()
i is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label i is Element of the carrier of ()
n is Element of NonTerminals ()
<*u,dn*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
u1 is V86() V87() ext-real integer Element of INT
aux . s is V86() V87() ext-real integer Element of INT
i2 is V86() V87() ext-real integer Element of INT
aux . i is V86() V87() ext-real integer Element of INT
(n,u1,i2) is V86() V87() ext-real integer set
(INT,(id INT),(n,u1,i2)) is V86() V87() ext-real integer Element of INT
(n,s,i) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
aux . (n,s,i) is V86() V87() ext-real integer Element of INT
n is V1() V4( TS ()) V5( INT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),INT:]
n . f is V86() V87() ext-real integer Element of INT
s is Element of Terminals ()
Term . s is V86() V87() ext-real integer set
(INT,(id INT),(Term . s)) is V86() V87() ext-real integer Element of INT
(s) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
n . (s) is V86() V87() ext-real integer Element of INT
dn is Element of the carrier of ()
i is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label i is Element of the carrier of ()
u1 is Element of the carrier of ()
u is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label u is Element of the carrier of ()
s is Element of NonTerminals ()
<*dn,u1*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
i2 is V86() V87() ext-real integer Element of INT
n . i is V86() V87() ext-real integer Element of INT
u2 is V86() V87() ext-real integer Element of INT
n . u is V86() V87() ext-real integer Element of INT
(s,i2,u2) is V86() V87() ext-real integer set
(INT,(id INT),(s,i2,u2)) is V86() V87() ext-real integer Element of INT
(s,i,u) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
n . (s,i,u) is V86() V87() ext-real integer Element of INT
Term is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
f is Element of Terminals ()
(f) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(Term,(f)) is V86() V87() ext-real integer set
Term . f is V86() V87() ext-real integer set
F is V1() V4( TS ()) V5( INT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),INT:]
F . (f) is V86() V87() ext-real integer Element of INT
Term is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
f is Element of NonTerminals ()
F is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(f,F,term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(Term,(f,F,term)) is V86() V87() ext-real integer set
(Term,F) is V86() V87() ext-real integer set
(Term,term) is V86() V87() ext-real integer set
(f,(Term,F),(Term,term)) is V86() V87() ext-real integer set
aux is V1() V4( TS ()) V5( INT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),INT:]
aux . (f,F,term) is V86() V87() ext-real integer Element of INT
root-label F is Element of the carrier of ()
root-label term is Element of the carrier of ()
<*(root-label F),(root-label term)*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
aux . F is V86() V87() ext-real integer Element of INT
aux . term is V86() V87() ext-real integer Element of INT
Term is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
f is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
F is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,0] -tree (f,F) is V1() Function-like DecoratedTree-like set
(Term,(f,F)) is V86() V87() ext-real integer set
(Term,f) is V86() V87() ext-real integer set
(Term,F) is V86() V87() ext-real integer set
(Term,f) + (Term,F) is V86() V87() ext-real integer set
(f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,1] -tree (f,F) is V1() Function-like DecoratedTree-like set
(Term,(f,F)) is V86() V87() ext-real integer set
(Term,f) - (Term,F) is V86() V87() ext-real integer set
(f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,2] -tree (f,F) is V1() Function-like DecoratedTree-like set
(Term,(f,F)) is V86() V87() ext-real integer set
(Term,f) * (Term,F) is V86() V87() ext-real integer set
(f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,3] -tree (f,F) is V1() Function-like DecoratedTree-like set
(Term,(f,F)) is V86() V87() ext-real integer set
(Term,f) div (Term,F) is V86() V87() ext-real integer set
(f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
[0,4] -tree (f,F) is V1() Function-like DecoratedTree-like set
(Term,(f,F)) is V86() V87() ext-real integer set
(Term,f) mod (Term,F) is V86() V87() ext-real integer set
nt0 is Element of NonTerminals ()
(nt0,(Term,f),(Term,F)) is V86() V87() ext-real integer set
nt1 is Element of NonTerminals ()
(nt1,(Term,f),(Term,F)) is V86() V87() ext-real integer set
nt2 is Element of NonTerminals ()
(nt2,(Term,f),(Term,F)) is V86() V87() ext-real integer set
nt3 is Element of NonTerminals ()
(nt3,(Term,f),(Term,F)) is V86() V87() ext-real integer set
nt4 is Element of NonTerminals ()
(nt4,(Term,f),(Term,F)) is V86() V87() ext-real integer set
Term is Element of NonTerminals ()
f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. f is Int-like Element of the carrier of SCM
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty V127() V128() set
f + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. (f + 1) is Int-like Element of the carrier of SCM
[1,(f + 1)] is V15() set
{1,(f + 1)} is non empty set
{{1,(f + 1)},{1}} is non empty V127() V128() set
AddTo ((dl. f),(dl. (f + 1))) is Element of the InstructionsF of SCM
<*(dl. f),(dl. (f + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[2,{},<*(dl. f),(dl. (f + 1))*>] is V15() V16() set
[2,{}] is V15() set
{2,{}} is non empty set
{2} is non empty V127() V128() set
{{2,{}},{2}} is non empty V127() V128() set
[[2,{}],<*(dl. f),(dl. (f + 1))*>] is V15() set
{[2,{}],<*(dl. f),(dl. (f + 1))*>} is non empty set
{[2,{}]} is Function-like non empty set
{{[2,{}],<*(dl. f),(dl. (f + 1))*>},{[2,{}]}} is non empty V127() V128() set
<%(AddTo ((dl. f),(dl. (f + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(AddTo ((dl. f),(dl. (f + 1))))) is set
SubFrom ((dl. f),(dl. (f + 1))) is Element of the InstructionsF of SCM
[3,{},<*(dl. f),(dl. (f + 1))*>] is V15() V16() set
[3,{}] is V15() set
{3,{}} is non empty set
{3} is non empty V127() V128() set
{{3,{}},{3}} is non empty V127() V128() set
[[3,{}],<*(dl. f),(dl. (f + 1))*>] is V15() set
{[3,{}],<*(dl. f),(dl. (f + 1))*>} is non empty set
{[3,{}]} is Function-like non empty set
{{[3,{}],<*(dl. f),(dl. (f + 1))*>},{[3,{}]}} is non empty V127() V128() set
<%(SubFrom ((dl. f),(dl. (f + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(SubFrom ((dl. f),(dl. (f + 1))))) is set
MultBy ((dl. f),(dl. (f + 1))) is Element of the InstructionsF of SCM
[4,{},<*(dl. f),(dl. (f + 1))*>] is V15() V16() set
[4,{}] is V15() set
{4,{}} is non empty set
{4} is non empty V127() V128() set
{{4,{}},{4}} is non empty V127() V128() set
[[4,{}],<*(dl. f),(dl. (f + 1))*>] is V15() set
{[4,{}],<*(dl. f),(dl. (f + 1))*>} is non empty set
{[4,{}]} is Function-like non empty set
{{[4,{}],<*(dl. f),(dl. (f + 1))*>},{[4,{}]}} is non empty V127() V128() set
<%(MultBy ((dl. f),(dl. (f + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(MultBy ((dl. f),(dl. (f + 1))))) is set
Divide ((dl. f),(dl. (f + 1))) is Element of the InstructionsF of SCM
[5,{},<*(dl. f),(dl. (f + 1))*>] is V15() V16() set
[5,{}] is V15() set
{5,{}} is non empty set
{5} is non empty V127() V128() set
{{5,{}},{5}} is non empty V127() V128() set
[[5,{}],<*(dl. f),(dl. (f + 1))*>] is V15() set
{[5,{}],<*(dl. f),(dl. (f + 1))*>} is non empty set
{[5,{}]} is Function-like non empty set
{{[5,{}],<*(dl. f),(dl. (f + 1))*>},{[5,{}]}} is non empty V127() V128() set
<%(Divide ((dl. f),(dl. (f + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(Divide ((dl. f),(dl. (f + 1))))) is set
(dl. f) := (dl. (f + 1)) is Element of the InstructionsF of SCM
[1,{},<*(dl. f),(dl. (f + 1))*>] is V15() V16() set
[1,{}] is V15() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty V127() V128() set
[[1,{}],<*(dl. f),(dl. (f + 1))*>] is V15() set
{[1,{}],<*(dl. f),(dl. (f + 1))*>} is non empty set
{[1,{}]} is Function-like non empty set
{{[1,{}],<*(dl. f),(dl. (f + 1))*>},{[1,{}]}} is non empty V127() V128() set
<%(Divide ((dl. f),(dl. (f + 1)))),((dl. f) := (dl. (f + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() 2 -element initial set
<%((dl. f) := (dl. (f + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. f) := (dl. (f + 1)))) is set
<%(Divide ((dl. f),(dl. (f + 1))))%> ^ <%((dl. f) := (dl. (f + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
[0,2] `2 is set
[0,3] `2 is set
[0,0] `2 is set
[0,1] `2 is set
F is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
term is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
aux is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
n is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
s is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
i is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
u is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
dn is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
u1 is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
i2 is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
the InstructionsF of SCM ^omega is functional non empty set
[:NAT,( the InstructionsF of SCM ^omega):] is non empty set
bool [:NAT,( the InstructionsF of SCM ^omega):] is non empty set
Funcs (NAT,( the InstructionsF of SCM ^omega)) is functional non empty FUNCTION_DOMAIN of NAT , the InstructionsF of SCM ^omega
[:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):] is non empty set
bool [:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):] is non empty set
Term is V1() V4( TS ()) V5( Funcs (NAT,( the InstructionsF of SCM ^omega))) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):]
f is Element of Terminals ()
(f) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (f) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(f) is Int-like Element of the carrier of SCM
F is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F . term is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
dl. term is Int-like Element of the carrier of SCM
[1,term] is V15() set
{1,term} is non empty set
{{1,term},{1}} is non empty V127() V128() set
(dl. term) := (f) is Element of the InstructionsF of SCM
<*(dl. term),(f)*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[1,{},<*(dl. term),(f)*>] is V15() V16() set
[[1,{}],<*(dl. term),(f)*>] is V15() set
{[1,{}],<*(dl. term),(f)*>} is non empty set
{{[1,{}],<*(dl. term),(f)*>},{[1,{}]}} is non empty V127() V128() set
<%((dl. term) := (f))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. term) := (f))) is set
Down <%((dl. term) := (f))%> is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
f is Element of NonTerminals ()
F is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label F is Element of the carrier of ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
(f,F,term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (f,F,term) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . F is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
aux is Element of the carrier of ()
n is Element of the carrier of ()
<*aux,n*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
s is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
i is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
s . dn is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
i . dn is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
dn + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dn + 1) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(i . dn) ^ (u . (dn + 1)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(f,dn) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
((i . dn) ^ (u . (dn + 1))) ^ (f,dn) is V1() V4( NAT ) Function-like V25() V28() initial set
Down (f,dn) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
((i . dn) ^ (u . (dn + 1))) ^ (Down (f,dn)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
f is Element of Terminals ()
(f) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (f) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(f) is Int-like Element of the carrier of SCM
n is Element of the carrier of ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
s is Element of the carrier of ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label aux is Element of the carrier of ()
F is Element of NonTerminals ()
<*n,s*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (F,term,aux) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . aux is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term is V1() V4( TS ()) V5( Funcs (NAT,( the InstructionsF of SCM ^omega))) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):]
f is V1() V4( TS ()) V5( Funcs (NAT,( the InstructionsF of SCM ^omega))) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):]
F is Element of Terminals ()
(F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (F) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(F) is Int-like Element of the carrier of SCM
term is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term . aux is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
dl. aux is Int-like Element of the carrier of SCM
[1,aux] is V15() set
{1,aux} is non empty set
{{1,aux},{1}} is non empty V127() V128() set
(dl. aux) := (F) is Element of the InstructionsF of SCM
<*(dl. aux),(F)*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[1,{},<*(dl. aux),(F)*>] is V15() V16() set
[[1,{}],<*(dl. aux),(F)*>] is V15() set
{[1,{}],<*(dl. aux),(F)*>} is non empty set
{{[1,{}],<*(dl. aux),(F)*>},{[1,{}]}} is non empty V127() V128() set
<%((dl. aux) := (F))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. aux) := (F))) is set
Down <%((dl. aux) := (F))%> is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
F is Element of NonTerminals ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label aux is Element of the carrier of ()
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
Term . (F,term,aux) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
Term . aux is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
n is Element of the carrier of ()
s is Element of the carrier of ()
<*n,s*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
i is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
dn is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i . u1 is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
u . u1 is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
u1 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dn . (u1 + 1) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(u . u1) ^ (dn . (u1 + 1)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(F,u1) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
Down (F,u1) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
((u . u1) ^ (dn . (u1 + 1))) ^ (Down (F,u1)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
F is Element of Terminals ()
(F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
f . (F) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(F) is Int-like Element of the carrier of SCM
term is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term . aux is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
dl. aux is Int-like Element of the carrier of SCM
[1,aux] is V15() set
{1,aux} is non empty set
{{1,aux},{1}} is non empty V127() V128() set
(dl. aux) := (F) is Element of the InstructionsF of SCM
<*(dl. aux),(F)*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[1,{},<*(dl. aux),(F)*>] is V15() V16() set
[[1,{}],<*(dl. aux),(F)*>] is V15() set
{[1,{}],<*(dl. aux),(F)*>} is non empty set
{{[1,{}],<*(dl. aux),(F)*>},{[1,{}]}} is non empty V127() V128() set
<%((dl. aux) := (F))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. aux) := (F))) is set
Down <%((dl. aux) := (F))%> is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
F is Element of NonTerminals ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label aux is Element of the carrier of ()
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
f . (F,term,aux) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
f . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
f . aux is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
n is Element of the carrier of ()
s is Element of the carrier of ()
<*n,s*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
i is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
dn is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i . u1 is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
u . u1 is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
u1 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dn . (u1 + 1) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(u . u1) ^ (dn . (u1 + 1)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
(F,u1) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
Down (F,u1) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
((u . u1) ^ (dn . (u1 + 1))) ^ (Down (F,u1)) is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
() is V1() V4( TS ()) V5( Funcs (NAT,( the InstructionsF of SCM ^omega))) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),(Funcs (NAT,( the InstructionsF of SCM ^omega))):]
Term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
() . Term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(() . Term) . f is set
F is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
F . f is V1() V4( NAT ) Function-like V25() V28() initial Element of the InstructionsF of SCM ^omega
Term is Element of Terminals ()
(Term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(Term) is Int-like Element of the carrier of SCM
f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
((Term),f) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . (Term) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . (Term)) . f is set
dl. f is Int-like Element of the carrier of SCM
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty V127() V128() set
(dl. f) := (Term) is Element of the InstructionsF of SCM
<*(dl. f),(Term)*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[1,{},<*(dl. f),(Term)*>] is V15() V16() set
[[1,{}],<*(dl. f),(Term)*>] is V15() set
{[1,{}],<*(dl. f),(Term)*>} is non empty set
{{[1,{}],<*(dl. f),(Term)*>},{[1,{}]}} is non empty V127() V128() set
<%((dl. f) := (Term))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. f) := (Term))) is set
F is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
Term is Element of NonTerminals ()
f is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label f is Element of the carrier of ()
F is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label F is Element of the carrier of ()
(Term,f,F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
((Term,f,F),term) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . (Term,f,F) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . (Term,f,F)) . term is set
(f,term) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . f is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . f) . term is set
term + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(F,(term + 1)) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . F is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . F) . (term + 1) is set
(f,term) ^ (F,(term + 1)) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
(Term,term) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
((f,term) ^ (F,(term + 1))) ^ (Term,term) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
aux is Element of the carrier of ()
n is Element of the carrier of ()
<*aux,n*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
s is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
i is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
u is V1() V4( NAT ) V5( the InstructionsF of SCM ^omega ) Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,( the InstructionsF of SCM ^omega):]
Term is Element of Terminals ()
[:{1},NAT:] is non empty set
f is set
F is set
[f,F] is V15() set
{f,F} is non empty set
{f} is non empty set
{{f,F},{f}} is non empty V127() V128() set
term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. term is Int-like Element of the carrier of SCM
[1,term] is V15() set
{1,term} is non empty set
{{1,term},{1}} is non empty V127() V128() set
f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. f is Int-like Element of the carrier of SCM
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty V127() V128() set
F is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. F is Int-like Element of the carrier of SCM
[1,F] is V15() set
{1,F} is non empty set
{{1,F},{1}} is non empty V127() V128() set
[:(TS ()),NAT:] is non empty set
bool [:(TS ()),NAT:] is non empty set
Term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
f is V1() V4( TS ()) V5( NAT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),NAT:]
f . Term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term is Element of Terminals ()
(term) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
f . (term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i is Element of the carrier of ()
n is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label n is Element of the carrier of ()
u is Element of the carrier of ()
s is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label s is Element of the carrier of ()
aux is Element of NonTerminals ()
<*i,u*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f . n is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f . s is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(aux,n,s) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
f . (aux,n,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
max (dn,u1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term is V1() V4( TS ()) V5( NAT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),NAT:]
term . Term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
aux is V1() V4( TS ()) V5( NAT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),NAT:]
aux . Term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
the V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS () is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
( the V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f is V1() V4( TS ()) V5( NAT ) Function-like non empty V14( TS ()) quasi_total Element of bool [:(TS ()),NAT:]
f . the V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS () is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is Element of Terminals ()
(F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(F) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f . (F) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is Element of NonTerminals ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F,term,aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
max ((term),(aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f . term is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
f . aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
root-label term is Element of the carrier of ()
root-label aux is Element of the carrier of ()
<*(root-label term),(root-label aux)*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
f . (F,term,aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
F is Element of Terminals ()
(F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
aux is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
(term,(F)) is V86() V87() ext-real integer set
(aux,(F)) is V86() V87() ext-real integer set
(F) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. (F) is Int-like Element of the carrier of SCM
[1,(F)] is V15() set
{1,(F)} is non empty set
{{1,(F)},{1}} is non empty V127() V128() set
term . (dl. (F)) is V86() V87() ext-real integer set
aux . (dl. (F)) is V86() V87() ext-real integer set
term . F is V86() V87() ext-real integer set
aux . F is V86() V87() ext-real integer set
F is Element of NonTerminals ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label aux is Element of the carrier of ()
<*(root-label term),(root-label aux)*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
K205( the carrier of ()) is functional non empty FinSequence-membered M19( the carrier of ())
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F,term,aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
s is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
(n,(F,term,aux)) is V86() V87() ext-real integer set
(s,(F,term,aux)) is V86() V87() ext-real integer set
max ((term),(aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. dn is Int-like Element of the carrier of SCM
[1,dn] is V15() set
{1,dn} is non empty set
{{1,dn},{1}} is non empty V127() V128() set
n . (dl. dn) is V86() V87() ext-real integer set
s . (dl. dn) is V86() V87() ext-real integer set
(n,term) is V86() V87() ext-real integer set
(s,term) is V86() V87() ext-real integer set
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. dn is Int-like Element of the carrier of SCM
[1,dn] is V15() set
{1,dn} is non empty set
{{1,dn},{1}} is non empty V127() V128() set
n . (dl. dn) is V86() V87() ext-real integer set
s . (dl. dn) is V86() V87() ext-real integer set
(n,aux) is V86() V87() ext-real integer set
(s,aux) is V86() V87() ext-real integer set
(F,(n,term),(n,aux)) is V86() V87() ext-real integer set
F is Element of NonTerminals ()
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label term is Element of the carrier of ()
aux is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
root-label aux is Element of the carrier of ()
<*(root-label term),(root-label aux)*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like M20( the carrier of (),K205( the carrier of ()))
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(F,term,aux) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F,term,aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V14( NAT ) set
s is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
((F,term,aux),s) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . (F,term,aux) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . (F,term,aux)) . s is set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Shift (((F,term,aux),s),i) is V1() Function-like set
len ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer set
dl. s is Int-like Element of the carrier of SCM
[1,s] is V15() set
{1,s} is non empty set
{{1,s},{1}} is non empty V127() V128() set
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) i -started set
(u,(F,term,aux)) is V86() V87() ext-real integer set
max ((term),(aux)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
s + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(term,s) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . term) . s is set
(aux,(s + 1)) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . aux is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . aux) . (s + 1) is set
(term,s) ^ (aux,(s + 1)) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
(F,s) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
((term,s) ^ (aux,(s + 1))) ^ (F,s) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
(aux,(s + 1)) ^ (F,s) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
(term,s) ^ ((aux,(s + 1)) ^ (F,s)) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
Shift ((term,s),i) is V1() Function-like set
len (term,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (term,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
(u,term) is V86() V87() ext-real integer set
u1 is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dn + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(dn + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,dn) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,dn)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
IC u1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (dn + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u1 . (dl. s) is V86() V87() ext-real integer set
Shift (((aux,(s + 1)) ^ (F,s)),(i + (dn + 1))) is V1() Function-like set
Shift ((aux,(s + 1)),(i + (dn + 1))) is V1() Function-like set
len (aux,(s + 1)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (aux,(s + 1)) is V21() V22() V23() V27() V86() V87() ext-real integer set
dl. (s + 1) is Int-like Element of the carrier of SCM
[1,(s + 1)] is V15() set
{1,(s + 1)} is non empty set
{{1,(s + 1)},{1}} is non empty V127() V128() set
(u1,aux) is V86() V87() ext-real integer set
u2 is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
i2 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i2 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u1,(i2 + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u1,i2) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u1,i2)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(i + (dn + 1)) + i2 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
IC u2 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(i + (dn + 1)) + (i2 + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u2 . (dl. (s + 1)) is V86() V87() ext-real integer set
(dn + 1) + (i2 + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,((dn + 1) + (i2 + 1))) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. i is Int-like Element of the carrier of SCM
[1,i] is V15() set
{1,i} is non empty set
{{1,i},{1}} is non empty V127() V128() set
u . (dl. i) is V86() V87() ext-real integer set
u1 . (dl. i) is V86() V87() ext-real integer set
(u,aux) is V86() V87() ext-real integer set
(F,(u,term),(u,aux)) is V86() V87() ext-real integer set
len ((term,s) ^ (aux,(s + 1))) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 ((term,s) ^ (aux,(s + 1))) is V21() V22() V23() V27() V86() V87() ext-real integer set
(u,term) + (u,aux) is V86() V87() ext-real integer set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. s) is V86() V87() ext-real integer set
AddTo ((dl. s),(dl. (s + 1))) is Element of the InstructionsF of SCM
<*(dl. s),(dl. (s + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[2,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[2,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[2,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[2,{}],<*(dl. s),(dl. (s + 1))*>},{[2,{}]}} is non empty V127() V128() set
<%(AddTo ((dl. s),(dl. (s + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(AddTo ((dl. s),(dl. (s + 1))))) is set
len (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
((dn + 1) + (i2 + 1)) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
n . (i + i) is Element of the InstructionsF of SCM
((F,term,aux),s) . i is set
(i + i) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u2 . (dl. s) is V86() V87() ext-real integer set
(u2 . (dl. s)) + (u2 . (dl. (s + 1))) is V86() V87() ext-real integer set
(u1 . (dl. s)) + (u1,aux) is V86() V87() ext-real integer set
k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. k is Int-like Element of the carrier of SCM
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty V127() V128() set
u . (dl. k) is V86() V87() ext-real integer set
u . (dl. k) is V86() V87() ext-real integer set
u1 . (dl. k) is V86() V87() ext-real integer set
u2 . (dl. k) is V86() V87() ext-real integer set
(u,term) - (u,aux) is V86() V87() ext-real integer set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. s) is V86() V87() ext-real integer set
SubFrom ((dl. s),(dl. (s + 1))) is Element of the InstructionsF of SCM
<*(dl. s),(dl. (s + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[3,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[3,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[3,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[3,{}],<*(dl. s),(dl. (s + 1))*>},{[3,{}]}} is non empty V127() V128() set
<%(SubFrom ((dl. s),(dl. (s + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(SubFrom ((dl. s),(dl. (s + 1))))) is set
len (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
((dn + 1) + (i2 + 1)) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
n . (i + i) is Element of the InstructionsF of SCM
((F,term,aux),s) . i is set
(i + i) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u2 . (dl. s) is V86() V87() ext-real integer set
(u2 . (dl. s)) - (u2 . (dl. (s + 1))) is V86() V87() ext-real integer set
(u1 . (dl. s)) - (u1,aux) is V86() V87() ext-real integer set
k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. k is Int-like Element of the carrier of SCM
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty V127() V128() set
u . (dl. k) is V86() V87() ext-real integer set
u . (dl. k) is V86() V87() ext-real integer set
u1 . (dl. k) is V86() V87() ext-real integer set
u2 . (dl. k) is V86() V87() ext-real integer set
(u,term) * (u,aux) is V86() V87() ext-real integer set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. s) is V86() V87() ext-real integer set
MultBy ((dl. s),(dl. (s + 1))) is Element of the InstructionsF of SCM
<*(dl. s),(dl. (s + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[4,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[4,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[4,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[4,{}],<*(dl. s),(dl. (s + 1))*>},{[4,{}]}} is non empty V127() V128() set
<%(MultBy ((dl. s),(dl. (s + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(MultBy ((dl. s),(dl. (s + 1))))) is set
len (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
((dn + 1) + (i2 + 1)) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
n . (i + i) is Element of the InstructionsF of SCM
((F,term,aux),s) . i is set
(i + i) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u2 . (dl. s) is V86() V87() ext-real integer set
(u2 . (dl. s)) * (u2 . (dl. (s + 1))) is V86() V87() ext-real integer set
(u1 . (dl. s)) * (u1,aux) is V86() V87() ext-real integer set
k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. k is Int-like Element of the carrier of SCM
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty V127() V128() set
u . (dl. k) is V86() V87() ext-real integer set
u . (dl. k) is V86() V87() ext-real integer set
u1 . (dl. k) is V86() V87() ext-real integer set
u2 . (dl. k) is V86() V87() ext-real integer set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. s) is V86() V87() ext-real integer set
Divide ((dl. s),(dl. (s + 1))) is Element of the InstructionsF of SCM
<*(dl. s),(dl. (s + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[5,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[5,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[5,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[5,{}],<*(dl. s),(dl. (s + 1))*>},{[5,{}]}} is non empty V127() V128() set
<%(Divide ((dl. s),(dl. (s + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(Divide ((dl. s),(dl. (s + 1))))) is set
len (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
((dn + 1) + (i2 + 1)) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
n . (i + i) is Element of the InstructionsF of SCM
((F,term,aux),s) . i is set
(u,term) div (u,aux) is V86() V87() ext-real integer set
(i + i) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u2 . (dl. s) is V86() V87() ext-real integer set
(u2 . (dl. s)) div (u2 . (dl. (s + 1))) is V86() V87() ext-real integer set
(u1 . (dl. s)) div (u1,aux) is V86() V87() ext-real integer set
k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. k is Int-like Element of the carrier of SCM
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty V127() V128() set
u . (dl. k) is V86() V87() ext-real integer set
u . (dl. k) is V86() V87() ext-real integer set
u1 . (dl. k) is V86() V87() ext-real integer set
u2 . (dl. k) is V86() V87() ext-real integer set
(u,term) mod (u,aux) is V86() V87() ext-real integer set
((dn + 1) + (i2 + 1)) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(((dn + 1) + (i2 + 1)) + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
k + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (n,u,(k + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (n,u,k) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (n,u,k)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + k is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + (k + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
v is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC v is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
v . (dl. s) is V86() V87() ext-real integer set
Divide ((dl. s),(dl. (s + 1))) is Element of the InstructionsF of SCM
<*(dl. s),(dl. (s + 1))*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[5,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[5,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[5,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[5,{}],<*(dl. s),(dl. (s + 1))*>},{[5,{}]}} is non empty V127() V128() set
(dl. s) := (dl. (s + 1)) is Element of the InstructionsF of SCM
[1,{},<*(dl. s),(dl. (s + 1))*>] is V15() V16() set
[[1,{}],<*(dl. s),(dl. (s + 1))*>] is V15() set
{[1,{}],<*(dl. s),(dl. (s + 1))*>} is non empty set
{{[1,{}],<*(dl. s),(dl. (s + 1))*>},{[1,{}]}} is non empty V127() V128() set
<%(Divide ((dl. s),(dl. (s + 1)))),((dl. s) := (dl. (s + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() 2 -element initial set
<%(Divide ((dl. s),(dl. (s + 1))))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(Divide ((dl. s),(dl. (s + 1))))) is set
<%((dl. s) := (dl. (s + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. s) := (dl. (s + 1)))) is set
<%(Divide ((dl. s),(dl. (s + 1))))%> ^ <%((dl. s) := (dl. (s + 1)))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
len (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer set
dom (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
1 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
((dn + 1) + (i2 + 1)) + (1 + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F,term,aux),s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
n . (i + k) is Element of the InstructionsF of SCM
((F,term,aux),s) . k is set
(F,s) . 1 is set
((dn + 1) + (i2 + 1)) + 0 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + ((dn + 1) + (i2 + 1)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n . (i + ((dn + 1) + (i2 + 1))) is Element of the InstructionsF of SCM
((F,term,aux),s) . (((dn + 1) + (i2 + 1)) + 0) is set
(F,s) . 0 is set
(i + ((dn + 1) + (i2 + 1))) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(i + k) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(Comput (n,u,(((dn + 1) + (i2 + 1)) + 1))) . (dl. (s + 1)) is V86() V87() ext-real integer set
u2 . (dl. s) is V86() V87() ext-real integer set
(u2 . (dl. s)) mod (u2 . (dl. (s + 1))) is V86() V87() ext-real integer set
(u1 . (dl. s)) mod (u1,aux) is V86() V87() ext-real integer set
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. dn is Int-like Element of the carrier of SCM
[1,dn] is V15() set
{1,dn} is non empty set
{{1,dn},{1}} is non empty V127() V128() set
u . (dl. dn) is V86() V87() ext-real integer set
v . (dl. dn) is V86() V87() ext-real integer set
u1 . (dl. dn) is V86() V87() ext-real integer set
u2 . (dl. dn) is V86() V87() ext-real integer set
(Comput (n,u,(((dn + 1) + (i2 + 1)) + 1))) . (dl. dn) is V86() V87() ext-real integer set
F is Element of Terminals ()
(F) is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
((F)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V14( NAT ) set
aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
((F),aux) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . (F) is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . (F)) . aux is set
n is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Shift (((F),aux),n) is V1() Function-like set
len ((F),aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 ((F),aux) is V21() V22() V23() V27() V86() V87() ext-real integer set
dl. aux is Int-like Element of the carrier of SCM
[1,aux] is V15() set
{1,aux} is non empty set
{{1,aux},{1}} is non empty V127() V128() set
s is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) n -started set
(s,(F)) is V86() V87() ext-real integer set
i is Function-like functional empty V21() V22() V23() V25() V26() V27() FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (term,s,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (term,s,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (term,s,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
0 + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (term,s,(0 + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. aux) is V86() V87() ext-real integer set
(F) is Int-like Element of the carrier of SCM
(dl. aux) := (F) is Element of the InstructionsF of SCM
<*(dl. aux),(F)*> is V1() V4( NAT ) Function-like non empty V28() 2 -element FinSequence-like FinSubsequence-like set
[1,{},<*(dl. aux),(F)*>] is V15() V16() set
[[1,{}],<*(dl. aux),(F)*>] is V15() set
{[1,{}],<*(dl. aux),(F)*>} is non empty set
{{[1,{}],<*(dl. aux),(F)*>},{[1,{}]}} is non empty V127() V128() set
<%((dl. aux) := (F))%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,((dl. aux) := (F))) is set
<%((dl. aux) := (F))%> . 0 is set
Comput (term,s,0) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
len <%((dl. aux) := (F))%> is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 <%((dl. aux) := (F))%> is V21() V22() V23() V27() V86() V87() ext-real integer set
n + 0 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((F),aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
IC s is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term . (n + 0) is Element of the InstructionsF of SCM
s . F is V86() V87() ext-real integer set
dn is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dl. dn is Int-like Element of the carrier of SCM
[1,dn] is V15() set
{1,dn} is non empty set
{{1,dn},{1}} is non empty V127() V128() set
s . (dl. dn) is V86() V87() ext-real integer set
u . (dl. dn) is V86() V87() ext-real integer set
n is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(term,aux) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . term) . aux is set
Shift ((term,aux),n) is V1() Function-like set
F is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V14( NAT ) set
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
s is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) n -started set
len (term,aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (term,aux) is V21() V22() V23() V27() V86() V87() ext-real integer set
dl. aux is Int-like Element of the carrier of SCM
[1,aux] is V15() set
{1,aux} is non empty set
{{1,aux},{1}} is non empty V127() V128() set
(s,term) is V86() V87() ext-real integer set
halt SCM is Element of the InstructionsF of SCM
<%(halt SCM)%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like non empty V25() V28() 1 -element initial set
K117(0,(halt SCM)) is set
F is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V14( NAT ) set
term is V1() V5( the carrier of ()) Function-like DecoratedTree-like binary Element of TS ()
(term) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
aux is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
(term,aux) is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
() . term is V1() Function-like Element of Funcs (NAT,( the InstructionsF of SCM ^omega))
(() . term) . aux is set
(term,aux) ^ <%(halt SCM)%> is V1() V4( NAT ) V5( the InstructionsF of SCM) Function-like V25() V28() initial set
n is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Shift (((term,aux) ^ <%(halt SCM)%>),n) is V1() Function-like set
dl. aux is Int-like Element of the carrier of SCM
[1,aux] is V15() set
{1,aux} is non empty set
{{1,aux},{1}} is non empty V127() V128() set
len (term,aux) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 (term,aux) is V21() V22() V23() V27() V86() V87() ext-real integer set
s is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) n -started set
Result (F,s) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
(Result (F,s)) . (dl. aux) is V86() V87() ext-real integer set
(s,term) is V86() V87() ext-real integer set
LifeSpan (F,s) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Shift ((term,aux),n) is V1() Function-like set
u is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
i + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
Comput (F,s,(i + 1)) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
Comput (F,s,i) is V1() V4( the carrier of SCM) Function-like K529(2,SCM) -compatible V14( the carrier of SCM) set
IC (Comput (F,s,i)) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n + i is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
IC u is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
n + (i + 1) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
u . (dl. aux) is V86() V87() ext-real integer set
len <%(halt SCM)%> is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 <%(halt SCM)%> is V21() V22() V23() V27() V86() V87() ext-real integer set
len ((term,aux) ^ <%(halt SCM)%>) is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
proj1 ((term,aux) ^ <%(halt SCM)%>) is V21() V22() V23() V27() V86() V87() ext-real integer set
(i + 1) + 1 is V21() V22() V23() V27() V86() V87() ext-real integer Element of NAT
dom ((term,aux) ^ <%(halt SCM)%>) is V21() V22() V23() V27() V86() V87() ext-real integer Element of bool NAT
F . (n + (i + 1)) is Element of the InstructionsF of SCM
((term,aux) ^ <%(halt SCM)%>) . (i + 1) is set