:: AMI_WSTD semantic presentation

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

union { ((NIC (b

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

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)