:: PEPIN semantic presentation

REAL is set

K6(REAL) is V35() V37() V38() set

K6(omega) is V2() V35() V37() V38() non finite set
K6(NAT) is V2() V35() V37() V38() non finite set
K163(NAT) is non empty V35() V37() V38() set
RAT is set
INT is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is V35() V37() V38() set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is V35() V37() V38() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V35() V37() V38() set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is V35() V37() V38() set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is V35() V37() V38() set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is V35() V37() V38() set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is V35() V37() V38() set
K7(INT,INT) is set
K6(K7(INT,INT)) is V35() V37() V38() set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is V35() V37() V38() set
K7(NAT,NAT) is V2() non finite set
K7(K7(NAT,NAT),NAT) is V2() non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() V35() V37() V38() non finite set
K389() is set

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

1 - 1 is V11() ext-real real integer set
r - 1 is V11() ext-real real integer set
- 1 is V11() ext-real non positive real integer set
r + (- 1) is V11() ext-real real integer set
(r + (- 1)) + 1 is V11() ext-real real integer set
(r + 1) - 1 is V11() ext-real real integer set

r ^2 is set

1 / r is V11() ext-real real set
[\(1 / r)/] is V11() ext-real real integer set

1 - (0 * r) is V11() ext-real real integer set

m / r is V11() ext-real non negative real set
[\(m / r)/] is V11() ext-real real integer set

r / m is V11() ext-real non negative real set
[\(r / m)/] is V11() ext-real real integer set

((r * m) * n) + (n mod (r * m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(m * (r * n)) + (n mod (r * m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(m * r) + 1 is V11() ext-real real integer set
((m * r) + 1) mod r is V11() ext-real real integer set

(m * n) + 1 is V11() ext-real real integer set
((m * n) + 1) mod n is V11() ext-real real integer set
((m * n) + 1) div n is V11() ext-real real integer set
((m * n) + 1) / n is V11() ext-real real set
[\(((m * n) + 1) / n)/] is V11() ext-real real integer set
(((m * n) + 1) div n) * n is V11() ext-real real integer set
((m * n) + 1) - ((((m * n) + 1) div n) * n) is V11() ext-real real integer set
(m * n) / n is V11() ext-real real set
1 / n is V11() ext-real real set
((m * n) / n) + (1 / n) is V11() ext-real real set
[\(((m * n) / n) + (1 / n))/] is V11() ext-real real integer set
[\(((m * n) / n) + (1 / n))/] * n is V11() ext-real real integer set
((m * n) + 1) - ([\(((m * n) / n) + (1 / n))/] * n) is V11() ext-real real integer set
m + (1 / n) is V11() ext-real real set
[\(m + (1 / n))/] is V11() ext-real real integer set
[\(m + (1 / n))/] * n is V11() ext-real real integer set
((m * n) + 1) - ([\(m + (1 / n))/] * n) is V11() ext-real real integer set
[\(1 / n)/] is V11() ext-real real integer set
m + [\(1 / n)/] is V11() ext-real real integer set
(m + [\(1 / n)/]) * n is V11() ext-real real integer set
((m * n) + 1) - ((m + [\(1 / n)/]) * n) is V11() ext-real real integer set

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

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

r * (n - m) is V11() ext-real real integer set
m - 1 is V11() ext-real real integer set
n * (m - 1) is V11() ext-real real integer set

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

(x * y) + 1 is V11() ext-real real integer set

(((r |^ m) mod n) * (r mod n)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(((r mod n) |^ m) * (r mod n)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(r * (2 |^ (m + 1))) / 2 is V11() ext-real non negative real set
[\((r * (2 |^ (m + 1))) / 2)/] is V11() ext-real real integer set

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

((n mod (r + 1)) + 1) mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(((m * m) * m) + (r * m)) + (m * r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * ((((m * m) * m) + (r * m)) + (m * r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * ((((m * m) * m) + (r * m)) + (m * r))) + (r ^2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

- 1 is V11() ext-real non positive real integer set

m / r is V11() ext-real non negative real set
[\(m / r)/] is V11() ext-real real integer set

m - ((m div r) * r) is V11() ext-real real integer set
((m div r) * r) - 1 is V11() ext-real real integer set
((m div r) * r) - 2 is V11() ext-real real integer set
(((m div r) * r) - 2) * (m div r) is V11() ext-real real integer set
((((m div r) * r) - 2) * (m div r)) * r is V11() ext-real real integer set
(((((m div r) * r) - 2) * (m div r)) * r) + 1 is V11() ext-real real integer set

(2 |^ (2 |^ r)) * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(2 |^ (2 |^ m)) * (2 |^ (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(2 |^ (2 |^ (m + 1))) * (2 |^ (2 |^ (m + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(2 |^ (2 |^ (m + 1))) * (2 |^ (2 |^ (m + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(2 |^ ((2 |^ m) * 2)) * (2 |^ ((2 |^ m) * 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

((2 |^ (2 |^ m)) |^ 2) * ((2 |^ (2 |^ m)) |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

((2 |^ (2 |^ m)) ^2) * ((2 |^ (2 |^ m)) ^2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(2 |^ (2 |^ 0)) * (2 |^ (2 |^ 0)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

m / 2 is V11() ext-real non negative real set
[\(m / 2)/] is V11() ext-real real integer set

(r |^ (m div 2)) * (r |^ (m div 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set

(m + m) / 2 is V11() ext-real non negative real set
[\((m + m) / 2)/] is V11() ext-real real integer set

(2 * m) / 2 is V11() ext-real non negative real set
[\((2 * m) / 2)/] is V11() ext-real real integer set

(r |^ m) / r is V11() ext-real non negative real set
[\((r |^ m) / r)/] is V11() ext-real real integer set

1 - 1 is V11() ext-real real integer set
m - 1 is V11() ext-real real integer set
(m - 1) + 1 is V11() ext-real real integer set

(2 |^ (m + 1)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (m + 1)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT

(2 * (2 |^ m)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 * (2 |^ m)) + (2 * (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT

(m + m) - m is V11() ext-real real integer set

(m + 1) - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set

(2 |^ m) / (2 |^ r) is V11() ext-real non negative real set
[\((2 |^ m) / (2 |^ r))/] is V11() ext-real real integer set
(2 |^ r) * ((2 |^ m) div (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT