REAL is V29() V30() V31() V35() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V29() V30() V31() V32() V33() V34() V35() Element of K32(REAL)
K32(REAL) is non empty set
COMPLEX is V29() V35() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V29() V30() V31() V32() V33() V34() V35() set
K32(NAT) is non empty set
K32(NAT) is non empty set
K33(NAT,REAL) is set
K32(K33(NAT,REAL)) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() ext-real non positive non negative real V29() V30() V31() V32() V33() V34() V35() V36() V53() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib 0 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib 1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau is V24() ext-real real set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
sqrt 5 is V24() ext-real real Element of REAL
1 + (sqrt 5) is V24() ext-real real set
K135((1 + (sqrt 5)),2) is V24() ext-real real Element of COMPLEX
tau_bar is V24() ext-real real set
1 - (sqrt 5) is V24() ext-real real set
K135((1 - (sqrt 5)),2) is V24() ext-real real Element of COMPLEX
3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 / tau is V24() ext-real real set
- (1 / tau) is V24() ext-real real set
a is V24() ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a to_power n is V24() ext-real real set
a |^ n is set
a is V24() ext-real non negative real set
sqrt a is V24() ext-real real set
(sqrt a) * (sqrt a) is V24() ext-real real set
a ^2 is V24() ext-real real set
a * a is V24() ext-real non negative real set
sqrt (a ^2) is V24() ext-real real set
a is V24() ext-real real set
a to_power 2 is V24() ext-real real set
- a is V24() ext-real real set
(- a) to_power 2 is V24() ext-real real set
1 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real set
a -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) -' 1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a * a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + n) |^ 2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a * n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a * a) + (a * n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a * a) + (a * n)) + (a * n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a * a) + (a * n)) + (a * n)) + (n * n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + n) * (a + n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n * a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a * a) + (a * n)) + (n * a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a * a) + (a * n)) + (n * a)) + (n * n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 * a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is non empty V24() ext-real real set
n to_power a is V24() ext-real real set
(n to_power a) to_power 2 is V24() ext-real real set
n to_power (2 * a) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n to_power a) to_power (1 + 1) is V24() ext-real real set
(n to_power a) to_power 1 is V24() ext-real real set
((n to_power a) to_power 1) * ((n to_power a) to_power 1) is V24() ext-real real set
(n to_power a) * ((n to_power a) to_power 1) is V24() ext-real real set
(n to_power a) * (n to_power a) is V24() ext-real real set
a + a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n to_power (a + a) is V24() ext-real real set
a is V24() ext-real real set
n is V24() ext-real real set
a + n is V24() ext-real real set
a - n is V24() ext-real real set
(a + n) * (a - n) is V24() ext-real real set
a to_power 2 is V24() ext-real real set
n to_power 2 is V24() ext-real real set
(a to_power 2) - (n to_power 2) is V24() ext-real real set
a ^2 is V24() ext-real real set
a * a is V24() ext-real real set
n ^2 is V24() ext-real real set
n * n is V24() ext-real real set
(a ^2) - (n ^2) is V24() ext-real real set
(a to_power 2) - (n ^2) is V24() ext-real real set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is non empty V24() ext-real real set
n is non empty V24() ext-real real set
n * n is non empty V24() ext-real real set
(n * n) to_power a is V24() ext-real real set
n to_power a is V24() ext-real real set
n to_power a is V24() ext-real real set
(n to_power a) * (n to_power a) is V24() ext-real real set
n #Z a is set
(n * n) #Z a is set
n #Z a is set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
tau to_power a is V24() ext-real real set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (a + 1) is V24() ext-real real set
(tau to_power a) + (tau to_power (a + 1)) is V24() ext-real real set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (a + 2) is V24() ext-real real set
tau to_power 0 is V24() ext-real real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (0 + 1) is V24() ext-real real set
(tau to_power 0) + (tau to_power (0 + 1)) is V24() ext-real real set
tau to_power 1 is V24() ext-real real set
1 + (tau to_power 1) is V24() ext-real real set
(1 + (sqrt 5)) / 2 is V24() ext-real real set
1 + ((1 + (sqrt 5)) / 2) is V24() ext-real real set
(1 + (sqrt 5)) + (sqrt 5) is V24() ext-real real set
((1 + (sqrt 5)) + (sqrt 5)) + 5 is V24() ext-real real set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((1 + (sqrt 5)) + (sqrt 5)) + 5) / 4 is V24() ext-real real set
5 ^2 is V24() ext-real real Element of REAL
5 * 5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real set
sqrt (5 ^2) is V24() ext-real real Element of REAL
((1 + (sqrt 5)) + (sqrt 5)) + (sqrt (5 ^2)) is V24() ext-real real set
(((1 + (sqrt 5)) + (sqrt 5)) + (sqrt (5 ^2))) / 4 is V24() ext-real real set
1 * (sqrt 5) is V24() ext-real real set
1 + (1 * (sqrt 5)) is V24() ext-real real set
(sqrt 5) * 1 is V24() ext-real real set
(1 + (1 * (sqrt 5))) + ((sqrt 5) * 1) is V24() ext-real real set
(sqrt 5) * (sqrt 5) is V24() ext-real real set
((1 + (1 * (sqrt 5))) + ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5)) is V24() ext-real real set
(((1 + (1 * (sqrt 5))) + ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 is V24() ext-real real set
tau * tau is non empty V24() ext-real positive non negative real set
(tau to_power 1) * tau is V24() ext-real real set
(tau to_power 1) * (tau to_power 1) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (1 + 1) is V24() ext-real real set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (0 + 2) is V24() ext-real real set
1 + tau is non empty V24() ext-real positive non negative real set
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
tau to_power n is V24() ext-real real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (n + 1) is V24() ext-real real set
(tau to_power n) + (tau to_power (n + 1)) is V24() ext-real real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (n + 2) is V24() ext-real real set
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 1) + 1) is V24() ext-real real set
(tau to_power (n + 1)) + (tau to_power ((n + 1) + 1)) is V24() ext-real real set
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 1) + 2) is V24() ext-real real set
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 2) + 1) is V24() ext-real real set
(tau to_power (n + 2)) + (tau to_power ((n + 2) + 1)) is V24() ext-real real set
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 2) + 2) is V24() ext-real real set
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 2) + 1) is V24() ext-real real set
(tau to_power (n + 2)) + (tau to_power ((n + 2) + 1)) is V24() ext-real real set
(tau to_power (n + 2)) * (tau to_power 1) is V24() ext-real real set
(tau to_power (n + 2)) + ((tau to_power (n + 2)) * (tau to_power 1)) is V24() ext-real real set
(tau to_power (n + 2)) * (1 + (tau to_power 1)) is V24() ext-real real set
tau to_power 2 is V24() ext-real real set
(tau to_power (n + 2)) * (tau to_power 2) is V24() ext-real real set
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power ((n + 2) + 2) is V24() ext-real real set
(tau to_power 1) + (tau to_power (1 + 1)) is V24() ext-real real set
tau + (tau to_power (1 + 1)) is V24() ext-real real set
tau + ((tau to_power 1) * (tau to_power 1)) is V24() ext-real real set
tau + ((tau to_power 1) * tau) is V24() ext-real real set
tau + (tau * tau) is non empty V24() ext-real positive non negative real set
tau * (1 + tau) is non empty V24() ext-real positive non negative real set
tau to_power 2 is V24() ext-real real set
(tau to_power 1) * (tau to_power 2) is V24() ext-real real set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (1 + 2) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (1 + 1) is V24() ext-real real set
(tau to_power 1) + (tau to_power (1 + 1)) is V24() ext-real real set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (1 + 2) is V24() ext-real real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (0 + 1) is V24() ext-real real set
(tau to_power 0) + (tau to_power (0 + 1)) is V24() ext-real real set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (0 + 2) is V24() ext-real real set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
tau_bar to_power a is V24() ext-real real set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (a + 1) is V24() ext-real real set
(tau_bar to_power a) + (tau_bar to_power (a + 1)) is V24() ext-real real set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (a + 2) is V24() ext-real real set
tau_bar to_power 0 is V24() ext-real real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (0 + 1) is V24() ext-real real set
(tau_bar to_power 0) + (tau_bar to_power (0 + 1)) is V24() ext-real real set
tau_bar to_power 1 is V24() ext-real real set
1 + (tau_bar to_power 1) is V24() ext-real real set
(1 - (sqrt 5)) / 2 is V24() ext-real real set
1 + ((1 - (sqrt 5)) / 2) is V24() ext-real real set
(1 - (sqrt 5)) - (sqrt 5) is V24() ext-real real set
((1 - (sqrt 5)) - (sqrt 5)) + 5 is V24() ext-real real set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((1 - (sqrt 5)) - (sqrt 5)) + 5) / 4 is V24() ext-real real set
5 ^2 is V24() ext-real real Element of REAL
5 * 5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real set
sqrt (5 ^2) is V24() ext-real real Element of REAL
((1 - (sqrt 5)) - (sqrt 5)) + (sqrt (5 ^2)) is V24() ext-real real set
(((1 - (sqrt 5)) - (sqrt 5)) + (sqrt (5 ^2))) / 4 is V24() ext-real real set
1 * (sqrt 5) is V24() ext-real real set
1 - (1 * (sqrt 5)) is V24() ext-real real set
(sqrt 5) * 1 is V24() ext-real real set
(1 - (1 * (sqrt 5))) - ((sqrt 5) * 1) is V24() ext-real real set
(sqrt 5) * (sqrt 5) is V24() ext-real real set
((1 - (1 * (sqrt 5))) - ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5)) is V24() ext-real real set
(((1 - (1 * (sqrt 5))) - ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 is V24() ext-real real set
tau_bar * tau_bar is non empty V24() ext-real positive non negative real set
(tau_bar to_power 1) * tau_bar is V24() ext-real real set
(tau_bar to_power 1) * (tau_bar to_power 1) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (1 + 1) is V24() ext-real real set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (0 + 2) is V24() ext-real real set
tau_bar + 1 is V24() ext-real real set
tau_bar + (tau_bar to_power 0) is V24() ext-real real set
tau_bar to_power 2 is V24() ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
tau_bar to_power n is V24() ext-real real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (n + 1) is V24() ext-real real set
(tau_bar to_power n) + (tau_bar to_power (n + 1)) is V24() ext-real real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (n + 2) is V24() ext-real real set
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 1) + 1) is V24() ext-real real set
(tau_bar to_power (n + 1)) + (tau_bar to_power ((n + 1) + 1)) is V24() ext-real real set
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 1) + 2) is V24() ext-real real set
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 2) + 1) is V24() ext-real real set
(tau_bar to_power (n + 2)) + (tau_bar to_power ((n + 2) + 1)) is V24() ext-real real set
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 2) + 2) is V24() ext-real real set
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 2) + 1) is V24() ext-real real set
(tau_bar to_power (n + 2)) + (tau_bar to_power ((n + 2) + 1)) is V24() ext-real real set
(tau_bar to_power (n + 2)) * (tau_bar to_power 1) is V24() ext-real real set
(tau_bar to_power (n + 2)) + ((tau_bar to_power (n + 2)) * (tau_bar to_power 1)) is V24() ext-real real set
(tau_bar to_power (n + 2)) * (1 + (tau_bar to_power 1)) is V24() ext-real real set
(tau_bar to_power (n + 2)) * (tau_bar to_power 2) is V24() ext-real real set
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power ((n + 2) + 2) is V24() ext-real real set
(tau_bar to_power 1) + (tau_bar to_power (1 + 1)) is V24() ext-real real set
tau_bar + (tau_bar to_power (1 + 1)) is V24() ext-real real set
tau_bar + ((tau_bar to_power 1) * (tau_bar to_power 1)) is V24() ext-real real set
tau_bar + ((tau_bar to_power 1) * tau_bar) is V24() ext-real real set
tau_bar + (tau_bar * tau_bar) is V24() ext-real real set
1 + tau_bar is V24() ext-real real set
tau_bar * (1 + tau_bar) is V24() ext-real real set
(tau_bar to_power 1) * (tau_bar to_power 2) is V24() ext-real real set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (1 + 2) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (1 + 1) is V24() ext-real real set
(tau_bar to_power 1) + (tau_bar to_power (1 + 1)) is V24() ext-real real set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (1 + 2) is V24() ext-real real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (0 + 1) is V24() ext-real real set
(tau_bar to_power 0) + (tau_bar to_power (0 + 1)) is V24() ext-real real set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power (0 + 2) is V24() ext-real real set
[:NAT,NAT:] is non empty Element of K32(K33(REAL,REAL))
K33(REAL,REAL) is set
K32(K33(REAL,REAL)) is non empty set
K33(NAT,[:NAT,NAT:]) is non empty set
K32(K33(NAT,[:NAT,NAT:])) is non empty set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
[2,1] is Element of K33(NAT,NAT)
K33(NAT,NAT) is non empty set
n is V12() V50( NAT ,[:NAT,NAT:]) Element of K32(K33(NAT,[:NAT,NAT:]))
n . 0 is Element of [:NAT,NAT:]
n . a is Element of [:NAT,NAT:]
(n . a) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n . (n + 1) is Element of [:NAT,NAT:]
n . n is Element of [:NAT,NAT:]
(n . n) `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n . n) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n . n) `1) + ((n . n) `2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[((n . n) `2),(((n . n) `1) + ((n . n) `2))] is Element of K33(NAT,NAT)
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
k is V12() V50( NAT ,[:NAT,NAT:]) Element of K32(K33(NAT,[:NAT,NAT:]))
k . a is Element of [:NAT,NAT:]
(k . a) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
k . 0 is Element of [:NAT,NAT:]
c is V12() V50( NAT ,[:NAT,NAT:]) Element of K32(K33(NAT,[:NAT,NAT:]))
c . a is Element of [:NAT,NAT:]
(c . a) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
c . 0 is Element of [:NAT,NAT:]
(0) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is V12() V50( NAT ,[:NAT,NAT:]) Element of K32(K33(NAT,[:NAT,NAT:]))
a . 0 is Element of [:NAT,NAT:]
[2,1] `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a . (0 + 1) is Element of [:NAT,NAT:]
(a . (0 + 1)) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a . 0) `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a . 0) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a . 0) `1) + ((a . 0) `2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[((a . 0) `2),(((a . 0) `1) + ((a . 0) `2))] is Element of K33(NAT,NAT)
[((a . 0) `2),(((a . 0) `1) + ((a . 0) `2))] `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[2,1] `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((n + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n) + ((n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a . (n + 1) is Element of [:NAT,NAT:]
(a . (n + 1)) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a . n is Element of [:NAT,NAT:]
(a . n) `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a . n) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a . n) `1) + ((a . n) `2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[((a . n) `2),(((a . n) `1) + ((a . n) `2))] is Element of K33(NAT,NAT)
[((a . n) `2),(((a . n) `1) + ((a . n) `2))] `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a . ((n + 1) + 1) is Element of [:NAT,NAT:]
(a . ((n + 1) + 1)) `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a . (n + 1)) `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a . (n + 1)) `1) + ((a . (n + 1)) `2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[((a . (n + 1)) `2),(((a . (n + 1)) `1) + ((a . (n + 1)) `2))] is Element of K33(NAT,NAT)
[((a . (n + 1)) `2),(((a . (n + 1)) `1) + ((a . (n + 1)) `2))] `1 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
[((a . n) `2),(((a . n) `1) + ((a . n) `2))] `2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a . n) `1) + ((a . (n + 1)) `1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n) + ((a . (n + 1)) `1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) + ((a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) + ((a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 3)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((((a + 1) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(0 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((0 + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(3) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((1 + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(4) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((1 + 1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((((1 + 1) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
4 + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) + (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) + (a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real set
(n) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((n + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((n + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n + 2)) + ((n + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
n + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((n + 3)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((2 + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 * ((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 3)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a) + ((a + 3)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) + ((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) + ((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) + (a) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1)) + (a)) + ((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (a + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib a) + (Fib (a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (a + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 1) + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib (a + 1)) + (Fib ((a + 1) + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 2) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 2) + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib (a + 2)) + (Fib ((a + 2) + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 2) + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (((a + 2) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib (a + 2)) + (Fib ((a + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 2) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) + (((a + 1) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib a) + (Fib (a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((Fib a) + (Fib (a + 1))) + (Fib (a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 1) + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((Fib a) + (Fib (a + 1))) + (Fib (a + 2))) + (Fib ((a + 1) + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib ((a + 1) + 1)) + (Fib (a + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((Fib ((a + 1) + 1)) + (Fib (a + 2))) + (Fib ((a + 1) + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib (a + 2)) + (Fib ((a + 2) + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(0 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib 2 is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((1 + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (1 + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib 1) + (Fib (1 + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((0 + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (0 + 2) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(Fib 0) + (Fib (0 + 2)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau_bar to_power 0 is V24() ext-real real set
tau to_power 0 is V24() ext-real real set
(tau to_power 0) + (tau_bar to_power 0) is V24() ext-real real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power a is V24() ext-real real set
tau_bar to_power a is V24() ext-real real set
(tau to_power a) + (tau_bar to_power a) is V24() ext-real real set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (a + 1) is V24() ext-real real set
tau_bar to_power (a + 1) is V24() ext-real real set
(tau to_power (a + 1)) + (tau_bar to_power (a + 1)) is V24() ext-real real set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power (a + 2) is V24() ext-real real set
tau_bar to_power (a + 2) is V24() ext-real real set
(tau to_power (a + 2)) + (tau_bar to_power (a + 2)) is V24() ext-real real set
((tau to_power a) + (tau_bar to_power a)) + ((a + 1)) is V24() ext-real real set
(tau to_power a) + (tau to_power (a + 1)) is V24() ext-real real set
((tau to_power a) + (tau to_power (a + 1))) + (tau_bar to_power a) is V24() ext-real real set
(((tau to_power a) + (tau to_power (a + 1))) + (tau_bar to_power a)) + (tau_bar to_power (a + 1)) is V24() ext-real real set
(tau to_power (a + 2)) + (tau_bar to_power a) is V24() ext-real real set
((tau to_power (a + 2)) + (tau_bar to_power a)) + (tau_bar to_power (a + 1)) is V24() ext-real real set
(tau_bar to_power a) + (tau_bar to_power (a + 1)) is V24() ext-real real set
(tau to_power (a + 2)) + ((tau_bar to_power a) + (tau_bar to_power (a + 1))) is V24() ext-real real set
tau_bar to_power 1 is V24() ext-real real set
tau to_power 1 is V24() ext-real real set
(tau to_power 1) + (tau_bar to_power 1) is V24() ext-real real set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
tau to_power a is V24() ext-real real set
tau_bar to_power a is V24() ext-real real set
(tau to_power a) + (tau_bar to_power a) is V24() ext-real real set
a is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real set
(a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 * (a) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(2 * (a)) + ((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib (a + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
5 * (Fib (a + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 * ((a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 1) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(2 * ((a + 1))) + (((a + 1) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
5 * (Fib ((a + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
2 * ((a + 2)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 2) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(2 * ((a + 2))) + (((a + 2) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
Fib ((a + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
5 * (Fib ((a + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() ext-real non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(a + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(((a + 2) + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V24() ext-real positive non negative real V29() V30() V31() V32() V33() V34() V36() V53() Element of NAT
(2 * ((a + 2))) + (((a