:: PRE_FF semantic presentation

REAL is V35() V36() V37() V41() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() Element of bool REAL
bool REAL is non empty set
COMPLEX is V35() V41() set
omega is non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() set
bool omega is non empty set
bool NAT is non empty set

K2({},1) is non empty V35() V36() V37() V38() V39() V40() set
is non empty V7() V10( REAL ) V11( REAL ) Element of bool

bool is non empty set
is non empty set
bool is non empty set

[0,1] is Element of
is non empty set

n . 0 is Element of

n . fusc is Element of
(n . fusc) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
n . single1 is Element of
(n . single1) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

n . (A + 1) is Element of
n . A is Element of

((n . A) `1) + ((n . A) `2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
[((n . A) `2),(((n . A) `1) + ((n . A) `2))] is Element of

A . single1 is Element of
(A . single1) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
A . 0 is Element of

B . single1 is Element of
(B . single1) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
B . 0 is Element of

single1 is V7() V10( NAT ) V11() Function-like V30( NAT ,) Element of bool
single1 . 0 is Element of

single1 . (0 + 1) is Element of
(single1 . (0 + 1)) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 . 0) `2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 . 0) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((single1 . 0) `1) + ((single1 . 0) `2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
[((single1 . 0) `2),(((single1 . 0) `1) + ((single1 . 0) `2))] is Element of
[((single1 . 0) `2),(((single1 . 0) `1) + ((single1 . 0) `2))] `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

fusc + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(((fusc + 1) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((fusc + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc) + ((fusc + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

single1 . (n + 1) is Element of
(single1 . (n + 1)) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
single1 . n is Element of
(single1 . n) `2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 . n) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((single1 . n) `1) + ((single1 . n) `2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
[((single1 . n) `2),(((single1 . n) `1) + ((single1 . n) `2))] is Element of
[((single1 . n) `2),(((single1 . n) `1) + ((single1 . n) `2))] `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(((n + 1) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
single1 . ((n + 1) + 1) is Element of
(single1 . ((n + 1) + 1)) `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 . (n + 1)) `2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((single1 . (n + 1)) `1) + ((single1 . (n + 1)) `2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
[((single1 . (n + 1)) `2),(((single1 . (n + 1)) `1) + ((single1 . (n + 1)) `2))] is Element of
[((single1 . (n + 1)) `2),(((single1 . (n + 1)) `1) + ((single1 . (n + 1)) `2))] `1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
[((single1 . n) `2),(((single1 . n) `1) + ((single1 . n) `2))] `2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((single1 . n) `1) + ((single1 . (n + 1)) `1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(n) + ((single1 . (n + 1)) `1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(n) + ((n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
single1 is ext-real V27() real integer set
single1 div 1 is ext-real V27() real integer set
single1 / 1 is ext-real V27() real set
[\(single1 / 1)/] is ext-real V27() real integer set
fusc is ext-real V27() real integer set
single1 is ext-real V27() real integer set
single1 div fusc is ext-real V27() real integer set
single1 / fusc is ext-real V27() real set
[\(single1 / fusc)/] is ext-real V27() real integer set
(single1 / fusc) - 1 is ext-real V27() real set

1 * fusc is ext-real V27() real integer set
(single1 / fusc) * fusc is ext-real V27() real set
single1 is ext-real V27() real integer set
fusc is ext-real V27() real integer set
single1 div fusc is ext-real V27() real integer set
fusc / fusc is ext-real V27() real set
single1 / fusc is ext-real V27() real set

(single1 / fusc) - 1 is ext-real V27() real set
[\(single1 / fusc)/] is ext-real V27() real integer set

single1 is ext-real V27() real integer set
fusc is ext-real V27() real integer set
single1 div fusc is ext-real V27() real integer set
(single1 div fusc) div n is ext-real V27() real integer set
fusc * n is ext-real V27() real integer set
single1 div (fusc * n) is ext-real V27() real integer set
single1 / fusc is ext-real V27() real set
[\(single1 / fusc)/] is ext-real V27() real integer set
[\(single1 / fusc)/] / n is ext-real V27() real set
[\([\(single1 / fusc)/] / n)/] is ext-real V27() real integer set
single1 / (fusc * n) is ext-real V27() real set
[\(single1 / (fusc * n))/] is ext-real V27() real integer set
[\(single1 / fusc)/] div n is ext-real V27() real integer set
([\(single1 / fusc)/] / n) - 1 is ext-real V27() real set
[\([\(single1 / fusc)/] / n)/] + 1 is ext-real V27() real integer set
[\(single1 / (fusc * n))/] * n is ext-real V27() real integer set
([\(single1 / fusc)/] / n) * n is ext-real V27() real set
[\(single1 / fusc)/] + 1 is ext-real V27() real integer set
(single1 / (fusc * n)) * n is ext-real V27() real set
(single1 / fusc) / n is ext-real V27() real set
((single1 / fusc) / n) * n is ext-real V27() real set
(single1 / fusc) - 1 is ext-real V27() real set
(single1 / (fusc * n)) - 1 is ext-real V27() real set
[\(single1 / (fusc * n))/] + 1 is ext-real V27() real integer set
single1 is ext-real V27() real integer set
single1 mod 2 is ext-real V27() real integer set
single1 div 2 is ext-real V27() real integer set
(single1 div 2) * 2 is ext-real V27() real integer set
single1 / 2 is ext-real V27() real set
[\(single1 / 2)/] is ext-real V27() real integer set
(single1 / 2) - 1 is ext-real V27() real set
((single1 / 2) - 1) * 2 is ext-real V27() real set
single1 - 2 is ext-real V27() real integer set
- (single1 - 2) is ext-real V27() real integer set
- ((single1 div 2) * 2) is ext-real V27() real integer set
2 - single1 is ext-real V27() real integer set
single1 + (2 - single1) is ext-real V27() real integer set
single1 + (- ((single1 div 2) * 2)) is ext-real V27() real integer set
single1 - ((single1 div 2) * 2) is ext-real V27() real integer set
(single1 / 2) * 2 is ext-real V27() real set
- single1 is ext-real V27() real integer set
single1 + (- single1) is ext-real V27() real integer set

{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT : not 2 <= b1 } is set
single1 is ext-real V27() real integer set
single1 div 2 is ext-real V27() real integer set
single1 / 2 is ext-real V27() real set
[\(single1 / 2)/] is ext-real V27() real integer set
(single1 / 2) - 1 is ext-real V27() real set
[\(single1 / 2)/] + 1 is ext-real V27() real integer set

single1 is ext-real V27() real set
fusc is ext-real V27() real set
n is ext-real V27() real set
n to_power single1 is ext-real V27() real set
n to_power fusc is ext-real V27() real set
fusc is ext-real V27() real set
single1 is ext-real V27() real set
[\fusc/] is ext-real V27() real integer set
[\single1/] is ext-real V27() real integer set
single1 - 1 is ext-real V27() real set
[\single1/] + 1 is ext-real V27() real integer set
(single1 - 1) + 1 is ext-real V27() real set
single1 is ext-real V27() real set
fusc is ext-real V27() real set
n is ext-real V27() real set
log (single1,fusc) is ext-real V27() real set
log (single1,n) is ext-real V27() real set

2 * single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,(2 * single1)) is ext-real V27() real Element of REAL
[\(log (2,(2 * single1)))/] is ext-real V27() real integer set
[\(log (2,(2 * single1)))/] + 1 is ext-real V27() real integer set
(2 * single1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,((2 * single1) + 1)) is ext-real V27() real Element of REAL
[\(log (2,((2 * single1) + 1)))/] is ext-real V27() real integer set
(log (2,(2 * single1))) + 1 is ext-real V27() real set
[\((log (2,(2 * single1))) + 1)/] is ext-real V27() real integer set
((log (2,(2 * single1))) + 1) - 1 is ext-real V27() real set
2 to_power [\((log (2,(2 * single1))) + 1)/] is ext-real V27() real set
2 to_power (log (2,(2 * single1))) is ext-real V27() real Element of REAL

2 to_power (log (2,((2 * single1) + 1))) is ext-real V27() real Element of REAL

log (2,1) is ext-real V27() real Element of REAL

1 - 1 is ext-real V27() real integer set
((2 * single1) + 1) - 1 is ext-real V27() real integer set

2 * (2 |^ l2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * (2 |^ l2)) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((2 * single1) + 1) mod 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

2 * single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * single1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,((2 * single1) + 1)) is ext-real V27() real Element of REAL
[\(log (2,((2 * single1) + 1)))/] is ext-real V27() real integer set
log (2,(2 * single1)) is ext-real V27() real Element of REAL
[\(log (2,(2 * single1)))/] is ext-real V27() real integer set
[\(log (2,(2 * single1)))/] + 1 is ext-real V27() real integer set

1 * single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(1 * single1) + single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * single1) + (2 * single1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * (2 * single1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,(2 * (2 * single1))) is ext-real V27() real Element of REAL

log (2,2) is ext-real V27() real Element of REAL
(log (2,2)) + (log (2,(2 * single1))) is ext-real V27() real set
(log (2,(2 * single1))) + 1 is ext-real V27() real set
[\((log (2,(2 * single1))) + 1)/] is ext-real V27() real integer set

2 * single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,(2 * single1)) is ext-real V27() real Element of REAL
[\(log (2,(2 * single1)))/] is ext-real V27() real integer set
(2 * single1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,((2 * single1) + 1)) is ext-real V27() real Element of REAL
[\(log (2,((2 * single1) + 1)))/] is ext-real V27() real integer set
[\(log (2,(2 * single1)))/] + 1 is ext-real V27() real integer set
([\(log (2,(2 * single1)))/] + 1) - 1 is ext-real V27() real integer set

log (2,single1) is ext-real V27() real set
[\(log (2,single1))/] is ext-real V27() real integer set
[\(log (2,single1))/] + 1 is ext-real V27() real integer set
2 * single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * single1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
log (2,((2 * single1) + 1)) is ext-real V27() real Element of REAL
[\(log (2,((2 * single1) + 1)))/] is ext-real V27() real integer set
log (2,(2 * single1)) is ext-real V27() real Element of REAL
[\(log (2,(2 * single1)))/] is ext-real V27() real integer set
log (2,2) is ext-real V27() real Element of REAL
(log (2,2)) + (log (2,single1)) is ext-real V27() real set
[\((log (2,2)) + (log (2,single1)))/] is ext-real V27() real integer set
(log (2,single1)) + 1 is ext-real V27() real set
[\((log (2,single1)) + 1)/] is ext-real V27() real integer set

[:NAT,():] is non empty set
bool [:NAT,():] is non empty set
single1 is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,():]

single1 . fusc is FinSequence-like set
single1 . fusc is FinSequence-like Element of NAT *
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
single1 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

single1 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 + 2) mod 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 + 2) div 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
fusc /. ((single1 + 2) div 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(fusc /. ((single1 + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*(fusc /. ((single1 + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
((single1 + 2) div 2) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
fusc /. (((single1 + 2) div 2) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*((fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

<*(fusc /. B)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*(fusc /. B)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

(2 * B) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

fusc /. (B + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc /. B) + (fusc /. (B + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc /. B) + (fusc /. (B + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*((fusc /. B) + (fusc /. (B + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

single1 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(single1 + 2) div 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * ((single1 + 2) div 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(single1 + 2) mod 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((single1 + 2) div 2)) + ((single1 + 2) mod 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((single1 + 2) div 2)) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((single1 + 2) div 2)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
fusc /. ((single1 + 2) div 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(fusc /. ((single1 + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*(fusc /. ((single1 + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
((single1 + 2) div 2) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
fusc /. (((single1 + 2) div 2) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
fusc ^ <*((fusc /. ((single1 + 2) div 2)) + (fusc /. (((single1 + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

single1 is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like Element of NAT *
fusc is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,():]
(fusc,0) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

fusc . n is FinSequence-like Element of NAT *

(fusc,(n + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

(fusc . n) /. A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc . n) /. A)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc . n) ^ <*((fusc . n) /. A)*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

(2 * B) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc . n) /. B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc . n) /. (B + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((fusc . n) /. B) + ((fusc . n) /. (B + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(((fusc . n) /. B) + ((fusc . n) /. (B + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc . n) ^ <*(((fusc . n) /. B) + ((fusc . n) /. (B + 1)))*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

fusc . A is FinSequence-like Element of NAT *
(fusc . A) /. n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

k is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,():]

l2 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

2 * fusc2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
l2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(k,(l2 + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
k . l2 is FinSequence-like Element of NAT *
(k . l2) /. fusc2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((k . l2) /. fusc2)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(k . l2) ^ <*((k . l2) /. fusc2)*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

c10 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * c11) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c10 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(k,(c10 + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
k . c10 is FinSequence-like Element of NAT *
(k . c10) /. c11 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c11 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(k . c10) /. (c11 + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((k . c10) /. c11) + ((k . c10) /. (c11 + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(((k . c10) /. c11) + ((k . c10) /. (c11 + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(k . c10) ^ <*(((k . c10) /. c11) + ((k . c10) /. (c11 + 1)))*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

l2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
fusc2 is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,():]
(fusc2,l2) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc2,l2) /. n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc2,0) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

c10 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

c10 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc2,(c10 + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
fusc2 . c10 is FinSequence-like Element of NAT *
(fusc2 . c10) /. c11 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc2 . c10) /. c11)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc2 . c10) ^ <*((fusc2 . c10) /. c11)*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

c12 + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * c13) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c12 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc2,(c12 + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
fusc2 . c12 is FinSequence-like Element of NAT *
(fusc2 . c12) /. c13 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c13 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc2 . c12) /. (c13 + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((fusc2 . c12) /. c13) + ((fusc2 . c12) /. (c13 + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(((fusc2 . c12) /. c13) + ((fusc2 . c12) /. (c13 + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc2 . c12) ^ <*(((fusc2 . c12) /. c13) + ((fusc2 . c12) /. (c13 + 1)))*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

((2 * n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(((2 * n) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

((n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(n) + ((n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc,B) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (fusc,B) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc,(B + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (fusc,(B + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(B + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(B + 2) div 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,B) /. ((B + 2) div 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((B + 2) div 2) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,B) /. (((B + 2) div 2) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((fusc,B) /. ((B + 2) div 2)) + ((fusc,B) /. (((B + 2) div 2) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(((fusc,B) /. ((B + 2) div 2)) + ((fusc,B) /. (((B + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
len <*(((fusc,B) /. ((B + 2) div 2)) + ((fusc,B) /. (((B + 2) div 2) + 1)))*> is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * ((B + 2) div 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(B + 2) mod 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((B + 2) div 2)) + ((B + 2) mod 2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((B + 2) div 2)) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * ((B + 2) div 2)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc,B) /. ((B + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
len <*((fusc,B) /. ((B + 2) div 2))*> is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,B) ^ <*((fusc,B) /. ((B + 2) div 2))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

(fusc,(B + 1)) /. (N + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((N + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
dom (fusc,B) is V35() V36() V37() V38() V39() V40() Element of bool NAT
(fusc,B) /. (N + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,B) ^ <*(((fusc,B) /. ((B + 2) div 2)) + ((fusc,B) /. (((B + 2) div 2) + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

(fusc,(B + 1)) /. (N + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((N + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
dom (fusc,B) is V35() V36() V37() V38() V39() V40() Element of bool NAT
(fusc,B) /. (N + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * B) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

((2 * B) + 1) + (1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((2 * B) + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(((2 * B) + 1) + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc,(2 * N)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,((2 * B) + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,((2 * B) + 1)) /. N is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc,((2 * B) + 1)) /. (N + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((fusc,((2 * B) + 1)) /. N) + ((fusc,((2 * B) + 1)) /. (N + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*(((fusc,((2 * B) + 1)) /. N) + ((fusc,((2 * B) + 1)) /. (N + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,((2 * B) + 1)) ^ <*(((fusc,((2 * B) + 1)) /. N) + ((fusc,((2 * B) + 1)) /. (N + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (fusc,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(fusc,0) /. (k + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((k + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
len (fusc,((2 * B) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(1 + 1) * B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,((2 * B) + 1)) /. (n + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,(2 * B)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (fusc,(2 * B)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,((2 * B) + 1)) /. n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * B) + (2 * 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,(2 * B)) /. N is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc,(2 * B)) /. N)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,(2 * B)) ^ <*((fusc,(2 * B)) /. N)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,(2 * B)) /. n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc,(2 * B)) /. n)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,(2 * B)) ^ <*((fusc,(2 * B)) /. n)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
((fusc,(2 * B)) ^ <*((fusc,(2 * B)) /. n)*>) /. (((2 * B) + 1) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(fusc,(2 * n)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc,(2 * n)) /. ((2 * n) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

- (1 * n) is ext-real non positive V27() real integer set
(1 * n) + (- (1 * n)) is ext-real V27() real integer set
(2 * n) + (- (1 * n)) is ext-real V27() real integer set

(2 * n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(n * (0)) + (A * (1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

(2 * n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(((2 * n) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
A * (((2 * n) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT

((2 * n) + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
((((2 * n) + 1) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
B * ((((2 * n) + 1) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(A * (((2 * n) + 1))) + (B * ((((2 * n) + 1) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36()