REAL is non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero set
NAT is ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero Element of bool REAL
bool REAL is set
omega is ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero set
bool omega is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is complex-membered V52() set
RAT is complex-membered ext-real-membered real-membered rational-membered V52() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V52() set
{} is set
the Relation-like non-empty empty-yielding NAT -defined ordinal natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V55() V56() V57() V58() Cardinal-yielding countable V93() V94() Function-yielding V160() V161() set is Relation-like non-empty empty-yielding NAT -defined ordinal natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V55() V56() V57() V58() Cardinal-yielding countable V93() V94() Function-yielding V160() V161() set
2 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
3 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{1} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{1,2} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable set
{0} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
[:NAT,NAT,NAT:] is set
[0,0,0] is V23() V24() Element of [:NAT,NAT,NAT:]
[0,0] is V23() set
{0,0} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable set
{0} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{{0,0},{0}} is finite V30() countable set
[[0,0],0] is V23() set
{[0,0],0} is finite countable set
{[0,0]} is Relation-like non empty trivial Function-like constant finite 1 -element countable V94() set
{{[0,0],0},{[0,0]}} is finite V30() countable set
[1,0,0] is V23() V24() Element of [:NAT,NAT,NAT:]
[1,0] is V23() set
{1,0} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable set
{{1,0},{1}} is finite V30() countable set
[[1,0],0] is V23() set
{[1,0],0} is finite countable set
{[1,0]} is Relation-like non empty trivial Function-like constant finite 1 -element countable V94() set
{{[1,0],0},{[1,0]}} is finite V30() countable set
{[0,0,0],[1,0,0]} is Relation-like non empty finite countable standard-ins V131() V132() V134() Element of bool [:NAT,NAT,NAT:]
bool [:NAT,NAT,NAT:] is set
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued non empty trivial Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V94() set
{0} --> 0 is Relation-like {0} -defined NAT -valued {0} -valued non empty Function-like constant finite total quasi_total Cardinal-yielding countable V94() Element of bool [:{0},{0}:]
[:{0},{0}:] is Relation-like finite countable set
bool [:{0},{0}:] is finite V30() countable set
III is non empty with_zero set
III is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
f is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
f /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len f is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (len f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
f /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len f is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (len f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f ^' f is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
(f ^' f) /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len (f ^' f) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(f ^' f) /. (len (f ^' f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(f ^' f) /. (n + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(f ^' f) /. n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC (((f ^' f) /. n),N) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,((f ^' f) /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
union { ((NIC (b1,((f ^' f) /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
(len (f ^' f)) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(len f) + (len f) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (n + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
1 + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (1 + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(len f) + NN is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(len f) + a is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(len f) + 0 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
((len f) + a) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
a + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(len f) + (a + 1) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(f ^' f) /. ((len f) + (a + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(a + 1) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. ((a + 1) + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. (a + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
III is non empty with_zero set
III is non empty with_zero set
[:NAT,NAT:] is Relation-like non trivial non finite set
bool [:NAT,NAT:] is non trivial non finite set
III is non empty with_zero set
k is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
N is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
S is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
dom N is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
dom S is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . l is set
S . l is set
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
N . l is set
S . l is set
rng N is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
rng S is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is set
N . f is set
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is set
S . NN is set
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
III is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
<*S*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
l is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
l /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len l is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
l /. (len l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
l /. (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l /. f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((l /. f),N) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,(l /. f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
union { ((NIC (b1,(l /. f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
III is non empty with_zero set
k is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
N is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
N . S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . (S + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
l /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len l is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
l /. (len l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l -| (N . (S + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V94() set
(N . (S + 1)) .. l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
rng l is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
len (l -| (N . (S + 1))) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((N . (S + 1)) .. l) - 1 is V16() V17() ext-real set
(len (l -| (N . (S + 1)))) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
dom l is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l /. ((len (l -| (N . (S + 1)))) + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . ((N . (S + 1)) .. l) is set
l . 1 is set
dom N is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
0 + S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
rng N is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
n is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
len n is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
l /. (len n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is set
N . NN is set
dom n is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
n /. (len n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . (len n) is set
l . (len n) is set
rng n is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{(N . (S + 1))} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
(rng n) /\ {(N . (S + 1))} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l /. ((N . (S + 1)) .. l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
<*(l /. (len n)),(l /. ((N . (S + 1)) .. l))*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
n is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
len n is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
dom n is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
n /. (len n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . 2 is set
y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n /. y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . 1 is set
y + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
n /. (y + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(len n) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
l /. ((len n) + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((n /. y),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of k is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,(n /. y))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(n /. y))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
y + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
n /. y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . y is set
l . y is set
l /. y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n /. (y + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . (y + 1) is set
l . (y + 1) is set
l /. (y + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((n /. y),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(n /. y))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(n /. y))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
n /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . 1 is set
SUCC ((N . S),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(N . S))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(N . S))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . y is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
t is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
fj is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
<*t,fj*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
F is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
len F is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
dom F is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
F /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
F . 1 is set
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
F /. n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
F /. (n + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
F . 2 is set
SUCC ((F /. n),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(F /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(F /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
F /. (len F) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l -' S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
(l -' S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
len n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom n is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
NN is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
NN /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len NN is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
NN /. (len NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom NN is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
NN . 1 is set
S + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(S + 1) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . ((S + 1) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l - S is V16() V17() ext-real set
NN . (len NN) is set
S + ((l -' S) + 1) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(S + ((l -' S) + 1)) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . ((S + ((l -' S) + 1)) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S + (l -' S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(S + (l -' S)) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
((S + (l -' S)) + 1) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . (((S + (l -' S)) + 1) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
NN /. (a + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN /. a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((NN /. a),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(NN /. a))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(NN /. a))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
NN . a is set
S + a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(S + a) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . ((S + a) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN . (a + 1) is set
S + (a + 1) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(S + (a + 1)) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . ((S + (a + 1)) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(S + a) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
((S + a) + 1) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . (((S + a) + 1) -' 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((S + a) -' 1) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
N . (((S + a) -' 1) + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
f /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len f is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (len f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is set
N . n is set
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((f /. f),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(f /. f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(f /. f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
III is non empty with_zero set
k is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
N is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
N . (S + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((N . S),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of k is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,(N . S))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(N . S))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((N . l),k) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(N . l))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
union { ((NIC (b1,(N . l))) \ (JUMP b1)) where b1 is Element of the InstructionsF of k : verum } is set
N is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{[1,0,0],[0,0,0]} is Relation-like non empty finite countable standard-ins V131() V132() V134() set
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) AMI-Struct over k
the InstructionsF of (STC k) is Relation-like non empty standard-ins V131() V132() V134() set
the carrier of (STC k) is set
the_Values_of (STC k) is Relation-like non-empty the carrier of (STC k) -defined Function-like total set
the Object-Kind of (STC k) is Relation-like the carrier of (STC k) -defined k -valued Function-like total quasi_total Element of bool [: the carrier of (STC k),k:]
[: the carrier of (STC k),k:] is Relation-like set
bool [: the carrier of (STC k),k:] is set
the ValuesF of (STC k) is Relation-like k -defined Function-like total set
the Object-Kind of (STC k) * the ValuesF of (STC k) is Relation-like the carrier of (STC k) -defined Function-like set
N is V133( the InstructionsF of (STC k)) Element of the InstructionsF of (STC k)
InsCode N is ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (STC k)
InsCodes the InstructionsF of (STC k) is non empty set
K68(N) is set
K68(K68(N)) is set
S is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total set
Exec (N,S) is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total set
product ( the Object-Kind of (STC k) * the ValuesF of (STC k)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k)))) is non empty functional set
the Execution of (STC k) is Relation-like the InstructionsF of (STC k) -defined Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k)))) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):]
[: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):] is Relation-like set
bool [: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):] is set
the Execution of (STC k) . N is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))
( the Execution of (STC k) . N) . S is Relation-like Function-like set
IC (Exec (N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
IC is Element of the carrier of (STC k)
the ZeroF of (STC k) is Element of the carrier of (STC k)
(Exec (N,S)) . (IC ) is set
IC S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . (IC ) is set
succ (IC S) is set
(IC S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
{[0,0,0]} is Relation-like non empty trivial finite 1 -element countable standard-ins V131() V132() V134() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element countable standard-ins set
S . 0 is set
succ (S . 0) is set
0 .--> (succ (S . 0)) is Relation-like NAT -defined {0} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{0} --> (succ (S . 0)) is Relation-like {0} -defined {(succ (S . 0))} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{0},{(succ (S . 0))}:]
{(succ (S . 0))} is non empty trivial finite 1 -element countable set
[:{0},{(succ (S . 0))}:] is Relation-like finite countable set
bool [:{0},{(succ (S . 0))}:] is finite V30() countable set
dom (0 .--> (succ (S . 0))) is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool {0}
bool {0} is finite V30() countable set
product (the_Values_of (STC k)) is non empty functional with_common_domain product-like set
[:(product (the_Values_of (STC k))),(product (the_Values_of (STC k))):] is Relation-like set
bool [:(product (the_Values_of (STC k))),(product (the_Values_of (STC k))):] is set
id (product (the_Values_of (STC k))) is Relation-like product (the_Values_of (STC k)) -defined product (the_Values_of (STC k)) -valued non empty Function-like one-to-one total quasi_total onto bijective V83() V85() V86() V90() Function-yielding V160() Element of bool [:(product (the_Values_of (STC k))),(product (the_Values_of (STC k))):]
[0,0,0] .--> (id (product (the_Values_of (STC k)))) is Relation-like {[0,0,0]} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V94() Function-yielding V160() set
{[0,0,0]} --> (id (product (the_Values_of (STC k)))) is Relation-like non-empty {[0,0,0]} -defined {(id (product (the_Values_of (STC k))))} -valued non empty Function-like constant finite total quasi_total countable V94() Function-yielding V160() Element of bool [:{[0,0,0]},{(id (product (the_Values_of (STC k))))}:]
{(id (product (the_Values_of (STC k))))} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of (STC k))))}:] is Relation-like finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of (STC k))))}:] is finite V30() countable set
f is Relation-like product (the_Values_of (STC k)) -defined product (the_Values_of (STC k)) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [:(product (the_Values_of (STC k))),(product (the_Values_of (STC k))):]
[1,0,0] .--> f is Relation-like {[1,0,0]} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V94() Function-yielding V160() set
{[1,0,0]} --> f is Relation-like non-empty {[1,0,0]} -defined {f} -valued non empty Function-like constant finite total quasi_total countable V94() Function-yielding V160() Element of bool [:{[1,0,0]},{f}:]
{f} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[1,0,0]},{f}:] is Relation-like finite countable set
bool [:{[1,0,0]},{f}:] is finite V30() countable set
([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC k))))) is Relation-like non empty Function-like finite countable V94() Function-yielding V160() set
f is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total set
f . f is Relation-like Function-like set
f . 0 is set
succ (f . 0) is set
0 .--> (succ (f . 0)) is Relation-like NAT -defined {0} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{0} --> (succ (f . 0)) is Relation-like {0} -defined {(succ (f . 0))} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{0},{(succ (f . 0))}:]
{(succ (f . 0))} is non empty trivial finite 1 -element countable set
[:{0},{(succ (f . 0))}:] is Relation-like finite countable set
bool [:{0},{(succ (f . 0))}:] is finite V30() countable set
f +* (0 .--> (succ (f . 0))) is Relation-like non empty Function-like set
n is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total Element of product (the_Values_of (STC k))
f . n is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total Element of product (the_Values_of (STC k))
n . 0 is set
succ (n . 0) is set
0 .--> (succ (n . 0)) is Relation-like NAT -defined {0} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{0} --> (succ (n . 0)) is Relation-like {0} -defined {(succ (n . 0))} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{0},{(succ (n . 0))}:]
{(succ (n . 0))} is non empty trivial finite 1 -element countable set
[:{0},{(succ (n . 0))}:] is Relation-like finite countable set
bool [:{0},{(succ (n . 0))}:] is finite V30() countable set
n +* (0 .--> (succ (n . 0))) is Relation-like non empty Function-like set
dom ([0,0,0] .--> (id (product (the_Values_of (STC k))))) is Relation-like non empty trivial finite 1 -element countable Element of bool {[0,0,0]}
bool {[0,0,0]} is finite V30() countable set
([1,0,0] .--> f) . N is Relation-like Function-like set
S +* (0 .--> (succ (S . 0))) is Relation-like non empty Function-like set
(S +* (0 .--> (succ (S . 0)))) . 0 is set
(0 .--> (succ (S . 0))) . 0 is set
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
k + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
{(k + 1)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
N is non empty with_zero set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(N) AMI-Struct over N
the InstructionsF of (STC N) is Relation-like non empty standard-ins V131() V132() V134() set
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is V133( the InstructionsF of (STC N)) Element of the InstructionsF of (STC N)
InsCode l is ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (STC N)
InsCodes the InstructionsF of (STC N) is non empty set
K68(l) is set
K68(K68(l)) is set
NIC (l,S) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
the carrier of (STC N) is set
the_Values_of (STC N) is Relation-like non-empty the carrier of (STC N) -defined Function-like total set
the Object-Kind of (STC N) is Relation-like the carrier of (STC N) -defined N -valued Function-like total quasi_total Element of bool [: the carrier of (STC N),N:]
[: the carrier of (STC N),N:] is Relation-like set
bool [: the carrier of (STC N),N:] is set
the ValuesF of (STC N) is Relation-like N -defined Function-like total set
the Object-Kind of (STC N) * the ValuesF of (STC N) is Relation-like the carrier of (STC N) -defined Function-like set
product (the_Values_of (STC N)) is non empty functional with_common_domain product-like set
{ (IC (Exec (l,b1))) where b1 is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total Element of product (the_Values_of (STC N)) : IC b1 = S } is set
NAT --> l is Relation-like NAT -defined the InstructionsF of (STC N) -valued T-Sequence-like non empty non trivial Function-like constant non finite total quasi_total Element of bool [:NAT, the InstructionsF of (STC N):]
[:NAT, the InstructionsF of (STC N):] is Relation-like non trivial non finite set
bool [:NAT, the InstructionsF of (STC N):] is non trivial non finite set
{l} is non empty trivial finite 1 -element countable set
[:NAT,{l}:] is Relation-like non trivial non finite set
IC is Element of the carrier of (STC N)
the ZeroF of (STC N) is Element of the carrier of (STC N)
Values (IC ) is non empty set
(the_Values_of (STC N)) . (IC ) is set
the Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total S -started set is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total S -started set
NN is Element of Values (IC )
(IC ) .--> NN is Relation-like {(IC )} -defined Values (IC ) -valued Values (IC ) -valued non empty trivial Function-like one-to-one constant the_Values_of (STC N) -compatible finite 1 -element countable V94() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> NN is Relation-like {(IC )} -defined Values (IC ) -valued {NN} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(IC )},{NN}:]
{NN} is non empty trivial finite 1 -element countable set
[:{(IC )},{NN}:] is Relation-like finite countable set
bool [:{(IC )},{NN}:] is finite V30() countable set
dom ((IC ) .--> NN) is non empty trivial finite 1 -element countable Element of bool {(IC )}
bool {(IC )} is finite V30() countable set
a is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total Element of product (the_Values_of (STC N))
a +* ((IC ) .--> NN) is Relation-like the carrier of (STC N) -defined non empty Function-like the_Values_of (STC N) -compatible set
y is set
succ k is set
fj is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total Element of product (the_Values_of (STC N))
Exec (l,fj) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total set
product ( the Object-Kind of (STC N) * the ValuesF of (STC N)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N)))) is non empty functional set
the Execution of (STC N) is Relation-like the InstructionsF of (STC N) -defined Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N)))) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):]
[: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):] is Relation-like set
bool [: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):] is set
the Execution of (STC N) . l is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))
( the Execution of (STC N) . l) . fj is Relation-like Function-like set
IC (Exec (l,fj)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Exec (l,fj)) . (IC ) is set
IC fj is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
fj . (IC ) is set
t is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total Element of product (the_Values_of (STC N))
IC t is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
t . (IC ) is set
((IC ) .--> NN) . (IC ) is set
Exec (l,t) is Relation-like the carrier of (STC N) -defined Function-like the_Values_of (STC N) -compatible total set
product ( the Object-Kind of (STC N) * the ValuesF of (STC N)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N)))) is non empty functional set
the Execution of (STC N) is Relation-like the InstructionsF of (STC N) -defined Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N)))) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):]
[: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):] is Relation-like set
bool [: the InstructionsF of (STC N),(Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))):] is set
the Execution of (STC N) . l is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (STC N) * the ValuesF of (STC N))),(product ( the Object-Kind of (STC N) * the ValuesF of (STC N))))
( the Execution of (STC N) . l) . t is Relation-like Function-like set
IC (Exec (l,t)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Exec (l,t)) . (IC ) is set
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) AMI-Struct over k
id NAT is Relation-like NAT -defined NAT -valued non empty Function-like one-to-one total quasi_total onto bijective V83() V85() V86() V90() Element of bool [:NAT,NAT:]
N is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC (f,(STC k)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of (STC k) is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,f)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
union { ((NIC (b1,f)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
l + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
{l,(l + 1)} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
N . (l + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((N . l),(STC k)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(N . l))) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
union { ((NIC (b1,(N . l))) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) (k) AMI-Struct over k
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . S is set
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . S is set
n is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . S is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . l is set
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . S is set
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
l . 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
rng l is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
dom l is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
f is set
l . f is set
f is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,S) is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(k,N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . l is set
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . S is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(k,N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(k,N,l)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is non empty with_non-empty_values IC-Ins-separated (k) AMI-Struct over k
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,f,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,f,n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,S) + l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + l)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 0)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
N is non empty with_zero set
S is non empty with_non-empty_values IC-Ins-separated (N) (N) AMI-Struct over N
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l,k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l) + k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,((N,S,l) + k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,f,k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,f) + k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,((N,S,f) + k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
N is non empty with_zero set
S is non empty with_non-empty_values IC-Ins-separated (N) (N) AMI-Struct over N
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(N,S,l) + k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l,k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,((N,S,l) + k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(N,S,l,k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,l) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((k,N,S) + 1) - 1 is V16() V17() ext-real set
((k,N,l) + 1) - 1 is V16() V17() ext-real set
(k,N,l) + 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
N is non empty with_zero set
STC N is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(N) (N) (N) AMI-Struct over N
(N,(STC N),k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
id NAT is Relation-like NAT -defined NAT -valued non empty Function-like one-to-one total quasi_total onto bijective V83() V85() V86() V90() Element of bool [:NAT,NAT:]
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . k is set
l is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC (n,(STC N)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of (STC N) is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,n)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC N) : verum } is set
union { ((NIC (b1,n)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC N) : verum } is set
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
{f,(f + 1)} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
l . (f + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((l . f),(STC N)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(l . f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC N) : verum } is set
union { ((NIC (b1,(l . f))) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC N) : verum } is set
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l . a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) (k) (k) AMI-Struct over k
the InstructionsF of (STC k) is Relation-like non empty standard-ins V131() V132() V134() set
the carrier of (STC k) is set
the_Values_of (STC k) is Relation-like non-empty the carrier of (STC k) -defined Function-like total set
the Object-Kind of (STC k) is Relation-like the carrier of (STC k) -defined k -valued Function-like total quasi_total Element of bool [: the carrier of (STC k),k:]
[: the carrier of (STC k),k:] is Relation-like set
bool [: the carrier of (STC k),k:] is set
the ValuesF of (STC k) is Relation-like k -defined Function-like total set
the Object-Kind of (STC k) * the ValuesF of (STC k) is Relation-like the carrier of (STC k) -defined Function-like set
N is V133( the InstructionsF of (STC k)) Element of the InstructionsF of (STC k)
InsCode N is ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (STC k)
InsCodes the InstructionsF of (STC k) is non empty set
K68(N) is set
K68(K68(N)) is set
S is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total set
Exec (N,S) is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total set
product ( the Object-Kind of (STC k) * the ValuesF of (STC k)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k)))) is non empty functional set
the Execution of (STC k) is Relation-like the InstructionsF of (STC k) -defined Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k)))) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):]
[: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):] is Relation-like set
bool [: the InstructionsF of (STC k),(Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))):] is set
the Execution of (STC k) . N is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (STC k) * the ValuesF of (STC k))),(product ( the Object-Kind of (STC k) * the ValuesF of (STC k))))
( the Execution of (STC k) . N) . S is Relation-like Function-like set
IC (Exec (N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
IC is Element of the carrier of (STC k)
the ZeroF of (STC k) is Element of the carrier of (STC k)
(Exec (N,S)) . (IC ) is set
IC S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . (IC ) is set
(k,(STC k),(IC S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),(IC S),1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),(IC S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),(IC S)) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,(STC k),((k,(STC k),(IC S)) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
succ (IC S) is set
(IC S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,(STC k),(k,(STC k),(IC S))) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) (k) (k) AMI-Struct over k
the InstructionsF of (STC k) is Relation-like non empty standard-ins V131() V132() V134() set
N is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,(STC k),((k,(STC k),N) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{(k,(STC k),N)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
S is V133( the InstructionsF of (STC k)) Element of the InstructionsF of (STC k)
InsCode S is ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (STC k)
InsCodes the InstructionsF of (STC k) is non empty set
K68(S) is set
K68(K68(S)) is set
NIC (S,N) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
the carrier of (STC k) is set
the_Values_of (STC k) is Relation-like non-empty the carrier of (STC k) -defined Function-like total set
the Object-Kind of (STC k) is Relation-like the carrier of (STC k) -defined k -valued Function-like total quasi_total Element of bool [: the carrier of (STC k),k:]
[: the carrier of (STC k),k:] is Relation-like set
bool [: the carrier of (STC k),k:] is set
the ValuesF of (STC k) is Relation-like k -defined Function-like total set
the Object-Kind of (STC k) * the ValuesF of (STC k) is Relation-like the carrier of (STC k) -defined Function-like set
product (the_Values_of (STC k)) is non empty functional with_common_domain product-like set
{ (IC (Exec (S,b1))) where b1 is Relation-like the carrier of (STC k) -defined Function-like the_Values_of (STC k) -compatible total Element of product (the_Values_of (STC k)) : IC b1 = N } is set
f is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,(STC k),f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
STC k is non empty finite with_non-empty_values IC-Ins-separated strict halting V154(k) (k) (k) AMI-Struct over k
N is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC (N,(STC k)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of (STC k) is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,N)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
union { ((NIC (b1,N)) \ (JUMP b1)) where b1 is Element of the InstructionsF of (STC k) : verum } is set
(k,(STC k),N) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,(STC k),N) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,(STC k),((k,(STC k),N) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{N,(k,(STC k),N)} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,(STC k),l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
{l,(l + 1)} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable set
(k,(STC k),(l + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{l,(k,(STC k),(l + 1))} is finite V30() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{(k,N,S)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l is Element of the InstructionsF of N
NIC (l,S) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
the carrier of N is set
the_Values_of N is Relation-like non-empty the carrier of N -defined Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined k -valued Function-like total quasi_total Element of bool [: the carrier of N,k:]
[: the carrier of N,k:] is Relation-like set
bool [: the carrier of N,k:] is set
the ValuesF of N is Relation-like k -defined Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined Function-like set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (l,b1))) where b1 is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b1 = S } is set
IC is Element of the carrier of N
the ZeroF of N is Element of the carrier of N
Values (IC ) is non empty set
(the_Values_of N) . (IC ) is set
the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set is Relation-like NAT -defined the InstructionsF of N -valued Function-like total set
f is set
f is Element of Values (IC )
the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set +* ((IC ),f) is Relation-like the carrier of N -defined Function-like total set
dom the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l) is Relation-like NAT -defined the InstructionsF of N -valued Function-like total set
( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)) /. S is Element of the InstructionsF of N
( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)) . S is Element of the InstructionsF of N
dom the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set is Element of bool the carrier of N
bool the carrier of N is set
n is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
IC n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n . (IC ) is set
Following (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n) is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n) is Element of the InstructionsF of N
( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)) /. (IC n) is Element of the InstructionsF of N
Exec ((CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n)),n) is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V160() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is set
the Execution of N . (CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . (CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n))) . n is Relation-like Function-like set
IC (Following (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Following (( the Relation-like NAT -defined the InstructionsF of N -valued Function-like total set +* (S,l)),n)) . (IC ) is set
f is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
Exec (l,f) is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
the Execution of N . l is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . l) . f is Relation-like Function-like set
IC (Exec (l,f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Exec (l,f)) . (IC ) is set
IC f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . (IC ) is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Element of the InstructionsF of N
the carrier of N is set
the_Values_of N is Relation-like non-empty the carrier of N -defined Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined k -valued Function-like total quasi_total Element of bool [: the carrier of N,k:]
[: the carrier of N,k:] is Relation-like set
bool [: the carrier of N,k:] is set
the ValuesF of N is Relation-like k -defined Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined Function-like set
the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
IC is Element of the carrier of N
the ZeroF of N is Element of the carrier of N
the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set . (IC ) is set
NIC (S,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (S,b1))) where b1 is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b1 = IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set } is set
(k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set ),1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )) + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{(k,N,(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set ))} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{(IC the Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set )} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Element of the InstructionsF of N
S is Element of the InstructionsF of N
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S is Relation-like NAT -defined the InstructionsF of N -valued Function-like finite countable V94() set
dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
the carrier of N is set
the_Values_of N is Relation-like non-empty the carrier of N -defined Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined k -valued Function-like total quasi_total Element of bool [: the carrier of N,k:]
[: the carrier of N,k:] is Relation-like set
bool [: the carrier of N,k:] is set
the ValuesF of N is Relation-like k -defined Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined Function-like set
l is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
IC l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
IC is Element of the carrier of N
the ZeroF of N is Element of the carrier of N
l . (IC ) is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
Comput (S,l,f) is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
IC (Comput (S,l,f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Comput (S,l,f)) . (IC ) is set
l is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
IC l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
IC is Element of the carrier of N
the ZeroF of N is Element of the carrier of N
l . (IC ) is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
Comput (S,l,f) is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
IC (Comput (S,l,f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(Comput (S,l,f)) . (IC ) is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom ((k,N,0) .--> (halt N)) is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
((k,N,0) .--> (halt N)) /. l is Element of the InstructionsF of N
NIC ((((k,N,0) .--> (halt N)) /. l),l) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
the carrier of N is set
the_Values_of N is Relation-like non-empty the carrier of N -defined Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined k -valued Function-like total quasi_total Element of bool [: the carrier of N,k:]
[: the carrier of N,k:] is Relation-like set
bool [: the carrier of N,k:] is set
the ValuesF of N is Relation-like k -defined Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined Function-like set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec ((((k,N,0) .--> (halt N)) /. l),b1))) where b1 is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b1 = l } is set
dom ((k,N,0) .--> (halt N)) is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool {(k,N,0)}
bool {(k,N,0)} is finite V30() countable set
S is Relation-like NAT -defined the InstructionsF of N -valued Function-like finite countable V94() set
dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
S /. l is Element of the InstructionsF of N
S . l is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued Function-like finite countable V94() set
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S is Element of the InstructionsF of N
(k,N,0) .--> S is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> S is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {S} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{S}:]
{S} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{S}:] is Relation-like finite countable set
bool [:{(k,N,0)},{S}:] is finite V30() countable set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom ((k,N,0) .--> S) is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
dom ((k,N,0) .--> S) is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool {(k,N,0)}
bool {(k,N,0)} is finite V30() countable set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
the Element of the InstructionsF of N is Element of the InstructionsF of N
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,0) .--> the Element of the InstructionsF of N is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> the Element of the InstructionsF of N is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued { the Element of the InstructionsF of N} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{ the Element of the InstructionsF of N}:]
{ the Element of the InstructionsF of N} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{ the Element of the InstructionsF of N}:] is Relation-like finite countable set
bool [:{(k,N,0)},{ the Element of the InstructionsF of N}:] is finite V30() countable set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l is set
f is Relation-like NAT -defined NAT -valued non empty Function-like total quasi_total Element of bool [:NAT,NAT:]
f . 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
rng f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
dom f is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V55() countable Element of bool NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is set
f . n is set
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f . NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
N is non empty with_zero set
S is non empty with_non-empty_values IC-Ins-separated (N) (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins V131() V132() V134() set
(N,S,k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V94() (N,S) set
card l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of omega
dom l is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
{ b1 where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : S1[b1] } is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is set
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
NN is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(N,S,NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{ b1 where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : H1(b1) in dom l } is set
f is ordinal cardinal set
card f is ordinal cardinal set
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,a) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
card k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of omega
card (card l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of omega
card (dom l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of omega
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{ (k,N,b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom S } is set
{ H1(b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom S } is set
the ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() Element of dom S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() Element of dom S
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is set
NN is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,NN) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
max n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max n)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
max f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
max n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max n)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{ (k,N,b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom S } is set
l is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
max l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max l)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
l is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom l is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{ (k,N,b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom l } is set
f is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
max f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
{ (k,N,b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom S } is set
f is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
max f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
a is set
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,n) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is non empty finite complex-membered ext-real-membered real-membered V53() V54() V55() V56() V57() countable Element of bool REAL
max n is V16() V17() ext-real set
NN is non empty finite complex-membered ext-real-membered real-membered V53() V54() V55() V56() V57() countable Element of bool REAL
max NN is V16() V17() ext-real set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
{ (k,N,b1) where b1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT : b1 in dom S } is set
f is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
max f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V68() set
(k,N,(max f)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(k,N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() set
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
dom l is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
f is set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
card S is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of omega
(card S) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((card S) -' 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((card S) -' 1) + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
(k,N,(f + 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f + 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
S is Relation-like NAT -defined the InstructionsF of N -valued Function-like finite countable V94() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
dom S is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable Element of bool NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
dom ((k,N,0) .--> (halt N)) is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool {(k,N,0)}
bool {(k,N,0)} is finite V30() countable set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
card (dom ((k,N,0) .--> (halt N))) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of omega
(k,N,((k,N,0) .--> (halt N))) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
card ((k,N,0) .--> (halt N)) is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of omega
(card ((k,N,0) .--> (halt N))) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((card ((k,N,0) .--> (halt N))) -' 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(card (dom ((k,N,0) .--> (halt N)))) -' 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((card (dom ((k,N,0) .--> (halt N)))) -' 1)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((k,N,0) .--> (halt N)) . (k,N,((k,N,0) .--> (halt N))) is set
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((k,N,0) .--> (halt N)) . l is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . (k,N,S) is set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . l is set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . (k,N,S) is set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . l is set
k is non empty with_zero set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated halting (k) (k) AMI-Struct over k
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
(k,N,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
halt N is halting non sequential (k,N) Element of the InstructionsF of N
(k,N,0) .--> (halt N) is Relation-like NAT -defined {(k,N,0)} -defined the InstructionsF of N -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V94() set
{(k,N,0)} is non empty trivial finite V30() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable set
{(k,N,0)} --> (halt N) is Relation-like {(k,N,0)} -defined the InstructionsF of N -valued {(halt N)} -valued non empty Function-like constant finite total quasi_total countable V94() Element of bool [:{(k,N,0)},{(halt N)}:]
{(halt N)} is non empty trivial finite 1 -element countable set
[:{(k,N,0)},{(halt N)}:] is Relation-like finite countable set
bool [:{(k,N,0)},{(halt N)}:] is finite V30() countable set
S is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) set
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . (k,N,S) is set
dom S is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable Element of bool NAT
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
S . l is set
l is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like finite countable V94() (k,N) (k,N) (k,N) set
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC (S,N) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
the InstructionsF of N is Relation-like non empty standard-ins V131() V132() V134() set
{ ((NIC (b1,S)) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
union { ((NIC (b1,S)) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
len f is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V94() FinSequence of NAT
f /. 1 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
len f is ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (len f) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
n + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
f /. (n + 1) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
f /. n is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
SUCC ((f /. n),N) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() countable Element of bool NAT
{ ((NIC (b1,(f /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
union { ((NIC (b1,(f /. n))) \ (JUMP b1)) where b1 is Element of the InstructionsF of N : verum } is set
1 + 1 is ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
l is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
(k,N,S) -' l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) -' l)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is non empty with_zero set
N is non empty with_non-empty_values IC-Ins-separated (k) (k) AMI-Struct over k
S is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S,0) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,S) -' 0 is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,((k,N,S) -' 0)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(k,N,(k,N,S)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
k is ordinal natural V16() V17() finite cardinal ext-real non negative countable set
N is non empty with_zero set
S is non empty with_non-empty_values IC-Ins-separated (N) (N) AMI-Struct over N
l is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l,k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,l) + k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,((N,S,l) + k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(N,S,l,k),k) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(N,S,l,k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(N,S,l,k)) -' k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,((N,S,(N,S,l,k)) -' k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
((N,S,l) + k) -' k is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(((N,S,l) + k) -' k)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT
(N,S,(N,S,l)) is ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() Element of NAT