:: GR_CY_3 semantic presentation

REAL is set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is set

the carrier of K677() is set

NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set
K6(NAT) is V2() non finite set
K6(NAT) is V2() non finite set
1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
K7(1,1) is Relation-like finite set
K6(K7(1,1)) is finite V40() set
K7(K7(1,1),1) is Relation-like finite set
K6(K7(K7(1,1),1)) is finite V40() set
K7(K7(1,1),REAL) is Relation-like set
K6(K7(K7(1,1),REAL)) is set

K7(K7(REAL,REAL),REAL) is Relation-like set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
K7(2,2) is Relation-like finite set
K7(K7(2,2),REAL) is Relation-like set
K6(K7(K7(2,2),REAL)) is set
RAT is set
INT is set
K6(K7(REAL,REAL)) is set
K339(2) is V159() L15()
the carrier of K339(2) is set

the carrier of K480() is non empty V139() set

addint is Relation-like Function-like V32(K7(INT,INT), INT ) Element of K6(K7(K7(INT,INT),INT))
K7(INT,INT) is Relation-like set
K7(K7(INT,INT),INT) is Relation-like set
K6(K7(K7(INT,INT),INT)) is set
multint is Relation-like Function-like V32(K7(INT,INT), INT ) Element of K6(K7(K7(INT,INT),INT))
In (1,INT) is V11() V12() integer ext-real Element of INT

In (0,INT) is V11() V12() integer ext-real Element of INT
doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is strict doubleLoopStr
the carrier of INT.Ring is non empty V2() non finite V139() set
K7( the carrier of INT.Ring,NAT) is V2() Relation-like non finite set
K6(K7( the carrier of INT.Ring,NAT)) is V2() non finite set

K6(K7(COMPLEX,COMPLEX)) is set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is Relation-like set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is Relation-like set
K6(K7(K7(RAT,RAT),RAT)) is set
K6(K7(INT,INT)) is set
K7(NAT,NAT) is V2() Relation-like non finite set
K7(K7(NAT,NAT),NAT) is V2() Relation-like non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() non finite set
K588() is set

K6(K7(NAT,REAL)) is set
K313(1,NAT) is M11( NAT )
K7(NAT, the carrier of K677()) is Relation-like set
K6(K7(NAT, the carrier of K677())) is set
K6( the carrier of K677()) is set
3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
6 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
- 1 is V11() V12() integer ext-real non positive set
is non empty V2() finite V40() 1 -element Element of K6(NAT)
8 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
F * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a gcd F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
f * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F * (f * g) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a gcd F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 - 2 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 gcd 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * a) + 1) - 1 is V11() V12() integer ext-real set
2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 4) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 * F)) mod (2 * 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * F) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 mod 3) * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 mod 3) * (F mod 3)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (((2 mod 3) * (F mod 3)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (F mod 3)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (F mod 3)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * 2) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * 2) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + (3 * 1) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(1 + (3 * 1)) mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((1 + (3 * 1)) mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (1 mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod (3 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (F mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
6 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F + (6 * F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F + (6 * F)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) + (4 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 * F) + (4 * F)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * 1) + (2 * 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 * 1) + (2 * 1)) mod 6 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
12 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
11 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 - 2 is V11() V12() integer ext-real set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
9 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
9 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(9 * F) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (3 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * (3 * F)) mod (3 * 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * F) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((3 * F) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 mod 4) * (F mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((3 mod 4) * (F mod 4)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (((3 mod 4) * (F mod 4)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(3 * 3) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((3 * 3) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + (4 * 2) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(1 + (4 * 2)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * ((1 + (4 * 2)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * (1 mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) mod (4 * 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F mod 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * (F mod 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
12 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F + (12 * F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F + (12 * F)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * F) + (9 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((4 * F) + (9 * F)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * 2) + (3 * 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((4 * 2) + (3 * 1)) mod 12 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * a) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 2) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 5 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 8) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 8) + 6 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 8) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 8) * 4) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 8) * 4) + 3) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 2) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(((F div 4) * 2) + 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
0 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
Euler F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F - 1 is V11() V12() integer ext-real set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
Euler a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
Euler G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
Euler F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
() * () is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * g) * f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set

Segm0 F is non empty finite Element of K6(NAT)
multint0 F is Relation-like Function-like V28(K7((),())) V32(K7((),()), Segm0 F) finite Element of K6(K7(K7((),()),()))
K7((),()) is Relation-like finite set
K7(K7((),()),()) is Relation-like finite set
K6(K7(K7((),()),())) is finite V40() set
multint F is Relation-like Function-like V28(K7((Segm F),(Segm F))) V32(K7((Segm F),(Segm F)), Segm F) Element of K6(K7(K7((Segm F),(Segm F)),(Segm F)))
Segm F is non empty V140() Element of K6(NAT)
K7((Segm F),(Segm F)) is Relation-like set
K7(K7((Segm F),(Segm F)),(Segm F)) is Relation-like set
K6(K7(K7((Segm F),(Segm F)),(Segm F))) is set
() || () is set
multMagma(# (),() #) is strict multMagma
card (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (Z/Z* F) is non empty finite set
card the carrier of (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * G) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F - 1 is V11() V12() integer ext-real set

card F is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of F is non empty finite set
card the carrier of F is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
G * a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
f is Element of the carrier of F
ord f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
f |^ a is Element of the carrier of F
power F is Relation-like Function-like V28(K7( the carrier of F,NAT)) V32(K7( the carrier of F,NAT), the carrier of F) Element of K6(K7(K7( the carrier of F,NAT), the carrier of F))
K7( the carrier of F,NAT) is V2() Relation-like non finite set
K7(K7( the carrier of F,NAT), the carrier of F) is V2() Relation-like non finite set
K6(K7(K7( the carrier of F,NAT), the carrier of F)) is V2() non finite set
() . (f,a) is set
ord (f |^ a) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
g is Element of the carrier of F
ord g is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{g} is non empty V2() finite 1 -element Element of K6( the carrier of F)
K6( the carrier of F) is finite V40() set

F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set

Segm0 F is non empty finite Element of K6(NAT)
multint0 F is Relation-like Function-like V28(K7((),())) V32(K7((),()), Segm0 F) finite Element of K6(K7(K7((),()),()))
K7((),()) is Relation-like finite set
K7(K7((),()),()) is Relation-like finite set
K6(K7(K7((),()),())) is finite V40() set
multint F is Relation-like Function-like V28(K7((Segm F),(Segm F))) V32(K7((Segm F),(Segm F)), Segm F) Element of K6(K7(K7((Segm F),(Segm F)),(Segm F)))
Segm F is non empty V140() Element of K6(NAT)
K7((Segm F),(Segm F)) is Relation-like set
K7(K7((Segm F),(Segm F)),(Segm F)) is Relation-like set
K6(K7(K7((Segm F),(Segm F)),(Segm F))) is set
() || () is set
multMagma(# (),() #) is strict multMagma
card (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (Z/Z* F) is non empty finite set
card the carrier of (Z/Z* F) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
G is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
2 * G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
a is Element of the carrier of (Z/Z* F)
ord a is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{a} is non empty V2() finite 1 -element Element of K6( the carrier of (Z/Z* F))
K6( the carrier of (Z/Z* F)) is finite V40() set

f is Element of the carrier of (Z/Z* F)
ord f is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
{f} is non empty V2() finite 1 -element Element of K6( the carrier of (Z/Z* F))

card (gr {f}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {f}) is non empty finite set
card the carrier of (gr {f}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card ((1). (Z/Z* F)) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of ((1). (Z/Z* F)) is non empty finite set
card the carrier of ((1). (Z/Z* F)) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card g is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of g is non empty finite set
card the carrier of g is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card y is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of y is non empty finite set
card the carrier of y is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set
card (gr {a}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of (gr {a}) is non empty finite set
card the carrier of (gr {a}) is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of x is non empty finite set
card the carrier of x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of x is non empty finite set
card the carrier of x is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card gg is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of gg is non empty finite set
card the carrier of gg is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

card n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
the carrier of n is non empty finite set
card the carrier of n is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal set

F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 |^ 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (1 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ 1) * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (2 + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
16 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (2 + 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
4 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
256 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 + 4 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (4 + 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
16 * 16 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(0) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 0) - 1 is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
(1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 1) - 1 is V11() V12() integer ext-real set
2 - 1 is V11() V12() integer ext-real set
(2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 2) - 1 is V11() V12() integer ext-real set
(3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 3 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 3) - 1 is V11() V12() integer ext-real set
(5) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 5 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 5) - 1 is V11() V12() integer ext-real set
31 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
3 + 2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (3 + 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (3 + 2)) - 1 is V11() V12() integer ext-real set
(2 |^ 3) * (2 |^ 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 3) * (2 |^ 2)) - 1 is V11() V12() integer ext-real set
(7) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 7 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 7) - 1 is V11() V12() integer ext-real set
127 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
4 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (4 + 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (4 + 3)) - 1 is V11() V12() integer ext-real set
(2 |^ 4) * (2 |^ 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 4) * (2 |^ 3)) - 1 is V11() V12() integer ext-real set
(11) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ 11 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ 11) - 1 is V11() V12() integer ext-real set
23 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
89 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
23 * 89 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
8 + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 |^ (8 + 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ (8 + 3)) - 1 is V11() V12() integer ext-real set
(2 |^ 8) * (2 |^ 3) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ 8) * (2 |^ 3)) - 1 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 - 1 is V11() V12() integer ext-real set
F -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ (F -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) - 1 is V11() V12() integer ext-real set
((2 * (2 |^ (F -' 1))) - 1) mod (2 * F) is V11() V12() integer ext-real set
(2 * (2 |^ (F -' 1))) mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod (2 * F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * (2 |^ (F -' 1))) mod (2 * F)) - (1 mod (2 * F)) is V11() V12() integer ext-real set
(((2 * (2 |^ (F -' 1))) mod (2 * F)) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 |^ (F -' 1)) mod F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 1)) mod F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 |^ (F -' 1)) mod F)) - (1 mod (2 * F)) is V11() V12() integer ext-real set
((2 * ((2 |^ (F -' 1)) mod F)) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 * 1) - (1 mod (2 * F)) is V11() V12() integer ext-real set
((2 * 1) - (1 mod (2 * F))) mod (2 * F) is V11() V12() integer ext-real set
(2 * 1) - 1 is V11() V12() integer ext-real set
((2 * 1) - 1) mod (2 * F) is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal set
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
(F) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
2 + 0 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
F - 2 is V11() V12() integer ext-real set
2 - 2 is V11() V12() integer ext-real set
F -' 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ (F -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) - 1 is V11() V12() integer ext-real set
((2 * (2 |^ (F -' 1))) - 1) mod 8 is V11() V12() integer ext-real set
2 * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 1))) mod (2 * 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * (2 |^ (F -' 1))) mod (2 * 4)) - (1 mod 8) is V11() V12() integer ext-real set
(((2 * (2 |^ (F -' 1))) mod (2 * 4)) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(2 |^ (F -' 1)) mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 1)) mod 4) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 |^ (F -' 1)) mod 4)) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 |^ (F -' 1)) mod 4)) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(F -' 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((F -' 1) -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ ((F -' 1) -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 * (2 |^ ((F -' 1) -' 1))) mod (2 * 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
2 |^ (F -' 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 |^ (F -' 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 |^ (F -' 2))) mod (2 * 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * ((2 * (2 |^ (F -' 2))) mod (2 * 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
(2 |^ (F -' 2)) mod 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * ((2 |^ (F -' 2)) mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 * (2 * ((2 |^ (F -' 2)) mod 2)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * (2 * ((2 |^ (F -' 2)) mod 2))) - (1 mod 8) is V11() V12() integer ext-real set
((2 * (2 * ((2 |^ (F -' 2)) mod 2))) - (1 mod 8)) mod 8 is V11() V12() integer ext-real set
4 * ((2 |^ (F -' 2)) mod 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(4 * ((2 |^ (F -' 2)) mod 2)) - 1 is V11() V12() integer ext-real set
((4 * ((2 |^ (F -' 2)) mod 2)) - 1) mod 8 is V11() V12() integer ext-real set

(4 * 0) - 1 is non empty V11() V12() integer ext-real non positive negative set
((4 * 0) - 1) mod 8 is V11() V12() integer ext-real set
8 * 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(- 1) + (8 * 1) is V11() V12() integer ext-real set
((- 1) + (8 * 1)) mod 8 is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 - 3 is V11() V12() integer ext-real set
2 gcd ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 8) + 7 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
7 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(((2 * F) + 1) -' 1) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((((2 * F) + 1) -' 1) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((((2 * F) + 1) -' 1) div 2)) - 1 is V11() V12() integer ext-real set
((2 |^ ((((2 * F) + 1) -' 1) div 2)) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(2 * F) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((2 * F) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((2 * F) div 2)) - 1 is V11() V12() integer ext-real set
((2 |^ ((2 * F) div 2)) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
((2 |^ F) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
F is non empty V4() V5() V6() V10() V11() V12() integer prime ext-real positive non negative finite cardinal () set
F mod 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
2 |^ F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ F) - 1 is V11() V12() integer ext-real set
2 * F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 * F) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
5 - 3 is V11() V12() integer ext-real set
2 gcd ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
F div 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(F div 4) * 4 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 4) + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
(F div 4) * 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((F div 4) * 8) + 3 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
3 mod 8 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(((2 * F) + 1) -' 1) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((((2 * F) + 1) -' 1) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((((2 * F) + 1) -' 1) div 2)) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 * F) + 1) - 1 is V11() V12() integer ext-real set
(2 * F) div 2 is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
2 |^ ((2 * F) div 2) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ ((2 * F) div 2)) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
5 - 4 is V11() V12() integer ext-real set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((2 * F) + 1) - 2 is V11() V12() integer ext-real set
(F) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
(2 |^ F) mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
1 mod ((2 * F) + 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of NAT
((2 |^ F) mod ((2 * F) + 1)) - (1 mod ((2 * F) + 1)) is V11() V12() integer ext-real set
(((2 |^ F) mod ((2 * F) + 1)) - (1 mod ((2 * F) + 1))) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(((2 * F) + 1) - 1) - (1 mod ((2 * F) + 1)) is V11() V12() integer ext-real set
((((2 * F) + 1) - 1) - (1 mod ((2 * F) + 1))) mod ((2 * F) + 1) is V11() V12() integer ext-real set
(((2 * F) + 1) - 1) - 1 is V11() V12() integer ext-real set
((((2 * F) + 1) - 1) - 1) mod ((2 * F) + 1) is V11() V12() integer ext-real set
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F - 1 is V11() V12() integer ext-real set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ G) - 1 is V11() V12() integer ext-real set
2 |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal Element of REAL
(2 |^ G) - 1 is V11() V12() integer ext-real set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative finite cardinal Element of NAT
((F |^ G) - 1) mod (F - 1) is V11() V12() integer ext-real set
2 - 1 is V11() V12() integer ext-real set
F mod (F - 1) is V11() V12() integer ext-real set
(F - 1) * (- 1) is V11() V12() integer ext-real set
F + ((F - 1) * (- 1)) is V11() V12() integer ext-real set
(F + ((F - 1) * (- 1))) mod (F - 1) is V11() V12() integer ext-real set
(F |^ G) mod (F - 1) is V11() V12() integer ext-real set
((F |^ G) - 1) mod (F - 1) is V11() V12() integer ext-real set
1 mod (F - 1) is V11() V12() integer ext-real set
((F |^ G) mod (F - 1)) - (1 mod (F - 1)) is V11() V12() integer ext-real set
(((F |^ G) mod (F - 1)) - (1 mod (F - 1))) mod (F - 1) is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
(1 - 1) mod (F - 1) is V11() V12() integer ext-real set
G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
F |^ G is V4() V5() V6() V10() V11() V12() integer ext-real non negative finite cardinal set
(F |^ G) - 1 is V11() V12() integer ext-real set
0 - 1 is non empty V11() V12() integer ext-real non positive negative set
1 - 1 is V11() V12() integer ext-real