REAL is non empty non trivial non finite V107() V108() V109() V113() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V107() V108() V109() V110() V111() V112() V113() countable denumerable Element of bool REAL
bool REAL is non empty non trivial V14() non finite set
omega is non empty non trivial ordinal non finite cardinal limit_cardinal V107() V108() V109() V110() V111() V112() V113() countable denumerable set
bool omega is non empty non trivial V14() non finite set
K202() is L6()
the carrier of K202() is set
[:NAT,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:NAT,REAL:] is non empty non trivial V14() non finite set
COMPLEX is non empty non trivial non finite V107() V113() set
bool NAT is non empty non trivial V14() non finite set
RAT is non empty non trivial non finite V107() V108() V109() V110() V113() set
INT is non empty non trivial non finite V107() V108() V109() V110() V111() V113() set
[:REAL,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:REAL,REAL:] is non empty non trivial V14() non finite set
{} is empty ordinal natural V11() real Function-like functional finite V37() cardinal {} -element integer ext-real non positive non negative V107() V108() V109() V110() V111() V112() V113() countable set
the empty ordinal natural V11() real Function-like functional finite V37() cardinal {} -element integer ext-real non positive non negative V107() V108() V109() V110() V111() V112() V113() countable set is empty ordinal natural V11() real Function-like functional finite V37() cardinal {} -element integer ext-real non positive non negative V107() V108() V109() V110() V111() V112() V113() countable set
1 is non empty ordinal natural V11() real finite cardinal integer V83() ext-real positive non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
{{},1} is non empty finite V37() V107() V108() V109() V110() V111() V112() countable set
K491() is set
bool K491() is set
K492() is Element of bool K491()
K605() is set
K637() is non empty strict DTConstrStr
the carrier of K637() is non empty set
K495( the carrier of K637()) is non empty M26( the carrier of K637())
K636(K637()) is Element of bool K495( the carrier of K637())
bool K495( the carrier of K637()) is V14() set
[:K636(K637()),NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued disjoint_with_NAT set
bool [:K636(K637()),NAT:] is set
[:NAT,K636(K637()):] is disjoint_with_NAT set
bool [:NAT,K636(K637()):] is set
ExtREAL is non empty V108() set
0 is empty ordinal natural V11() real Function-like functional finite V37() cardinal {} -element integer V83() ext-real non positive non negative V107() V108() V109() V110() V111() V112() V113() countable Element of NAT
0 ! is V11() real ext-real Element of REAL
1 ! is V11() real ext-real Element of REAL
2 is non empty ordinal natural V11() real finite cardinal integer V83() ext-real positive non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
Fib 0 is ordinal natural V11() real finite cardinal integer V83() ext-real non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
Fib 1 is ordinal natural V11() real finite cardinal integer V83() ext-real non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
- 1 is non empty V11() real integer ext-real non positive negative set
card omega is non empty non trivial ordinal non finite cardinal set
ECIW-signature is non empty Relation-like NAT -defined NAT -valued Function-like V85() complex-valued ext-real-valued real-valued natural-valued M13( NAT )
g is set
S is set
T is set
A is set
X is set
b is set
S .--> X is Relation-like {S} -defined Function-like one-to-one finite countable set
{S} is non empty trivial finite 1 -element countable set
{S} --> X is non empty Relation-like {S} -defined {X} -valued Function-like constant V29({S}) quasi_total finite countable Element of bool [:{S},{X}:]
{X} is non empty trivial finite 1 -element countable set
[:{S},{X}:] is finite countable disjoint_with_NAT set
bool [:{S},{X}:] is finite V37() countable set
dom (S .--> X) is finite countable Element of bool {S}
bool {S} is V14() finite V37() countable set
T .--> b is Relation-like {T} -defined Function-like one-to-one finite countable set
{T} is non empty trivial finite 1 -element countable set
{T} --> b is non empty Relation-like {T} -defined {b} -valued Function-like constant V29({T}) quasi_total finite countable Element of bool [:{T},{b}:]
{b} is non empty trivial finite 1 -element countable set
[:{T},{b}:] is finite countable disjoint_with_NAT set
bool [:{T},{b}:] is finite V37() countable set
g .--> A is Relation-like {g} -defined Function-like one-to-one finite countable set
{g} is non empty trivial finite 1 -element countable set
{g} --> A is non empty Relation-like {g} -defined {A} -valued Function-like constant V29({g}) quasi_total finite countable Element of bool [:{g},{A}:]
{A} is non empty trivial finite 1 -element countable set
[:{g},{A}:] is finite countable disjoint_with_NAT set
bool [:{g},{A}:] is finite V37() countable set
(g .--> A) +* (S .--> X) is Relation-like Function-like finite countable set
((g .--> A) +* (S .--> X)) +* (T .--> b) is Relation-like Function-like finite countable set
d is Relation-like Function-like finite countable set
d . g is set
d . S is set
d . T is set
dom (T .--> b) is finite countable Element of bool {T}
bool {T} is V14() finite V37() countable set
((g .--> A) +* (S .--> X)) . g is set
(g .--> A) . g is set
((g .--> A) +* (S .--> X)) . S is set
(S .--> X) . S is set
(T .--> b) . T is set
A is non empty functional set
X is set
b is set
{ b1 where b1 is Relation-like Function-like Element of A : not b1 . X = b } is set
bool A is V14() set
S is set
T is Relation-like Function-like Element of A
T . X is set
A is non empty functional set
X is set
b is set
(A,X,b) is functional Element of bool A
bool A is V14() set
{ b1 where b1 is Relation-like Function-like Element of A : not b1 . X = b } is set
g is Relation-like Function-like Element of A
g . X is set
S is Relation-like Function-like Element of A
S . X is set
S is Relation-like Function-like Element of A
S . X is set
A is set
Funcs (A,INT) is non empty functional FUNCTION_DOMAIN of A, INT
X is set
[:(Funcs (A,INT)),X:] is disjoint_with_NAT set
b is set
[:[:(Funcs (A,INT)),X:],b:] is disjoint_with_NAT set
bool [:[:(Funcs (A,INT)),X:],b:] is set
A is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 A is set
X is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 X is set
(proj1 A) /\ (proj1 X) is set
b is Relation-like Function-like set
proj1 b is set
g is set
proj2 b is set
S is set
b . S is set
A . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
(A . S) div (X . S) is V11() real integer ext-real set
g is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 g is set
S is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 S is set
T is set
g . T is V11() real integer ext-real set
A . T is V11() real integer ext-real set
X . T is V11() real integer ext-real set
(A . T) div (X . T) is V11() real integer ext-real set
S . T is V11() real integer ext-real set
b is Relation-like Function-like set
proj1 b is set
g is set
proj2 b is set
S is set
b . S is set
A . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
(A . S) mod (X . S) is V11() real integer ext-real set
g is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 g is set
S is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 S is set
T is set
g . T is V11() real integer ext-real set
A . T is V11() real integer ext-real set
X . T is V11() real integer ext-real set
(A . T) mod (X . T) is V11() real integer ext-real set
S . T is V11() real integer ext-real set
b is Relation-like Function-like set
proj1 b is set
g is set
proj2 b is set
S is set
b . S is set
A . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
IFGT ((A . S),(X . S),0,1) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
g is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 g is set
S is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 S is set
T is set
g . T is V11() real integer ext-real set
A . T is V11() real integer ext-real set
X . T is V11() real integer ext-real set
IFGT ((A . T),(X . T),0,1) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
S . T is V11() real integer ext-real set
b is Relation-like Function-like set
proj1 b is set
g is set
proj2 b is set
S is set
b . S is set
A . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
IFGT ((A . S),(X . S),1,0) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
g is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 g is set
S is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 S is set
T is set
g . T is V11() real integer ext-real set
A . T is V11() real integer ext-real set
X . T is V11() real integer ext-real set
IFGT ((A . T),(X . T),1,0) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
S . T is V11() real integer ext-real set
b is Relation-like Function-like set
proj1 b is set
g is set
proj2 b is set
S is set
b . S is set
A . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
IFEQ ((A . S),(X . S),1,0) is ordinal natural V11() real finite cardinal integer V83() ext-real non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
g is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 g is set
S is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
proj1 S is set
T is set
g . T is V11() real integer ext-real set
A . T is V11() real integer ext-real set
X . T is V11() real integer ext-real set
IFEQ ((A . T),(X . T),1,0) is ordinal natural V11() real finite cardinal integer V83() ext-real non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
S . T is V11() real integer ext-real set
A is non empty set
[:A,INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:A,INT:] is non empty non trivial V14() non finite set
X is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
b is V11() real integer ext-real set
b + X is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
g is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom X is Element of bool A
bool A is V14() set
dom (b + X) is Element of bool A
S is Element of A
g . S is V11() real integer V83() ext-real Element of INT
X . S is V11() real integer V83() ext-real Element of INT
(X . S) + b is V11() real integer ext-real set
dom g is Element of bool A
S is set
g . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
b + (X . S) is V11() real integer ext-real set
b + X is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
X - b is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
- b is V11() real integer ext-real set
(- b) + X is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
g is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom g is Element of bool A
bool A is V14() set
dom X is Element of bool A
X - b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
S is Element of A
g . S is V11() real integer V83() ext-real Element of INT
X . S is V11() real integer V83() ext-real Element of INT
(X . S) - b is V11() real integer ext-real set
(X . S) + (- b) is V11() real integer ext-real set
S is set
g . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
(X . S) - b is V11() real integer ext-real set
(X . S) + (- b) is V11() real integer ext-real set
(X - b) . S is V11() real integer ext-real set
dom (X - b) is Element of bool A
X - b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
b (#) X is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
g is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom (b (#) X) is Element of bool A
bool A is V14() set
dom X is Element of bool A
S is Element of A
g . S is V11() real integer V83() ext-real Element of INT
X . S is V11() real integer V83() ext-real Element of INT
(X . S) * b is V11() real integer ext-real set
dom g is Element of bool A
S is set
g . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
b * (X . S) is V11() real integer ext-real set
b (#) X is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
A is set
[:A,INT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:A,INT:] is set
X is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
b is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
(X,b) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
dom b is Element of bool A
bool A is set
proj1 (X,b) is set
dom X is Element of bool A
(dom X) /\ (dom b) is Element of bool A
rng (X,b) is V107() V108() V109() V110() V111() Element of bool INT
bool INT is non empty non trivial V14() non finite set
(X,b) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
dom b is Element of bool A
bool A is set
proj1 (X,b) is set
dom X is Element of bool A
(dom X) /\ (dom b) is Element of bool A
rng (X,b) is V107() V108() V109() V110() V111() Element of bool INT
bool INT is non empty non trivial V14() non finite set
(X,b) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
dom b is Element of bool A
bool A is set
proj1 (X,b) is set
dom X is Element of bool A
(dom X) /\ (dom b) is Element of bool A
rng (X,b) is V107() V108() V109() V110() V111() Element of bool INT
bool INT is non empty non trivial V14() non finite set
(X,b) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
dom b is Element of bool A
bool A is set
proj1 (X,b) is set
dom X is Element of bool A
(dom X) /\ (dom b) is Element of bool A
rng (X,b) is V107() V108() V109() V110() V111() Element of bool INT
bool INT is non empty non trivial V14() non finite set
(X,b) is Relation-like INT -valued Function-like complex-valued ext-real-valued real-valued set
dom b is Element of bool A
bool A is set
proj1 (X,b) is set
dom X is Element of bool A
(dom X) /\ (dom b) is Element of bool A
rng (X,b) is V107() V108() V109() V110() V111() Element of bool INT
bool INT is non empty non trivial V14() non finite set
A is non empty set
[:A,INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:A,INT:] is non empty non trivial V14() non finite set
X is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
X - b is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
- b is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
(- 1) (#) b is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
X + (- b) is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
g is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom X is Element of bool A
bool A is V14() set
X - b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
S is Element of A
g . S is V11() real integer V83() ext-real Element of INT
X . S is V11() real integer V83() ext-real Element of INT
b . S is V11() real integer V83() ext-real Element of INT
(X . S) - (b . S) is V11() real integer ext-real set
- (b . S) is V11() real integer ext-real set
(X . S) + (- (b . S)) is V11() real integer ext-real set
dom g is Element of bool A
S is set
g . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
b . S is V11() real integer ext-real set
(X . S) - (b . S) is V11() real integer ext-real set
- (b . S) is V11() real integer ext-real set
(X . S) + (- (b . S)) is V11() real integer ext-real set
(X - b) . S is V11() real integer ext-real set
dom b is Element of bool A
dom (X - b) is Element of bool A
(dom X) /\ (dom b) is Element of bool A
X - b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
X + b is Relation-like A -defined INT -valued Function-like V29(A) complex-valued ext-real-valued real-valued set
g is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom X is Element of bool A
bool A is V14() set
dom b is Element of bool A
X + b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
dom (X + b) is Element of bool A
(dom X) /\ (dom b) is Element of bool A
S is Element of A
g . S is V11() real integer V83() ext-real Element of INT
X . S is V11() real integer V83() ext-real Element of INT
b . S is V11() real integer V83() ext-real Element of INT
(X . S) + (b . S) is V11() real integer ext-real set
dom g is Element of bool A
S is set
g . S is V11() real integer ext-real set
X . S is V11() real integer ext-real set
b . S is V11() real integer ext-real set
(X . S) + (b . S) is V11() real integer ext-real set
X + b is non empty Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of bool [:A,INT:]
A is non empty set
X is non empty non trivial non finite set
Funcs (A,X) is non empty functional FUNCTION_DOMAIN of A,X
card X is non empty non trivial ordinal non finite cardinal set
card (card X) is non empty non trivial ordinal non finite cardinal set
card A is non empty ordinal cardinal set
card (card A) is non empty ordinal cardinal set
card (Funcs (A,X)) is non empty ordinal cardinal set
exp ((card X),(card A)) is ordinal cardinal set
Funcs ((card A),(card X)) is non empty functional set
card (Funcs ((card A),(card X))) is non empty ordinal cardinal set
the Element of A is Element of A
{ the Element of A} is non empty trivial finite 1 -element countable set
card { the Element of A} is non empty ordinal natural V11() real finite cardinal integer V83() ext-real positive non negative V107() V108() V109() V110() V111() V112() countable Element of omega
exp ((card X),1) is ordinal cardinal set
Funcs (1,(card X)) is non empty functional set
card (Funcs (1,(card X))) is non empty ordinal cardinal set
X is Relation-like Function-like set
proj1 X is set
A is set
b is Relation-like Function-like set
g is Relation-like Function-like set
proj1 g is set
S is Relation-like Function-like set
proj1 S is set
T is set
Funcs (A,T) is functional set
x is set
Funcs (A,x) is functional set
y is set
m is Relation-like Function-like set
proj2 m is set
m is Relation-like Function-like set
proj2 m is set
y is set
m is Relation-like Function-like set
b (#) m is Relation-like Function-like set
m is Relation-like Function-like set
b (#) m is Relation-like Function-like set
y is set
m is Relation-like Function-like set
b (#) m is Relation-like Function-like set
g . y is set
X . (b (#) m) is set
S . y is set
g is set
x is Relation-like Function-like set
S is set
proj2 x is set
y is Relation-like Function-like set
T is set
proj2 y is set
g is set
union g is set
Funcs (A,(union g)) is functional set
T is set
x is set
y is Relation-like Function-like set
b (#) y is Relation-like Function-like set
X . (b (#) y) is set
x is Relation-like Function-like set
proj1 x is set
m is set
y is set
d is set
C is set
s is Relation-like Function-like set
proj2 s is set
d is Relation-like Function-like set
proj2 d is set
m is set
Funcs (A,y) is functional set
d is Relation-like Function-like set
b (#) d is Relation-like Function-like set
y is Relation-like Function-like set
x . y is set
b (#) y is Relation-like Function-like set
X . (b (#) y) is set
m is Relation-like Function-like set
b (#) m is Relation-like Function-like set
X . (b (#) m) is set
A is non empty set
X is non empty set
Funcs (A,X) is non empty functional FUNCTION_DOMAIN of A,X
b is non empty set
Funcs ((Funcs (A,X)),b) is non empty functional FUNCTION_DOMAIN of Funcs (A,X),b
g is non empty set
[:A,g:] is disjoint_with_NAT set
bool [:A,g:] is set
S is Relation-like Funcs (A,X) -defined b -valued Function-like V29( Funcs (A,X)) quasi_total Element of Funcs ((Funcs (A,X)),b)
T is non empty Relation-like A -defined g -valued Function-like V29(A) quasi_total Element of bool [:A,g:]
(g,S,T) is Relation-like Function-like set
Funcs (g,X) is non empty functional FUNCTION_DOMAIN of g,X
Funcs ((Funcs (g,X)),b) is non empty functional FUNCTION_DOMAIN of Funcs (g,X),b
dom S is functional Element of bool (Funcs (A,X))
bool (Funcs (A,X)) is V14() set
proj1 (g,S,T) is set
x is set
Funcs (g,x) is functional set
y is set
m is Relation-like Function-like set
proj2 m is set
y is set
[:A,X:] is disjoint_with_NAT set
bool [:A,X:] is set
m is Element of X
A --> m is non empty Relation-like A -defined X -valued Function-like constant V29(A) quasi_total Element of bool [:A,X:]
{m} is non empty trivial finite 1 -element countable set
[:A,{m}:] is disjoint_with_NAT set
d is non empty Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of bool [:A,X:]
rng d is Element of bool X
bool X is V14() set
y is set
y is set
[:g,X:] is disjoint_with_NAT set
bool [:g,X:] is set
m is non empty Relation-like g -defined X -valued Function-like V29(g) quasi_total Element of bool [:g,X:]
m * T is non empty Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of bool [:A,X:]
[:A,X:] is disjoint_with_NAT set
bool [:A,X:] is set
proj2 (g,S,T) is set
y is set
m is set
(g,S,T) . m is set
d is Relation-like g -defined X -valued Function-like V29(g) quasi_total Element of Funcs (g,X)
d * T is non empty Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of bool [:A,X:]
[:A,X:] is disjoint_with_NAT set
bool [:A,X:] is set
C is Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of Funcs (A,X)
S . C is Element of b
b is Relation-like Function-like set
proj2 b is set
X is Relation-like Function-like set
proj1 X is set
A is Relation-like Function-like set
A +* X is Relation-like Function-like set
b (#) (A +* X) is Relation-like Function-like set
b (#) X is Relation-like Function-like set
g is set
proj1 b is set
(b (#) X) . g is set
b . g is set
X . (b . g) is set
(b (#) (A +* X)) . g is set
(A +* X) . (b . g) is set
proj1 (A +* X) is set
proj1 A is set
(proj1 A) \/ (proj1 X) is set
proj1 (b (#) (A +* X)) is set
proj1 (b (#) X) is set
A is non empty set
b is non empty set
[:A,b:] is disjoint_with_NAT set
bool [:A,b:] is set
X is non empty set
[:A,X:] is disjoint_with_NAT set
bool [:A,X:] is set
[:X,b:] is disjoint_with_NAT set
bool [:X,b:] is set
g is non empty Relation-like A -defined b -valued Function-like V29(A) quasi_total Element of bool [:A,b:]
S is non empty Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of bool [:A,X:]
S " is Relation-like Function-like set
(S ") (#) g is Relation-like Function-like set
proj1 (S ") is set
rng S is Element of bool X
bool X is V14() set
T is Element of b
X --> T is non empty Relation-like X -defined b -valued Function-like constant V29(X) quasi_total Element of bool [:X,b:]
{T} is non empty trivial finite 1 -element countable set
[:X,{T}:] is disjoint_with_NAT set
(X --> T) +* ((S ") (#) g) is Relation-like Function-like set
proj1 ((S ") (#) g) is set
proj2 ((S ") (#) g) is set
rng g is Element of bool b
bool b is V14() set
rng (X --> T) is trivial finite countable Element of bool b
(rng (X --> T)) \/ (proj2 ((S ") (#) g)) is set
dom (X --> T) is Element of bool X
proj2 ((X --> T) +* ((S ") (#) g)) is set
proj1 ((X --> T) +* ((S ") (#) g)) is set
(dom (X --> T)) \/ (proj1 ((S ") (#) g)) is set
X is non empty set
b is non empty set
Funcs (X,b) is non empty functional FUNCTION_DOMAIN of X,b
A is non empty set
[:X,A:] is disjoint_with_NAT set
bool [:X,A:] is set
g is Relation-like Function-like set
proj1 g is set
S is Relation-like Function-like set
proj1 S is set
proj2 g is set
proj2 S is set
T is non empty set
x is non empty set
T \/ x is non empty set
y is non empty set
Funcs ((Funcs (X,b)),y) is non empty functional FUNCTION_DOMAIN of Funcs (X,b),y
C is non empty Relation-like X -defined A -valued Function-like V29(X) quasi_total Element of bool [:X,A:]
(A,g,C) is Relation-like Function-like set
(A,S,C) is Relation-like Function-like set
Funcs (A,b) is non empty functional FUNCTION_DOMAIN of A,b
d is Relation-like Funcs (X,b) -defined y -valued Function-like V29( Funcs (X,b)) quasi_total Element of Funcs ((Funcs (X,b)),y)
(X,b,y,A,d,C) is Relation-like Funcs (A,b) -defined y -valued Function-like V29( Funcs (A,b)) quasi_total Element of Funcs ((Funcs (A,b)),y)
Funcs ((Funcs (A,b)),y) is non empty functional FUNCTION_DOMAIN of Funcs (A,b),y
dom (X,b,y,A,d,C) is functional Element of bool (Funcs (A,b))
bool (Funcs (A,b)) is V14() set
m is Relation-like Funcs (X,b) -defined y -valued Function-like V29( Funcs (X,b)) quasi_total Element of Funcs ((Funcs (X,b)),y)
(X,b,y,A,m,C) is Relation-like Funcs (A,b) -defined y -valued Function-like V29( Funcs (A,b)) quasi_total Element of Funcs ((Funcs (A,b)),y)
dom (X,b,y,A,m,C) is functional Element of bool (Funcs (A,b))
the Element of b is Element of b
dom C is Element of bool X
bool X is V14() set
n is set
A --> the Element of b is non empty Relation-like A -defined b -valued Function-like constant V29(A) quasi_total Element of bool [:A,b:]
[:A,b:] is disjoint_with_NAT set
bool [:A,b:] is set
{ the Element of b} is non empty trivial finite 1 -element countable set
[:A,{ the Element of b}:] is disjoint_with_NAT set
C " is Relation-like Function-like set
I is Relation-like X -defined b -valued Function-like V29(X) quasi_total Element of Funcs (X,b)
(C ") (#) I is Relation-like Function-like set
(A --> the Element of b) +* ((C ") (#) I) is Relation-like Function-like set
dom I is Element of bool X
proj2 (C ") is set
proj1 ((C ") (#) I) is set
proj1 (C ") is set
rng C is Element of bool A
bool A is V14() set
C (#) ((A --> the Element of b) +* ((C ") (#) I)) is Relation-like Function-like set
C (#) ((C ") (#) I) is Relation-like Function-like set
C (#) (C ") is Relation-like Function-like set
(C (#) (C ")) (#) I is Relation-like Function-like set
id X is non empty Relation-like X -defined X -valued Function-like one-to-one V29(X) quasi_total Element of bool [:X,X:]
[:X,X:] is disjoint_with_NAT set
bool [:X,X:] is set
I * (id X) is non empty Relation-like X -defined b -valued Function-like V29(X) quasi_total Element of bool [:X,b:]
[:X,b:] is disjoint_with_NAT set
bool [:X,b:] is set
(A,g,C) . ((A --> the Element of b) +* ((C ") (#) I)) is set
g . n is set
S . n is set
A is set
card A is ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
b is Relation-like A -defined card A -valued Function-like quasi_total Element of bool [:A,(card A):]
rng b is Element of bool (card A)
bool (card A) is set
[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
b is Relation-like card A -defined A -valued Function-like quasi_total Element of bool [:(card A),A:]
rng b is Element of bool A
bool A is set
A is set
card A is ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
A is set
card A is ordinal cardinal set
[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
A is non empty set
card A is non empty ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Element of A
b is Element of A
g is non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):]
g . b is Element of card A
g +* (X,(g . b)) is non empty Relation-like A -defined card A -valued Function-like V29(A) quasi_total Element of bool [:A,(card A):]
g . X is Element of card A
(g +* (X,(g . b))) +* (b,(g . X)) is non empty Relation-like A -defined card A -valued Function-like V29(A) quasi_total Element of bool [:A,(card A):]
dom ((g +* (X,(g . b))) +* (b,(g . X))) is Element of bool A
bool A is V14() set
dom (g +* (X,(g . b))) is Element of bool A
dom g is Element of bool A
rng g is Element of bool (card A)
bool (card A) is V14() set
rng ((g +* (X,(g . b))) +* (b,(g . X))) is Element of bool (card A)
{(g . X)} is non empty trivial finite 1 -element countable set
(rng g) \/ {(g . X)} is non empty set
rng (g +* (X,(g . b))) is Element of bool (card A)
(rng (g +* (X,(g . b)))) \/ {(g . X)} is non empty set
{(g . b)} is non empty trivial finite 1 -element countable set
(rng g) \/ {(g . b)} is non empty set
x is set
y is set
g . y is set
((g +* (X,(g . b))) +* (b,(g . X))) . y is set
(g +* (X,(g . b))) . y is set
((g +* (X,(g . b))) +* (b,(g . X))) . b is Element of card A
((g +* (X,(g . b))) +* (b,(g . X))) . X is Element of card A
g +* (X,x) is Relation-like Function-like set
(g +* (X,x)) . X is set
x is set
proj1 ((g +* (X,(g . b))) +* (b,(g . X))) is set
y is set
((g +* (X,(g . b))) +* (b,(g . X))) . x is set
((g +* (X,(g . b))) +* (b,(g . X))) . y is set
(g +* (X,(g . b))) . x is set
g . x is set
(g +* (X,(g . b))) . y is set
g . y is set
A is non empty set
card A is non empty ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Element of A
the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] is non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):]
rng the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] is Element of bool (card A)
bool (card A) is V14() set
dom the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] is Element of bool A
bool A is V14() set
g is set
the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] . g is set
S is Element of A
the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] . X is Element of card A
the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] +* (S,( the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] . X)) is non empty Relation-like A -defined card A -valued Function-like V29(A) quasi_total Element of bool [:A,(card A):]
( the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] +* (S,( the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] . X))) +* (X,0) is Relation-like Function-like set
T is non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):]
T . X is Element of card A
dom ( the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] +* (S,( the non empty Relation-like A -defined card A -valued Function-like one-to-one V29(A) quasi_total onto bijective Element of bool [:A,(card A):] . X))) is Element of bool A
A is non empty set
card A is non empty ordinal cardinal set
[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is set
X is non empty Relation-like card A -defined A -valued Function-like one-to-one V29( card A) quasi_total onto bijective Element of bool [:(card A),A:]
X . 0 is set
A is countable set
card A is ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Relation-like A -defined card A -valued Function-like one-to-one quasi_total onto bijective Element of bool [:A,(card A):]
rng X is Element of bool (card A)
bool (card A) is set
A is set
card A is ordinal cardinal set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
X is Relation-like A -defined card A -valued Function-like one-to-one quasi_total onto bijective Element of bool [:A,(card A):]
X " is Relation-like Function-like one-to-one set
[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is set
rng X is Element of bool (card A)
bool (card A) is set
proj1 (X ") is set
dom X is Element of bool A
bool A is set
proj2 (X ") is set
A is set
card A is ordinal cardinal set
[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is set
X is Relation-like card A -defined A -valued Function-like one-to-one quasi_total onto bijective Element of bool [:(card A),A:]
X " is Relation-like Function-like one-to-one set
[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set
rng X is Element of bool A
bool A is set
proj1 (X ") is set
dom X is Element of bool (card A)
bool (card A) is set
proj2 (X ") is set
A is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
X is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
A + X is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
0 to_power (A + X) is V11() real ext-real set
0 |^ (A + X) is set
0 to_power A is V11() real ext-real set
0 |^ A is set
0 to_power X is V11() real ext-real set
0 |^ X is set
(0 to_power A) * (0 to_power X) is V11() real ext-real set
A is V11() real ext-real set
X is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
A to_power X is V11() real ext-real set
A |^ X is set
b is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
(A to_power X) to_power b is V11() real ext-real set
(A to_power X) |^ b is set
X * b is ordinal natural V11() real finite cardinal integer ext-real non negative countable set
A to_power (X * b) is V11() real ext-real set
A |^ (X * b) is set
A is non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction L9()
the carrier of A is non empty set
b is non empty set
Funcs (b,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of b, INT
bool (Funcs (b,INT)) is non empty non trivial V14() non finite set
[:(Funcs (b,INT)), the carrier of A:] is non empty non trivial non finite disjoint_with_NAT set
g is functional Element of bool (Funcs (b,INT))
X is non empty set
Funcs (X,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of X, INT
bool (Funcs (X,INT)) is non empty non trivial V14() non finite set
A is non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction L9()
the carrier of A is non empty set
[:(Funcs (X,INT)), the carrier of A:] is non empty non trivial non finite disjoint_with_NAT set
b is functional Element of bool (Funcs (X,INT))
[:(Funcs (X,INT)),X:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (X,INT)),X:] is non empty non trivial V14() non finite set
[:(Funcs (X,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (X,INT)),INT:] is non empty non trivial V14() non finite set
X is non empty set
Funcs (X,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of X, INT
bool (Funcs (X,INT)) is non empty non trivial V14() non finite set
A is non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction L9()
the carrier of A is non empty set
[:(Funcs (X,INT)), the carrier of A:] is non empty non trivial non finite disjoint_with_NAT set
b is functional Element of bool (Funcs (X,INT))
g is non empty Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (X,INT) -valued Function-like V29([:(Funcs (X,INT)), the carrier of A:]) quasi_total Function-yielding V89() complying_with_empty-instruction complying_with_catenation ExecutionFunction of A, Funcs (X,INT),b
[:(Funcs (X,INT)),X:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (X,INT)),X:] is non empty non trivial V14() non finite set
[:(Funcs (X,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (X,INT)),INT:] is non empty non trivial V14() non finite set
S is Element of the carrier of A
S is Element of the carrier of A
T is non empty Relation-like Funcs (X,INT) -defined X -valued Function-like V29( Funcs (X,INT)) quasi_total Element of bool [:(Funcs (X,INT)),X:]
x is non empty Relation-like Funcs (X,INT) -defined INT -valued Function-like V29( Funcs (X,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (X,INT)),INT:]
ElementaryInstructions A is Element of bool the carrier of A
bool the carrier of A is V14() set
y is Relation-like X -defined INT -valued Function-like V29(X) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (X,INT)
g . (y,S) is Relation-like Function-like Element of Funcs (X,INT)
[y,S] is V16() set
{y,S} is non empty finite countable set
{y} is non empty trivial functional finite 1 -element with_common_domain countable set
{{y,S},{y}} is non empty finite V37() countable set
g . [y,S] is Relation-like Function-like set
T . y is Element of X
x . y is V11() real integer V83() ext-real Element of INT
y +* ((T . y),(x . y)) is non empty Relation-like X -defined INT -valued Function-like V29(X) quasi_total complex-valued ext-real-valued real-valued Element of bool [:X,INT:]
[:X,INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:X,INT:] is non empty non trivial V14() non finite set
X is non empty set
Funcs (X,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of X, INT
bool (Funcs (X,INT)) is non empty non trivial V14() non finite set
A is non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction L9()
the carrier of A is non empty set
[:(Funcs (X,INT)), the carrier of A:] is non empty non trivial non finite disjoint_with_NAT set
b is functional Element of bool (Funcs (X,INT))
g is non empty Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (X,INT) -valued Function-like V29([:(Funcs (X,INT)), the carrier of A:]) quasi_total Function-yielding V89() complying_with_empty-instruction complying_with_catenation ExecutionFunction of A, Funcs (X,INT),b
[:(Funcs (X,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (X,INT)),INT:] is non empty non trivial V14() non finite set
[:(Funcs (X,INT)),X:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (X,INT)),X:] is non empty non trivial V14() non finite set
S is Element of the carrier of A
S is Element of the carrier of A
T is non empty Relation-like Funcs (X,INT) -defined X -valued Function-like V29( Funcs (X,INT)) quasi_total Element of bool [:(Funcs (X,INT)),X:]
x is non empty Relation-like Funcs (X,INT) -defined INT -valued Function-like V29( Funcs (X,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (X,INT)),INT:]
ElementaryInstructions A is Element of bool the carrier of A
bool the carrier of A is V14() set
y is Relation-like X -defined INT -valued Function-like V29(X) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (X,INT)
g . (y,S) is Relation-like Function-like Element of Funcs (X,INT)
[y,S] is V16() set
{y,S} is non empty finite countable set
{y} is non empty trivial functional finite 1 -element with_common_domain countable set
{{y,S},{y}} is non empty finite V37() countable set
g . [y,S] is Relation-like Function-like set
T . y is Element of X
x . y is V11() real integer V83() ext-real Element of INT
y +* ((T . y),(x . y)) is non empty Relation-like X -defined INT -valued Function-like V29(X) quasi_total complex-valued ext-real-valued real-valued Element of bool [:X,INT:]
[:X,INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:X,INT:] is non empty non trivial V14() non finite set
A is non empty set
X is non empty set
Funcs (A,X) is non empty functional FUNCTION_DOMAIN of A,X
b is Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of Funcs (A,X)
g is Element of A
b . g is set
b . g is Element of X
rng b is Element of bool X
bool X is V14() set
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
[:(Funcs (A,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
X is Element of A
b is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
g is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
S is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (A,INT)
b . S is V11() real integer V83() ext-real Element of INT
(A,INT,S,X) is V11() real integer V83() ext-real Element of INT
g . S is V11() real integer V83() ext-real Element of INT
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
[:(Funcs (A,INT)),A:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (A,INT)),A:] is non empty non trivial V14() non finite set
[:(Funcs (A,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
X is non empty Relation-like Funcs (A,INT) -defined A -valued Function-like V29( Funcs (A,INT)) quasi_total Element of bool [:(Funcs (A,INT)),A:]
b is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
g is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
S is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (A,INT)
b . S is V11() real integer V83() ext-real Element of INT
X . S is Element of A
(A,INT,S,(X . S)) is V11() real integer V83() ext-real Element of INT
g . S is V11() real integer V83() ext-real Element of INT
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
X is Element of A
(Funcs (A,INT)) --> X is non empty non trivial Relation-like Funcs (A,INT) -defined A -valued Function-like constant V29( Funcs (A,INT)) quasi_total non finite Element of bool [:(Funcs (A,INT)),A:]
[:(Funcs (A,INT)),A:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (A,INT)),A:] is non empty non trivial V14() non finite set
{X} is non empty trivial finite 1 -element countable set
[:(Funcs (A,INT)),{X}:] is non empty non trivial non finite disjoint_with_NAT set
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
X is Element of A
(A,X) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
[:(Funcs (A,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
(A,X) is non empty Relation-like Funcs (A,INT) -defined A -valued Function-like V29( Funcs (A,INT)) quasi_total Element of bool [:(Funcs (A,INT)),A:]
[:(Funcs (A,INT)),A:] is non empty non trivial non finite disjoint_with_NAT set
bool [:(Funcs (A,INT)),A:] is non empty non trivial V14() non finite set
(Funcs (A,INT)) --> X is non empty non trivial Relation-like Funcs (A,INT) -defined A -valued Function-like constant V29( Funcs (A,INT)) quasi_total non finite Element of bool [:(Funcs (A,INT)),A:]
{X} is non empty trivial finite 1 -element countable set
[:(Funcs (A,INT)),{X}:] is non empty non trivial non finite disjoint_with_NAT set
(A,(A,X)) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
b is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (A,INT)
(A,(A,X)) . b is V11() real integer V83() ext-real Element of INT
(A,INT,b,X) is V11() real integer V83() ext-real Element of INT
(A,X) . b is Element of A
(A,INT,b,((A,X) . b)) is V11() real integer V83() ext-real Element of INT
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
X is V11() real integer ext-real set
(Funcs (A,INT)) --> X is non empty non trivial Relation-like Funcs (A,INT) -defined INT -valued {X} -valued Function-like constant V29( Funcs (A,INT)) quasi_total non finite complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),{X}:]
{X} is non empty trivial finite 1 -element V107() V108() V109() V110() V111() countable set
[:(Funcs (A,INT)),{X}:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),{X}:] is non empty non trivial V14() non finite set
[:(Funcs (A,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
A is non empty set
Funcs (A,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of A, INT
[:(Funcs (A,INT)),INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
(A,0) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
(Funcs (A,INT)) --> 0 is non empty non trivial Relation-like Funcs (A,INT) -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant V29( Funcs (A,INT)) quasi_total non finite complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding Element of bool [:(Funcs (A,INT)),{0}:]
{0} is non empty trivial finite V37() 1 -element V107() V108() V109() V110() V111() V112() countable set
[:(Funcs (A,INT)),{0}:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),{0}:] is non empty non trivial V14() non finite set
(A,1) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
(Funcs (A,INT)) --> 1 is non empty non trivial Relation-like non-empty Funcs (A,INT) -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant V29( Funcs (A,INT)) quasi_total non finite complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding Element of bool [:(Funcs (A,INT)),{1}:]
{1} is non empty trivial finite V37() 1 -element V107() V108() V109() V110() V111() V112() countable set
[:(Funcs (A,INT)),{1}:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued disjoint_with_NAT set
bool [:(Funcs (A,INT)),{1}:] is non empty non trivial V14() non finite set
X is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
((Funcs (A,INT)),X,(A,0)) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
X (#) (A,1) is non empty Relation-like Funcs (A,INT) -defined INT -valued Function-like V29( Funcs (A,INT)) quasi_total complex-valued ext-real-valued real-valued Element of bool [:(Funcs (A,INT)),INT:]
b is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (A,INT)
(A,0) . b is V11() real integer V83() ext-real Element of INT
dom ((Funcs (A,INT)),X,(A,0)) is functional Element of bool (Funcs (A,INT))
bool (Funcs (A,INT)) is non empty non trivial V14() non finite set
((Funcs (A,INT)),X,(A,0)) . b is V11() real integer V83() ext-real Element of INT
X . b is V11() real integer V83() ext-real Element of INT
(X . b) + ((A,0) . b) is V11() real integer ext-real set
dom (X (#) (A,1)) is functional Element of bool (Funcs (A,INT))
b is Relation-like A -defined INT -valued Function-like V29(A) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (A,INT)
(X (#) (A,1)) . b is V11() real integer V83() ext-real Element of INT
X . b is V11() real integer V83() ext-real Element of INT
(A,1) . b is V11() real integer V83() ext-real Element of INT
(X . b) * ((A,1) . b) is V11() real integer ext-real set
(X . b) * 1 is V11() real integer ext-real set
X is non empty set
Funcs (X,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of X, INT
bool (Funcs (X,INT)) is non empty non trivial V14() non finite set
A is non empty V157() V158() V159() with_empty-instruction with_catenation with_if-instruction with_while-instruction L9()
the carrier of A is non empty set
[:(Funcs (X,INT)), the carrier of A:] is non empty non trivial non finite disjoint_with_NAT set
b is functional Element of bool (Funcs (X,INT))
Funcs (NAT,INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of NAT , INT
Funcs ((Funcs (NAT,INT)),NAT) is non empty non trivial functional non finite FUNCTION_DOMAIN of Funcs (NAT,INT), NAT
Funcs ((Funcs (NAT,INT)),INT) is non empty non trivial functional non finite FUNCTION_DOMAIN of Funcs (NAT,INT), INT
[:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):] is non empty non trivial non finite disjoint_with_NAT set
() is non empty non trivial non finite disjoint_with_NAT set
FreeUnivAlgNSG (ECIW-signature,()) is non empty V156() V157() V158() V159() V203() with_empty-instruction with_catenation with_if-instruction with_while-instruction infinite non degenerated V214() ECIW-strict L9()
DTConUA (ECIW-signature,()) is non empty strict V175() V176() V177() DTConstrStr
K262(ECIW-signature) is V107() V108() V109() V110() V111() V112() countable Element of bool NAT
K262(ECIW-signature) \/ () is non empty set
K673(ECIW-signature,()) is Relation-like K262(ECIW-signature) \/ () -defined K339((K262(ECIW-signature) \/ ())) -valued Element of bool [:(K262(ECIW-signature) \/ ()),K339((K262(ECIW-signature) \/ ())):]
K339((K262(ECIW-signature) \/ ())) is M16(K262(ECIW-signature) \/ ())
[:(K262(ECIW-signature) \/ ()),K339((K262(ECIW-signature) \/ ())):] is disjoint_with_NAT set
bool [:(K262(ECIW-signature) \/ ()),K339((K262(ECIW-signature) \/ ())):] is set
DTConstrStr(# (K262(ECIW-signature) \/ ()),K673(ECIW-signature,()) #) is strict DTConstrStr
K636((DTConUA (ECIW-signature,()))) is Element of bool K495( the carrier of (DTConUA (ECIW-signature,())))
the carrier of (DTConUA (ECIW-signature,())) is non empty set
K495( the carrier of (DTConUA (ECIW-signature,()))) is non empty M26( the carrier of (DTConUA (ECIW-signature,())))
bool K495( the carrier of (DTConUA (ECIW-signature,()))) is V14() set
FreeOpSeqNSG (ECIW-signature,()) is Relation-like NAT -defined K133(K339(K636((DTConUA (ECIW-signature,())))),K636((DTConUA (ECIW-signature,())))) -valued Function-like V85() M13(K133(K339(K636((DTConUA (ECIW-signature,())))),K636((DTConUA (ECIW-signature,())))))
K339(K636((DTConUA (ECIW-signature,())))) is M16(K636((DTConUA (ECIW-signature,()))))
K133(K339(K636((DTConUA (ECIW-signature,())))),K636((DTConUA (ECIW-signature,())))) is set
G9(K636((DTConUA (ECIW-signature,()))),(FreeOpSeqNSG (ECIW-signature,()))) is V156() L9()
the carrier of (FreeUnivAlgNSG (ECIW-signature,())) is non empty set
[:(Funcs (NAT,INT)), the carrier of (FreeUnivAlgNSG (ECIW-signature,())):] is non empty non trivial non finite disjoint_with_NAT set
((Funcs (NAT,INT)),0,0) is functional Element of bool (Funcs (NAT,INT))
bool (Funcs (NAT,INT)) is non empty non trivial V14() non finite set
{ b1 where b1 is Relation-like Function-like Element of Funcs (NAT,INT) : not b1 . 0 = 0 } is set
Terminals (DTConUA (ECIW-signature,())) is set
A is V11() real integer V83() ext-real Element of INT
NAT --> A is non empty non trivial T-Sequence-like Relation-like NAT -defined RAT -valued INT -valued Function-like constant V29( NAT ) quasi_total non finite complex-valued ext-real-valued real-valued Element of bool [:NAT,INT:]
[:NAT,INT:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
bool [:NAT,INT:] is non empty non trivial V14() non finite set
{A} is non empty trivial finite 1 -element V107() V108() V109() V110() V111() countable set
[:NAT,{A}:] is non empty non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued disjoint_with_NAT set
ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,())) is non empty non trivial non finite Element of bool the carrier of (FreeUnivAlgNSG (ECIW-signature,()))
bool the carrier of (FreeUnivAlgNSG (ECIW-signature,())) is V14() set
FreeGenSetNSG (ECIW-signature,()) is V202( FreeUnivAlgNSG (ECIW-signature,())) M47( FreeUnivAlgNSG (ECIW-signature,()))
K638((DTConUA (ECIW-signature,()))) is non empty Element of bool the carrier of (DTConUA (ECIW-signature,()))
bool the carrier of (DTConUA (ECIW-signature,())) is V14() set
{ (root-tree b1) where b1 is Element of the carrier of (DTConUA (ECIW-signature,())) : b1 in K638((DTConUA (ECIW-signature,()))) } is set
[:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,()))):] is non empty non trivial non finite disjoint_with_NAT set
y is set
m is set
d is set
[m,d] is V16() set
{m,d} is non empty finite countable set
{m} is non empty trivial finite 1 -element countable set
{{m,d},{m}} is non empty finite V37() countable set
s is Element of the carrier of (DTConUA (ECIW-signature,()))
root-tree s is Element of K495( the carrier of (DTConUA (ECIW-signature,())))
n is set
I is set
[n,I] is V16() set
{n,I} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,I},{n}} is non empty finite V37() countable set
C is Relation-like NAT -defined INT -valued Function-like V29( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of Funcs (NAT,INT)
s0 is Relation-like Funcs (NAT,INT) -defined NAT -valued Function-like V29( Funcs (NAT,INT)) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of Funcs ((Funcs (NAT,INT)),NAT)
((Funcs (NAT,INT)),NAT,s0,C) is ordinal natural V11() real finite cardinal integer V83() ext-real non negative V107() V108() V109() V110() V111() V112() countable Element of NAT
J is Relation-like Funcs (NAT,INT) -defined INT -valued Function-like V29( Funcs (NAT,INT)) quasi_total complex-valued ext-real-valued real-valued Element of Funcs ((Funcs (NAT,INT)),INT)
((Funcs (NAT,INT)),INT,J,C) is V11() real integer V83() ext-real Element of INT
C +* (((Funcs (NAT,INT)),NAT,s0,C),((Funcs (NAT,INT)),INT,J,C)) is non empty Relation-like NAT -defined INT -valued Function-like V29( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,INT:]
fs is non empty Relation-like NAT -defined INT -valued Function-like V29( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,INT:]
[s0,J] is V16() set
{s0,J} is non empty functional finite countable set
{s0} is non empty trivial functional finite 1 -element with_common_domain countable set
{{s0,J},{s0}} is non empty finite V37() countable set
root-tree [s0,J] is Relation-like Function-like V122() set
[C,(root-tree [s0,J])] is V16() set
{C,(root-tree [s0,J])} is non empty functional finite countable set
{C} is non empty trivial functional finite 1 -element with_common_domain countable set
{{C,(root-tree [s0,J])},{C}} is non empty finite V37() countable set
y is Relation-like Function-like set
proj1 y is set
proj2 y is set
[:[:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,()))):],(Funcs (NAT,INT)):] is non empty non trivial non finite disjoint_with_NAT set
bool [:[:(Funcs (NAT,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,()))):],(Funcs (NAT,INT)):] is non empty non trivial V14() non finite set
m is non empty Relation-like [:(Funcs (NAT,INT)),(ElementaryInstructions (