:: AOFA_I00 semantic presentation

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

bool 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

bool is non empty non trivial V14() non finite 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

bool [:K636(K637()),NAT:] is set

bool [:NAT,K636(K637()):] is set
ExtREAL is non empty V108() set

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

- 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

g is set
S is set
T is set
A is set
X is set
b is set

{S} is non empty trivial finite 1 -element countable set

{X} is non empty trivial finite 1 -element countable set

dom (S .--> X) is finite countable Element of bool {S}

{T} is non empty trivial finite 1 -element countable set

{b} is non empty trivial finite 1 -element countable set

{g} is non empty trivial finite 1 -element countable set

{A} is non empty trivial finite 1 -element 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 . g is set
d . S is set
d . T is set
dom (T .--> b) is finite countable Element of bool {T}

((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 . 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 . X is set

S . X is set

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

proj1 A is set

proj1 X is set
() /\ () is set

proj1 b is set
g is set
proj2 b is set
S is set
b . S is set

(A . S) div (X . S) is V11() real integer ext-real set

proj1 g is set

proj1 S is set
T is set

(A . T) div (X . T) is V11() real integer ext-real set

proj1 b is set
g is set
proj2 b is set
S is set
b . S is set

(A . S) mod (X . S) is V11() real integer ext-real set

proj1 g is set

proj1 S is set
T is set

(A . T) mod (X . T) is V11() real integer ext-real set

proj1 b is set
g is set
proj2 b is set
S is set
b . S is set

IFGT ((A . S),(X . S),0,1) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set

proj1 g is set

proj1 S is set
T is set

IFGT ((A . T),(X . T),0,1) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set

proj1 b is set
g is set
proj2 b is set
S is set
b . S is set

IFGT ((A . S),(X . S),1,0) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set

proj1 g is set

proj1 S is set
T is set

IFGT ((A . T),(X . T),1,0) is ordinal natural V11() real finite cardinal integer ext-real non negative countable set

proj1 b is set
g is set
proj2 b is set
S is set
b . S is 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

proj1 g is set

proj1 S is set
T is 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

A is non empty set

bool [:A,INT:] is non empty non trivial V14() non finite set

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

b + (X . S) is V11() real integer ext-real set

dom g 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
(X . S) + (- b) is V11() real integer ext-real set
S is 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

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

b * (X . S) is V11() real integer ext-real set

A is set

bool [:A,INT:] is 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

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

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

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

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

bool [:A,INT:] is non empty non trivial V14() non finite set

dom X is Element of bool A
bool A is V14() set

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

(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

dom X is Element of bool A
bool A is V14() 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
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

(X . S) + (b . S) is V11() real integer ext-real set

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

proj1 X is set
A is set

proj1 g is 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

proj2 m is set

proj2 m is set
y is set

y is set

g . y is set
X . (b (#) m) is set
S . y is set
g is set

S is set
proj2 x is set

T is set
proj2 y is set
g is set
union g is set
Funcs (A,()) is functional set
T is set
x is set

X . (b (#) y) is set

proj1 x is set
m is set
y is set
d is set
C is set

proj2 s is set

proj2 d is set
m is set
Funcs (A,y) is functional set

x . y is set

X . (b (#) y) is 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

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

proj2 m is set
y is set

bool [:A,X:] is set
m is Element of X

{m} is non empty trivial finite 1 -element countable 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

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:]

bool [:A,X:] is set
proj2 (g,S,T) is set
y is set
m is set
(g,S,T) . m is set

d * T is non empty Relation-like A -defined X -valued Function-like V29(A) quasi_total Element of bool [:A,X:]

bool [:A,X:] is set

S . C is Element of b

proj2 b is set

proj1 X is set

b (#) (A +* 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
() \/ () is set
proj1 (b (#) (A +* X)) is set
proj1 (b (#) X) is set
A is non empty set
b is non empty set

bool [:A,b:] is set
X is non empty set

bool [:A,X:] is 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:]

proj1 (S ") is set
rng S is Element of bool X
bool X is V14() set
T is Element of b

{T} is non empty trivial finite 1 -element countable 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

bool [:X,A:] is set

proj1 g is 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:]

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

(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 ")) (#) I is Relation-like Function-like 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:]

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

[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set

proj1 X is set
proj2 X is set

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

proj1 X is set
proj2 X is set

rng b is Element of bool A
bool A is set
A is set

[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set

proj1 X is set
proj2 X is set
A is set

[:(card A),A:] is disjoint_with_NAT set
bool [:(card A),A:] is 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 . 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

bool (card A) is V14() set

bool A is V14() set
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):] +* (S,()) 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,())) +* (X,0) is Relation-like Function-like set

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,())) 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 . 0 is set
A is countable set

[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is set

rng X is Element of bool (card A)
bool (card A) is set
A is set

[:A,(card A):] is disjoint_with_NAT set
bool [:A,(card A):] is 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),A:] is disjoint_with_NAT set
bool [:(card A),A:] is 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

0 to_power (A + X) is V11() real ext-real set
0 |^ (A + X) is set

0 |^ A is set

0 |^ X is set
() * () is V11() real ext-real set
A is V11() real ext-real set

A |^ X is set

(A to_power X) to_power b is V11() real ext-real set
(A to_power X) |^ b is set

A to_power (X * b) is V11() real ext-real set
A |^ (X * b) is set

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

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

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

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

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:]

ElementaryInstructions A is Element of bool the carrier of A
bool the carrier of A is V14() set

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,S},{y}} is non empty finite V37() countable 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:]

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

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

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:]

ElementaryInstructions A is Element of bool the carrier of A
bool the carrier of A is V14() set

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,S},{y}} is non empty finite V37() countable 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:]

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

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

bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set
X is Element of A

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

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 . 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

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:]

(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 non empty trivial finite 1 -element V107() V108() V109() V110() V111() countable set

bool [:(Funcs (A,INT)),{X}:] is non empty non trivial V14() non finite 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

bool [:(Funcs (A,INT)),INT:] is non empty non trivial V14() non finite set

is non empty trivial finite V37() 1 -element V107() V108() V109() V110() V111() V112() countable set

bool [:(Funcs (A,INT)),:] is non empty non trivial V14() non finite set

{1} is non empty trivial finite V37() 1 -element V107() V108() V109() V110() V111() V112() countable set

bool [:(Funcs (A,INT)),{1}:] is non empty non trivial V14() non finite set

((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:]

(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))

(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

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

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(()) -valued Element of bool [:(),K339(()):]
K339(()) is M16(K262(ECIW-signature) \/ ())
[:(),K339(()):] is disjoint_with_NAT set
bool [:(),K339(()):] is set
DTConstrStr(# (),K673(ECIW-signature,()) #) is strict DTConstrStr
K636(()) is Element of bool K495( the carrier of ())
the carrier of () is non empty set
K495( the carrier of ()) is non empty M26( the carrier of ())
bool K495( the carrier of ()) is V14() set
FreeOpSeqNSG (ECIW-signature,()) is Relation-like NAT -defined K133(K339(K636(())),K636(())) -valued Function-like V85() M13(K133(K339(K636(())),K636(())))
K339(K636(())) is M16(K636(()))
K133(K339(K636(())),K636(())) is set
G9(K636(()),()) is V156() L9()
the carrier of () is non empty set
[:(Funcs (NAT,INT)), the carrier of ():] 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 () is set
A is V11() real integer V83() ext-real Element of INT

bool is non empty non trivial V14() non finite set
{A} is non empty trivial finite 1 -element V107() V108() V109() V110() V111() countable set

ElementaryInstructions () is non empty non trivial non finite Element of bool the carrier of ()
bool the carrier of () is V14() set

K638(()) is non empty Element of bool the carrier of ()
bool the carrier of () is V14() set
{ () where b1 is Element of the carrier of () : b1 in K638(()) } is set
[:(Funcs (NAT,INT)),:] 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 ()
root-tree s is Element of K495( the carrier of ())
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

((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

((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

[s0,J] is V16() set
{s0,J} is non empty functional finite countable set

{{s0,J},{s0}} is non empty finite V37() countable set

[C,(root-tree [s0,J])] is V16() set
{C,(root-tree [s0,J])} is non empty functional finite countable set

{{C,(root-tree [s0,J])},{C}} is non empty finite V37() countable set

proj1 y is set
proj2 y is set
[:[:(Funcs (NAT,INT)),:],(Funcs (NAT,INT)):] is non empty non trivial non finite disjoint_with_NAT set
bool [:[:(Funcs (NAT,INT)),:],(Funcs (NAT,INT)):] is non empty non trivial V14() non finite set
m is non empty Relation-like [:(Funcs (NAT,INT)),