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

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

{ b

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

{ b

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

{ b

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 b

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