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

5 is non empty V21() V22() V23() V27() V86() V87() ext-real positive integer V127() Element of NAT

{ b

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

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

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<