REAL is set
NAT is V1() V4() V5() V6() Element of K6(REAL)
K6(REAL) is set
SCM is V44() V83(2) IC-Ins-separated strict V91(2) AMI-Struct over 2
2 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
the U1 of SCM is set
K320(2,SCM) is Relation-like the U1 of SCM -defined Function-like total set
COMPLEX is set
NAT is V1() V4() V5() V6() set
K6(NAT) is set
K6(NAT) is set
9 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
K113(9) is Element of K6(NAT)
K225() is set
K232() is set
K6(K232()) is set
K7(K232(),2) is set
K6(K7(K232(),2)) is set
K234() is Function-like V40(K232(),2) Element of K6(K7(K232(),2))
K235() is V1() Relation-like 2 -defined Function-like total set
K234() * K235() is Relation-like set
K214((K234() * K235())) is set
K226() is V1() set
K176(K214((K234() * K235())),K214((K234() * K235()))) is set
K7(K226(),K176(K214((K234() * K235())),K214((K234() * K235())))) is set
K6(K7(K226(),K176(K214((K234() * K235())),K214((K234() * K235()))))) is set
the InstructionsF of SCM is V1() Relation-like V72() V73() V74() V76() set
INT is set
RAT is set
1 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
3 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dl. 0 is V63() Element of the U1 of SCM
dl. 1 is V63() Element of the U1 of SCM
dl. 2 is V63() Element of the U1 of SCM
dl. 3 is V63() Element of the U1 of SCM
halt SCM is Element of the InstructionsF of SCM
K69((halt SCM)) is V4() V5() V6() V10() V11() V12() integer ext-real set
4 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
5 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
6 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
7 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
8 is V1() V4() V5() V6() V10() V11() V12() integer V64() ext-real positive Element of NAT
Fib 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
0 is set
{0,1,2,3,4,5,6,7,8} is set
log (2,1) is V11() V12() ext-real Element of REAL
[\(log (2,1))/] is V11() V12() integer ext-real set
[\0/] is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,F) is V11() V12() ext-real set
[\(log (2,F))/] is V11() V12() integer ext-real set
[\(log (2,F))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,F))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,F))/] + 1)) + 1 is V11() V12() integer ext-real set
0 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
[\0/] is V11() V12() integer ext-real set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * N) + (6 * 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 * N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(2 * N) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,N) is V11() V12() ext-real set
[\(log (2,N))/] is V11() V12() integer ext-real set
[\(log (2,N))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,N))/] + 1)) + 1 is V11() V12() integer ext-real set
6 + ((6 * ([\(log (2,N))/] + 1)) + 1) is V11() V12() integer ext-real set
log (2,F) is V11() V12() ext-real set
[\(log (2,F))/] is V11() V12() integer ext-real set
[\(log (2,F))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,F))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,F))/] + 1)) + 1 is V11() V12() integer ext-real set
1 + ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
6 * (1 + ([\(log (2,N))/] + 1)) is V11() V12() integer ext-real set
(6 * (1 + ([\(log (2,N))/] + 1))) + 1 is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,(2 * F)) is V11() V12() ext-real Element of REAL
log (2,F) is V11() V12() ext-real set
1 + (log (2,F)) is V11() V12() ext-real set
(log (2,F)) + 1 is V11() V12() ext-real set
log (2,2) is V11() V12() ext-real Element of REAL
(log (2,2)) + (log (2,F)) is V11() V12() ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 * N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,N) is V11() V12() ext-real set
[\(log (2,N))/] is V11() V12() integer ext-real set
[\(log (2,N))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,N))/] + 1)) + 1 is V11() V12() integer ext-real set
6 + ((6 * ([\(log (2,N))/] + 1)) + 1) is V11() V12() integer ext-real set
log (2,F) is V11() V12() ext-real set
[\(log (2,F))/] is V11() V12() integer ext-real set
[\(log (2,F))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,F))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,F))/] + 1)) + 1 is V11() V12() integer ext-real set
1 + ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
6 * (1 + ([\(log (2,N))/] + 1)) is V11() V12() integer ext-real set
(6 * (1 + ([\(log (2,N))/] + 1))) + 1 is V11() V12() integer ext-real set
(log (2,N)) + 1 is V11() V12() ext-real set
[\((log (2,N)) + 1)/] is V11() V12() integer ext-real set
1 + [\((log (2,N)) + 1)/] is V11() V12() integer ext-real set
6 * (1 + [\((log (2,N)) + 1)/]) is V11() V12() integer ext-real set
(6 * (1 + [\((log (2,N)) + 1)/])) + 1 is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * F is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * F) - 4 is V11() V12() integer ext-real set
N is V4() V5() V6() V10() V11() V12() integer ext-real set
N + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * n) + 2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dl. 4 is V63() Element of the U1 of SCM
(dl. 1) >0_goto 2 is Element of the InstructionsF of SCM
<%((dl. 1) >0_goto 2)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
<%(halt SCM)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(dl. 3) := (dl. 0) is Element of the InstructionsF of SCM
<%((dl. 3) := (dl. 0))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
SubFrom ((dl. 1),(dl. 0)) is Element of the InstructionsF of SCM
<%(SubFrom ((dl. 1),(dl. 0)))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(dl. 1) =0_goto 1 is Element of the InstructionsF of SCM
<%((dl. 1) =0_goto 1)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(dl. 4) := (dl. 2) is Element of the InstructionsF of SCM
<%((dl. 4) := (dl. 2))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(dl. 2) := (dl. 3) is Element of the InstructionsF of SCM
<%((dl. 2) := (dl. 3))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
AddTo ((dl. 3),(dl. 4)) is Element of the InstructionsF of SCM
<%(AddTo ((dl. 3),(dl. 4)))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
SCM-goto 3 is Element of the InstructionsF of SCM
<%(SCM-goto 3)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
() is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
F . 0 is Element of the InstructionsF of SCM
F . 1 is Element of the InstructionsF of SCM
F . 2 is Element of the InstructionsF of SCM
F . 3 is Element of the InstructionsF of SCM
F . 4 is Element of the InstructionsF of SCM
F . 5 is Element of the InstructionsF of SCM
F . 6 is Element of the InstructionsF of SCM
F . 7 is Element of the InstructionsF of SCM
F . 8 is Element of the InstructionsF of SCM
N is Element of the InstructionsF of SCM
<%N%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
n is Element of the InstructionsF of SCM
<%n%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
<%N%> ^ <%n%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
a is Element of the InstructionsF of SCM
<%a%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(<%N%> ^ <%n%>) ^ <%a%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
b is Element of the InstructionsF of SCM
<%b%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
aux is Element of the InstructionsF of SCM
<%aux%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
nn is Element of the InstructionsF of SCM
<%nn%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
n2 is Element of the InstructionsF of SCM
<%n2%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
N is Element of the InstructionsF of SCM
<%N%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
A is Element of the InstructionsF of SCM
<%A%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 2 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 3 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 6 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 7 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 4 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 5 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 8 is set
len ((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dom ((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) is V4() V5() V6() V10() V11() V12() integer ext-real set
dom ((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) is V4() V5() V6() V10() V11() V12() integer ext-real Element of K6(NAT)
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 0 is set
((((((((<%N%> ^ <%n%>) ^ <%a%>) ^ <%b%>) ^ <%aux%>) ^ <%nn%>) ^ <%n2%>) ^ <%N%>) ^ <%A%>) . 1 is set
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%1,N,0,0%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
6 * N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * N) - 2 is V11() V12() integer ext-real set
Fib N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%1,N,0,0%>
LifeSpan (F,n) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Result (F,n) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,n)) . (dl. 3) is V11() V12() integer ext-real set
IC n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F . 0 is Element of the InstructionsF of SCM
0 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(0 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
Comput (F,n,0) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
n . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,(0 + 1))) . (dl. 0) is V11() V12() integer ext-real set
F . 3 is Element of the InstructionsF of SCM
n . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,(0 + 1))) . (dl. 2) is V11() V12() integer ext-real set
F . 4 is Element of the InstructionsF of SCM
n . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,(0 + 1))) . (dl. 3) is V11() V12() integer ext-real set
F . 6 is Element of the InstructionsF of SCM
N - 1 is V11() V12() integer ext-real set
F . 2 is Element of the InstructionsF of SCM
F . 7 is Element of the InstructionsF of SCM
F . 8 is Element of the InstructionsF of SCM
F . 5 is Element of the InstructionsF of SCM
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * nn9) + 3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((6 * nn9) + 3)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(N - 1) - nn9 is V11() V12() integer ext-real set
Fib nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * (nn9 + 1)) + 3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((6 * (nn9 + 1)) + 3)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(N - 1) - (nn9 + 1) is V11() V12() integer ext-real set
(nn9 + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib ((nn9 + 1) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((6 * nn9) + 3) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(((6 * nn9) + 3) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(((6 * nn9) + 3) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((((6 * nn9) + 3) + 1) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
((((6 * nn9) + 3) + 1) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(((((6 * nn9) + 3) + 1) + 1) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC (Comput (F,n,((6 * nn9) + 3))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
t5 is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
t5 . (dl. 0) is V11() V12() integer ext-real set
t5 . (dl. 1) is V11() V12() integer ext-real set
t5 . (dl. 2) is V11() V12() integer ext-real set
t5 . (dl. 3) is V11() V12() integer ext-real set
IC t5 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,((6 * nn9) + 3))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (F,n,(((6 * nn9) + 3) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
4 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,((((6 * nn9) + 3) + 1) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
5 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
7 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,((((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,((6 * nn9) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,(((6 * nn9) + 3) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,((((6 * nn9) + 3) + 1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,n,((6 * nn9) + 3))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,(((6 * nn9) + 3) + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,((((6 * nn9) + 3) + 1) + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,((6 * nn9) + 3))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,(((6 * nn9) + 3) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,((((6 * nn9) + 3) + 1) + 1))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1))) . (dl. 3) is V11() V12() integer ext-real set
((Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 4)) + ((Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 3)) is V11() V12() integer ext-real set
(Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,n,(((6 * nn9) + 3) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,((((6 * nn9) + 3) + 1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,(((((6 * nn9) + 3) + 1) + 1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,((((((6 * nn9) + 3) + 1) + 1) + 1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,(((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,((((((((6 * nn9) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((N - 1) - nn9) - 1 is V11() V12() integer ext-real set
F . 1 is Element of the InstructionsF of SCM
n . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,(0 + 1))) . (dl. 1) is V11() V12() integer ext-real set
6 * 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * 0) + 3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((6 * 0) + 3)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(N - 1) - 0 is V11() V12() integer ext-real set
Fib (0 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(2 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
1 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(1 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC (Comput (F,n,(0 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,(1 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,n,(1 + 1))) . (dl. 0) is V11() V12() integer ext-real set
m is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
m . (dl. 0) is V11() V12() integer ext-real set
m . (dl. 1) is V11() V12() integer ext-real set
m . (dl. 2) is V11() V12() integer ext-real set
m . (dl. 3) is V11() V12() integer ext-real set
IC m is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,(1 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,n,(1 + 1))) . (dl. 2) is V11() V12() integer ext-real set
IC (Comput (F,n,(1 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,(2 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,n,(0 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F . (IC (Comput (F,n,(0 + 1)))) is Element of the InstructionsF of SCM
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real set
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real set
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * nn9) + 3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,((6 * nn9) + 3)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC (Comput (F,n,((6 * nn9) + 3))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,((6 * nn9) + 3))) . (dl. 3) is V11() V12() integer ext-real set
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((6 * nn9) + 3) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,n,(((6 * nn9) + 3) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Comput (F,n,((6 * nn9) + 3))) . (dl. 1) is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
nn9 + (1 - 1) is V11() V12() integer ext-real set
(nn9 + (1 - 1)) - nn9 is V11() V12() integer ext-real set
IC (Comput (F,n,(((6 * nn9) + 3) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,n,(((6 * nn9) + 3) + 1))) . (dl. 3) is V11() V12() integer ext-real set
F is V11() V12() integer ext-real set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
a is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc a is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
b is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc b is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(dl. 1) =0_goto 8 is Element of the InstructionsF of SCM
<%((dl. 1) =0_goto 8)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(dl. 4) := (dl. 0) is Element of the InstructionsF of SCM
<%((dl. 4) := (dl. 0))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
Divide ((dl. 1),(dl. 4)) is Element of the InstructionsF of SCM
<%(Divide ((dl. 1),(dl. 4)))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(dl. 4) =0_goto 6 is Element of the InstructionsF of SCM
<%((dl. 4) =0_goto 6)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
AddTo ((dl. 3),(dl. 2)) is Element of the InstructionsF of SCM
<%(AddTo ((dl. 3),(dl. 2)))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
SCM-goto 0 is Element of the InstructionsF of SCM
<%(SCM-goto 0)%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
AddTo ((dl. 2),(dl. 3)) is Element of the InstructionsF of SCM
<%(AddTo ((dl. 2),(dl. 3)))%> is V1() V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V35(1) V71() set
(((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
(((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%> is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
() is V8() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V28() V71() set
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
s5 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,s5,1,0%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
Fusc s5 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,s5) is V11() V12() ext-real set
[\(log (2,s5))/] is V11() V12() integer ext-real set
[\(log (2,s5))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,s5))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,s5))/] + 1)) + 1 is V11() V12() integer ext-real set
(log (2,s5)) - 1 is V11() V12() ext-real set
0 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 to_power (s3 + 1) is V11() V12() ext-real Element of REAL
2 to_power (log (2,s5)) is V11() V12() ext-real set
2 |^ (s3 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s2 is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,s5,1,0%>
Result (F,s2) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,s2)) . (dl. 3) is V11() V12() integer ext-real set
LifeSpan (F,s2) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(log (2,s5)) + 1 is V11() V12() ext-real set
F . 0 is Element of the InstructionsF of SCM
F . 7 is Element of the InstructionsF of SCM
F . 1 is Element of the InstructionsF of SCM
F . 4 is Element of the InstructionsF of SCM
F . 2 is Element of the InstructionsF of SCM
F . 6 is Element of the InstructionsF of SCM
F . 3 is Element of the InstructionsF of SCM
F . 5 is Element of the InstructionsF of SCM
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,(6 * nn9)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
2 |^ nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s5 div (2 |^ nn9) is V11() V12() integer ext-real set
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,(6 * (nn9 + 1))) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
2 |^ (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s5 div (2 |^ (nn9 + 1)) is V11() V12() integer ext-real set
2 to_power nn9 is V11() V12() ext-real set
(Comput (F,nn9,(6 * nn9))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (F,nn9,(6 * nn9))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * nn9) + 3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 3)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(6 * nn9) + 2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 2)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(6 * nn9) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
((6 * nn9) + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,nn9,((6 * nn9) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,nn9,((6 * nn9) + 2))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((6 * nn9) + 2) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,nn9,((6 * nn9) + 3))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 2))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 1)) mod 2 is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 1)) div 2 is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * nn9))) . (dl. 1)) div 2) * 2 is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 1)) - ((((Comput (F,nn9,(6 * nn9))) . (dl. 1)) div 2) * 2) is V11() V12() integer ext-real set
u is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC u is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
u . (dl. 0) is V11() V12() integer ext-real set
u . (dl. 1) is V11() V12() integer ext-real set
u . (dl. 2) is V11() V12() integer ext-real set
((u . (dl. 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 2)) * ((u . (dl. 1))) is V11() V12() integer ext-real set
u . (dl. 3) is V11() V12() integer ext-real set
(u . (dl. 1)) + 1 is V11() V12() integer ext-real set
(((u . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 3)) * (((u . (dl. 1)) + 1)) is V11() V12() integer ext-real set
((u . (dl. 2)) * ((u . (dl. 1)))) + ((u . (dl. 3)) * (((u . (dl. 1)) + 1))) is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * nn9))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 2))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 2))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(2 |^ nn9) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s5 div ((2 |^ nn9) * 2) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 3))) . (dl. 4) is V11() V12() integer ext-real set
(6 * nn9) + 6 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 6)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(6 * nn9) + 5 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 5)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(6 * nn9) + 4 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * nn9) + 4)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
((6 * nn9) + 3) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * nn9))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 2))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 3))) . (dl. 3) is V11() V12() integer ext-real set
((6 * nn9) + 5) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * nn9))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 3))) . (dl. 2) is V11() V12() integer ext-real set
((6 * nn9) + 4) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 2) is V11() V12() integer ext-real set
IC (Comput (F,nn9,((6 * nn9) + 4))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,nn9,((6 * nn9) + 5))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
4 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 1) is V11() V12() integer ext-real set
tn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((((Comput (F,nn9,(6 * nn9))) . (dl. 1)) div 2) * 2) + (((Comput (F,nn9,(6 * nn9))) . (dl. 1)) mod 2) is V11() V12() integer ext-real set
un is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 * un is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(2 * un) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tn + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
un + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
2 * (un + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 0) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 1)) + 1 is V11() V12() integer ext-real set
((((Comput (F,nn9,(6 * nn9))) . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (tn + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (un + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 3) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 3)) + ((Comput (F,nn9,(6 * nn9))) . (dl. 2)) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 3) is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * nn9))) . (dl. 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc tn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc un is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Fusc un) + (Fusc (un + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((u . (dl. 1))) + (Fusc (un + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((u . (dl. 1))) + (((u . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 2) is V11() V12() integer ext-real set
un is V11() V12() integer ext-real set
tb is V11() V12() integer ext-real set
(tb) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
un * (tb) is V11() V12() integer ext-real set
tn is V11() V12() integer ext-real set
tb + 1 is V11() V12() integer ext-real set
((tb + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tn * ((tb + 1)) is V11() V12() integer ext-real set
(un * (tb)) + (tn * ((tb + 1))) is V11() V12() integer ext-real set
ta is V11() V12() integer ext-real set
(ta) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 2)) * (ta) is V11() V12() integer ext-real set
ta + 1 is V11() V12() integer ext-real set
((ta + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 3)) * ((ta + 1)) is V11() V12() integer ext-real set
((u . (dl. 2)) * (ta)) + ((u . (dl. 3)) * ((ta + 1))) is V11() V12() integer ext-real set
IC (Comput (F,nn9,((6 * nn9) + 4))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,nn9,((6 * nn9) + 5))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 1)) + 1 is V11() V12() integer ext-real set
((((Comput (F,nn9,(6 * nn9))) . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tn + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (tn + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
un is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc un is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
un + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (un + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Fusc un) + (Fusc (un + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Fusc un) + (((u . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((u . (dl. 1))) + (((u . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 0) is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * nn9))) . (dl. 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc tn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * nn9) + 4))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 5))) . (dl. 2) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * nn9))) . (dl. 2)) + ((Comput (F,nn9,(6 * nn9))) . (dl. 3)) is V11() V12() integer ext-real set
(Comput (F,nn9,((6 * nn9) + 6))) . (dl. 2) is V11() V12() integer ext-real set
ta is V11() V12() integer ext-real set
tn is V11() V12() integer ext-real set
(tn) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
ta * (tn) is V11() V12() integer ext-real set
tb is V11() V12() integer ext-real set
tn + 1 is V11() V12() integer ext-real set
((tn + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tb * ((tn + 1)) is V11() V12() integer ext-real set
(ta * (tn)) + (tb * ((tn + 1))) is V11() V12() integer ext-real set
ta + tb is V11() V12() integer ext-real set
un is V11() V12() integer ext-real set
(un) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(ta + tb) * (un) is V11() V12() integer ext-real set
un + 1 is V11() V12() integer ext-real set
((un + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
tb * ((un + 1)) is V11() V12() integer ext-real set
((ta + tb) * (un)) + (tb * ((un + 1))) is V11() V12() integer ext-real set
6 * (s3 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * (s3 + 1)) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,((6 * (s3 + 1)) + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
Comput (F,nn9,(6 * (s3 + 1))) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
nn9 . (dl. 1) is V11() V12() integer ext-real set
nn9 . (dl. 2) is V11() V12() integer ext-real set
nn9 . (dl. 3) is V11() V12() integer ext-real set
6 * 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,nn9,(6 * 0)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
2 |^ 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s5 div (2 |^ 0) is V11() V12() integer ext-real set
u is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC u is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
u . (dl. 0) is V11() V12() integer ext-real set
u . (dl. 1) is V11() V12() integer ext-real set
u . (dl. 2) is V11() V12() integer ext-real set
((u . (dl. 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 2)) * ((u . (dl. 1))) is V11() V12() integer ext-real set
u . (dl. 3) is V11() V12() integer ext-real set
(u . (dl. 1)) + 1 is V11() V12() integer ext-real set
(((u . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(u . (dl. 3)) * (((u . (dl. 1)) + 1)) is V11() V12() integer ext-real set
((u . (dl. 2)) * ((u . (dl. 1)))) + ((u . (dl. 3)) * (((u . (dl. 1)) + 1))) is V11() V12() integer ext-real set
s5 div 1 is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1) is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 2)) * (((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1))) is V11() V12() integer ext-real set
(Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 3) is V11() V12() integer ext-real set
((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)) + 1 is V11() V12() integer ext-real set
((((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)) + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 3)) * ((((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)) + 1)) is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 2)) * (((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)))) + (((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 3)) * ((((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)) + 1))) is V11() V12() integer ext-real set
IC (Comput (F,nn9,(6 * (s3 + 1)))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,nn9,((6 * (s3 + 1)) + 1))) . (dl. 3) is V11() V12() integer ext-real set
s5 div (2 |^ (s3 + 1)) is V11() V12() integer ext-real set
IC (Comput (F,nn9,((6 * (s3 + 1)) + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F . (IC (Comput (F,nn9,(6 * (s3 + 1))))) is Element of the InstructionsF of SCM
F . 8 is Element of the InstructionsF of SCM
((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 2)) * 0 is V11() V12() integer ext-real set
(((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 2)) * 0) + (((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 3)) * ((((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 1)) + 1))) is V11() V12() integer ext-real set
Fusc (0 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((Comput (F,nn9,(6 * (s3 + 1)))) . (dl. 3)) * (Fusc (0 + 1)) is V11() V12() integer ext-real set
F . (IC (Comput (F,nn9,((6 * (s3 + 1)) + 1)))) is Element of the InstructionsF of SCM
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
nn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * nn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * nn) - 4 is V11() V12() integer ext-real set
nn + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * (nn + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * (nn + 1)) - 4 is V11() V12() integer ext-real set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
A is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%1,(nn + 1),N,A%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
n2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib n2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n2 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (n2 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n2 + (nn + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(n2 + (nn + 1)) - 1 is V11() V12() integer ext-real set
B is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 3 -started State-consisting of <%1,(nn + 1),N,A%>
LifeSpan (F,B) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Result (F,B) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,B)) . (dl. 2) is V11() V12() integer ext-real set
(Result (F,B)) . (dl. 3) is V11() V12() integer ext-real set
F . 3 is Element of the InstructionsF of SCM
Comput (F,B,0) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
0 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,B,(0 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
F . 1 is Element of the InstructionsF of SCM
IC B is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,B,(0 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,B,(1 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
F . 4 is Element of the InstructionsF of SCM
B . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,B,(0 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,B,(1 + 1))) . (dl. 3) is V11() V12() integer ext-real set
F . 7 is Element of the InstructionsF of SCM
B . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,B,(0 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,B,(1 + 1))) . (dl. 2) is V11() V12() integer ext-real set
F . 6 is Element of the InstructionsF of SCM
B . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(0 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(1 + 1))) . (dl. 0) is V11() V12() integer ext-real set
B . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,B,(0 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(nn + 1) - 1 is V11() V12() integer ext-real set
(Comput (F,B,(1 + 1))) . (dl. 1) is V11() V12() integer ext-real set
F . 5 is Element of the InstructionsF of SCM
F . 8 is Element of the InstructionsF of SCM
IC (Comput (F,B,(1 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F . (IC (Comput (F,B,(1 + 1)))) is Element of the InstructionsF of SCM
F . (IC (Comput (F,B,(0 + 1)))) is Element of the InstructionsF of SCM
s6 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib s6 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s6 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (s6 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(n2 + 1) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib ((n2 + 1) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
5 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,B,(5 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
4 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,B,(4 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
Comput (F,B,(3 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
2 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,B,(2 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
IC (Comput (F,B,(1 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,B,(2 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,B,(3 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,B,(4 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
7 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,B,(2 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,B,(3 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,B,(3 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,B,(4 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,B,(5 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,B,(2 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(3 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(4 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(5 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,B,(2 + 1))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,B,(3 + 1))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,B,(4 + 1))) . (dl. 3) is V11() V12() integer ext-real set
((Comput (F,B,(3 + 1))) . (dl. 4)) + ((Comput (F,B,(3 + 1))) . (dl. 3)) is V11() V12() integer ext-real set
(Comput (F,B,(5 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,B,(2 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,B,(3 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,B,(4 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,B,(5 + 1))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (F,B,(5 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%1,nn,A,(Fib ((n2 + 1) + 1))%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
(n2 + 1) + nn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((n2 + 1) + nn) - 1 is V11() V12() integer ext-real set
Result (F,(Comput (F,B,(5 + 1)))) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,(Comput (F,B,(5 + 1))))) . (dl. 2) is V11() V12() integer ext-real set
(Result (F,(Comput (F,B,(5 + 1))))) . (dl. 3) is V11() V12() integer ext-real set
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
LifeSpan (F,(Comput (F,B,(5 + 1)))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + ((6 * nn) - 4) is V11() V12() integer ext-real set
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * 0) - 4 is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
a is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%1,0,n,a%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fib (N + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
b is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 3 -started State-consisting of <%1,0,n,a%>
LifeSpan (F,b) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N + 0 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(N + 0) - 1 is V11() V12() integer ext-real set
Result (F,b) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,b)) . (dl. 2) is V11() V12() integer ext-real set
(Result (F,b)) . (dl. 3) is V11() V12() integer ext-real set
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
nn is V4() V5() V6() V10() V11() V12() integer ext-real set
Fusc nn is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (nn + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,nn) is V11() V12() ext-real set
[\(log (2,nn))/] is V11() V12() integer ext-real set
[\(log (2,nn))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,nn))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,nn))/] + 1)) + 1 is V11() V12() integer ext-real set
A is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
B is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,nn,A,B%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
A * (Fusc nn) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
B * (Fusc (nn + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(A * (Fusc nn)) + (B * (Fusc (nn + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,nn,A,B%>
Result (F,s) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,s)) . (dl. 3) is V11() V12() integer ext-real set
LifeSpan (F,s) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s . (dl. 1) is V11() V12() integer ext-real set
Comput (F,s,0) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
F . 0 is Element of the InstructionsF of SCM
0 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(0 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
F . 8 is Element of the InstructionsF of SCM
F . 3 is Element of the InstructionsF of SCM
IC s is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
s . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(0 + 1))) . (dl. 2) is V11() V12() integer ext-real set
s . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(0 + 1))) . (dl. 0) is V11() V12() integer ext-real set
F . 2 is Element of the InstructionsF of SCM
s . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(0 + 1))) . (dl. 3) is V11() V12() integer ext-real set
IC (Comput (F,s,(0 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
F . (IC (Comput (F,s,(0 + 1)))) is Element of the InstructionsF of SCM
F . 1 is Element of the InstructionsF of SCM
F . 5 is Element of the InstructionsF of SCM
F . 4 is Element of the InstructionsF of SCM
F . 7 is Element of the InstructionsF of SCM
F . 6 is Element of the InstructionsF of SCM
(Comput (F,s,(0 + 1))) . (dl. 1) is V11() V12() integer ext-real set
5 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(5 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
4 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(4 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
3 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(3 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
2 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(2 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
1 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Comput (F,s,(1 + 1)) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
nn mod 2 is V11() V12() integer ext-real set
nn div 2 is V11() V12() integer ext-real set
(nn div 2) * 2 is V11() V12() integer ext-real set
nn - ((nn div 2) * 2) is V11() V12() integer ext-real set
IC (Comput (F,s,(1 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,s,(2 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(1 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(2 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(1 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(2 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(1 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(2 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(1 + 1))) . (dl. 4) is V11() V12() integer ext-real set
(Comput (F,s,(1 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(2 + 1))) . (dl. 1) is V11() V12() integer ext-real set
n2 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n2 div 2 is V11() V12() integer ext-real set
(Comput (F,s,(2 + 1))) . (dl. 4) is V11() V12() integer ext-real set
IC (Comput (F,s,(3 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,s,(4 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(3 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(3 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 3) is V11() V12() integer ext-real set
B + A is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(3 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(3 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 0) is V11() V12() integer ext-real set
IC (Comput (F,s,(5 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(5 + 1))) . (dl. 3) is V11() V12() integer ext-real set
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,nn9,A,(B + A)%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
(nn mod 2) + ((nn div 2) * 2) is V11() V12() integer ext-real set
Fusc nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
A * (Fusc nn9) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(B + A) * (Fusc (nn9 + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(A * (Fusc nn9)) + ((B + A) * (Fusc (nn9 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
LifeSpan (F,(Comput (F,s,(5 + 1)))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,nn9) is V11() V12() ext-real set
[\(log (2,nn9))/] is V11() V12() integer ext-real set
[\(log (2,nn9))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,nn9))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,nn9))/] + 1)) + 1 is V11() V12() integer ext-real set
Result (F,(Comput (F,s,(5 + 1)))) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) is V11() V12() integer ext-real set
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * (nn9 + 1)) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + ((6 * (nn9 + 1)) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,s,(3 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,s,(4 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(3 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (F,s,(3 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 3) is V11() V12() integer ext-real set
(Comput (F,s,(3 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(5 + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (F,s,(3 + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (F,s,(4 + 1))) . (dl. 2) is V11() V12() integer ext-real set
A + B is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
IC (Comput (F,s,(5 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(Comput (F,s,(5 + 1))) . (dl. 2) is V11() V12() integer ext-real set
nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,nn9,(A + B),B%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
Fusc nn9 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(A + B) * (Fusc nn9) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
nn9 + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (nn9 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
B * (Fusc (nn9 + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Result (F,(Comput (F,s,(5 + 1)))) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) is V11() V12() integer ext-real set
LifeSpan (F,(Comput (F,s,(5 + 1)))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,nn9) is V11() V12() ext-real set
[\(log (2,nn9))/] is V11() V12() integer ext-real set
[\(log (2,nn9))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,nn9))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,nn9))/] + 1)) + 1 is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
m + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 * (m + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(6 * (m + 1)) + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
6 + ((6 * (m + 1)) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
a is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
b is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,N,a,b%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
a * (Fusc N) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (N + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
b * (Fusc (N + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(a * (Fusc N)) + (b * (Fusc (N + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
aux is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,N,a,b%>
Result (F,aux) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,aux)) . (dl. 3) is V11() V12() integer ext-real set
LifeSpan (F,aux) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,N) is V11() V12() ext-real set
[\(log (2,N))/] is V11() V12() integer ext-real set
[\(log (2,N))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,N))/] + 1)) + 1 is V11() V12() integer ext-real set
F is V1() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
<%2,N,1,0%> is V8() Relation-like NAT -defined INT -valued Function-like V28() V71() set
Fusc N is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
log (2,N) is V11() V12() ext-real set
[\(log (2,N))/] is V11() V12() integer ext-real set
[\(log (2,N))/] + 1 is V11() V12() integer ext-real set
6 * ([\(log (2,N))/] + 1) is V11() V12() integer ext-real set
(6 * ([\(log (2,N))/] + 1)) + 1 is V11() V12() integer ext-real set
1 * (Fusc N) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
N + 1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Fusc (N + 1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
0 * (Fusc (N + 1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(1 * (Fusc N)) + (0 * (Fusc (N + 1))) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,N,1,0%>
a is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,N,1,0%>
Result (F,a) is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total set
(Result (F,a)) . (dl. 3) is V11() V12() integer ext-real set
b is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,N,1,0%>
LifeSpan (F,b) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
aux is Relation-like the U1 of SCM -defined Function-like K320(2,SCM) -compatible total 0 -started State-consisting of <%2,N,1,0%>
LifeSpan (F,aux) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT