:: FIB_NUM2 semantic presentation

bool REAL is non empty non empty-membered set
bool NAT is non empty non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered complex-membered V92() set

bool omega is non empty non empty-membered set
K158(NAT) is V35() set
is Relation-like V76() V77() V78() set

K325() is set

K520() is set
bool K520() is set
K521() is Element of bool K520()

sqrt 4 is V11() real ext-real Element of REAL

{ } is set

{ } is set

{ } is set

{ } is set
K603(1,2,3,4) is finite with_non-empty_elements set

sqrt 5 is V11() real ext-real Element of REAL
1 + (sqrt 5) is V11() real ext-real set
K65((1 + (sqrt 5)),2) is V11() real ext-real Element of COMPLEX

1 - (sqrt 5) is V11() real ext-real set
K65((1 - (sqrt 5)),2) is V11() real ext-real Element of COMPLEX

(n + 2) - 1 is V11() real integer ext-real set
- 1 is V11() real integer ext-real non positive set
n is non empty V11() real integer ext-real non even set
(- 1) to_power n is V11() real ext-real set

- (1 to_power n) is V11() real ext-real set

(- 1) to_power n is V11() real ext-real set

n is non empty V11() real ext-real set
(- 1) * n is V11() real ext-real set

((- 1) * n) to_power n is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set

((- 1) to_power n) * (n to_power n) is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power n is V11() real ext-real set
- (n to_power n) is V11() real ext-real set
(- 1) * (n to_power n) is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power n is V11() real ext-real set
1 * (n to_power n) is V11() real ext-real set

C is V11() real ext-real set
C to_power (n + n) is V11() real ext-real set

(C to_power n) * (C to_power n) is V11() real ext-real set
C |^ (n + n) is V11() real ext-real set
C |^ n is V11() real ext-real set
C |^ n is V11() real ext-real set
(C |^ n) * (C |^ n) is V11() real ext-real set
(C to_power n) * (C |^ n) is V11() real ext-real set

n is non empty V11() real ext-real set
C is non empty V11() real integer ext-real non even set

(n to_power C) to_power n is V11() real ext-real set

n to_power (C * n) is V11() real ext-real set
n #Z (C * n) is V11() real ext-real set
n #Z C is V11() real ext-real set
(n #Z C) #Z n is V11() real ext-real set
(n to_power C) #Z n is V11() real ext-real set

(- 1) to_power (- n) is V11() real ext-real set
((- 1) to_power (- n)) ^2 is V11() real ext-real set
((- 1) to_power (- n)) * ((- 1) to_power (- n)) is V11() real ext-real set
(- 1) #Z (- n) is V11() real ext-real set
((- 1) #Z (- n)) ^2 is V11() real ext-real set
((- 1) #Z (- n)) * ((- 1) #Z (- n)) is V11() real ext-real set
(- 1) #Z n is V11() real ext-real set
1 / ((- 1) #Z n) is V11() real ext-real set
(1 / ((- 1) #Z n)) ^2 is V11() real ext-real set
(1 / ((- 1) #Z n)) * (1 / ((- 1) #Z n)) is V11() real ext-real set
(1 / ((- 1) #Z n)) to_power 2 is V11() real ext-real set
(1 / ((- 1) #Z n)) |^ 2 is V11() real ext-real set
((- 1) #Z n) |^ 2 is V11() real ext-real set
1 / (((- 1) #Z n) |^ 2) is V11() real ext-real set
((- 1) #Z n) #Z 2 is V11() real ext-real set
1 / (((- 1) #Z n) #Z 2) is V11() real ext-real set

(- 1) #Z (n * 2) is V11() real ext-real set
1 / ((- 1) #Z (n * 2)) is V11() real ext-real set

(- 1) |^ (2 * n) is V11() real ext-real set
1 / ((- 1) |^ (2 * n)) is V11() real ext-real set

1 / (1 |^ (2 * n)) is V11() real ext-real non negative set

1 / ((1 |^ 2) |^ n) is V11() real ext-real non negative set

1 / (1 |^ n) is V11() real ext-real non negative set
1 / 1 is V11() real ext-real non negative set

(- n) - n is V11() real integer ext-real non positive set
r is non empty V11() real ext-real set
r to_power (- n) is V11() real ext-real set
r to_power (- n) is V11() real ext-real set
(r to_power (- n)) * (r to_power (- n)) is V11() real ext-real set
r to_power ((- n) - n) is V11() real ext-real set
r #Z (- n) is V11() real ext-real set
(r #Z (- n)) * (r to_power (- n)) is V11() real ext-real set
r #Z (- n) is V11() real ext-real set
(r #Z (- n)) * (r #Z (- n)) is V11() real ext-real set
(- n) + (- n) is V11() real integer ext-real non positive set
r #Z ((- n) + (- n)) is V11() real ext-real set

- (2 * n) is V11() real integer ext-real non positive set
(- 1) to_power (- (2 * n)) is V11() real ext-real set
(- 1) * (2 * n) is V11() real integer ext-real non positive even set
(- 1) #Z ((- 1) * (2 * n)) is V11() real ext-real set
(- 1) #Z (- 1) is V11() real ext-real set
((- 1) #Z (- 1)) #Z (2 * n) is V11() real ext-real set
(- 1) #Z 1 is V11() real ext-real set
1 / ((- 1) #Z 1) is V11() real ext-real set
(1 / ((- 1) #Z 1)) #Z (2 * n) is V11() real ext-real set
1 / (- 1) is V11() real ext-real non positive set
(1 / (- 1)) #Z (2 * n) is V11() real ext-real set
(- 1) |^ (2 * n) is V11() real ext-real set

n is non empty V11() real ext-real set

n to_power (- n) is V11() real ext-real set
(n to_power n) * (n to_power (- n)) is V11() real ext-real set
n #Z n is V11() real ext-real set
(n #Z n) * (n to_power (- n)) is V11() real ext-real set
n #Z (- n) is V11() real ext-real set
(n #Z n) * (n #Z (- n)) is V11() real ext-real set
n + (- n) is V11() real integer ext-real set
n #Z (n + (- n)) is V11() real ext-real set
n is non empty V11() real integer ext-real non even set

2 * (- 1) is V11() real integer ext-real non positive even set
(2 * (- 1)) + 1 is non empty V11() real integer ext-real non even set
n is non empty V11() real integer ext-real non even set
n * n is non empty V11() real integer ext-real non even set

(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set
n is non empty V11() real integer ext-real non even set
- n is non empty V11() real integer ext-real non even set
(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set

(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set

dom (n | n) is finite set

{ } is set
r is set

dom n is set

rng (Seq n) is finite set
rng n is set

dom (n | n) is finite set

(Sgm (dom (n | n))) (#) (n | n) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V76() V77() V78() V79() set
rng (Seq (n | n)) is finite set

(n + C) - n is V11() real integer ext-real set

C is set
[n,C] is set
{n,C} is non empty finite set

{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
C is set
[n,C] is set
{n,C} is non empty finite set

{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,C],[n,C]} is non empty Relation-like finite set

k is set

{ } is set

dom r is set

C is set
[n,C] is set
{n,C} is non empty finite set

{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
C is set
[n,C] is set
{n,C} is non empty finite set

{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,C],[n,C]} is non empty Relation-like finite set

[1,C] is set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,C]} is non empty Relation-like Function-like finite set

[1,C] is set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,C]} is non empty Relation-like Function-like finite set

dom r is set

(n,n) --> (C,C) is finite set

{ } is set

[1,n] is set

{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set

[1,n] is set

{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set

r . n is set
r . n is set

[1,(r . n)] is set
{1,(r . n)} is non empty finite set
{{1,(r . n)},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,(r . n)]} is non empty Relation-like Function-like finite set

[1,(r . n)] is set
{1,(r . n)} is non empty finite set
{{1,(r . n)},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,(r . n)]} is non empty Relation-like Function-like finite set

{ } is set

bool n is set
n is Element of bool n

n is set
n /\ n is set
bool n is set

n is set
[n,n] is set
{n,n} is non empty finite set

{{n,n},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,n]} is non empty Relation-like Function-like finite set

dom C is set

{ } is set
C is set

n is set
[1,n] is set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set
[(1 + n),n] is set
{(1 + n),n} is non empty finite set

{{(1 + n),n},{(1 + n)}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[(1 + n),n]} is non empty Relation-like Function-like finite set

card (n Shift C) is cardinal set
dom C is set

dom (n Shift C) is set

r is set
{ } is set

r is set
(n Shift C) . (1 + n) is set
C . 1 is set
r is set
{r} is non empty finite set

dom n is set

{ } is set

{ } is set

dom (C +* n) is set
dom C is set
(dom C) \/ (dom n) is set
(Seg C) \/ (dom n) is set

dom n is set

{ } is set

dom (C +* n) is set
dom C is set
(dom C) \/ (dom n) is set
(Seg n) \/ (dom n) is set

n - 1 is V11() real integer ext-real set
1 - 1 is V11() real integer ext-real set

(Fib (((2 * n) + 2) + 1)) + (Fib ((((2 * n) + 2) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

(Fib (n + 3)) - (Fib (n + 1)) is V11() real integer ext-real set