REAL is with_zero V122() V123() V124() V128() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V31() cardinal limit_cardinal with_zero V122() V123() V124() V125() V126() V127() V128() Element of bool REAL
bool REAL is set
INT is V122() V123() V124() V125() V126() V128() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V31() cardinal limit_cardinal with_zero V122() V123() V124() V125() V126() V127() 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
the Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional empty V31() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() set is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional empty V31() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() 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
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
{{}} is non empty trivial 1 -element Tree-like set
TrivialInfiniteTree is non empty V31() Tree-like set
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() FinSequence of NAT
N is with_zero set
S is V122() V123() V124() V125() V126() V127() Element of bool NAT
RelIncl S is Relation-like set
order_type_of (RelIncl S) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl S)) is Relation-like set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S)) is Relation-like Function-like set
card S is epsilon-transitive epsilon-connected ordinal cardinal set
M is Relation-like T-Sequence-like Function-like set
dom M is epsilon-transitive epsilon-connected ordinal set
E is set
rng M is set
n is set
M . n is set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
E is Relation-like NAT -valued T-Sequence-like Function-like V112() V113() V114() V115() set
dom E is epsilon-transitive epsilon-connected ordinal set
n is set
E . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
M is Relation-like NAT -valued T-Sequence-like Function-like V112() V113() V114() V115() set
dom M is epsilon-transitive epsilon-connected ordinal set
E is Relation-like NAT -valued T-Sequence-like Function-like V112() V113() V114() V115() set
dom E is epsilon-transitive epsilon-connected ordinal set
n is set
M . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
{N} is non empty trivial 1 -element V122() V123() V124() V125() V126() V127() set
0 .--> N is Relation-like NAT -defined {0} -defined RAT -valued Function-like one-to-one V112() V113() V114() V115() set
{0} is non empty trivial 1 -element Tree-like V122() V123() V124() V125() V126() V127() set
{0} --> N is Relation-like {0} -defined INT -valued RAT -valued Function-like constant non empty total V25({0},{N}) DecoratedTree-like V112() V113() V114() V115() Element of bool [:{0},{N}:]
[:{0},{N}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:{0},{N}:] is set
D is with_zero set
S is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over D
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
card M is epsilon-transitive epsilon-connected ordinal cardinal set
E is set
RelIncl {N} is Relation-like set
order_type_of (RelIncl {N}) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl {N})) is Relation-like set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {N}))),(RelIncl {N})) is Relation-like Function-like set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {N}))),(RelIncl {N}))) . 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
(0 .--> N) . 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V111() set
dom (D,S,M) is epsilon-transitive epsilon-connected ordinal set
E is set
(D,S,M) . E is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(0 .--> N) . E is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V111() set
RelIncl M is Relation-like set
order_type_of (RelIncl M) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl M)) is Relation-like set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M)) is Relation-like Function-like set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . E is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
dom (0 .--> N) is set
N is with_zero set
D is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
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
RelIncl S is Relation-like set
order_type_of (RelIncl S) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl S)) is Relation-like set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S)) is Relation-like Function-like set
n is set
dom (N,D,S) is epsilon-transitive epsilon-connected ordinal set
f0 is set
(N,D,S) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(N,D,S) . f0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
card S is epsilon-transitive epsilon-connected ordinal cardinal set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl S))),(RelIncl S))) . f0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
f1 is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom f1 is epsilon-transitive epsilon-connected ordinal set
rng f1 is set
N is with_zero set
D is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
the InstructionsF of D is V50() V51() V52() V54() set
S is Relation-like NAT -defined the InstructionsF of D -valued Function-like non empty V31() set
FirstLoc S 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 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
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
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
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
dom (N,D,(NIC ((S /. n),n))) is epsilon-transitive epsilon-connected ordinal set
a 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,D,(NIC ((S /. n),n))) is epsilon-transitive epsilon-connected ordinal set
[:NAT,NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
[:[:NAT,NAT:],NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
bool [:[:NAT,NAT:],NAT:] is non empty V31() set
n is Relation-like INT -valued Function-like V25([:NAT,NAT:], NAT ) V112() V113() V114() V115() Element of bool [:[:NAT,NAT:],NAT:]
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
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
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
a is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
f0 is Relation-like NAT -valued Function-like DecoratedTree-like V112() V113() V114() V115() set
f0 . {} is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
dom f0 is non empty Tree-like set
f1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom f0
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 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*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
f1 ^ <*n*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
f0 . (f1 ^ <*n*>) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
(N,D,(NIC ((S /. (f0 . f1)),(f0 . f1)))) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
a 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 . (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
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
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
M is Relation-like NAT -valued Function-like DecoratedTree-like V112() V113() V114() V115() set
M . {} is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
dom M is non empty Tree-like set
E is Relation-like NAT -valued Function-like DecoratedTree-like V112() V113() V114() V115() set
E . {} is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
dom E is non empty Tree-like set
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
(dom M) -level n is Level of dom M
(dom E) -level n is Level of dom E
n + 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
(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
{ 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
{ 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 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
t is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M
succ t is Element of bool (dom M)
bool (dom M) is set
len 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
k is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E
len k 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 (len t) is V31() len t -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg (len t)) is Relation-like Seg (len t) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
bool [:NAT,NAT:] is non empty V31() set
k 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 k is V31() k -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
k | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
M . (t | (Seg k)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg k)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
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
Seg (k + 1) is V31() k + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg (k + 1)) is Relation-like Seg (k + 1) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
k | (Seg (k + 1)) is Relation-like Seg (k + 1) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,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 . (k + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
(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
(k | (Seg (k + 1))) | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
(t | (Seg (k + 1))) | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
t1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M
succ t1 is Element of bool (dom M)
M . t1 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 /. (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
k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
t1 ^ <*k*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
t2 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E
E . t2 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 /. (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
Seg 0 is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional empty V31() cardinal 0 -element FinSequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Element of bool NAT
t | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:NAT,NAT:]
k | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:NAT,NAT:]
M . (t | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
M . 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
E . t 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
E . k 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 /. (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
t is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E
succ t is Element of bool (dom E)
len 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
k is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M
len k 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 (len t) is V31() len t -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg (len t)) is Relation-like Seg (len t) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
k 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 k is V31() k -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
k | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
M . (t | (Seg k)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg k)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
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
Seg (k + 1) is V31() k + 1 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
t | (Seg (k + 1)) is Relation-like Seg (k + 1) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
k | (Seg (k + 1)) is Relation-like Seg (k + 1) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,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 . (k + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
(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
(k | (Seg (k + 1))) | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
(t | (Seg (k + 1))) | (Seg k) is Relation-like Seg k -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
t1 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M
succ t1 is Element of bool (dom M)
M . t1 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 /. (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
k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
t1 ^ <*k*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
t2 is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E
E . t2 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 /. (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
t | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:NAT,NAT:]
k | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:NAT,NAT:]
M . (t | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (t | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
M . t is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . 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
succ k is Element of bool (dom M)
M . k 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 /. (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
n is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
M . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
len 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
Seg (len n) is V31() len n -element V122() V123() V124() V125() V126() V127() Element of bool NAT
n | (Seg (len n)) is Relation-like Seg (len n) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
bool [:NAT,NAT:] is non empty V31() set
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
Seg f0 is V31() f0 -element V122() V123() V124() V125() V126() V127() Element of bool NAT
n | (Seg f0) is Relation-like Seg f0 -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
M . (n | (Seg f0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (n | (Seg f0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
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
n | (Seg (f0 + 1)) is Relation-like Seg (f0 + 1) -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,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 . (f0 + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
(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
(n | (Seg (f0 + 1))) | (Seg f0) is Relation-like Seg f0 -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
a is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom M
succ a is Element of bool (dom M)
bool (dom M) is set
M . a 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 /. (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
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
<*t*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
a ^ <*t*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
n is Relation-like NAT -defined INT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of dom E
E . 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 /. (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
Seg 0 is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional empty V31() cardinal 0 -element FinSequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Element of bool NAT
n | (Seg 0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:NAT,NAT:]
M . (n | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
E . (n | (Seg 0)) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
TrivialInfiniteTree --> 0 is Relation-like TrivialInfiniteTree -defined NAT -valued INT -valued RAT -valued Function-like constant non empty total V25( TrivialInfiniteTree , NAT ) DecoratedTree-like V112() V113() V114() V115() Element of bool [:TrivialInfiniteTree,NAT:]
[:TrivialInfiniteTree,NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
bool [:TrivialInfiniteTree,NAT:] is non empty V31() set
{0} is non empty trivial 1 -element Tree-like V122() V123() V124() V125() V126() V127() set
[:TrivialInfiniteTree,{0}:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
N is with_zero set
S is non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N
Stop S is Relation-like NAT -defined the InstructionsF of S -valued Function-like non empty trivial V31() 1 -element V49() non halt-free halt-ending unique-halt really-closed 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
0 .--> (halt S) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> (halt S) is Relation-like {0} -defined Function-like constant non empty total V25({0},{(halt S)}) DecoratedTree-like Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial 1 -element set
[:{0},{(halt S)}:] is Relation-like set
bool [:{0},{(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 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))
(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
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
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 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))
(N,S,(Stop S)) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real 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 epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
0 .--> f0 is Relation-like NAT -defined {0} -defined NAT -valued INT -valued RAT -valued Function-like one-to-one V112() V113() V114() V115() set
{0} --> f0 is Relation-like {0} -defined NAT -valued INT -valued RAT -valued Function-like constant non empty total V25({0},{f0}) DecoratedTree-like V112() V113() V114() V115() Element of bool [:{0},{f0}:]
{f0} is non empty trivial 1 -element V122() V123() V124() V125() V126() V127() set
[:{0},{f0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:{0},{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
<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
n ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
{(n ^ <*0*>)} is non empty trivial 1 -element set
f1 is set
a is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
n ^ <*a*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
f1 is set
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
<*f1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
n ^ <*f1*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
(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,S,(Stop S)) . {} is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
FirstLoc (Stop S) 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,S,(Stop S)) . (<*> NAT) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
n is set
(N,S,(Stop S)) . n is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
f0 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))
(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
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
(dom (N,S,(Stop S))) -level n is Level of dom (N,S,(Stop S))
TrivialInfiniteTree -level n is Level of TrivialInfiniteTree
n + 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
(dom (N,S,(Stop S))) -level (n + 1) is Level of dom (N,S,(Stop S))
TrivialInfiniteTree -level (n + 1) is Level of TrivialInfiniteTree
n |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V31() n -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n } is set
Seg n is V31() n -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined Seg n -defined NAT -valued INT -valued RAT -valued Function-like constant total total V25( Seg n,{0}) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg n),{0}:]
[:(Seg n),{0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg n),{0}:] is set
(n + 1) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V31() n + 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of (n + 1) -tuples_on NAT
(n + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n + 1 } 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),{0}) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg (n + 1)),{0}:]
[:(Seg (n + 1)),{0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg (n + 1)),{0}:] 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
n 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 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
n | (Seg n) is Relation-like Seg n -defined NAT -defined INT -valued RAT -valued Function-like V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like INT -valued RAT -valued non empty V31() V112() V113() V114() V115() set
bool [:NAT,NAT:] is non empty V31() set
t 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))
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
<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
t ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
{(t ^ <*0*>)} is non empty trivial 1 -element set
k is set
k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() V111() V122() V123() V124() V125() V126() V127() Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() V116() V117() V118() V119() FinSequence of NAT
t ^ <*k*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
k is set
n . (n + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
<*(n . (n + 1))*> is Relation-like NAT -defined Function-like non empty trivial V31() 1 -element FinSequence-like FinSubsequence-like set
t ^ <*(n . (n + 1))*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like 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
len 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
{(n |-> 0)} is non empty trivial 1 -element set
k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal ext-real set
n . k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
((n + 1) |-> 0) . k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
t . k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real V110() set
(n |-> 0) . k is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V105() V106() ext-real set
a is set
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
n |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V31() n -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n } is set
Seg n is V31() n -element V122() V123() V124() V125() V126() V127() Element of bool NAT
(Seg n) --> 0 is Relation-like Seg n -defined Seg n -defined NAT -valued INT -valued RAT -valued Function-like constant total total V25( Seg n,{0}) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg n),{0}:]
[:(Seg n),{0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg n),{0}:] is set
n + 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 + 1) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V31() n + 1 -element FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of (n + 1) -tuples_on NAT
(n + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = n + 1 } 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),{0}) V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() Element of bool [:(Seg (n + 1)),{0}:]
[:(Seg (n + 1)),{0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg (n + 1)),{0}:] is set
t 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))
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
t ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V31() FinSequence-like FinSubsequence-like V112() V113() V114() V115() FinSequence of NAT
0 |-> 0 is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 0 } is set
Seg 0 is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural functional empty V31() cardinal 0 -element FinSequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Element of bool NAT
(Seg 0) --> 0 is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -defined NAT -valued INT -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like constant functional empty total total V25( Seg 0,{0}) V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V112() V113() V114() V115() V122() V123() V124() V125() V126() V127() V128() Function-yielding V153() Element of bool [:(Seg 0),{0}:]
[:(Seg 0),{0}:] is Relation-like INT -valued RAT -valued V112() V113() V114() V115() set
bool [:(Seg 0),{0}:] is set
(dom (N,S,(Stop S))) -level 0 is Level of dom (N,S,(Stop S))
TrivialInfiniteTree -level 0 is Level of TrivialInfiniteTree