:: TURING_1 semantic presentation

REAL is non empty non trivial non finite set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty non trivial non finite set

RAT is non empty non trivial non finite set

INT is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is non empty set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is non empty set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is non empty set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty set

[:[:NAT,NAT:],NAT:] is non empty set

bool [:[:NAT,NAT:],NAT:] is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is non empty set

bool NAT is non empty set

K240(NAT) is V46() set

K384() is V72() V100() L8()

K189() is Relation-like [:INT,INT:] -defined INT -valued Function-like quasi_total Element of bool [:[:INT,INT:],INT:]

G8(INT,K189()) is V100() L8()

the U1 of K384() is set

{} is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer finite V36() FinSequence-membered ext-real set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT

{{},1} is non empty finite set

K503() is set

NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT

K518(NAT) is non empty functional M13(NAT * , NAT )

K453((NAT *),NAT) is M13(NAT * , NAT )

{ b

bool K518(NAT) is non empty set

K396(K518(NAT)) is non empty Element of bool (bool K518(NAT))

bool (bool K518(NAT)) is non empty set

[:NAT,K396(K518(NAT)):] is non empty set

bool [:NAT,K396(K518(NAT)):] is non empty set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT

0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer finite V36() FinSequence-membered ext-real Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT

Seg 1 is non empty finite V39(1) Element of bool NAT

{ b

Seg 2 is non empty finite V39(2) Element of bool NAT

{ b

[+] is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(2) set

1 proj 1 is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(1) set

1 |-> NAT is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of 1 -tuples_on (bool REAL)

1 -tuples_on (bool REAL) is FinSequenceSet of bool REAL

K408((1 |-> NAT),1) is Relation-like Function-like set

3 succ 3 is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(3) set

K523((1 proj 1),(3 succ 3),2) is non empty Relation-like NAT * -defined NAT -valued Function-like V53() homogeneous quasi_total V147() V152() V153(2) M14(NAT * , NAT ,K518(NAT))

4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT

s is non empty set

t is non empty set

[:s,t:] is non empty set

bool [:s,t:] is non empty set

h is Relation-like s -defined t -valued Function-like quasi_total Element of bool [:s,t:]

n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]

h +* n is Relation-like Function-like set

h1 is set

proj1 n is set

h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]

(h +* n) . h1 is set

n . h1 is set

proj1 n is set

h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]

(h +* n) . h1 is set

h . h1 is set

proj1 n is set

h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]

h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]

proj1 h is set

proj1 n is set

proj1 (h +* n) is set

(proj1 h) \/ (proj1 n) is set

s is non empty set

t is non empty set

h is Element of s

n is Element of t

h .--> n is Relation-like s -defined {h} -defined t -valued Function-like one-to-one finite set

{h} is non empty finite set

{h} --> n is non empty Relation-like {h} -defined t -valued {n} -valued Function-like constant total quasi_total finite Element of bool [:{h},{n}:]

{n} is non empty finite set

[:{h},{n}:] is non empty finite set

bool [:{h},{n}:] is non empty finite V36() set

[:s,t:] is non empty set

bool [:s,t:] is non empty set

proj1 (h .--> n) is finite set

{h} is non empty finite Element of bool s

bool s is non empty set

proj2 (h .--> n) is finite set

{n} is non empty finite Element of bool t

bool t is non empty set

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

succ s is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

{ b

t is Element of bool NAT

h is Element of bool NAT

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

(s) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of bool NAT

{ b

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(t) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer finite ext-real Element of bool NAT

{ b

h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s is Relation-like Function-like set

h1 is set

t is set

h is set

[t,h] is V1() set

n is set

[t,h] .--> n is Relation-like {[t,h]} -defined Function-like one-to-one finite set

{[t,h]} is non empty finite set

{[t,h]} --> n is non empty Relation-like {[t,h]} -defined {n} -valued Function-like constant total quasi_total finite Element of bool [:{[t,h]},{n}:]

{n} is non empty finite set

[:{[t,h]},{n}:] is non empty finite set

bool [:{[t,h]},{n}:] is non empty finite V36() set

s +* ([t,h] .--> n) is Relation-like Function-like set

s1 is set

[h1,s1] is V1() set

(s +* ([t,h] .--> n)) . [h1,s1] is set

s . [h1,s1] is set

proj1 ([t,h] .--> n) is finite set

s is Relation-like Function-like set

s1 is set

h is set

t is set

[t,h] is V1() set

n is set

[t,h] .--> n is Relation-like {[t,h]} -defined Function-like one-to-one finite set

{[t,h]} is non empty finite set

{[t,h]} --> n is non empty Relation-like {[t,h]} -defined {n} -valued Function-like constant total quasi_total finite Element of bool [:{[t,h]},{n}:]

{n} is non empty finite set

[:{[t,h]},{n}:] is non empty finite set

bool [:{[t,h]},{n}:] is non empty finite V36() set

s +* ([t,h] .--> n) is Relation-like Function-like set

h1 is set

[h1,s1] is V1() set

(s +* ([t,h] .--> n)) . [h1,s1] is set

s . [h1,s1] is set

proj1 ([t,h] .--> n) is finite set

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

t | s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg s is finite V39(s) Element of bool NAT

{ b

t | (Seg s) is Relation-like finite FinSubsequence-like set

t | (Seg s) is Relation-like NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty set

n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

proj1 (t | (Seg s)) is finite set

dom t is finite Element of bool NAT

t . n is set

(t | (Seg s)) . n is set

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

<*s,t*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of NAT

<*s*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,s] is V1() set

{[1,s]} is non empty finite set

<*t*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,t] is V1() set

{[1,t]} is non empty finite set

<*s*> ^ <*t*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(1,<*s,t*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

<*s,t*> | (Seg 1) is Relation-like finite FinSubsequence-like set

Sum (1,<*s,t*>) is V24() V25() integer ext-real Element of INT

K241(INT,(1,<*s,t*>),K189()) is V24() V25() integer ext-real Element of INT

(2,<*s,t*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

<*s,t*> | (Seg 2) is Relation-like finite FinSubsequence-like set

Sum (2,<*s,t*>) is V24() V25() integer ext-real Element of INT

K241(INT,(2,<*s,t*>),K189()) is V24() V25() integer ext-real Element of INT

s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h is V24() V25() integer ext-real Element of INT

<*h*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like FinSequence of INT

[1,h] is V1() set

{[1,h]} is non empty finite set

Sum <*h*> is V24() V25() integer ext-real Element of INT

K241(INT,<*h*>,K189()) is V24() V25() integer ext-real Element of INT

len <*s,t*> is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

n is V24() V25() integer ext-real Element of INT

<*h,n*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of INT

<*h*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

<*n*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,n] is V1() set

{[1,n]} is non empty finite set

<*h*> ^ <*n*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set

Sum <*h,n*> is V24() V25() integer ext-real Element of INT

K241(INT,<*h,n*>,K189()) is V24() V25() integer ext-real Element of INT

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

<*s,t,h*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V39(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*s*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,s] is V1() set

{[1,s]} is non empty finite set

<*t*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,t] is V1() set

{[1,t]} is non empty finite set

<*s*> ^ <*t*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

<*h*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,h] is V1() set

{[1,h]} is non empty finite set

(<*s*> ^ <*t*>) ^ <*h*> is non empty Relation-like NAT -defined Function-like finite V39((1 + 1) + 1) FinSequence-like FinSubsequence-like set

(1 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(1,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

<*s,t,h*> | (Seg 1) is Relation-like finite FinSubsequence-like set

Sum (1,<*s,t,h*>) is V24() V25() integer ext-real Element of INT

K241(INT,(1,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT

(2,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

<*s,t,h*> | (Seg 2) is Relation-like finite FinSubsequence-like set

Sum (2,<*s,t,h*>) is V24() V25() integer ext-real Element of INT

K241(INT,(2,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT

s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(3,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

Seg 3 is non empty finite V39(3) Element of bool NAT

{ b

<*s,t,h*> | (Seg 3) is Relation-like finite FinSubsequence-like set

Sum (3,<*s,t,h*>) is V24() V25() integer ext-real Element of INT

K241(INT,(3,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT

(s + t) + h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

n is V24() V25() integer ext-real Element of INT

<*n*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like FinSequence of INT

[1,n] is V1() set

{[1,n]} is non empty finite set

Sum <*n*> is V24() V25() integer ext-real Element of INT

K241(INT,<*n*>,K189()) is V24() V25() integer ext-real Element of INT

h1 is V24() V25() integer ext-real Element of INT

<*n,h1*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of INT

<*n*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

<*h1*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,h1] is V1() set

{[1,h1]} is non empty finite set

<*n*> ^ <*h1*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set

Sum <*n,h1*> is V24() V25() integer ext-real Element of INT

K241(INT,<*n,h1*>,K189()) is V24() V25() integer ext-real Element of INT

len <*s,t,h*> is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s1 is V24() V25() integer ext-real Element of INT

<*n,h1,s1*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(3) FinSequence-like FinSubsequence-like FinSequence of INT

<*s1*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set

[1,s1] is V1() set

{[1,s1]} is non empty finite set

(<*n*> ^ <*h1*>) ^ <*s1*> is non empty Relation-like NAT -defined Function-like finite V39((1 + 1) + 1) FinSequence-like FinSubsequence-like set

Sum <*n,h1,s1*> is V24() V25() integer ext-real Element of INT

K241(INT,<*n,h1,s1*>,K189()) is V24() V25() integer ext-real Element of INT

- 1 is V24() V25() integer ext-real Element of REAL

{(- 1),0,1} is non empty finite Element of bool REAL

s is ()

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

t is Relation-like INT -defined the of s -valued Function-like quasi_total Element of Funcs (INT, the of s)

h is V24() V25() integer ext-real set

n is Element of the of s

h .--> n is Relation-like {h} -defined the of s -valued Function-like one-to-one finite set

{h} is non empty finite set

{h} --> n is non empty Relation-like {h} -defined the of s -valued {n} -valued Function-like constant total quasi_total finite Element of bool [:{h},{n}:]

{n} is non empty finite set

[:{h},{n}:] is non empty finite set

bool [:{h},{n}:] is non empty finite V36() set

t +* (h .--> n) is Relation-like Function-like set

proj2 (h .--> n) is finite set

{n} is non empty finite Element of bool the of s

bool the of s is non empty finite V36() set

proj2 (t +* (h .--> n)) is set

proj2 t is set

(proj2 t) \/ (proj2 (h .--> n)) is set

t2 is Relation-like Function-like set

proj1 t2 is set

proj2 t2 is set

proj1 (t +* (h .--> n)) is set

proj1 t is set

proj1 (h .--> n) is finite set

(proj1 t) \/ (proj1 (h .--> n)) is set

(proj1 t) \/ {h} is non empty set

t2 is Relation-like Function-like set

proj1 t2 is set

proj2 t2 is set

s is ()

the of s is non empty finite set

the of s is non empty finite set

[: the of s, the of s,{(- 1),0,1}:] is non empty finite set

t is Element of [: the of s, the of s,{(- 1),0,1}:]

t `3_3 is Element of {(- 1),0,1}

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

t `2_3 is V24() V25() integer ext-real Element of INT

t `1 is set

(t `1) `2 is set

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

the of s is Relation-like [: the of s, the of s:] -defined [: the of s, the of s,{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:]

[: the of s, the of s:] is non empty finite set

[: the of s, the of s,{(- 1),0,1}:] is non empty finite set

[:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite set

bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite V36() set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

t `1_3 is Element of the of s

t `1 is set

(t `1) `1 is set

t `3_3 is Element of Funcs (INT, the of s)

(s,t) is V24() V25() integer ext-real set

t `2_3 is V24() V25() integer ext-real Element of INT

(t `1) `2 is set

(t `3_3) . (s,t) is set

[(t `1_3),((t `3_3) . (s,t))] is V1() set

the of s . [(t `1_3),((t `3_3) . (s,t))] is set

h is V24() V25() integer ext-real Element of INT

(t `3_3) . h is Element of the of s

[(t `1_3),((t `3_3) . h)] is V1() Element of [: the of s, the of s:]

the of s . [(t `1_3),((t `3_3) . h)] is Element of [: the of s, the of s,{(- 1),0,1}:]

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

t `1_3 is Element of the of s

t `1 is set

(t `1) `1 is set

the of s is Element of the of s

(s,t) is Element of [: the of s, the of s,{(- 1),0,1}:]

[: the of s, the of s,{(- 1),0,1}:] is non empty finite set

the of s is Relation-like [: the of s, the of s:] -defined [: the of s, the of s,{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:]

[: the of s, the of s:] is non empty finite set

[:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite set

bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite V36() set

t `3_3 is Element of Funcs (INT, the of s)

(s,t) is V24() V25() integer ext-real set

t `2_3 is V24() V25() integer ext-real Element of INT

(t `1) `2 is set

(t `3_3) . (s,t) is set

[(t `1_3),((t `3_3) . (s,t))] is V1() set

the of s . [(t `1_3),((t `3_3) . (s,t))] is set

(s,t) `1_3 is Element of the of s

(s,t) `1 is set

((s,t) `1) `1 is set

(s,(s,t)) is V24() V25() integer ext-real set

(s,t) `3_3 is Element of {(- 1),0,1}

(s,t) + (s,(s,t)) is V24() V25() integer ext-real set

(s,t) `2_3 is Element of the of s

((s,t) `1) `2 is set

(s,(t `3_3),(s,t),((s,t) `2_3)) is Relation-like INT -defined the of s -valued Function-like quasi_total Element of Funcs (INT, the of s)

(s,t) .--> ((s,t) `2_3) is Relation-like {(s,t)} -defined the of s -valued Function-like one-to-one finite set

{(s,t)} is non empty finite set

{(s,t)} --> ((s,t) `2_3) is non empty Relation-like {(s,t)} -defined the of s -valued {((s,t) `2_3)} -valued Function-like constant total quasi_total finite Element of bool [:{(s,t)},{((s,t) `2_3)}:]

{((s,t) `2_3)} is non empty finite set

[:{(s,t)},{((s,t) `2_3)}:] is non empty finite set

bool [:{(s,t)},{((s,t) `2_3)}:] is non empty finite V36() set

(t `3_3) +* ((s,t) .--> ((s,t) `2_3)) is Relation-like Function-like set

[((s,t) `1_3),((s,t) + (s,(s,t))),(s,(t `3_3),(s,t),((s,t) `2_3))] is V1() V2() set

[((s,t) `1_3),((s,t) + (s,(s,t)))] is V1() set

[[((s,t) `1_3),((s,t) + (s,(s,t)))],(s,(t `3_3),(s,t),((s,t) `2_3))] is V1() set

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

h . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

n + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h . (n + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h . n is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,(h . n)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

h . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

n is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

n . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h . (h1 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,(h . h1)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

n . (h1 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

n . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,(n . h1)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

t `1_3 is Element of the of s

t `1 is set

(t `1) `1 is set

the of s is Element of the of s

(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

(s,t) . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

t is ()

the of t is non empty finite set

the of t is non empty finite set

Funcs (INT, the of t) is non empty FUNCTION_DOMAIN of INT , the of t

[: the of t,INT,(Funcs (INT, the of t)):] is non empty set

h is Element of [: the of t,INT,(Funcs (INT, the of t)):]

(t,h) is Relation-like NAT -defined [: the of t,INT,(Funcs (INT, the of t)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:]

[:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:] is non empty set

bool [:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:] is non empty set

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(t,h) . (s + 1) is Element of [: the of t,INT,(Funcs (INT, the of t)):]

(t,h) . s is Element of [: the of t,INT,(Funcs (INT, the of t)):]

(t,((t,h) . s)) is Element of [: the of t,INT,(Funcs (INT, the of t)):]

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

(s,t) . 1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . (0 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,((s,t) . 0)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h is ()

the of h is non empty finite set

the of h is non empty finite set

Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h

[: the of h,INT,(Funcs (INT, the of h)):] is non empty set

n is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]

[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

(h,n) . (s + t) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]

(h,((h,n) . s)) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + h1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) . h1 is Element of [: the of h,INT,(Funcs (INT, the of h)):]

h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + (h1 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + (h1 + 1)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) . (h1 + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(s + h1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . ((s + h1) + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . (s + h1))) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + 0) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) . 0 is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h is ()

the of h is non empty finite set

the of h is non empty finite set

Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h

[: the of h,INT,(Funcs (INT, the of h)):] is non empty set

n is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]

[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,n) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

s + h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + s1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

s + (s1 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + (s1 + 1)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(s + s1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . ((s + s1) + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(h,n) . (s + 0) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

h is ()

the of h is non empty finite set

the of h is non empty finite set

Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h

[: the of h,INT,(Funcs (INT, the of h)):] is non empty set

the of h is Element of the of h

n is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]

[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set

(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]

((h,n) . s) `1_3 is Element of the of h

((h,n) . s) `1 is set

(((h,n) . s) `1) `1 is set

(h,n) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]

(h,((h,n) . s)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

the of s is Element of the of s

h is Element of [: the of s,INT,(Funcs (INT, the of s)):]

n is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . h1) `1_3 is Element of the of s

((s,t) . h1) `1 is set

(((s,t) . h1) `1) `1 is set

s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . s1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . s1) `1_3 is Element of the of s

((s,t) . s1) `1 is set

(((s,t) . s1) `1) `1 is set

h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . h) `1_3 is Element of the of s

((s,t) . h) `1 is set

(((s,t) . h) `1) `1 is set

s is ()

the of s is non empty finite set

the of s is non empty finite set

Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s

[: the of s,INT,(Funcs (INT, the of s)):] is non empty set

the of s is Element of the of s

t is Element of [: the of s,INT,(Funcs (INT, the of s)):]

(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]

[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set

(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]

h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . h) `1_3 is Element of the of s

((s,t) . h) `1 is set

(((s,t) . h) `1) `1 is set

h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set

(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . h) `1_3 is Element of the of s

((s,t) . h) `1 is set

(((s,t) . h) `1) `1 is set

n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . n is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . n) `1_3 is Element of the of s

((s,t) . n) `1 is set

(((s,t) . n) `1) `1 is set

h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(s,t) . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]

((s,t) . h1) `1_3 is Element of the of s

((s,t) . h1) `1 is set

(((s,t) . h1) `1) `1 is set

h is set

t is non empty set

s is non empty set

[:s,t:] is non empty set

[:s,[:s,t:]:] is non empty set

bool [:s,[:s,t:]:] is non empty set

n is Element of t

h1 is Relation-like s -defined [:s,t:] -valued Function-like quasi_total Element of bool [:s,[:s,t:]:]

s1 is Element of s

h1 . s1 is Element of [:s,t:]

[s1,h] is V1() set

5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT

(5) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer finite ext-real Element of bool NAT

{ b

{0,1} is non empty finite Element of bool NAT

[:(5),{0,1}:] is non empty Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty set

([:(5),{0,1}:],{(- 1),0,1},0) is Relation-like [:(5),{0,1}:] -defined [:[:(5),{0,1}:],{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:]

[:[:(5),{0,1}:],{(- 1),0,1}:] is non empty finite set

[:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:] is non empty finite set

bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:] is non empty finite V36() set

[:NAT,NAT,NAT:] is non empty set

[0,0] is V1() Element of [:NAT,NAT:]

[0,0,1] is V1() V2() Element of [:NAT,NAT,NAT:]

[0,0] is V1() set

[[0,0],1] is V1() set

([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1]) is Relation-like [:NAT,NAT:] -defined {[0,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[0,0]} is non empty finite set

[:[:NAT,NAT:],[:NAT,NAT,NAT:]:] is non empty set

bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:] is non empty set

{[0,0]} --> [0,0,1] is non empty Relation-like {[0,0]} -defined [:NAT,NAT,NAT:] -valued {[0,0,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[0,0]},{[0,0,1]}:]

{[0,0,1]} is non empty finite set

[:{[0,0]},{[0,0,1]}:] is non empty finite set

bool [:{[0,0]},{[0,0,1]}:] is non empty finite V36() set

([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1]) is Relation-like Function-like finite set

[0,1] is V1() Element of [:NAT,NAT:]

[1,0,1] is V1() V2() Element of [:NAT,NAT,NAT:]

[1,0] is V1() set

[[1,0],1] is V1() set

([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1]) is Relation-like [:NAT,NAT:] -defined {[0,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[0,1]} is non empty finite set

{[0,1]} --> [1,0,1] is non empty Relation-like {[0,1]} -defined [:NAT,NAT,NAT:] -valued {[1,0,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[0,1]},{[1,0,1]}:]

{[1,0,1]} is non empty finite set

[:{[0,1]},{[1,0,1]}:] is non empty finite set

bool [:{[0,1]},{[1,0,1]}:] is non empty finite V36() set

(([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1]) is Relation-like Function-like finite set

[1,1] is V1() Element of [:NAT,NAT:]

[1,1,1] is V1() V2() Element of [:NAT,NAT,NAT:]

[1,1] is V1() set

[[1,1],1] is V1() set

([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1]) is Relation-like [:NAT,NAT:] -defined {[1,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[1,1]} is non empty finite set

{[1,1]} --> [1,1,1] is non empty Relation-like {[1,1]} -defined [:NAT,NAT,NAT:] -valued {[1,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[1,1]},{[1,1,1]}:]

{[1,1,1]} is non empty finite set

[:{[1,1]},{[1,1,1]}:] is non empty finite set

bool [:{[1,1]},{[1,1,1]}:] is non empty finite V36() set

((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1]) is Relation-like Function-like finite set

[1,0] is V1() Element of [:NAT,NAT:]

[2,1,1] is V1() V2() Element of [:NAT,NAT,NAT:]

[2,1] is V1() set

[[2,1],1] is V1() set

([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1]) is Relation-like [:NAT,NAT:] -defined {[1,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[1,0]} is non empty finite set

{[1,0]} --> [2,1,1] is non empty Relation-like {[1,0]} -defined [:NAT,NAT,NAT:] -valued {[2,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[1,0]},{[2,1,1]}:]

{[2,1,1]} is non empty finite set

[:{[1,0]},{[2,1,1]}:] is non empty finite set

bool [:{[1,0]},{[2,1,1]}:] is non empty finite V36() set

(((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1]) is Relation-like Function-like finite set

[2,1] is V1() Element of [:NAT,NAT:]

([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1]) is Relation-like [:NAT,NAT:] -defined {[2,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[2,1]} is non empty finite set

{[2,1]} --> [2,1,1] is non empty Relation-like {[2,1]} -defined [:NAT,NAT,NAT:] -valued {[2,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[2,1]},{[2,1,1]}:]

[:{[2,1]},{[2,1,1]}:] is non empty finite set

bool [:{[2,1]},{[2,1,1]}:] is non empty finite V36() set

((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1]) is Relation-like Function-like finite set

[:NAT,NAT,REAL:] is non empty set

[2,0] is V1() Element of [:NAT,NAT:]

[3,0,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]

[3,0] is V1() set

[[3,0],(- 1)] is V1() set

([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[2,0]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]

{[2,0]} is non empty finite set

[:[:NAT,NAT:],[:NAT,NAT,REAL:]:] is non empty set

bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:] is non empty set

{[2,0]} --> [3,0,(- 1)] is non empty Relation-like {[2,0]} -defined [:NAT,NAT,REAL:] -valued {[3,0,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[2,0]},{[3,0,(- 1)]}:]

{[3,0,(- 1)]} is non empty finite set

[:{[2,0]},{[3,0,(- 1)]}:] is non empty finite set

bool [:{[2,0]},{[3,0,(- 1)]}:] is non empty finite V36() set

(((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)]) is Relation-like Function-like finite set

[3,1] is V1() Element of [:NAT,NAT:]

[4,0,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]

[4,0] is V1() set

[[4,0],(- 1)] is V1() set

([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[3,1]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]

{[3,1]} is non empty finite set

{[3,1]} --> [4,0,(- 1)] is non empty Relation-like {[3,1]} -defined [:NAT,NAT,REAL:] -valued {[4,0,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[3,1]},{[4,0,(- 1)]}:]

{[4,0,(- 1)]} is non empty finite set

[:{[3,1]},{[4,0,(- 1)]}:] is non empty finite set

bool [:{[3,1]},{[4,0,(- 1)]}:] is non empty finite V36() set

((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)]) is Relation-like Function-like finite set

[4,1] is V1() Element of [:NAT,NAT:]

[4,1,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]

[4,1] is V1() set

[[4,1],(- 1)] is V1() set

([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[4,1]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]

{[4,1]} is non empty finite set

{[4,1]} --> [4,1,(- 1)] is non empty Relation-like {[4,1]} -defined [:NAT,NAT,REAL:] -valued {[4,1,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[4,1]},{[4,1,(- 1)]}:]

{[4,1,(- 1)]} is non empty finite set

[:{[4,1]},{[4,1,(- 1)]}:] is non empty finite set

bool [:{[4,1]},{[4,1,(- 1)]}:] is non empty finite V36() set

(((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)]) is Relation-like Function-like finite set

[4,0] is V1() Element of [:NAT,NAT:]

[5,0,0] is V1() V2() Element of [:NAT,NAT,NAT:]

[5,0] is V1() set

[[5,0],0] is V1() set

([:NAT,NAT:],[:NAT,NAT,NAT:],[4,0],[5,0,0]) is Relation-like [:NAT,NAT:] -defined {[4,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]

{[4,0]} is non empty finite set

{[4,0]} --> [5,0,0] is non empty Relation-like {[4,0]} -defined [:NAT,NAT,NAT:] -valued {[5,0,0]} -valued Function-like constant total quasi_total finite Element of bool [:{[4,0]},{[5,0,0]}:]

{[5,0,0]} is non empty finite set

[:{[4,0]},{[5,0,0]}:] is non empty finite set

bool [:{[4,0]},{[5,0,0]}:] is non empty finite V36() set

((((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[4,0],[5,0,0]) is Relation-like Function-like finite set

[:(5),{0,1},{(- 1),0,1}:] is non empty finite Element of bool [:NAT,NAT,REAL:]

bool [:NAT,NAT,REAL:] is non empty set

[:[:(5),{0,1}:],[:(5),{0,1},{(- 1),0,1}:]:] is non empty finite set

bool [:[:(5),{0,1}:],[:(5),{0,1},{(- 1),0,1}:]:] is non empty finite V36() set

[:[:(5),{0,1}:],{(- 1),0,1}:] is non empty Relation-like [:NAT,NAT:] -defined REAL -valued finite Element of bool [:[:NAT,NAT:],REAL:]

[:[:NAT,NAT:],REAL:] is non empty set

bool [:[:NAT,NAT:],REAL:] is non empty set

s1k is Element of {(- 1),0,1}

([:(5),{0,1}:],{(- 1),0,1},s1k) is Relation-like [:(5),{0,1}:] -defined [:[:(5),{0,1}:],{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:]

[:(5),{0,1}:] is non empty finite set

[:(5),{0,1},{(- 1),0,1}:] is non