:: TURING_1 semantic presentation

REAL is non empty non trivial non finite set

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
is non empty set
bool is non empty set
is non empty set

is non empty set
bool is non empty set
is non empty set
bool is non empty set
is non empty set
bool is non empty set
is non empty set
bool is non empty set
is non empty set
bool is non empty set
is non empty set
bool is non empty set
is non empty set
is non empty set
bool is non empty set

bool omega is non empty set
bool NAT is non empty set
K240(NAT) is V46() set
K384() is V72() V100() L8()

G8(INT,K189()) is V100() L8()
the U1 of K384() is set

{{},1} is non empty finite set
K503() is set

K518(NAT) is non empty functional M13(NAT * , NAT )
K453((),NAT) is M13(NAT * , NAT )
{ b1 where b1 is Relation-like NAT * -defined NAT -valued Function-like M14(NAT * , NAT ,K453((),NAT)) : b1 is homogeneous } is set
bool K518(NAT) is non empty set
K396(K518(NAT)) is non empty Element of bool ()
bool () is non empty set
[:NAT,K396(K518(NAT)):] is non empty set
bool [:NAT,K396(K518(NAT)):] is non empty set

Seg 1 is non empty finite V39(1) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
Seg 2 is non empty finite V39(2) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set

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

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

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

h1 is set
proj1 n is set

(h +* n) . h1 is set
n . h1 is set
proj1 n is set

(h +* n) . h1 is set
h . h1 is set
proj1 n is set

proj1 h is set
proj1 n is set
proj1 (h +* n) is set
() \/ () is set
s is non empty set
t is non empty set
h is Element of s
n is Element of t

{h} is non empty finite set

{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

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= s } is set
t is Element of bool NAT
h is Element of bool NAT

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= s } is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= t } is set

h1 is set
t is set
h is set
[t,h] is V1() set
n is set

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

{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

s1 is set
h is set
t is set
[t,h] is V1() set
n is set

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

{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

Seg s is finite V39(s) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= s ) } is set

bool is non empty set

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

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

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

[1,t] is V1() set
{[1,t]} is non empty finite 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

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

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

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

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

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

[1,n] is V1() set
{[1,n]} is non empty finite 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

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

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

[1,h] is V1() set
{[1,h]} is non empty finite 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

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

Seg 3 is non empty finite V39(3) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is 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

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

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

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

[1,h1] is V1() set
{[1,h1]} is non empty finite 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

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

[1,s1] is V1() set
{[1,s1]} is non empty finite 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} is non empty finite set

{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 (h .--> n)) is 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 (h .--> n)) is set
() \/ {h} is non empty 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)):]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

(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

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

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

(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

s1 is Element of s
h1 . s1 is Element of [:s,t:]
[s1,h] is V1() set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= 5 } is set
{0,1} is non empty finite Element of bool NAT

bool 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
is non empty set
[0,0] is V1() Element of
[0,0,1] is V1() V2() Element of
[0,0] is V1() set
[[0,0],1] is V1() set

is non empty finite set
is non empty set
bool is non empty set

{[0,0,1]} is non empty finite set
[:,{[0,0,1]}:] is non empty finite set
bool [:,{[0,0,1]}:] is non empty finite V36() set
([:(5),{0,1}:],{(- 1),0,1},0) +* (,,[0,0],[0,0,1]) is Relation-like Function-like finite set
[0,1] is V1() Element of
[1,0,1] is V1() V2() Element of
[1,0] is V1() set
[[1,0],1] is V1() set

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

{[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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1]) is Relation-like Function-like finite set
[1,1] is V1() Element of
[1,1,1] is V1() V2() Element of
[1,1] is V1() set
[[1,1],1] is V1() set

{[1,1]} is non empty finite set
{[1,1]} --> [1,1,1] is non empty Relation-like {[1,1]} -defined -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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1]) is Relation-like Function-like finite set
[1,0] is V1() Element of
[2,1,1] is V1() V2() Element of
[2,1] is V1() set
[[2,1],1] is V1() set

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

{[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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1]) is Relation-like Function-like finite set
[2,1] is V1() Element of

{[2,1]} is non empty finite set
{[2,1]} --> [2,1,1] is non empty Relation-like {[2,1]} -defined -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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1])) +* (,,[2,1],[2,1,1]) is Relation-like Function-like finite set
is non empty set
[2,0] is V1() Element of
[3,0,(- 1)] is V1() V2() Element of
[3,0] is V1() set
[[3,0],(- 1)] is V1() set

{[2,0]} is non empty finite set
is non empty set
bool is non empty set
{[2,0]} --> [3,0,(- 1)] is non empty Relation-like {[2,0]} -defined -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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1])) +* (,,[2,1],[2,1,1])) +* (,,[2,0],[3,0,(- 1)]) is Relation-like Function-like finite set
[3,1] is V1() Element of
[4,0,(- 1)] is V1() V2() Element of
[4,0] is V1() set
[[4,0],(- 1)] is V1() set

{[3,1]} is non empty finite set
{[3,1]} --> [4,0,(- 1)] is non empty Relation-like {[3,1]} -defined -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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1])) +* (,,[2,1],[2,1,1])) +* (,,[2,0],[3,0,(- 1)])) +* (,,[3,1],[4,0,(- 1)]) is Relation-like Function-like finite set
[4,1] is V1() Element of
[4,1,(- 1)] is V1() V2() Element of
[4,1] is V1() set
[[4,1],(- 1)] is V1() set

{[4,1]} is non empty finite set
{[4,1]} --> [4,1,(- 1)] is non empty Relation-like {[4,1]} -defined -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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1])) +* (,,[2,1],[2,1,1])) +* (,,[2,0],[3,0,(- 1)])) +* (,,[3,1],[4,0,(- 1)])) +* (,,[4,1],[4,1,(- 1)]) is Relation-like Function-like finite set
[4,0] is V1() Element of
[5,0,0] is V1() V2() Element of
[5,0] is V1() set
[[5,0],0] is V1() set

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

{[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) +* (,,[0,0],[0,0,1])) +* (,,[0,1],[1,0,1])) +* (,,[1,1],[1,1,1])) +* (,,[1,0],[2,1,1])) +* (,,[2,1],[2,1,1])) +* (,,[2,0],[3,0,(- 1)])) +* (,,[3,1],[4,0,(- 1)])) +* (,,[4,1],[4,1,(- 1)])) +* (,,[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
bool 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 -defined REAL -valued finite Element of bool
is non empty set
bool 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