:: 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
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 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
3 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
0 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered Element of NAT
{} is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered set
K2({},1) is non empty V35() V36() V37() V38() V39() V40() set
[:NAT,NAT:] is non empty V7() V10( REAL ) V11( REAL ) Element of bool [:REAL,REAL:]
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:NAT,[:NAT,NAT:]:] is non empty set
bool [:NAT,[:NAT,NAT:]:] is non empty set
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
[0,1] is Element of [:NAT,NAT:]
[:NAT,NAT:] is non empty set
n is V7() V10( NAT ) V11([:NAT,NAT:]) Function-like V30( NAT ,[:NAT,NAT:]) Element of bool [:NAT,[:NAT,NAT:]:]
n . 0 is Element of [:NAT,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
n . fusc is Element of [:NAT,NAT:]
(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 [:NAT,NAT:]
(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
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
A + 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 . (A + 1) is Element of [:NAT,NAT:]
n . A is Element of [:NAT,NAT:]
(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) `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) + ((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 [:NAT,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
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
A is V7() V10( NAT ) V11([:NAT,NAT:]) Function-like V30( NAT ,[:NAT,NAT:]) Element of bool [:NAT,[:NAT,NAT:]:]
A . single1 is Element of [:NAT,NAT:]
(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 [:NAT,NAT:]
B is V7() V10( NAT ) V11([:NAT,NAT:]) Function-like V30( NAT ,[:NAT,NAT:]) Element of bool [:NAT,[:NAT,NAT:]:]
B . single1 is Element of [:NAT,NAT:]
(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 [:NAT,NAT:]
(0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(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 V7() V10( NAT ) V11([:NAT,NAT:]) Function-like V30( NAT ,[:NAT,NAT:]) Element of bool [:NAT,[:NAT,NAT:]:]
single1 . 0 is Element of [:NAT,NAT:]
[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
0 + 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
single1 . (0 + 1) is Element of [:NAT,NAT:]
(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 [:NAT,NAT:]
[((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
[0,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
fusc is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
n 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 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 . (n + 1) is Element of [:NAT,NAT:]
(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 [:NAT,NAT:]
(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 [:NAT,NAT:]
[((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 [:NAT,NAT:]
(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 [:NAT,NAT:]
[((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) 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
0 + 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
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
0 + 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
(single1 / fusc) - 1 is ext-real V27() real set
[\(single1 / fusc)/] is ext-real V27() real integer set
n 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
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
{ b₁ where b₁ 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 <= b₁ } 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
fusc is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
0 / 2 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered 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
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural 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
[\(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 * 0 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered Element of NAT
2 to_power (log (2,((2 * single1) + 1))) is ext-real V27() real Element of REAL
0 + 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,1) is ext-real V27() real Element of REAL
[\0/] is ext-real V27() real integer set
B 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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
N 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 is ext-real V27() real integer set
((2 * single1) + 1) - 1 is ext-real V27() real integer set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
k + 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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
k + 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
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 |^ 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) 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
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural 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 * single1)))/] + 1 is ext-real V27() real integer set
0 + 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
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
2 * 0 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered Element of NAT
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
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural 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
2 * 0 is empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered Element of NAT
single1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural 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 functional FinSequence-membered M10( NAT )
[:NAT,(NAT *):] is non empty set
bool [:NAT,(NAT *):] is non empty set
single1 is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,(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
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
fusc is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like 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
n is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
A is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like Element of NAT *
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
(2 * B) + 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 /. 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)*> 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
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
(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 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 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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
fusc is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like Element of NAT *
n is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like Element of NAT *
A is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like 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
<*1*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) 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,(NAT *):]
(fusc,0) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
fusc . n is FinSequence-like Element of NAT *
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
(fusc,(n + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
n + 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
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
2 * 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 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
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
(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
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 + 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
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
A + 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 . 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
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
N 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 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
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
N 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 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 is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,(NAT *):]
(k,N) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(k,N) /. 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,0) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
l2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
fusc2 is ext-real 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
c₁₀ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
c₁₀ + 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
c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * c₁₁) + 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
c₁₀ + 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,(c₁₀ + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
k . c₁₀ is FinSequence-like Element of NAT *
(k . c₁₀) /. c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c₁₁ + 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 . c₁₀) /. (c₁₁ + 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 . c₁₀) /. c₁₁) + ((k . c₁₀) /. (c₁₁ + 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 . c₁₀) /. c₁₁) + ((k . c₁₀) /. (c₁₁ + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(k . c₁₀) ^ <*(((k . c₁₀) /. c₁₁) + ((k . c₁₀) /. (c₁₁ + 1)))*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
l2 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
fusc2 is V7() V10( NAT ) V11(NAT * ) Function-like V30( NAT ,NAT * ) Element of bool [:NAT,(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
c₁₀ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
c₁₀ + 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
c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c₁₀ + 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,(c₁₀ + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
fusc2 . c₁₀ is FinSequence-like Element of NAT *
(fusc2 . c₁₀) /. c₁₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
<*((fusc2 . c₁₀) /. c₁₁)*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc2 . c₁₀) ^ <*((fusc2 . c₁₀) /. c₁₁)*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
c₁₂ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
c₁₂ + 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
c₁₃ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
2 * c₁₃ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(2 * c₁₃) + 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
c₁₂ + 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,(c₁₂ + 1)) is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
fusc2 . c₁₂ is FinSequence-like Element of NAT *
(fusc2 . c₁₂) /. c₁₃ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
c₁₃ + 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 . c₁₂) /. (c₁₃ + 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 . c₁₂) /. c₁₃) + ((fusc2 . c₁₂) /. (c₁₃ + 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 . c₁₂) /. c₁₃) + ((fusc2 . c₁₂) /. (c₁₃ + 1)))*> is non empty V7() V10( NAT ) V11( NAT ) Function-like V42() V49(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(fusc2 . c₁₂) ^ <*(((fusc2 . c₁₂) /. c₁₃) + ((fusc2 . c₁₂) /. (c₁₃ + 1)))*> is V7() V10( NAT ) V11( NAT ) Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
(0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
0 + 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
<*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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(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 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)) 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
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
A + 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 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
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 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 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
N 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 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)) /. (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
N 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 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)) /. (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
B 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 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
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
((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
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 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 * 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
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
(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
k 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 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,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
B + B 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 * 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 * 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
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
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
- (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
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
n + n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
n * (0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
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
(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
N is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
(N) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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
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
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
((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() V37() V38() V39() V40() Element of NAT
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
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
B + A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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 + 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 + A) * ((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 * (n)) + ((B + A) * ((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) 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
A * ((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 * (n)) + (A * ((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
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
((A * (n)) + (A * ((n + 1)))) + (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
N is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
(N) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
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)) 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)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural 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
(((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
B * (((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))) + (B * (((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 + B is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer set
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() Element of NAT
(A + 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
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 + 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 * ((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 + B) * (n)) + (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
(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
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
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
(B * (n)) + (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
(A * (n)) + ((B * (n)) + (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