:: SCHEME1 semantic presentation

REAL is non empty set

NAT is non empty V18() V19() V20() Element of bool REAL

bool REAL is set

COMPLEX is non empty set

RAT is non empty set

INT is non empty set

0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

the empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() set is empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() set

1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

{} is set

[:NAT,REAL:] is set

bool [:NAT,REAL:] is set

NAT is non empty V18() V19() V20() set

2 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f div 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

2 * (f div 2) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(2 * (f div 2)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f mod 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(2 * (f div 2)) + (f mod 2) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f div 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * (f div 3) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * (f div 3)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * (f div 3)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f mod 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * (f div 3)) + (f mod 3) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f div 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * (f div 4) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * (f div 4)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * (f div 4)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * (f div 4)) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f mod 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

(4 * (f div 4)) + (f mod 4) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f div 5 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * (f div 5) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * (f div 5)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * (f div 5)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * (f div 5)) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * (f div 5)) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

f mod 5 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

3 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT

(5 * (f div 5)) + (f mod 5) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

f is ext-real V18() V19() V20() V24() V25() V32() set

F

v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

v + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

F

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

z is ext-real V18() V19() V20() V24() V25() V32() set

F

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

[:NAT,NAT:] is set

bool [:NAT,NAT:] is set

v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

v is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

v . 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

dom v is Element of bool NAT

bool NAT is set

rng v is V46() V47() V48() V51() Element of bool NAT

c

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

c

z is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

z is ext-real V18() V19() V20() V24() V25() V32() set

F

z . 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() set

F

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() set

F

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

z . c

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . (x + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of F

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . y is ext-real V25() V32() Element of REAL

y + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . (y + 1) is ext-real V25() V32() Element of REAL

z . y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . (y + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

c

F

F

z . 0 is ext-real V25() V32() Element of REAL

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

F

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . x is ext-real V25() V32() Element of REAL

bool NAT is set

f is Element of bool NAT

v is Element of bool NAT

v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

v / 2 is ext-real V25() V32() set

F

v - 1 is ext-real V25() V32() set

(v - 1) / 2 is ext-real V25() V32() set

F

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(2 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(2 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z is ext-real V25() V32() Element of REAL

v is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

c

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

F

(2 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

c

F

(2 * z) / 2 is ext-real V25() V32() set

F

((2 * z) + 1) - 1 is ext-real V25() V32() set

(((2 * z) + 1) - 1) / 2 is ext-real V25() V32() set

F

bool NAT is set

f is Element of bool NAT

v is Element of bool NAT

v is Element of bool NAT

c

c

F

c

(c

F

c

(c

F

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(3 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y is ext-real V25() V32() Element of REAL

c

z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

3 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . (3 * z) is ext-real V25() V32() Element of REAL

F

(3 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . ((3 * z) + 1) is ext-real V25() V32() Element of REAL

F

(3 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . ((3 * z) + 2) is ext-real V25() V32() Element of REAL

F

(3 * z) / 3 is ext-real V25() V32() set

F

((3 * z) + 1) - 1 is ext-real V25() V32() set

(((3 * z) + 1) - 1) / 3 is ext-real V25() V32() set

F

((3 * z) + 2) - 2 is ext-real V25() V32() set

(((3 * z) + 2) - 2) / 3 is ext-real V25() V32() set

F

bool NAT is set

f is Element of bool NAT

v is Element of bool NAT

v is Element of bool NAT

c

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z / 4 is ext-real V25() V32() set

F

z - 1 is ext-real V25() V32() set

(z - 1) / 4 is ext-real V25() V32() set

F

z - 2 is ext-real V25() V32() set

(z - 2) / 4 is ext-real V25() V32() set

F

z - 3 is ext-real V25() V32() set

(z - 3) / 4 is ext-real V25() V32() set

F

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * z) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V25() V32() Element of REAL

z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

4 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . (4 * y) is ext-real V25() V32() Element of REAL

F

(4 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . ((4 * y) + 1) is ext-real V25() V32() Element of REAL

F

(4 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . ((4 * y) + 2) is ext-real V25() V32() Element of REAL

F

(4 * y) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z . ((4 * y) + 3) is ext-real V25() V32() Element of REAL

F

(4 * y) / 4 is ext-real V25() V32() set

F

((4 * y) + 1) - 1 is ext-real V25() V32() set

(((4 * y) + 1) - 1) / 4 is ext-real V25() V32() set

F

((4 * y) + 2) - 2 is ext-real V25() V32() set

(((4 * y) + 2) - 2) / 4 is ext-real V25() V32() set

F

((4 * y) + 3) - 3 is ext-real V25() V32() set

(((4 * y) + 3) - 3) / 4 is ext-real V25() V32() set

F

bool NAT is set

f is Element of bool NAT

v is Element of bool NAT

v is Element of bool NAT

c

z is Element of bool NAT

z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

z / 5 is ext-real V25() V32() set

F

z - 1 is ext-real V25() V32() set

(z - 1) / 5 is ext-real V25() V32() set

F

z - 2 is ext-real V25() V32() set

(z - 2) / 5 is ext-real V25() V32() set

F

z - 3 is ext-real V25() V32() set

(z - 3) / 5 is ext-real V25() V32() set

F

z - 4 is ext-real V25() V32() set

(z - 4) / 5 is ext-real V25() V32() set

F

y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * y) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * y) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

d is ext-real V25() V32() Element of REAL

z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

y is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y . (5 * x) is ext-real V25() V32() Element of REAL

F

(5 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y . ((5 * x) + 1) is ext-real V25() V32() Element of REAL

F

(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y . ((5 * x) + 2) is ext-real V25() V32() Element of REAL

F

(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y . ((5 * x) + 3) is ext-real V25() V32() Element of REAL

F

(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

y . ((5 * x) + 4) is ext-real V25() V32() Element of REAL

F

(5 * x) / 5 is ext-real V25() V32() set

F

((5 * x) + 1) - 1 is ext-real V25() V32() set

(((5 * x) + 1) - 1) / 5 is ext-real V25() V32() set

F

((5 * x) + 2) - 2 is ext-real V25() V32() set

(((5 * x) + 2) - 2) / 5 is ext-real V25() V32() set

F

((5 * x) + 3) - 3 is ext-real V25() V32() set

(((5 * x) + 3) - 3) / 5 is ext-real V25() V32() set

F

((5 * x) + 4) - 4 is ext-real V25() V32() set

(((5 * x) + 4) - 4) / 5 is ext-real V25() V32() set

F

F

F

[:F

bool [:F

f is set

v is set

F

F

v is Element of F

v is Element of F

z is set

v is Relation-like Function-like set

dom v is set

v is set

rng v is set

v is set

c

v . c

F

F

v is Relation-like F

dom v is Element of bool F

bool F

c

z is Element of F

c

v . c

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

v is Element of F

F

F

z is set

v is Element of F

F

F

z is set

v is Element of F

z is set

v is Relation-like Function-like set

dom v is set

v is set

rng v is set

v is set

c

v . c

F

F

v is Relation-like F

dom v is Element of bool F

bool F

c

z is Element of F

c

v . c

F

F

F

F

[:F

bool [:F

f is Element of F

f is Relation-like F

dom f is Element of bool F

bool F

v is set

v is Element of F

v is Element of F

f . v is set

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

F

v is Element of F

v is Element of F

v is Element of F

z is set

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

F

F

F

v is set

v is Relation-like F

dom v is Element of bool F

bool F

c

z is Element of F

c

v . c

F

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

F

v is Element of F

F

F

F

z is set

F

z is set

z is set

v is Element of F

F

F

F

z is set

F

F

z is set

z is set

v is Element of F

F

F

F

z is set

F

F

z is set

z is set

v is Element of F

z is set

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

F

F

F

v is set

v is Relation-like F

dom v is Element of bool F

bool F

c

z is Element of F

c

v . c

F

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

F

F

v is Element of F

v is Element of F

v is Element of F

v is Element of F

z is set

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

F

F

F

F

v is set

v is Relation-like F

dom v is Element of bool F

bool F

c

z is Element of F

c

v . c

F

F

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

c

v is Relation-like Function-like set

dom v is set

v is set

rng v is set

v is set

c

v . c

F

F

v is Relation-like F

dom v is Element of bool F

bool F

c

z is set

c

v . c

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

F

c

v is Relation-like Function-like set

dom v is set

v is set

rng v is set

v is set

c

v . c

F

F

F

v is Relation-like F

dom v is Element of bool F

bool F

c

z is set

c

v . c

F

F

F

F

F

[:F

bool [:F

f is set

v is set

F

F

F

F

c

v is Relation-like Function-like set

dom v is set

v is set

rng v is set

v is set

c

v . c

F

F

F

F

v is Relation-like F

dom v is Element of bool F

bool F

c

z is set

c

v . c

F

F

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is set

v is set

v is set

c

[v,c

{v,c

{v} is set

{{v,c

z is Element of F

z is Element of F

F

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

y is Element of F

F

F

z is Element of F

z is Element of F

F

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

y is Element of F

F

F

z is Element of F

z is Element of F

y is Element of F

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

z is set

z is set

[z,z] is set

{z,z} is set

{z} is set

{{z,z},{z}} is set

x is Element of F

y is Element of F

[x,y] is set

{x,y} is set

{x} is set

{{x,y},{x}} is set

v . [x,y] is set

F

x is Element of F

y is Element of F

[x,y] is set

{x,y} is set

{x} is set

{{x,y},{x}} is set

v . [x,y] is set

F

x is Element of F

y is Element of F

v is set

v is Relation-like [:F

dom v is Relation-like F

bool [:F

c

z is Element of F

[c

{c

{c

{{c

z is Element of F

y is Element of F

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

c

z is Element of F

[c

{c

{c

{{c

v . [c

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is set

v is set

v is set

c

[v,c

{v,c

{v} is set

{{v,c

z is Element of F

z is Element of F

F

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

y is Element of F

F

F

F

z is Element of F

z is Element of F

F

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

y is Element of F

F

F

F

z is Element of F

z is Element of F

F

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

y is Element of F

F

F

F

z is Element of F

z is Element of F

y is Element of F

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

z is set

z is set

[z,z] is set

{z,z} is set

{z} is set

{{z,z},{z}} is set

x is Element of F

y is Element of F

[x,y] is set

{x,y} is set

{x} is set

{{x,y},{x}} is set

v . [x,y] is set

F

x is Element of F

y is Element of F

[x,y] is set

{x,y} is set

{x} is set

{{x,y},{x}} is set

v . [x,y] is set

F

x is Element of F

y is Element of F

[x,y] is set

{x,y} is set

{x} is set

{{x,y},{x}} is set

v . [x,y] is set

F

x is Element of F

y is Element of F

v is set

v is Relation-like [:F

dom v is Relation-like F

bool [:F

c

z is Element of F

[c

{c

{c

{{c

z is Element of F

y is Element of F

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

c

z is Element of F

[c

{c

{c

{{c

v . [c

F

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is set

v is set

v is set

c

[v,c

{v,c

{v} is set

{{v,c

F

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

z is set

F

F

F

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

z is set

F

F

z is set

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

z is set

z is set

[z,z] is set

{z,z} is set

{z} is set

{{z,z},{z}} is set

v . [z,z] is set

F

v . [z,z] is set

F

v is set

v is Relation-like [:F

dom v is Relation-like F

bool [:F

c

z is set

[c

{c

{c

{{c

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

c

z is set

[c

{c

{c

{{c

v . [c

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is set

v is set

v is set

c

[v,c

{v,c

{v} is set

{{v,c

F

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

z is set

F

F

F

F

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

z is set

F

F

F

F

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

z is set

F

F

F

z is set

v is Relation-like Function-like set

dom v is set

rng v is set

v is set

c

v . c

z is set

z is set

[z,z] is set

{z,z} is set

{z} is set

{{z,z},{z}} is set

v . [z,z] is set

F

v . [z,z] is set

F

v . [z,z] is set

F

v is set

v is Relation-like [:F

dom v is Relation-like F

bool [:F

c

z is set

[c

{c

{c

{{c

z is set

y is set

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

c

z is set

[c

{c

{c

{{c

v . [c

F

F

F

F

F

[:F

bool [:F

f is Element of F

v is Element of F

v is Element of F

f is Relation-like F

dom f is Element of bool F

bool F

v is set

c

v is Relation-like F

c

v . c

F

F

F

F

F

[:F

bool [:F

f is Element of F

v is Element of F

v is Element of F

c

z is Element of F

z is Element of F

f is Relation-like F

dom f is Element of bool F

bool F

v is set

c

v is Relation-like F

c

v . c

F

F

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of F

v is Element of F

f is Relation-like [:F

dom f is Relation-like F

bool [:F

v is Relation-like Function-like set

v is set

c

z is set

[c

{c

{c

{{c

y is Element of F

z is Element of F

v is Relation-like [:F

dom v is Relation-like F

c

z is Element of F

[c

{c

{c

{{c

v . [c

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of F

v is Element of F

v is Element of F

c

z is Element of F

z is Element of F

f is Relation-like [:F

dom f is Relation-like F

bool [:F

v is Relation-like Function-like set

v is set

c

z is set

[c

{c

{c

{{c

y is Element of F

z is Element of F

v is Relation-like [:F

dom v is Relation-like F

c

z is Element of F

[c

{c

{c

{{c

z is Element of F

y is Element of F

[z,y] is set

{z,y} is set

{z} is set

{{z,y},{z}} is set

x is Element of F

d is Element of F

[x,d] is set

{x,d} is set

{x} is set

{{x,d},{x}} is set

v . [x,d] is set

F

F

F