:: AMISTD_3 semantic presentation

REAL is with_zero V122() V123() V124() V128() set

INT is V122() V123() V124() V125() V126() V128() set

bool NAT is non empty V31() set
bool NAT is non empty V31() set
COMPLEX is V122() V128() set
RAT is V122() V123() V124() V125() V128() set
{} is set

2 is epsilon-transitive epsilon-connected ordinal natural non empty V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
1 is epsilon-transitive epsilon-connected ordinal natural non empty V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

is non empty trivial 1 -element Tree-like set
TrivialInfiniteTree is non empty V31() Tree-like set

N is with_zero set
S is V122() V123() V124() V125() V126() V127() Element of bool NAT

E is set
rng M is set
n is set
M . n is set

n is set

n is set

{N} is non empty trivial 1 -element V122() V123() V124() V125() V126() V127() set

is non empty trivial 1 -element Tree-like V122() V123() V124() V125() V126() V127() set

bool is set
D is with_zero set

M is V122() V123() V124() V125() V126() V127() Element of bool NAT
(D,S,M) is Relation-like NAT -valued T-Sequence-like Function-like V112() V113() V114() V115() set

E is set

E is set

dom () is set
N is with_zero set

S is V122() V123() V124() V125() V126() V127() Element of bool NAT
(N,D,S) is Relation-like NAT -valued T-Sequence-like Function-like V112() V113() V114() V115() set

n is set

f0 is set

rng f1 is set
N is with_zero set

the InstructionsF of D is V50() V51() V52() V54() set

S /. n is Element of the InstructionsF of D
NIC ((S /. n),n) is V122() V123() V124() V125() V126() V127() Element of bool NAT
(N,D,(NIC ((S /. n),n))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
(N,D,(NIC ((S /. n),n))) . f0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
dom (N,D,(NIC ((S /. n),n))) is epsilon-transitive epsilon-connected ordinal set

dom (N,D,(NIC ((S /. n),n))) is epsilon-transitive epsilon-connected ordinal set

dom (N,D,(NIC ((S /. n),n))) is epsilon-transitive epsilon-connected ordinal set

bool is non empty V31() set

S /. f0 is Element of the InstructionsF of D
NIC ((S /. f0),f0) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. f0),f0)) is epsilon-transitive epsilon-connected ordinal cardinal set

dom f0 is non empty Tree-like set

succ f1 is Element of bool (dom f0)
bool (dom f0) is set
f0 . f1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
S /. (f0 . f1) is Element of the InstructionsF of D
NIC ((S /. (f0 . f1)),(f0 . f1)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (f0 . f1)),(f0 . f1))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (f1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (f0 . f1)),(f0 . f1))) } is set
(N,D,(NIC ((S /. (f0 . f1)),(f0 . f1)))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
{ (f1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : S1[b1,f0 . f1] } is set

(N,D,(NIC ((S /. (f0 . f1)),(f0 . f1)))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

n . (a,n) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

S /. t is Element of the InstructionsF of D
NIC ((S /. t),t) is V122() V123() V124() V125() V126() V127() Element of bool NAT
(N,D,(NIC ((S /. t),t))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
dom (N,D,(NIC ((S /. t),t))) is epsilon-transitive epsilon-connected ordinal set
(N,D,(NIC ((S /. t),t))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

dom M is non empty Tree-like set

dom E is non empty Tree-like set

(dom M) -level n is Level of dom M
(dom E) -level n is Level of dom E

(dom M) -level (n + 1) is Level of dom M
(dom E) -level (n + 1) is Level of dom E
{ (succ b1) where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E : len b1 = n } is set
{ (succ b1) where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M : len b1 = n } is set
{ } is set
{ } is set
union { (succ b1) where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M : len b1 = n } is set
union { (succ b1) where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E : len b1 = n } is set
a is set
n is set

succ t is Element of bool (dom M)
bool (dom M) is set

Seg (len t) is V31() len t -element V122() V123() V124() V125() V126() V127() Element of bool NAT

bool is non empty V31() set

Seg k is V31() k -element V122() V123() V124() V125() V126() V127() Element of bool NAT

Seg (k + 1) is V31() k + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT

M . (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
len (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

(t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() set
dom t is V122() V123() V124() V125() V126() V127() Element of bool NAT
<*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like set
(t | (Seg k)) ^ <*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

succ t1 is Element of bool (dom M)

S /. (M . t1) is Element of the InstructionsF of D
NIC ((S /. (M . t1)),(M . t1)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (M . t1)),(M . t1))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (M . t1)),(M . t1))) } is set
t1 ^ <*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

S /. (E . t2) is Element of the InstructionsF of D
NIC ((S /. (E . t2)),(E . t2)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (E . t2)),(E . t2))) is epsilon-transitive epsilon-connected ordinal cardinal set
(N,D,(NIC ((S /. (M . t1)),(M . t1)))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
(N,D,(NIC ((S /. (M . t1)),(M . t1)))) . ((t | (Seg (k + 1))) . (len (t | (Seg (k + 1))))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

succ k is Element of bool (dom E)
bool (dom E) is set

S /. (E . k) is Element of the InstructionsF of D
NIC ((S /. (E . k)),(E . k)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (E . k)),(E . k))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (k ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (E . k)),(E . k))) } is set
S /. (M . t) is Element of the InstructionsF of D
NIC ((S /. (M . t)),(M . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (M . t)),(M . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (M . t)),(M . t))) } is set
a is set
n is set

succ t is Element of bool (dom E)

Seg (len t) is V31() len t -element V122() V123() V124() V125() V126() V127() Element of bool NAT

Seg k is V31() k -element V122() V123() V124() V125() V126() V127() Element of bool NAT

Seg (k + 1) is V31() k + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT

M . (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
len (t | (Seg (k + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

(t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() set
dom t is V122() V123() V124() V125() V126() V127() Element of bool NAT
<*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like set
(t | (Seg k)) ^ <*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

succ t1 is Element of bool (dom M)

S /. (M . t1) is Element of the InstructionsF of D
NIC ((S /. (M . t1)),(M . t1)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (M . t1)),(M . t1))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t1 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (M . t1)),(M . t1))) } is set
t1 ^ <*((t | (Seg (k + 1))) . (len (t | (Seg (k + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

S /. (E . t2) is Element of the InstructionsF of D
NIC ((S /. (E . t2)),(E . t2)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (E . t2)),(E . t2))) is epsilon-transitive epsilon-connected ordinal cardinal set
(N,D,(NIC ((S /. (M . t1)),(M . t1)))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
(N,D,(NIC ((S /. (M . t1)),(M . t1)))) . ((t | (Seg (k + 1))) . (len (t | (Seg (k + 1))))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

succ k is Element of bool (dom M)

S /. (M . k) is Element of the InstructionsF of D
NIC ((S /. (M . k)),(M . k)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (M . k)),(M . k))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (k ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (M . k)),(M . k))) } is set
S /. (E . t) is Element of the InstructionsF of D
NIC ((S /. (E . t)),(E . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (E . t)),(E . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (E . t)),(E . t))) } is set
(dom M) -level 0 is Level of dom M
(dom E) -level 0 is Level of dom E

Seg (len n) is V31() len n -element V122() V123() V124() V125() V126() V127() Element of bool NAT

bool is non empty V31() set

Seg f0 is V31() f0 -element V122() V123() V124() V125() V126() V127() Element of bool NAT

f0 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
Seg (f0 + 1) is V31() f0 + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT

M . (n | (Seg (f0 + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (n | (Seg (f0 + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
len (n | (Seg (f0 + 1))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

(n | (Seg (f0 + 1))) . (len (n | (Seg (f0 + 1)))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() set
dom n is V122() V123() V124() V125() V126() V127() Element of bool NAT
<*((n | (Seg (f0 + 1))) . (len (n | (Seg (f0 + 1)))))*> is Relation-like NAT -defined Function-like non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like set
(n | (Seg f0)) ^ <*((n | (Seg (f0 + 1))) . (len (n | (Seg (f0 + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

succ a is Element of bool (dom M)
bool (dom M) is set

S /. (M . a) is Element of the InstructionsF of D
NIC ((S /. (M . a)),(M . a)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (M . a)),(M . a))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (a ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC ((S /. (M . a)),(M . a))) } is set
a ^ <*((n | (Seg (f0 + 1))) . (len (n | (Seg (f0 + 1)))))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like set

S /. (E . n) is Element of the InstructionsF of D
NIC ((S /. (E . n)),(E . n)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((S /. (E . n)),(E . n))) is epsilon-transitive epsilon-connected ordinal cardinal set
(N,D,(NIC ((S /. (M . a)),(M . a)))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
(N,D,(NIC ((S /. (M . a)),(M . a)))) . ((n | (Seg (f0 + 1))) . (len (n | (Seg (f0 + 1))))) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

bool is non empty V31() set
is non empty trivial 1 -element Tree-like V122() V123() V124() V125() V126() V127() set

N is with_zero set

the InstructionsF of S is V50() V51() V52() V54() set
halt S is halting Element of the InstructionsF of S
K193( the InstructionsF of S) is Element of the InstructionsF of S
K174((halt S)) is set

{(halt S)} is non empty trivial 1 -element set

bool [:,{(halt S)}:] is set
(N,S,(Stop S)) is Relation-like NAT -valued Function-like DecoratedTree-like V112() V113() V114() V115() set
dom (Stop S) is non empty trivial 1 -element set
dom (N,S,(Stop S)) is non empty Tree-like set
(Stop S) . 0 is set

(N,S,(Stop S)) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
NIC ((halt S),((N,S,(Stop S)) . n)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((halt S),((N,S,(Stop S)) . n))) is epsilon-transitive epsilon-connected ordinal cardinal set

NIC ((halt S),f0) is V122() V123() V124() V125() V126() V127() Element of bool NAT
{f0} is non empty trivial 1 -element V122() V123() V124() V125() V126() V127() set

(N,S,(Stop S)) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(Stop S) /. ((N,S,(Stop S)) . n) is Element of the InstructionsF of S
(Stop S) . ((N,S,(Stop S)) . n) is set
NIC ((halt S),((N,S,(Stop S)) . n)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n))) is Relation-like set
order_type_of (RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n))))) is Relation-like set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))))),(RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n))))) is Relation-like Function-like set

{f0} is non empty trivial 1 -element V122() V123() V124() V125() V126() V127() set

bool [:,{f0}:] is set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))))),(RelIncl (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))))) . 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
card (NIC ((halt S),((N,S,(Stop S)) . n))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n))) is epsilon-transitive epsilon-connected ordinal cardinal set
succ n is Element of bool (dom (N,S,(Stop S)))
bool (dom (N,S,(Stop S))) is set
{ (n ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n))) } is set

{()} is non empty trivial 1 -element set
f1 is set

f1 is set

(N,S,(Stop S)) . (n ^ <*f1*>) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(N,S,(NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))) is Relation-like NAT -valued T-Sequence-like Function-like one-to-one V112() V113() V114() V115() set
(N,S,(NIC (((Stop S) /. ((N,S,(Stop S)) . n)),((N,S,(Stop S)) . n)))) . 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set

n is set

(N,S,(Stop S)) . f0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT

(dom (N,S,(Stop S))) -level n is Level of dom (N,S,(Stop S))

(dom (N,S,(Stop S))) -level (n + 1) is Level of dom (N,S,(Stop S))

{ } is set
Seg n is V31() n -element V122() V123() V124() V125() V126() V127() Element of bool NAT

bool [:(Seg n),:] is set

{ } is set
Seg (n + 1) is V31() n + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg (n + 1)) --> 0 is Relation-like Seg (n + 1) -defined Seg (n + 1) -defined NAT -valued INT -valued RAT -valued Function-like constant total total V25( Seg (n + 1),) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg (n + 1)),:]
[:(Seg (n + 1)),:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg (n + 1)),:] is set
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom (N,S,(Stop S)) : len b1 = n + 1 } is set
len ((n + 1) |-> 0) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
{((n + 1) |-> 0)} is non empty trivial 1 -element set
a is set

bool is non empty V31() set

succ t is Element of bool (dom (N,S,(Stop S)))
bool (dom (N,S,(Stop S))) is set
(N,S,(Stop S)) . t is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(Stop S) /. ((N,S,(Stop S)) . t) is Element of the InstructionsF of S
NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t))) } is set
NIC ((halt S),((N,S,(Stop S)) . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((halt S),((N,S,(Stop S)) . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
(Stop S) . ((N,S,(Stop S)) . t) is set

{()} is non empty trivial 1 -element set
k is set

k is set

dom n is V122() V123() V124() V125() V126() V127() Element of bool NAT
dom t is V122() V123() V124() V125() V126() V127() Element of bool NAT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom (N,S,(Stop S)) : len b1 = n } is set

{(n |-> 0)} is non empty trivial 1 -element set

a is set

{ } is set
Seg n is V31() n -element V122() V123() V124() V125() V126() V127() Element of bool NAT

bool [:(Seg n),:] is set

{ } is set
Seg (n + 1) is V31() n + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg (n + 1)) --> 0 is Relation-like Seg (n + 1) -defined Seg (n + 1) -defined NAT -valued INT -valued RAT -valued Function-like constant total total V25( Seg (n + 1),) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg (n + 1)),:]
[:(Seg (n + 1)),:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg (n + 1)),:] is set

succ t is Element of bool (dom (N,S,(Stop S)))
(N,S,(Stop S)) . t is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
(Stop S) /. ((N,S,(Stop S)) . t) is Element of the InstructionsF of S
NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (t ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT : b1 in card (NIC (((Stop S) /. ((N,S,(Stop S)) . t)),((N,S,(Stop S)) . t))) } is set
NIC ((halt S),((N,S,(Stop S)) . t)) is V122() V123() V124() V125() V126() V127() Element of bool NAT
card (NIC ((halt S),((N,S,(Stop S)) . t))) is epsilon-transitive epsilon-connected ordinal cardinal set
(Stop S) . ((N,S,(Stop S)) . t) is set

{ } is set

bool [:(),:] is set
(dom (N,S,(Stop S))) -level 0 is Level of dom (N,S,(Stop S))