:: SCMFSA_2 semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite countable denumerable V64() Element of bool REAL
bool REAL is set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite countable denumerable V64() set
bool omega is set
bool NAT is set
9 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
Segm 9 is countable Element of bool omega
SCM-Data-Loc is non empty set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K86(NAT,1) is finite countable V63() Element of bool NAT
[:K86(NAT,1),NAT:] is Relation-like NAT -defined REAL -valued Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is set
SCM-Memory is set
{NAT} is finite countable V63() set
{NAT} \/ SCM-Data-Loc is set
bool SCM-Memory is set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
[:SCM-Memory,2:] is Relation-like set
bool [:SCM-Memory,2:] is set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like V38( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]
SCM-VAL is Relation-like 2 -defined Function-like total set
INT is set
K276(NAT,INT) is set
SCM-OK * SCM-VAL is Relation-like SCM-Memory -defined Function-like set
product (SCM-OK * SCM-VAL) is functional with_common_domain product-like set
SCM-Instr is Relation-like non empty standard-ins V72() V73() V75() set
SCM-Halt is Element of Segm 9
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V24() V25() finite finite-yielding V30() Cardinal-yielding countable integer Function-yielding V94() ext-real non negative set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V24() V25() finite finite-yielding V30() Cardinal-yielding countable integer Function-yielding V94() ext-real non negative set
{} is set
[SCM-Halt,{},{}] is V13() V14() set
[SCM-Halt,{}] is non natural V13() set
{SCM-Halt,{}} is finite countable set
{SCM-Halt} is finite countable set
{{SCM-Halt,{}},{SCM-Halt}} is finite V30() countable set
[[SCM-Halt,{}],{}] is non natural V13() set
{[SCM-Halt,{}],{}} is finite countable set
{[SCM-Halt,{}]} is Relation-like Function-like finite countable set
{{[SCM-Halt,{}],{}},{[SCM-Halt,{}]}} is finite V30() countable set
{[SCM-Halt,{},{}]} is Relation-like non empty finite countable standard-ins V72() V73() V75() set
6 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{ [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b₁ = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b₁ = 6 } is set
7 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
8 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K87(NAT,7,8) is finite countable V63() Element of bool NAT
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K87(NAT,7,8) } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K87(NAT,7,8) } is set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
5 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K90(NAT,1,2,3,4,5) is finite countable V63() Element of bool NAT
{ [b₁,{},K149(SCM-Data-Loc,b₂,b₃)] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in K90(NAT,1,2,3,4,5) } is set
(({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in K87(NAT,7,8) } ) \/ { [b₁,{},K149(SCM-Data-Loc,b₂,b₃)] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in K90(NAT,1,2,3,4,5) } is set
K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is set
[:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is Relation-like set
bool [:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is set
SCM is non empty with_non-empty_values IC-Ins-separated strict strict halting AMI-Struct over 2
In (NAT,SCM-Memory) is Element of SCM-Memory
SCM-Exec is Relation-like SCM-Instr -defined K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) -valued Function-like V38( SCM-Instr ,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))) Element of bool [:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):]
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the InstructionsF of SCM is Relation-like non empty standard-ins V72() V73() V75() set
the carrier of SCM is non empty set
the_Values_of SCM is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V38( the carrier of SCM,2) Element of bool [: the carrier of SCM,2:]
[: the carrier of SCM,2:] is Relation-like set
bool [: the carrier of SCM,2:] is set
the ValuesF of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the ValuesF of SCM is Relation-like the carrier of SCM -defined Function-like set
SCM+FSA-Data*-Loc is non empty set
INT \ NAT is Element of bool INT
bool INT is set
SCM+FSA-Memory is non empty set
SCM-Memory \/ SCM+FSA-Data*-Loc is set
bool SCM+FSA-Memory is set
[:SCM+FSA-Memory,3:] is Relation-like set
bool [:SCM+FSA-Memory,3:] is set
SCM+FSA-OK is Relation-like SCM+FSA-Memory -defined 3 -valued Function-like V38( SCM+FSA-Memory ,3) Element of bool [:SCM+FSA-Memory,3:]
SCM+FSA-Memory --> 2 is Relation-like non-empty SCM+FSA-Memory -defined NAT -valued non empty Function-like constant total V38( SCM+FSA-Memory , NAT ) Element of bool [:SCM+FSA-Memory,NAT:]
[:SCM+FSA-Memory,NAT:] is Relation-like set
bool [:SCM+FSA-Memory,NAT:] is set
{2} is finite countable V63() set
[:SCM+FSA-Memory,{2}:] is Relation-like set
(SCM+FSA-Memory --> 2) +* SCM-OK is Relation-like Function-like set
SCM*-VAL is Relation-like 3 -defined Function-like total set
INT * is FinSequenceSet of INT
K277(NAT,INT,(INT *)) is set
SCM+FSA-OK * SCM*-VAL is Relation-like non-empty SCM+FSA-Memory -defined SCM+FSA-Memory -defined Function-like set
product (SCM+FSA-OK * SCM*-VAL) is non empty functional with_common_domain product-like set
SCM+FSA-Instr is Relation-like non empty standard-ins V72() V73() V75() set
13 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
Segm 13 is countable Element of bool omega
10 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{9,10} is finite countable V63() set
{ [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
11 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
12 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{11,12} is finite countable V63() set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
(SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } ) \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) is set
[:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):] is Relation-like set
bool [:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):] is set
COMPLEX is set
RAT is set
0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(SCM+FSA-OK * SCM*-VAL) . NAT is set
SCM+FSA-Data-Loc is non empty Element of bool SCM+FSA-Memory
SCM+FSA-Data*-Loc is non empty Element of bool SCM+FSA-Memory
SCM+FSA-Exec is Relation-like SCM+FSA-Instr -defined K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) -valued Function-like V38( SCM+FSA-Instr ,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL)))) Element of bool [:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):]
proj1 (SCM+FSA-OK * SCM*-VAL) is set
IC is V49( SCM ) Element of the carrier of SCM
the ZeroF of SCM is Element of the carrier of SCM
halt SCM is halting Element of the InstructionsF of SCM
halt the InstructionsF of SCM is V74( the InstructionsF of SCM) Element of the InstructionsF of SCM
[0,{},{}] is V13() V14() set
[0,{}] is non natural V13() set
{0,{}} is finite countable set
{0} is finite countable set
{{0,{}},{0}} is finite V30() countable set
[[0,{}],{}] is non natural V13() set
SCM-Data-Loc is non empty Element of bool SCM-Memory
{{}} is finite countable set
[:{{}},omega:] is Relation-like set
omega \/ [:{{}},omega:] is set
[{},{}] is non natural V13() set
{{},{}} is finite countable set
{{{},{}},{{}}} is finite V30() countable set
{[{},{}]} is Relation-like Function-like finite countable set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is set
In (NAT,SCM+FSA-Memory) is Element of SCM+FSA-Memory
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3
() is strict AMI-Struct over 3
the carrier of () is set
the_Values_of () is Relation-like the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
<*0*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
[6,<*0*>,{}] is V13() V14() set
[6,<*0*>] is non natural V13() set
{6,<*0*>} is finite countable set
{6} is finite countable V63() set
{{6,<*0*>},{6}} is finite V30() countable set
[[6,<*0*>],{}] is non natural V13() set
{[6,<*0*>],{}} is finite countable set
{[6,<*0*>]} is Relation-like Function-like finite countable set
{{[6,<*0*>],{}},{[6,<*0*>]}} is finite V30() countable set
the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
IC is V49(()) Element of the carrier of ()
the carrier of () is non empty set
the ZeroF of () is Element of the carrier of ()
bool the carrier of () is set
() is Element of bool the carrier of ()
the Element of SCM+FSA-Data-Loc is Element of SCM+FSA-Data-Loc
fa is Element of the carrier of ()
the Element of SCM+FSA-Data*-Loc is Element of SCM+FSA-Data*-Loc
a is Element of the carrier of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
dl. fa is Int-like Element of the carrier of SCM
[1,fa] is non natural V13() set
{1,fa} is finite countable set
{1} is finite countable V63() set
{{1,fa},{1}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
fa + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (fa + 1) is V24() V25() integer ext-real non positive set
- 0 is V24() V25() integer ext-real non positive set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a + 1) is V24() V25() integer ext-real non positive set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
(fa) is ()
fa + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (fa + 1) is V24() V25() integer ext-real non positive set
(a) is ()
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a + 1) is V24() V25() integer ext-real non positive set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of SCM
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
dl. c is Int-like Element of the carrier of SCM
[1,c] is non natural V13() set
{1,c} is finite countable set
{{1,c},{1}} is finite V30() countable set
(c) is Int-like Element of the carrier of ()
fa is ()
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
- a is V24() V25() integer ext-real non positive set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
c + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
[:NAT, the carrier of ():] is Relation-like set
bool [:NAT, the carrier of ():] is set
fa is Relation-like NAT -defined the carrier of () -valued Function-like V38( NAT , the carrier of ()) Element of bool [:NAT, the carrier of ():]
proj1 fa is set
proj2 fa is set
a is set
c is set
fa . a is set
fa . c is set
dom fa is countable Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
fa . s is Element of the carrier of ()
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(a3) is ()
a3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a3 + 1) is V24() V25() integer ext-real non positive set
dom fa is countable Element of bool NAT
rng fa is Element of bool the carrier of ()
a is set
c is set
fa . c is set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
a is set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(c) is ()
c + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (c + 1) is V24() V25() integer ext-real non positive set
fa . c is Element of the carrier of ()
fa is Int-like Element of the carrier of ()
fa is Int-like Element of the carrier of ()
Values fa is non empty set
the_Values_of () is Relation-like non-empty the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
(the_Values_of ()) . fa is set
fa is ()
Values fa is non empty set
the_Values_of () is Relation-like non-empty the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
(the_Values_of ()) . fa is set
the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM+FSA-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub> is Element of SCM+FSA-Data-Loc , b<sub>3</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {11,12} } is set
a is Element of the InstructionsF of SCM
InsCode a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K39( the InstructionsF of SCM) is set
proj1 the InstructionsF of SCM is non empty set
proj1 (proj1 the InstructionsF of SCM) is set
K29(a) is set
K29(K29(a)) is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
fa is Element of the InstructionsF of SCM
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 := t is Element of the InstructionsF of SCM
<*a3,t*> is set
[1,{},<*a3,t*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*a3,t*>] is non natural V13() set
{[1,{}],<*a3,t*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*a3,t*>},{[1,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t := w is Element of the InstructionsF of SCM
<*t,w*> is set
[1,{},<*t,w*>] is V13() V14() set
[[1,{}],<*t,w*>] is non natural V13() set
{[1,{}],<*t,w*>} is finite countable set
{{[1,{}],<*t,w*>},{[1,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
AddTo (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[2,{},<*a3,t*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*a3,t*>] is non natural V13() set
{[2,{}],<*a3,t*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*a3,t*>},{[2,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
AddTo (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[2,{},<*t,w*>] is V13() V14() set
[[2,{}],<*t,w*>] is non natural V13() set
{[2,{}],<*t,w*>} is finite countable set
{{[2,{}],<*t,w*>},{[2,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
SubFrom (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[3,{},<*a3,t*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*a3,t*>] is non natural V13() set
{[3,{}],<*a3,t*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*a3,t*>},{[3,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
SubFrom (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[3,{},<*t,w*>] is V13() V14() set
[[3,{}],<*t,w*>] is non natural V13() set
{[3,{}],<*t,w*>} is finite countable set
{{[3,{}],<*t,w*>},{[3,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
MultBy (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[4,{},<*a3,t*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*a3,t*>] is non natural V13() set
{[4,{}],<*a3,t*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*a3,t*>},{[4,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
MultBy (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[4,{},<*t,w*>] is V13() V14() set
[[4,{}],<*t,w*>] is non natural V13() set
{[4,{}],<*t,w*>} is finite countable set
{{[4,{}],<*t,w*>},{[4,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
Divide (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[5,{},<*a3,t*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*a3,t*>] is non natural V13() set
{[5,{}],<*a3,t*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*a3,t*>},{[5,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
Divide (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[5,{},<*t,w*>] is V13() V14() set
[[5,{}],<*t,w*>] is non natural V13() set
{[5,{}],<*t,w*>} is finite countable set
{{[5,{}],<*t,w*>},{[5,{}]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{6} is finite countable V63() set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
{[6,<*fa*>],{}} is finite countable set
{[6,<*fa*>]} is Relation-like Function-like finite countable set
{{[6,<*fa*>],{}},{[6,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 =0_goto fa is Element of the InstructionsF of SCM
<*a3*> is Relation-like Function-like set
[7,<*fa*>,<*a3*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*a3*>] is non natural V13() set
{[7,<*fa*>],<*a3*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*a3*>},{[7,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t =0_goto fa is Element of the InstructionsF of SCM
<*t*> is Relation-like Function-like set
[7,<*fa*>,<*t*>] is V13() V14() set
[[7,<*fa*>],<*t*>] is non natural V13() set
{[7,<*fa*>],<*t*>} is finite countable set
{{[7,<*fa*>],<*t*>},{[7,<*fa*>]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 >0_goto fa is Element of the InstructionsF of SCM
<*a3*> is Relation-like Function-like set
[8,<*fa*>,<*a3*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*a3*>] is non natural V13() set
{[8,<*fa*>],<*a3*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*a3*>},{[8,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t >0_goto fa is Element of the InstructionsF of SCM
<*t*> is Relation-like Function-like set
[8,<*fa*>,<*t*>] is V13() V14() set
[[8,<*fa*>],<*t*>] is non natural V13() set
{[8,<*fa*>],<*t*>} is finite countable set
{{[8,<*fa*>],<*t*>},{[8,<*fa*>]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
c is ()
a is Int-like Element of the carrier of ()
<*fa,c,a*> is set
[9,{},<*fa,c,a*>] is V13() V14() set
[9,{}] is non natural V13() set
{9,{}} is finite countable set
{9} is finite countable V63() set
{{9,{}},{9}} is finite V30() countable set
[[9,{}],<*fa,c,a*>] is non natural V13() set
{[9,{}],<*fa,c,a*>} is finite countable set
{[9,{}]} is Relation-like Function-like finite countable set
{{[9,{}],<*fa,c,a*>},{[9,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc
s is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[9,{},<*a3,s,t*>] is V13() V14() set
[[9,{}],<*a3,s,t*>] is non natural V13() set
{[9,{}],<*a3,s,t*>} is finite countable set
{{[9,{}],<*a3,s,t*>},{[9,{}]}} is finite V30() countable set
[10,{},<*fa,c,a*>] is V13() V14() set
[10,{}] is non natural V13() set
{10,{}} is finite countable set
{10} is finite countable V63() set
{{10,{}},{10}} is finite V30() countable set
[[10,{}],<*fa,c,a*>] is non natural V13() set
{[10,{}],<*fa,c,a*>} is finite countable set
{[10,{}]} is Relation-like Function-like finite countable set
{{[10,{}],<*fa,c,a*>},{[10,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc
s is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[10,{},<*a3,s,t*>] is V13() V14() set
[[10,{}],<*a3,s,t*>] is non natural V13() set
{[10,{}],<*a3,s,t*>} is finite countable set
{{[10,{}],<*a3,s,t*>},{[10,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is ()
<*fa,a*> is set
[11,{},<*fa,a*>] is V13() V14() set
[11,{}] is non natural V13() set
{11,{}} is finite countable set
{11} is finite countable V63() set
{{11,{}},{11}} is finite V30() countable set
[[11,{}],<*fa,a*>] is non natural V13() set
{[11,{}],<*fa,a*>} is finite countable set
{[11,{}]} is Relation-like Function-like finite countable set
{{[11,{}],<*fa,a*>},{[11,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc
c is Element of SCM+FSA-Data*-Loc
<*s,c*> is set
[11,{},<*s,c*>] is V13() V14() set
[[11,{}],<*s,c*>] is non natural V13() set
{[11,{}],<*s,c*>} is finite countable set
{{[11,{}],<*s,c*>},{[11,{}]}} is finite V30() countable set
[12,{},<*fa,a*>] is V13() V14() set
[12,{}] is non natural V13() set
{12,{}} is finite countable set
{12} is finite countable V63() set
{{12,{}},{12}} is finite V30() countable set
[[12,{}],<*fa,a*>] is non natural V13() set
{[12,{}],<*fa,a*>} is finite countable set
{[12,{}]} is Relation-like Function-like finite countable set
{{[12,{}],<*fa,a*>},{[12,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc
c is Element of SCM+FSA-Data*-Loc
<*s,c*> is set
[12,{},<*s,c*>] is V13() V14() set
[[12,{}],<*s,c*>] is non natural V13() set
{[12,{}],<*s,c*>} is finite countable set
{{[12,{}],<*s,c*>},{[12,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
InsCode (fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa)) is set
K29(K29((fa))) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*c*> is Relation-like Function-like set
[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*c*> is Relation-like Function-like set
[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
fa is ()
(a,c,fa) is Element of the InstructionsF of ()
<*a,fa,c*> is set
[9,{},<*a,fa,c*>] is V13() V14() set
[[9,{}],<*a,fa,c*>] is non natural V13() set
{[9,{}],<*a,fa,c*>} is finite countable set
{{[9,{}],<*a,fa,c*>},{[9,{}]}} is finite V30() countable set
InsCode (a,c,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,c,fa)) is set
K29(K29((a,c,fa))) is set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set
InsCode (c,a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((c,a,fa)) is set
K29(K29((c,a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set
InsCode (a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set
InsCode (a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM-goto c is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[6,<*c*>,{}] is V13() V14() set
[6,<*c*>] is non natural V13() set
{6,<*c*>} is finite countable set
{{6,<*c*>},{6}} is finite V30() countable set
[[6,<*c*>],{}] is non natural V13() set
{[6,<*c*>],{}} is finite countable set
{[6,<*c*>]} is Relation-like Function-like finite countable set
{{[6,<*c*>],{}},{[6,<*c*>]}} is finite V30() countable set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is Element of the InstructionsF of ()
SCM-goto s is Element of the InstructionsF of SCM
<*s*> is Relation-like Function-like set
[6,<*s*>,{}] is V13() V14() set
[6,<*s*>] is non natural V13() set
{6,<*s*>} is finite countable set
{{6,<*s*>},{6}} is finite V30() countable set
[[6,<*s*>],{}] is non natural V13() set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s is Int-like Element of the carrier of SCM
s =0_goto c is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
<*s*> is Relation-like Function-like set
[7,<*c*>,<*s*>] is V13() V14() set
[7,<*c*>] is non natural V13() set
{7,<*c*>} is finite countable set
{7} is finite countable V63() set
{{7,<*c*>},{7}} is finite V30() countable set
[[7,<*c*>],<*s*>] is non natural V13() set
{[7,<*c*>],<*s*>} is finite countable set
{[7,<*c*>]} is Relation-like Function-like finite countable set
{{[7,<*c*>],<*s*>},{[7,<*c*>]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a3 is Int-like Element of the carrier of ()
(t,a3) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s is Int-like Element of the carrier of SCM
s >0_goto c is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
<*s*> is Relation-like Function-like set
[8,<*c*>,<*s*>] is V13() V14() set
[8,<*c*>] is non natural V13() set
{8,<*c*>} is finite countable set
{8} is finite countable V63() set
{{8,<*c*>},{8}} is finite V30() countable set
[[8,<*c*>],<*s*>] is non natural V13() set
{[8,<*c*>],<*s*>} is finite countable set
{[8,<*c*>]} is Relation-like Function-like finite countable set
{{[8,<*c*>],<*s*>},{[8,<*c*>]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a3 is Int-like Element of the carrier of ()
(t,a3) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub> is Element of SCM+FSA-Data-Loc , b<sub>3</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
w is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
t is ()
(t,w,t) is Element of the InstructionsF of ()
<*t,t,w*> is set
[9,{},<*t,t,w*>] is V13() V14() set
[[9,{}],<*t,t,w*>] is non natural V13() set
{[9,{}],<*t,t,w*>} is finite countable set
{{[9,{}],<*t,t,w*>},{[9,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub> is Element of SCM+FSA-Data-Loc , b<sub>3</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
w is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
t is ()
(t,w,t) is Element of the InstructionsF of ()
<*t,t,w*> is set
[10,{},<*t,t,w*>] is V13() V14() set
[[10,{}],<*t,t,w*>] is non natural V13() set
{[10,{}],<*t,t,w*>} is finite countable set
{{[10,{}],<*t,t,w*>},{[10,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM+FSA-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM+FSA-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of ()
a3 is ()
(t,a3) is Element of the InstructionsF of ()
<*t,a3*> is set
[11,{},<*t,a3*>] is V13() V14() set
[[11,{}],<*t,a3*>] is non natural V13() set
{[11,{}],<*t,a3*>} is finite countable set
{{[11,{}],<*t,a3*>},{[11,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM+FSA-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
SCM-Instr \/ { [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>4</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub>, b<sub>3</sub> is Element of SCM+FSA-Data-Loc , b<sub>4</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {9,10} } is set
{ [b<sub>1</sub>,{},<*b<sub>2</sub>,b<sub>3</sub>*>] where b<sub>1</sub> is Element of Segm 13, b<sub>2</sub> is Element of SCM+FSA-Data-Loc , b<sub>3</sub> is Element of SCM+FSA-Data*-Loc : b<sub>1</sub> in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of ()
a3 is ()
(t,a3) is Element of the InstructionsF of ()
<*t,a3*> is set
[12,{},<*t,a3*>] is V13() V14() set
[[12,{}],<*t,a3*>] is non natural V13() set
{[12,{}],<*t,a3*>} is finite countable set
{{[12,{}],<*t,a3*>},{[12,{}]}} is finite V30() countable set
the_Values_of () is Relation-like non-empty the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
dom fa is Element of bool the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
dom a is Element of bool the carrier of ()
fa is ()
a is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
dom a is Element of bool the carrier of SCM
bool the carrier of SCM is set
() is non empty Element of bool the carrier of ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
dom fa is Element of bool the carrier of ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
dom fa is Element of bool the carrier of ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
fa | () is Relation-like () -defined the carrier of () -defined Function-like the_Values_of () -compatible set
dom (fa | ()) is Element of bool ()
bool () is set
dom fa is Element of bool the carrier of ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
fa | () is Relation-like () -defined the carrier of () -defined Function-like the_Values_of () -compatible set
dom (fa | ()) is Element of bool ()
bool () is set
dom fa is Element of bool the carrier of ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
fa | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
c is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
c | SCM-Memory is Relation-like SCM-Memory -defined SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of sproduct (SCM+FSA-OK * SCM*-VAL)
sproduct (SCM+FSA-OK * SCM*-VAL) is non empty functional set
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
fa +* a is Relation-like Function-like set
c is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
s is Relation-like Function-like Element of product (SCM-OK * SCM-VAL)
c +* s is Relation-like Function-like set
fa is Element of the InstructionsF of SCM
a is Element of the InstructionsF of ()
c is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec (fa,c) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . fa is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . fa) . c is set
s is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
s | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
Exec (a,s) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . a is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . a) . s is set
s +* (Exec (fa,c)) is Relation-like Function-like set
t is Element of SCM+FSA-Instr
InsCode t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes SCM+FSA-Instr
InsCodes SCM+FSA-Instr is non empty set
K39(SCM+FSA-Instr) is set
proj1 SCM+FSA-Instr is non empty set
proj1 (proj1 SCM+FSA-Instr) is set
K29(t) is set
K29(K29(t)) is set
a3 is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
a3 | SCM-Memory is Relation-like SCM-Memory -defined SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of sproduct (SCM+FSA-OK * SCM*-VAL)
sproduct (SCM+FSA-OK * SCM*-VAL) is non empty functional set
SCM+FSA-Exec-Res (t,a3) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
t is Element of SCM-Instr
w is Relation-like Function-like Element of product (SCM-OK * SCM-VAL)
SCM-Exec-Res (t,w) is Relation-like Function-like Element of product (SCM-OK * SCM-VAL)
a3 +* (SCM-Exec-Res (t,w)) is Relation-like Function-like set
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a is Int-like Element of the carrier of ()
fa . a is set
s is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
c is Element of SCM-Data-Loc
s . c is V24() V25() integer ext-real set
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a is ()
fa . a is set
s is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
c is Element of SCM+FSA-Data*-Loc
s . c is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
fa is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
a +* fa is Relation-like Function-like set
fa is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
fa . (IC ) is set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a . (IC ) is set
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
c +* fa is Relation-like Function-like set
dom fa is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of SCM
a is Int-like Element of the carrier of ()
c is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
c . fa is V24() V25() integer ext-real set
s is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
s . a is V24() V25() integer ext-real set
a3 is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a3 +* c is Relation-like Function-like set
dom c is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of SCM
a is Int-like Element of the carrier of ()
c is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
c . fa is V24() V25() integer ext-real set
s is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
s | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
s . a is V24() V25() integer ext-real set
s +* c is Relation-like Function-like set
Values (IC ) is non empty set
(the_Values_of ()) . (IC ) is set
fa is Int-like Element of the carrier of ()
[:{1},NAT:] is Relation-like set
fa is ()
[:{0},NAT:] is Relation-like set
NAT \/ [:{0},NAT:] is set
fa is Int-like Element of the carrier of ()
a is ()
Values a is non empty set
(the_Values_of ()) . a is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
[:{1},NAT:] is Relation-like set
c is set
s is set
[c,s] is non natural V13() set
{c,s} is finite countable set
{c} is finite countable set
{{c,s},{c}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
IC fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
fa . (IC ) is set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . (IC ) is set
dom (SCM+FSA-OK * SCM*-VAL) is Element of bool SCM+FSA-Memory
c is Relation-like Function-like set
proj1 c is set
s is Relation-like Function-like set
proj1 s is set
a3 is set
{(IC )} is finite countable set
{(IC )} \/ SCM-Data-Loc is set
({(IC )} \/ SCM-Data-Loc) \/ SCM+FSA-Data*-Loc is set
c . a3 is set
s . a3 is set
c . a3 is set
s . a3 is set
c . a3 is set
s . a3 is set
fa is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
IC fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
fa . (IC ) is set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
a | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . (IC ) is set
a +* fa is Relation-like Function-like set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,a),c)) . fa is V24() V25() integer ext-real set
c . a is V24() V25() integer ext-real set
s is Int-like Element of the carrier of SCM
a3 is Int-like Element of the carrier of SCM
s := a3 is Element of the InstructionsF of SCM
<*s,a3*> is set
[1,{},<*s,a3*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*s,a3*>] is non natural V13() set
{[1,{}],<*s,a3*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*s,a3*>},{[1,{}]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
t is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((s := a3),t) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (s := a3) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (s := a3)) . t is set
c +* (Exec ((s := a3),t)) is Relation-like Function-like set
(Exec ((s := a3),t)) . (IC ) is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((s := a3),t)) . s is V24() V25() integer ext-real set
t . a3 is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
w is Int-like Element of the carrier of SCM
(Exec ((s := a3),t)) . w is V24() V25() integer ext-real set
t . w is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((s := a3),t)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,a),c)) . fa is V24() V25() integer ext-real set
c . fa is V24() V25() integer ext-real set
c . a is V24() V25() integer ext-real set
(c . fa) + (c . a) is V24() V25() integer ext-real set
s is Int-like Element of the carrier of SCM
a3 is Int-like Element of the carrier of SCM
AddTo (s,a3) is Element of the InstructionsF of SCM
<*s,a3*> is set
[2,{},<*s,a3*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*s,a3*>] is non natural V13() set
{[2,{}],<*s,a3*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*s,a3*>},{[2,{}]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
t is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((AddTo (s,a3)),t) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (AddTo (s,a3)) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (AddTo (s,a3))) . t is set
c +* (Exec ((AddTo (s,a3)),t)) is Relation-like Function-like set
(Exec ((AddTo (s,a3)),t)) . (IC ) is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((AddTo (s,a3)),t)) . s is V24() V25() integer ext-real set
t . s is V24() V25() integer ext-real set
t . a3 is V24() V25() integer ext-real set
(t . s) + (t . a3) is V24() V25() integer ext-real set
(t . s) + (c . a) is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
w is Int-like Element of the carrier of SCM
(Exec ((AddTo (s,a3)),t)) . w is V24() V25() integer ext-real set
t . w is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((AddTo (s,a3)),t)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,a),c)) . fa is V24() V25() integer ext-real set
c . fa is V24() V25() integer ext-real set
c . a is V24() V25() integer ext-real set
(c . fa) - (c . a) is V24() V25() integer ext-real set
s is Int-like Element of the carrier of SCM
a3 is Int-like Element of the carrier of SCM
SubFrom (s,a3) is Element of the InstructionsF of SCM
<*s,a3*> is set
[3,{},<*s,a3*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*s,a3*>] is non natural V13() set
{[3,{}],<*s,a3*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*s,a3*>},{[3,{}]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
t is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((SubFrom (s,a3)),t) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (SubFrom (s,a3)) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (SubFrom (s,a3))) . t is set
c +* (Exec ((SubFrom (s,a3)),t)) is Relation-like Function-like set
(Exec ((SubFrom (s,a3)),t)) . (IC ) is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((SubFrom (s,a3)),t)) . s is V24() V25() integer ext-real set
t . s is V24() V25() integer ext-real set
t . a3 is V24() V25() integer ext-real set
(t . s) - (t . a3) is V24() V25() integer ext-real set
(t . s) - (c . a) is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
w is Int-like Element of the carrier of SCM
(Exec ((SubFrom (s,a3)),t)) . w is V24() V25() integer ext-real set
t . w is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((SubFrom (s,a3)),t)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,a),c)) . fa is V24() V25() integer ext-real set
c . fa is V24() V25() integer ext-real set
c . a is V24() V25() integer ext-real set
(c . fa) * (c . a) is V24() V25() integer ext-real set
s is Int-like Element of the carrier of SCM
a3 is Int-like Element of the carrier of SCM
MultBy (s,a3) is Element of the InstructionsF of SCM
<*s,a3*> is set
[4,{},<*s,a3*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*s,a3*>] is non natural V13() set
{[4,{}],<*s,a3*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*s,a3*>},{[4,{}]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
t is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((MultBy (s,a3)),t) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (MultBy (s,a3)) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (MultBy (s,a3))) . t is set
c +* (Exec ((MultBy (s,a3)),t)) is Relation-like Function-like set
(Exec ((MultBy (s,a3)),t)) . (IC ) is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((MultBy (s,a3)),t)) . s is V24() V25() integer ext-real set
t . s is V24() V25() integer ext-real set
t . a3 is V24() V25() integer ext-real set
(t . s) * (t . a3) is V24() V25() integer ext-real set
(t . s) * (c . a) is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
w is Int-like Element of the carrier of SCM
(Exec ((MultBy (s,a3)),t)) . w is V24() V25() integer ext-real set
t . w is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((MultBy (s,a3)),t)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,a),c)) . fa is V24() V25() integer ext-real set
c . fa is V24() V25() integer ext-real set
c . a is V24() V25() integer ext-real set
(c . fa) div (c . a) is V24() V25() integer ext-real set
(Exec ((fa,a),c)) . a is V24() V25() integer ext-real set
(c . fa) mod (c . a) is V24() V25() integer ext-real set
s is Int-like Element of the carrier of SCM
a3 is Int-like Element of the carrier of SCM
Divide (s,a3) is Element of the InstructionsF of SCM
<*s,a3*> is set
[5,{},<*s,a3*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*s,a3*>] is non natural V13() set
{[5,{}],<*s,a3*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*s,a3*>},{[5,{}]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
t is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((Divide (s,a3)),t) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (Divide (s,a3)) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (Divide (s,a3))) . t is set
c +* (Exec ((Divide (s,a3)),t)) is Relation-like Function-like set
(Exec ((Divide (s,a3)),t)) . (IC ) is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((Divide (s,a3)),t)) . s is V24() V25() integer ext-real set
t . s is V24() V25() integer ext-real set
t . a3 is V24() V25() integer ext-real set
(t . s) div (t . a3) is V24() V25() integer ext-real set
(t . s) div (c . a) is V24() V25() integer ext-real set
(Exec ((Divide (s,a3)),t)) . a3 is V24() V25() integer ext-real set
(t . s) mod (t . a3) is V24() V25() integer ext-real set
(t . s) mod (c . a) is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
w is Int-like Element of the carrier of SCM
(Exec ((Divide (s,a3)),t)) . w is V24() V25() integer ext-real set
t . w is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((Divide (s,a3)),t)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is Int-like Element of the carrier of ()
(fa,fa) is Element of the InstructionsF of ()
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa,fa),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,fa)) . a is set
(Exec ((fa,fa),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . (IC ) is set
succ (IC a) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC a) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((fa,fa),a)) . fa is V24() V25() integer ext-real set
a . fa is V24() V25() integer ext-real set
(a . fa) mod (a . fa) is V24() V25() integer ext-real set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
a | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
Divide (c,c) is Element of the InstructionsF of SCM
<*c,c*> is set
[5,{},<*c,c*>] is V13() V14() set
[[5,{}],<*c,c*>] is non natural V13() set
{[5,{}],<*c,c*>} is finite countable set
{{[5,{}],<*c,c*>},{[5,{}]}} is finite V30() countable set
a3 is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((Divide (c,c)),a3) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (Divide (c,c)) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (Divide (c,c))) . a3 is set
a +* (Exec ((Divide (c,c)),a3)) is Relation-like Function-like set
(Exec ((Divide (c,c)),a3)) . (IC ) is set
IC a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a3 . (IC ) is set
succ (IC a3) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC a3) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((Divide (c,c)),a3)) . c is V24() V25() integer ext-real set
a3 . c is V24() V25() integer ext-real set
(a3 . c) mod (a3 . c) is V24() V25() integer ext-real set
(a3 . c) mod (a . fa) is V24() V25() integer ext-real set
t is Int-like Element of the carrier of ()
(Exec ((fa,fa),a)) . t is V24() V25() integer ext-real set
t is Int-like Element of the carrier of SCM
(Exec ((Divide (c,c)),a3)) . t is V24() V25() integer ext-real set
a3 . t is V24() V25() integer ext-real set
a . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,fa),a)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(a,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((Divide (c,c)),a3)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((fa),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa)) . a is set
(Exec ((fa),a)) . (IC ) is set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM-goto c is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[6,<*c*>,{}] is V13() V14() set
[6,<*c*>] is non natural V13() set
{6,<*c*>} is finite countable set
{{6,<*c*>},{6}} is finite V30() countable set
[[6,<*c*>],{}] is non natural V13() set
{[6,<*c*>],{}} is finite countable set
{[6,<*c*>]} is Relation-like Function-like finite countable set
{{[6,<*c*>],{}},{[6,<*c*>]}} is finite V30() countable set
a | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
s is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((SCM-goto c),s) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (SCM-goto c) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (SCM-goto c)) . s is set
a +* (Exec ((SCM-goto c),s)) is Relation-like Function-like set
(Exec ((SCM-goto c),s)) . (IC ) is set
a3 is Int-like Element of the carrier of ()
(Exec ((fa),a)) . a3 is V24() V25() integer ext-real set
t is Int-like Element of the carrier of SCM
(Exec ((SCM-goto c),s)) . t is V24() V25() integer ext-real set
s . t is V24() V25() integer ext-real set
a . a3 is V24() V25() integer ext-real set
a3 is ()
((Exec ((fa),a)),a3) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(a,a3) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((SCM-goto c),s)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
c . a is V24() V25() integer ext-real set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s is Int-like Element of the carrier of SCM
s =0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*s*> is Relation-like Function-like set
[7,<*fa*>,<*s*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*s*>] is non natural V13() set
{[7,<*fa*>],<*s*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*s*>},{[7,<*fa*>]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
a3 is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((s =0_goto fa),a3) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (s =0_goto fa) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (s =0_goto fa)) . a3 is set
c +* (Exec ((s =0_goto fa),a3)) is Relation-like Function-like set
a3 . s is V24() V25() integer ext-real set
(Exec ((s =0_goto fa),a3)) . (IC ) is set
IC a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a3 . (IC ) is set
succ (IC a3) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC a3) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
t is Int-like Element of the carrier of SCM
(Exec ((s =0_goto fa),a3)) . t is V24() V25() integer ext-real set
a3 . t is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((s =0_goto fa),a3)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
c . a is V24() V25() integer ext-real set
Exec ((fa,a),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . c is set
(Exec ((fa,a),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s is Int-like Element of the carrier of SCM
s >0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*s*> is Relation-like Function-like set
[8,<*fa*>,<*s*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*s*>] is non natural V13() set
{[8,<*fa*>],<*s*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*s*>},{[8,<*fa*>]}} is finite V30() countable set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
a3 is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec ((s >0_goto fa),a3) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . (s >0_goto fa) is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . (s >0_goto fa)) . a3 is set
c +* (Exec ((s >0_goto fa),a3)) is Relation-like Function-like set
a3 . s is V24() V25() integer ext-real set
(Exec ((s >0_goto fa),a3)) . (IC ) is set
IC a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a3 . (IC ) is set
succ (IC a3) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC a3) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
t is Int-like Element of the carrier of ()
(Exec ((fa,a),c)) . t is V24() V25() integer ext-real set
t is Int-like Element of the carrier of SCM
(Exec ((s >0_goto fa),a3)) . t is V24() V25() integer ext-real set
a3 . t is V24() V25() integer ext-real set
c . t is V24() V25() integer ext-real set
t is ()
((Exec ((fa,a),c)),t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,t) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
dom (Exec ((s >0_goto fa),a3)) is Element of bool the carrier of SCM
bool the carrier of SCM is set
fa is ()
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
(a,c,fa) is Element of the InstructionsF of ()
<*a,fa,c*> is set
[9,{},<*a,fa,c*>] is V13() V14() set
[[9,{}],<*a,fa,c*>] is non natural V13() set
{[9,{}],<*a,fa,c*>} is finite countable set
{{[9,{}],<*a,fa,c*>},{[9,{}]}} is finite V30() countable set
s is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((a,c,fa),s) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,c,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,c,fa)) . s is set
(Exec ((a,c,fa),s)) . (IC ) is set
IC s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s . (IC ) is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC s) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s . c is V24() V25() integer ext-real set
abs (s . c) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((a,c,fa),s)) . a is V24() V25() integer ext-real set
(s,fa) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
w is Element of SCM+FSA-Instr
InsCode w is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes SCM+FSA-Instr
InsCodes SCM+FSA-Instr is non empty set
K39(SCM+FSA-Instr) is set
proj1 SCM+FSA-Instr is non empty set
proj1 (proj1 SCM+FSA-Instr) is set
K29(w) is set
K29(K29(w)) is set
e is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
w int_addr2 is Element of SCM-Data-Loc
e . (w int_addr2) is V24() V25() integer ext-real set
abs (e . (w int_addr2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
w coll_addr1 is Element of SCM+FSA-Data*-Loc
e . (w coll_addr1) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
SCM+FSA-Exec-Res (w,e) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
w int_addr1 is Element of SCM-Data-Loc
IC e is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
e . NAT is set
succ (IC e) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC e) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
S1 is V24() V25() integer ext-real set
(e . (w coll_addr1)) /. f is V24() V25() integer ext-real Element of INT
SCM+FSA-Chg (e,(w int_addr1),S1) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
(w int_addr1) .--> S1 is Relation-like SCM-Data-Loc -defined {(w int_addr1)} -defined Function-like one-to-one finite countable set
{(w int_addr1)} is finite countable set
{(w int_addr1)} --> S1 is Relation-like {(w int_addr1)} -defined {S1} -valued Function-like constant finite total V38({(w int_addr1)},{S1}) countable Element of bool [:{(w int_addr1)},{S1}:]
{S1} is finite countable set
[:{(w int_addr1)},{S1}:] is Relation-like finite countable set
bool [:{(w int_addr1)},{S1}:] is finite V30() countable set
e +* ((w int_addr1) .--> S1) is Relation-like Function-like set
SCM+FSA-Chg ((SCM+FSA-Chg (e,(w int_addr1),S1)),(succ (IC e))) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> (succ (IC e)) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ (IC e)) is Relation-like non-empty {NAT} -defined omega -valued {(succ (IC e))} -valued Function-like constant finite total V38({NAT},{(succ (IC e))}) countable Element of bool [:{NAT},{(succ (IC e))}:]
{(succ (IC e))} is finite countable V63() set
[:{NAT},{(succ (IC e))}:] is Relation-like finite countable set
bool [:{NAT},{(succ (IC e))}:] is finite V30() countable set
(SCM+FSA-Chg (e,(w int_addr1),S1)) +* (NAT .--> (succ (IC e))) is Relation-like Function-like set
k is Element of Segm 13
t is Element of SCM-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*t,a3,t*> is set
[k,{},<*t,a3,t*>] is V13() V14() set
[k,{}] is non natural V13() set
{k,{}} is finite countable set
{k} is finite countable set
{{k,{}},{k}} is finite V30() countable set
[[k,{}],<*t,a3,t*>] is non natural V13() set
{[k,{}],<*t,a3,t*>} is finite countable set
{[k,{}]} is Relation-like Function-like finite countable set
{{[k,{}],<*t,a3,t*>},{[k,{}]}} is finite V30() countable set
w `3_3 is Relation-like Function-like FinSequence-like set
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(SCM+FSA-Chg (e,(w int_addr1),S1)) . t is V24() V25() integer ext-real set
(s,fa) /. f is V24() V25() integer ext-real Element of INT
f is Int-like Element of the carrier of ()
(Exec ((a,c,fa),s)) . f is V24() V25() integer ext-real set
q is Element of SCM-Data-Loc
(SCM+FSA-Chg (e,(w int_addr1),S1)) . q is V24() V25() integer ext-real set
s . f is V24() V25() integer ext-real set
f is ()
((Exec ((a,c,fa),s)),f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(s,f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
q is Element of SCM+FSA-Data*-Loc
(SCM+FSA-Chg (e,(w int_addr1),S1)) . q is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
fa is ()
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
(c,a,fa) is Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set
s is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((c,a,fa),s) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (c,a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (c,a,fa)) . s is set
(Exec ((c,a,fa),s)) . (IC ) is set
IC s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s . (IC ) is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC s) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s . a is V24() V25() integer ext-real set
abs (s . a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
((Exec ((c,a,fa),s)),fa) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(s,fa) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
s . c is V24() V25() integer ext-real set
w is Element of SCM+FSA-Instr
InsCode w is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes SCM+FSA-Instr
InsCodes SCM+FSA-Instr is non empty set
K39(SCM+FSA-Instr) is set
proj1 SCM+FSA-Instr is non empty set
proj1 (proj1 SCM+FSA-Instr) is set
K29(w) is set
K29(K29(w)) is set
e is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
w int_addr2 is Element of SCM-Data-Loc
e . (w int_addr2) is V24() V25() integer ext-real set
abs (e . (w int_addr2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
w coll_addr1 is Element of SCM+FSA-Data*-Loc
e . (w coll_addr1) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
w int_addr1 is Element of SCM-Data-Loc
e . (w int_addr1) is V24() V25() integer ext-real set
SCM+FSA-Exec-Res (w,e) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
IC e is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
e . NAT is set
succ (IC e) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC e) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
S1 is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(e . (w coll_addr1)) +* (f,(e . (w int_addr1))) is Relation-like Function-like set
SCM+FSA-Chg (e,(w coll_addr1),S1) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
(w coll_addr1) .--> S1 is Relation-like SCM+FSA-Data*-Loc -defined {(w coll_addr1)} -defined Function-like one-to-one finite countable Function-yielding V94() set
{(w coll_addr1)} is finite countable set
{(w coll_addr1)} --> S1 is Relation-like {(w coll_addr1)} -defined {S1} -valued Function-like constant finite total V38({(w coll_addr1)},{S1}) countable Function-yielding V94() Element of bool [:{(w coll_addr1)},{S1}:]
{S1} is functional finite with_common_domain countable set
[:{(w coll_addr1)},{S1}:] is Relation-like finite countable set
bool [:{(w coll_addr1)},{S1}:] is finite V30() countable set
e +* ((w coll_addr1) .--> S1) is Relation-like Function-like set
SCM+FSA-Chg ((SCM+FSA-Chg (e,(w coll_addr1),S1)),(succ (IC e))) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> (succ (IC e)) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ (IC e)) is Relation-like non-empty {NAT} -defined omega -valued {(succ (IC e))} -valued Function-like constant finite total V38({NAT},{(succ (IC e))}) countable Element of bool [:{NAT},{(succ (IC e))}:]
{(succ (IC e))} is finite countable V63() set
[:{NAT},{(succ (IC e))}:] is Relation-like finite countable set
bool [:{NAT},{(succ (IC e))}:] is finite V30() countable set
(SCM+FSA-Chg (e,(w coll_addr1),S1)) +* (NAT .--> (succ (IC e))) is Relation-like Function-like set
k is Element of Segm 13
t is Element of SCM-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*t,a3,t*> is set
[k,{},<*t,a3,t*>] is V13() V14() set
[k,{}] is non natural V13() set
{k,{}} is finite countable set
{k} is finite countable set
{{k,{}},{k}} is finite V30() countable set
[[k,{}],<*t,a3,t*>] is non natural V13() set
{[k,{}],<*t,a3,t*>} is finite countable set
{[k,{}]} is Relation-like Function-like finite countable set
{{[k,{}],<*t,a3,t*>},{[k,{}]}} is finite V30() countable set
w `3_3 is Relation-like Function-like FinSequence-like set
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(SCM+FSA-Chg (e,(w coll_addr1),S1)) . a3 is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(s,fa) +* (f,(s . c)) is Relation-like Function-like set
f is Int-like Element of the carrier of ()
(Exec ((c,a,fa),s)) . f is V24() V25() integer ext-real set
q is Element of SCM-Data-Loc
(SCM+FSA-Chg (e,(w coll_addr1),S1)) . q is V24() V25() integer ext-real set
s . f is V24() V25() integer ext-real set
f is ()
((Exec ((c,a,fa),s)),f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(s,f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
q is Element of SCM+FSA-Data*-Loc
(SCM+FSA-Chg (e,(w coll_addr1),S1)) . q is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
fa is ()
a is Int-like Element of the carrier of ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((a,fa),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . c is set
(Exec ((a,fa),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(Exec ((a,fa),c)) . a is V24() V25() integer ext-real set
(c,fa) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
len (c,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
t is Element of SCM+FSA-Instr
t int_addr3 is Element of SCM-Data-Loc
t coll_addr2 is Element of SCM+FSA-Data*-Loc
s . (t coll_addr2) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
len (s . (t coll_addr2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2)))) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
(t int_addr3) .--> (len (s . (t coll_addr2))) is Relation-like SCM-Data-Loc -defined {(t int_addr3)} -defined NAT -valued Function-like one-to-one finite countable set
{(t int_addr3)} is finite countable set
{(t int_addr3)} --> (len (s . (t coll_addr2))) is Relation-like {(t int_addr3)} -defined NAT -valued {(len (s . (t coll_addr2)))} -valued Function-like constant finite total V38({(t int_addr3)},{(len (s . (t coll_addr2)))}) countable Element of bool [:{(t int_addr3)},{(len (s . (t coll_addr2)))}:]
{(len (s . (t coll_addr2)))} is finite countable set
[:{(t int_addr3)},{(len (s . (t coll_addr2)))}:] is Relation-like finite countable set
bool [:{(t int_addr3)},{(len (s . (t coll_addr2)))}:] is finite V30() countable set
s +* ((t int_addr3) .--> (len (s . (t coll_addr2)))) is Relation-like Function-like set
InsCode t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes SCM+FSA-Instr
InsCodes SCM+FSA-Instr is non empty set
K39(SCM+FSA-Instr) is set
proj1 SCM+FSA-Instr is non empty set
proj1 (proj1 SCM+FSA-Instr) is set
K29(t) is set
K29(K29(t)) is set
SCM+FSA-Exec-Res (t,s) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
IC s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s . NAT is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC s) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
SCM+FSA-Chg ((SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2))))),(succ (IC s))) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> (succ (IC s)) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ (IC s)) is Relation-like non-empty {NAT} -defined omega -valued {(succ (IC s))} -valued Function-like constant finite total V38({NAT},{(succ (IC s))}) countable Element of bool [:{NAT},{(succ (IC s))}:]
{(succ (IC s))} is finite countable V63() set
[:{NAT},{(succ (IC s))}:] is Relation-like finite countable set
bool [:{NAT},{(succ (IC s))}:] is finite V30() countable set
(SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2))))) +* (NAT .--> (succ (IC s))) is Relation-like Function-like set
w is Element of Segm 13
e is Element of SCM-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
<*e,a3*> is set
[w,{},<*e,a3*>] is V13() V14() set
[w,{}] is non natural V13() set
{w,{}} is finite countable set
{w} is finite countable set
{{w,{}},{w}} is finite V30() countable set
[[w,{}],<*e,a3*>] is non natural V13() set
{[w,{}],<*e,a3*>} is finite countable set
{[w,{}]} is Relation-like Function-like finite countable set
{{[w,{}],<*e,a3*>},{[w,{}]}} is finite V30() countable set
t `3_3 is Relation-like Function-like FinSequence-like set
(SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2))))) . e is V24() V25() integer ext-real set
k is Int-like Element of the carrier of ()
(Exec ((a,fa),c)) . k is V24() V25() integer ext-real set
S1 is Element of SCM-Data-Loc
(SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2))))) . S1 is V24() V25() integer ext-real set
c . k is V24() V25() integer ext-real set
k is ()
((Exec ((a,fa),c)),k) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,k) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
S1 is Element of SCM+FSA-Data*-Loc
(SCM+FSA-Chg (s,(t int_addr3),(len (s . (t coll_addr2))))) . S1 is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
fa is ()
a is Int-like Element of the carrier of ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec ((a,fa),c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . c is set
(Exec ((a,fa),c)) . (IC ) is set
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . (IC ) is set
succ (IC c) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC c) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
c . a is V24() V25() integer ext-real set
abs (c . a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
((Exec ((a,fa),c)),fa) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
t is Element of SCM+FSA-Instr
InsCode t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes SCM+FSA-Instr
InsCodes SCM+FSA-Instr is non empty set
K39(SCM+FSA-Instr) is set
proj1 SCM+FSA-Instr is non empty set
proj1 (proj1 SCM+FSA-Instr) is set
K29(t) is set
K29(K29(t)) is set
t is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
t int_addr3 is Element of SCM-Data-Loc
t . (t int_addr3) is V24() V25() integer ext-real set
abs (t . (t int_addr3)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM+FSA-Exec-Res (t,t) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
t coll_addr2 is Element of SCM+FSA-Data*-Loc
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . NAT is set
succ (IC t) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC t) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
e is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
k |-> 0 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Element of k -tuples_on NAT
k -tuples_on NAT is FinSequenceSet of NAT
SCM+FSA-Chg (t,(t coll_addr2),e) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
(t coll_addr2) .--> e is Relation-like SCM+FSA-Data*-Loc -defined {(t coll_addr2)} -defined Function-like one-to-one finite countable Function-yielding V94() set
{(t coll_addr2)} is finite countable set
{(t coll_addr2)} --> e is Relation-like {(t coll_addr2)} -defined {e} -valued Function-like constant finite total V38({(t coll_addr2)},{e}) countable Function-yielding V94() Element of bool [:{(t coll_addr2)},{e}:]
{e} is functional finite with_common_domain countable set
[:{(t coll_addr2)},{e}:] is Relation-like finite countable set
bool [:{(t coll_addr2)},{e}:] is finite V30() countable set
t +* ((t coll_addr2) .--> e) is Relation-like Function-like set
SCM+FSA-Chg ((SCM+FSA-Chg (t,(t coll_addr2),e)),(succ (IC t))) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> (succ (IC t)) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ (IC t)) is Relation-like non-empty {NAT} -defined omega -valued {(succ (IC t))} -valued Function-like constant finite total V38({NAT},{(succ (IC t))}) countable Element of bool [:{NAT},{(succ (IC t))}:]
{(succ (IC t))} is finite countable V63() set
[:{NAT},{(succ (IC t))}:] is Relation-like finite countable set
bool [:{NAT},{(succ (IC t))}:] is finite V30() countable set
(SCM+FSA-Chg (t,(t coll_addr2),e)) +* (NAT .--> (succ (IC t))) is Relation-like Function-like set
w is Element of Segm 13
a3 is Element of SCM-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*a3,s*> is set
[w,{},<*a3,s*>] is V13() V14() set
[w,{}] is non natural V13() set
{w,{}} is finite countable set
{w} is finite countable set
{{w,{}},{w}} is finite V30() countable set
[[w,{}],<*a3,s*>] is non natural V13() set
{[w,{}],<*a3,s*>} is finite countable set
{[w,{}]} is Relation-like Function-like finite countable set
{{[w,{}],<*a3,s*>},{[w,{}]}} is finite V30() countable set
t `3_3 is Relation-like Function-like FinSequence-like set
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(SCM+FSA-Chg (t,(t coll_addr2),e)) . s is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
f |-> 0 is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Element of f -tuples_on NAT
f -tuples_on NAT is FinSequenceSet of NAT
f is Int-like Element of the carrier of ()
(Exec ((a,fa),c)) . f is V24() V25() integer ext-real set
q is Element of SCM-Data-Loc
(SCM+FSA-Chg (t,(t coll_addr2),e)) . q is V24() V25() integer ext-real set
c . f is V24() V25() integer ext-real set
f is ()
((Exec ((a,fa),c)),f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
(c,f) is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
q is Element of SCM+FSA-Data*-Loc
(SCM+FSA-Chg (t,(t coll_addr2),e)) . q is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
a is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
IC fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
fa . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . NAT is set
fa is Element of the InstructionsF of SCM
a is Element of the InstructionsF of ()
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec (a,c) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . a is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . a) . c is set
c | SCM-Memory is Relation-like SCM-Memory -defined the carrier of () -defined Function-like the_Values_of () -compatible set
s is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
Exec (fa,s) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set
K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) -valued Function-like V38( the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):]
[: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is Relation-like set
bool [: the InstructionsF of SCM,K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))):] is set
the Execution of SCM . fa is Element of K165((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))
( the Execution of SCM . fa) . s is set
c +* (Exec (fa,s)) is Relation-like Function-like set
c +* s is Relation-like Function-like set
fa is Element of the InstructionsF of ()
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
Exec (fa,a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . fa is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . fa) . a is set
(Exec (fa,a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . (IC ) is set
succ (IC a) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC a) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
c is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
IC c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c . NAT is set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ s is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
IC (Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,a) is Element of the InstructionsF of ()
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
IC (Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,a) is Element of the InstructionsF of ()
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
IC (Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,a) is Element of the InstructionsF of ()
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
IC (Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,a) is Element of the InstructionsF of ()
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
IC (Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ s is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
NAT .--> (succ s) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ s) is Relation-like non-empty {NAT} -defined omega -valued {(succ s)} -valued Function-like constant finite total V38({NAT},{(succ s)}) countable Element of bool [:{NAT},{(succ s)}:]
{(succ s)} is finite countable V63() set
[:{NAT},{(succ s)}:] is Relation-like finite countable set
bool [:{NAT},{(succ s)}:] is finite V30() countable set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ s)) is Relation-like Function-like set
dom (NAT .--> (succ s)) is finite countable Element of bool {NAT}
bool {NAT} is finite V30() countable set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ s))) . NAT is set
(NAT .--> (succ s)) . NAT is set
dom (the_Values_of ()) is Element of bool the carrier of ()
t is set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ s))) . t is set
(the_Values_of ()) . t is set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) . t is set
proj1 ( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ s))) is set
dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) is Element of bool SCM+FSA-Memory
(dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)) \/ (dom (NAT .--> (succ s))) is set
SCM+FSA-Memory \/ (dom (NAT .--> (succ s))) is set
SCM+FSA-Memory \/ {NAT} is set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
NAT .--> fa is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> fa is Relation-like {NAT} -defined NAT -valued {fa} -valued Function-like constant finite total V38({NAT},{fa}) countable Element of bool [:{NAT},{fa}:]
{fa} is finite countable set
[:{NAT},{fa}:] is Relation-like finite countable set
bool [:{NAT},{fa}:] is finite V30() countable set
dom (NAT .--> fa) is finite countable Element of bool {NAT}
t is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
t +* (NAT .--> fa) is Relation-like Function-like set
(t +* (NAT .--> fa)) . NAT is set
(NAT .--> fa) . NAT is set
SCM+FSA-Chg (t,s) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> s is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> s is Relation-like {NAT} -defined NAT -valued {s} -valued Function-like constant finite total V38({NAT},{s}) countable Element of bool [:{NAT},{s}:]
{s} is finite countable set
[:{NAT},{s}:] is Relation-like finite countable set
bool [:{NAT},{s}:] is finite V30() countable set
t +* (NAT .--> s) is Relation-like Function-like set
(SCM+FSA-Chg (t,s)) . NAT is set
Exec ((fa),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa)) . t is set
(Exec ((fa),t)) . NAT is set
t . NAT is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is non halting Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
fa is Int-like Element of the carrier of ()
(a,fa) is Element of the InstructionsF of ()
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ a3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
a3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
NAT .--> (succ a3) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ a3) is Relation-like non-empty {NAT} -defined omega -valued {(succ a3)} -valued Function-like constant finite total V38({NAT},{(succ a3)}) countable Element of bool [:{NAT},{(succ a3)}:]
{(succ a3)} is finite countable V63() set
[:{NAT},{(succ a3)}:] is Relation-like finite countable set
bool [:{NAT},{(succ a3)}:] is finite V30() countable set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3)) is Relation-like Function-like set
proj1 ( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) is set
dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) is Element of bool SCM+FSA-Memory
dom (NAT .--> (succ a3)) is finite countable Element of bool {NAT}
bool {NAT} is finite V30() countable set
(dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)) \/ (dom (NAT .--> (succ a3))) is set
SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) is set
SCM+FSA-Memory \/ {NAT} is set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) . NAT is set
(NAT .--> (succ a3)) . NAT is set
dom (the_Values_of ()) is Element of bool the carrier of ()
t is set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) . t is set
(the_Values_of ()) . t is set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) . t is set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
NAT .--> a is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> a is Relation-like {NAT} -defined NAT -valued {a} -valued Function-like constant finite total V38({NAT},{a}) countable Element of bool [:{NAT},{a}:]
{a} is finite countable set
[:{NAT},{a}:] is Relation-like finite countable set
bool [:{NAT},{a}:] is finite V30() countable set
dom (NAT .--> a) is finite countable Element of bool {NAT}
w is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
w +* (NAT .--> a) is Relation-like Function-like set
(w +* (NAT .--> a)) . NAT is set
(NAT .--> a) . NAT is set
t . fa is V24() V25() integer ext-real set
IC w is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
w . NAT is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
Exec ((a,fa),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . t is set
(Exec ((a,fa),t)) . (IC ) is set
e is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ e is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
e + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
t . fa is V24() V25() integer ext-real set
SCM+FSA-Chg (w,a3) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> a3 is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> a3 is Relation-like {NAT} -defined NAT -valued {a3} -valued Function-like constant finite total V38({NAT},{a3}) countable Element of bool [:{NAT},{a3}:]
{a3} is finite countable set
[:{NAT},{a3}:] is Relation-like finite countable set
bool [:{NAT},{a3}:] is finite V30() countable set
w +* (NAT .--> a3) is Relation-like Function-like set
(SCM+FSA-Chg (w,a3)) . NAT is set
Exec ((a,fa),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . t is set
(Exec ((a,fa),t)) . NAT is set
t . NAT is set
t . fa is V24() V25() integer ext-real set
(a,fa) is Element of the InstructionsF of ()
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ a3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
a3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
NAT .--> (succ a3) is Relation-like {NAT} -defined omega -valued Function-like one-to-one finite countable set
{NAT} --> (succ a3) is Relation-like non-empty {NAT} -defined omega -valued {(succ a3)} -valued Function-like constant finite total V38({NAT},{(succ a3)}) countable Element of bool [:{NAT},{(succ a3)}:]
{(succ a3)} is finite countable V63() set
[:{NAT},{(succ a3)}:] is Relation-like finite countable set
bool [:{NAT},{(succ a3)}:] is finite V30() countable set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3)) is Relation-like Function-like set
proj1 ( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) is set
dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) is Element of bool SCM+FSA-Memory
dom (NAT .--> (succ a3)) is finite countable Element of bool {NAT}
bool {NAT} is finite V30() countable set
(dom the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)) \/ (dom (NAT .--> (succ a3))) is set
SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) is set
SCM+FSA-Memory \/ {NAT} is set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) . NAT is set
(NAT .--> (succ a3)) . NAT is set
dom (the_Values_of ()) is Element of bool the carrier of ()
t is set
( the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) +* (NAT .--> (succ a3))) . t is set
(the_Values_of ()) . t is set
the Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL) . t is set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
NAT .--> a is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> a is Relation-like {NAT} -defined NAT -valued {a} -valued Function-like constant finite total V38({NAT},{a}) countable Element of bool [:{NAT},{a}:]
{a} is finite countable set
[:{NAT},{a}:] is Relation-like finite countable set
bool [:{NAT},{a}:] is finite V30() countable set
dom (NAT .--> a) is finite countable Element of bool {NAT}
w is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
w +* (NAT .--> a) is Relation-like Function-like set
(w +* (NAT .--> a)) . NAT is set
(NAT .--> a) . NAT is set
t . fa is V24() V25() integer ext-real set
IC w is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
w . NAT is set
IC t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
t . (IC ) is set
Exec ((a,fa),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . t is set
(Exec ((a,fa),t)) . (IC ) is set
e is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
succ e is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
e + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
t . fa is V24() V25() integer ext-real set
SCM+FSA-Chg (w,a3) is Relation-like SCM+FSA-Memory -defined Function-like SCM+FSA-OK * SCM*-VAL -compatible Element of product (SCM+FSA-OK * SCM*-VAL)
NAT .--> a3 is Relation-like {NAT} -defined NAT -valued Function-like one-to-one finite countable set
{NAT} --> a3 is Relation-like {NAT} -defined NAT -valued {a3} -valued Function-like constant finite total V38({NAT},{a3}) countable Element of bool [:{NAT},{a3}:]
{a3} is finite countable set
[:{NAT},{a3}:] is Relation-like finite countable set
bool [:{NAT},{a3}:] is finite V30() countable set
w +* (NAT .--> a3) is Relation-like Function-like set
(SCM+FSA-Chg (w,a3)) . NAT is set
Exec ((a,fa),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (a,fa) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (a,fa)) . t is set
(Exec ((a,fa),t)) . NAT is set
t . NAT is set
t . fa is V24() V25() integer ext-real set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
fa is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
a is ()
(fa,c,a) is Element of the InstructionsF of ()
<*fa,a,c*> is set
[9,{},<*fa,a,c*>] is V13() V14() set
[[9,{}],<*fa,a,c*>] is non natural V13() set
{[9,{}],<*fa,a,c*>} is finite countable set
{{[9,{}],<*fa,a,c*>},{[9,{}]}} is finite V30() countable set
Exec ((fa,c,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,c,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,c,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
(Exec ((fa,c,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,c,a) is Element of the InstructionsF of ()
[10,{},<*fa,a,c*>] is V13() V14() set
[[10,{}],<*fa,a,c*>] is non natural V13() set
{[10,{}],<*fa,a,c*>} is finite countable set
{{[10,{}],<*fa,a,c*>},{[10,{}]}} is finite V30() countable set
Exec ((fa,c,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,c,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,c,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
(Exec ((fa,c,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
fa is ()
(a,c,fa) is non halting Element of the InstructionsF of ()
<*a,fa,c*> is set
[9,{},<*a,fa,c*>] is V13() V14() set
[[9,{}],<*a,fa,c*>] is non natural V13() set
{[9,{}],<*a,fa,c*>} is finite countable set
{{[9,{}],<*a,fa,c*>},{[9,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is non halting Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is ()
(fa,a) is Element of the InstructionsF of ()
<*fa,a*> is set
[11,{},<*fa,a*>] is V13() V14() set
[[11,{}],<*fa,a*>] is non natural V13() set
{[11,{}],<*fa,a*>} is finite countable set
{{[11,{}],<*fa,a*>},{[11,{}]}} is finite V30() countable set
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
(fa,a) is Element of the InstructionsF of ()
[12,{},<*fa,a*>] is V13() V14() set
[[12,{}],<*fa,a*>] is non natural V13() set
{[12,{}],<*fa,a*>} is finite countable set
{{[12,{}],<*fa,a*>},{[12,{}]}} is finite V30() countable set
Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
product ( the Object-Kind of () * the ValuesF of ()) is functional with_common_domain product-like set
K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like the InstructionsF of () -defined K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))) -valued Function-like V38( the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))) Element of bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):]
[: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is Relation-like set
bool [: the InstructionsF of (),K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ()))):] is set
the Execution of () . (fa,a) is Element of K165((product ( the Object-Kind of () * the ValuesF of ())),(product ( the Object-Kind of () * the ValuesF of ())))
( the Execution of () . (fa,a)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is set
(Exec ((fa,a), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real non negative Element of omega
(IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set ) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is non halting Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is non halting Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{1,2,3,4,5} is finite countable V63() set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } is set
a is Element of Segm 9
c is Element of SCM-Data-Loc
s is Element of SCM-Data-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
a is Element of Segm 9
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
<*c*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
[a,<*c*>,{}] is V13() V14() set
[a,<*c*>] is non natural V13() set
{a,<*c*>} is finite countable set
{a} is finite countable set
{{a,<*c*>},{a}} is finite V30() countable set
[[a,<*c*>],{}] is non natural V13() set
{[a,<*c*>],{}} is finite countable set
{[a,<*c*>]} is Relation-like Function-like finite countable set
{{[a,<*c*>],{}},{[a,<*c*>]}} is finite V30() countable set
{7,8} is finite countable V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in {7,8} } is set
a is Element of Segm 9
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
<*c*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
s is Element of SCM-Data-Loc
<*s*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like FinSequence-like FinSequence of SCM-Data-Loc
[a,<*c*>,<*s*>] is V13() V14() set
[a,<*c*>] is non natural V13() set
{a,<*c*>} is finite countable set
{a} is finite countable set
{{a,<*c*>},{a}} is finite V30() countable set
[[a,<*c*>],<*s*>] is non natural V13() set
{[a,<*c*>],<*s*>} is finite countable set
{[a,<*c*>]} is Relation-like Function-like finite countable set
{{[a,<*c*>],<*s*>},{[a,<*c*>]}} is finite V30() countable set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 13, b₂ is Element of SCM+FSA-Data-Loc , b₃ is Element of SCM+FSA-Data*-Loc : b₁ in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
{ [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM+FSA-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
SCM-Instr \/ { [b₁,{},<*b₂,b₄,b₃*>] where b₁ is Element of Segm 13, b₂, b₃ is Element of SCM+FSA-Data-Loc , b₄ is Element of SCM+FSA-Data*-Loc : b₁ in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in {7,8} } is set
fa is set
a is Element of the InstructionsF of ()
InsCode a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(a) is set
K29(K29(a)) is set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
(a,c) is non halting Element of the InstructionsF of ()
s is Int-like Element of the carrier of ()
a3 is Int-like Element of the carrier of ()
(s,a3) is non halting Element of the InstructionsF of ()
t is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(t,t) is non halting Element of the InstructionsF of ()
w is Int-like Element of the carrier of ()
e is Int-like Element of the carrier of ()
(w,e) is non halting Element of the InstructionsF of ()
k is Int-like Element of the carrier of ()
S1 is Int-like Element of the carrier of ()
(k,S1) is non halting Element of the InstructionsF of ()
f is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(f) is non halting Element of the InstructionsF of ()
SCM-goto f is Element of the InstructionsF of SCM
<*f*> is Relation-like Function-like set
[6,<*f*>,{}] is V13() V14() set
[6,<*f*>] is non natural V13() set
{6,<*f*>} is finite countable set
{{6,<*f*>},{6}} is finite V30() countable set
[[6,<*f*>],{}] is non natural V13() set
q is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
f is Int-like Element of the carrier of ()
(q,f) is non halting Element of the InstructionsF of ()
q is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
c₁₆ is Int-like Element of the carrier of ()
(q,c₁₆) is non halting Element of the InstructionsF of ()
c₁₈ is Int-like Element of the carrier of ()
c₁₇ is Int-like Element of the carrier of ()
c₁₉ is ()
(c₁₈,c₁₇,c₁₉) is non halting Element of the InstructionsF of ()
<*c₁₈,c₁₉,c₁₇*> is set
[9,{},<*c₁₈,c₁₉,c₁₇*>] is V13() V14() set
[[9,{}],<*c₁₈,c₁₉,c₁₇*>] is non natural V13() set
{[9,{}],<*c₁₈,c₁₉,c₁₇*>} is finite countable set
{{[9,{}],<*c₁₈,c₁₉,c₁₇*>},{[9,{}]}} is finite V30() countable set
c₂₁ is Int-like Element of the carrier of ()
c₂₀ is Int-like Element of the carrier of ()
c₂₂ is ()
(c₂₁,c₂₀,c₂₂) is non halting Element of the InstructionsF of ()
<*c₂₁,c₂₂,c₂₀*> is set
[10,{},<*c₂₁,c₂₂,c₂₀*>] is V13() V14() set
[[10,{}],<*c₂₁,c₂₂,c₂₀*>] is non natural V13() set
{[10,{}],<*c₂₁,c₂₂,c₂₀*>} is finite countable set
{{[10,{}],<*c₂₁,c₂₂,c₂₀*>},{[10,{}]}} is finite V30() countable set
c₂₃ is Int-like Element of the carrier of ()
c₂₄ is ()
(c₂₃,c₂₄) is non halting Element of the InstructionsF of ()
<*c₂₃,c₂₄*> is set
[11,{},<*c₂₃,c₂₄*>] is V13() V14() set
[[11,{}],<*c₂₃,c₂₄*>] is non natural V13() set
{[11,{}],<*c₂₃,c₂₄*>} is finite countable set
{{[11,{}],<*c₂₃,c₂₄*>},{[11,{}]}} is finite V30() countable set
c₂₅ is Int-like Element of the carrier of ()
c₂₆ is ()
(c₂₅,c₂₆) is non halting Element of the InstructionsF of ()
<*c₂₅,c₂₆*> is set
[12,{},<*c₂₅,c₂₆*>] is V13() V14() set
[[12,{}],<*c₂₅,c₂₆*>] is non natural V13() set
{[12,{}],<*c₂₅,c₂₆*>} is finite countable set
{{[12,{}],<*c₂₅,c₂₆*>},{[12,{}]}} is finite V30() countable set
a is Element of the InstructionsF of ()
c is Int-like Element of the carrier of ()
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is Int-like Element of the carrier of ()
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is Int-like Element of the carrier of ()
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is Int-like Element of the carrier of ()
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is Int-like Element of the carrier of ()
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(c) is non halting Element of the InstructionsF of ()
SCM-goto c is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[6,<*c*>,{}] is V13() V14() set
[6,<*c*>] is non natural V13() set
{6,<*c*>} is finite countable set
{{6,<*c*>},{6}} is finite V30() countable set
[[6,<*c*>],{}] is non natural V13() set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
s is Int-like Element of the carrier of ()
(c,s) is non halting Element of the InstructionsF of ()
s is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
a3 is ()
(s,c,a3) is non halting Element of the InstructionsF of ()
<*s,a3,c*> is set
[9,{},<*s,a3,c*>] is V13() V14() set
[[9,{}],<*s,a3,c*>] is non natural V13() set
{[9,{}],<*s,a3,c*>} is finite countable set
{{[9,{}],<*s,a3,c*>},{[9,{}]}} is finite V30() countable set
s is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
a3 is ()
(s,c,a3) is non halting Element of the InstructionsF of ()
<*s,a3,c*> is set
[10,{},<*s,a3,c*>] is V13() V14() set
[[10,{}],<*s,a3,c*>] is non natural V13() set
{[10,{}],<*s,a3,c*>} is finite countable set
{{[10,{}],<*s,a3,c*>},{[10,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of ()
s is ()
(c,s) is non halting Element of the InstructionsF of ()
<*c,s*> is set
[11,{},<*c,s*>] is V13() V14() set
[[11,{}],<*c,s*>] is non natural V13() set
{[11,{}],<*c,s*>} is finite countable set
{{[11,{}],<*c,s*>},{[11,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of ()
s is ()
(c,s) is non halting Element of the InstructionsF of ()
<*c,s*> is set
[12,{},<*c,s*>] is V13() V14() set
[[12,{}],<*c,s*>] is non natural V13() set
{[12,{}],<*c,s*>} is finite countable set
{{[12,{}],<*c,s*>},{[12,{}]}} is finite V30() countable set
halt () is Element of the InstructionsF of ()
halt the InstructionsF of () is V74( the InstructionsF of ()) Element of the InstructionsF of ()
halt () is halting Element of the InstructionsF of ()
halt the InstructionsF of () is V74( the InstructionsF of ()) Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
fa is Element of the InstructionsF of SCM
a is Element of the InstructionsF of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
(fa) is ()
fa + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (fa + 1) is V24() V25() integer ext-real non positive set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
(a) is Int-like Element of the carrier of ()
dl. a is Int-like Element of the carrier of SCM
[1,a] is non natural V13() set
{1,a} is finite countable set
{{1,a},{1}} is finite V30() countable set
NonZero () is Element of bool the carrier of ()
[#] () is non empty non proper Element of bool the carrier of ()
{(IC )} is finite countable set
([#] ()) \ {(IC )} is Element of bool the carrier of ()
() \/ () is Element of bool the carrier of ()
[:{0},NAT:] is Relation-like set
NAT \/ [:{0},NAT:] is set
[0,0] is non natural V13() set
{0,0} is finite countable set
{{0,0},{0}} is finite V30() countable set
{[0,0]} is Relation-like Function-like finite countable set
(NAT \/ [:{0},NAT:]) \ {[0,0]} is Element of bool (NAT \/ [:{0},NAT:])
bool (NAT \/ [:{0},NAT:]) is set
fa is set
a is set
[fa,a] is non natural V13() set
{fa,a} is finite countable set
{fa} is finite countable set
{{fa,a},{fa}} is finite V30() countable set
() \ {NAT} is Element of bool the carrier of ()
SCM-Memory \ {NAT} is Element of bool SCM-Memory
SCM-Data-Loc \ {NAT} is Element of bool SCM-Memory
SCM-Memory \/ () is set
(SCM-Memory \/ ()) \ {NAT} is Element of bool (SCM-Memory \/ ())
bool (SCM-Memory \/ ()) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
(fa) is Int-like Element of the carrier of ()
dl. fa is Int-like Element of the carrier of SCM
[1,fa] is non natural V13() set
{1,fa} is finite countable set
{{1,fa},{1}} is finite V30() countable set
(a) is Int-like Element of the carrier of ()
dl. a is Int-like Element of the carrier of SCM
[1,a] is non natural V13() set
{1,a} is finite countable set
{{1,a},{1}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
Start-At (fa,()) is Relation-like the carrier of () -defined non empty Function-like the_Values_of () -compatible finite countable fa -started set
(IC ) .--> fa is Relation-like {(IC )} -defined the carrier of () -defined {(IC )} -defined NAT -valued Function-like one-to-one finite countable set
{(IC )} --> fa is Relation-like {(IC )} -defined NAT -valued {fa} -valued Function-like constant finite total V38({(IC )},{fa}) countable Element of bool [:{(IC )},{fa}:]
{fa} is finite countable set
[:{(IC )},{fa}:] is Relation-like finite countable set
bool [:{(IC )},{fa}:] is finite V30() countable set
dom (Start-At (fa,())) is non empty finite countable Element of bool the carrier of ()
a is Int-like Element of the carrier of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
Start-At (fa,()) is Relation-like the carrier of () -defined non empty Function-like the_Values_of () -compatible finite countable fa -started set
(IC ) .--> fa is Relation-like {(IC )} -defined the carrier of () -defined {(IC )} -defined NAT -valued Function-like one-to-one finite countable set
{(IC )} --> fa is Relation-like {(IC )} -defined NAT -valued {fa} -valued Function-like constant finite total V38({(IC )},{fa}) countable Element of bool [:{(IC )},{fa}:]
{fa} is finite countable set
[:{(IC )},{fa}:] is Relation-like finite countable set
bool [:{(IC )},{fa}:] is finite V30() countable set
dom (Start-At (fa,())) is non empty finite countable Element of bool the carrier of ()
a is ()
fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
IC fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
fa . (IC ) is set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible total set
IC a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a . (IC ) is set
dom fa is Element of bool the carrier of ()
dom a is Element of bool the carrier of ()
DataPart fa is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible data-only set
fa | (NonZero ()) is Relation-like NonZero () -defined the carrier of () -defined Function-like the_Values_of () -compatible set
Start-At ((IC fa),()) is Relation-like the carrier of () -defined non empty Function-like the_Values_of () -compatible finite countable IC fa -started set
(IC ) .--> (IC fa) is Relation-like {(IC )} -defined the carrier of () -defined {(IC )} -defined NAT -valued Function-like one-to-one finite countable set
{(IC )} --> (IC fa) is Relation-like {(IC )} -defined NAT -valued {(IC fa)} -valued Function-like constant finite total V38({(IC )},{(IC fa)}) countable Element of bool [:{(IC )},{(IC fa)}:]
{(IC fa)} is finite countable set
[:{(IC )},{(IC fa)}:] is Relation-like finite countable set
bool [:{(IC )},{(IC fa)}:] is finite V30() countable set
(DataPart fa) +* (Start-At ((IC fa),())) is Relation-like Function-like IC fa -started set
DataPart a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible data-only set
a | (NonZero ()) is Relation-like NonZero () -defined the carrier of () -defined Function-like the_Values_of () -compatible set
Start-At ((IC a),()) is Relation-like the carrier of () -defined non empty Function-like the_Values_of () -compatible finite countable IC a -started set
(IC ) .--> (IC a) is Relation-like {(IC )} -defined the carrier of () -defined {(IC )} -defined NAT -valued Function-like one-to-one finite countable set
{(IC )} --> (IC a) is Relation-like {(IC )} -defined NAT -valued {(IC a)} -valued Function-like constant finite total V38({(IC )},{(IC a)}) countable Element of bool [:{(IC )},{(IC a)}:]
{(IC a)} is finite countable set
[:{(IC )},{(IC a)}:] is Relation-like finite countable set
bool [:{(IC )},{(IC a)}:] is finite V30() countable set
(DataPart a) +* (Start-At ((IC a),())) is Relation-like Function-like IC a -started set
dom (DataPart fa) is Element of bool the carrier of ()
dom (DataPart a) is Element of bool the carrier of ()
proj1 (DataPart fa) is set
c is set
(DataPart fa) . c is set
(DataPart a) . c is set
fa . c is set
a . c is set
fa . c is set
a . c is set
fa is ()
a is Relation-like NAT -defined INT -valued Function-like FinSequence-like FinSequence of INT
fa .--> a is Relation-like the carrier of () -defined {fa} -defined Function-like one-to-one finite countable Function-yielding V94() set
{fa} is finite countable set
{fa} --> a is Relation-like {fa} -defined {a} -valued Function-like constant finite total V38({fa},{a}) countable Function-yielding V94() Element of bool [:{fa},{a}:]
{a} is functional finite with_common_domain countable set
[:{fa},{a}:] is Relation-like finite countable set
bool [:{fa},{a}:] is finite V30() countable set
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible set
dom c is Element of bool the carrier of ()
fa is Int-like Element of the carrier of ()
a is V24() V25() integer ext-real set
fa .--> a is Relation-like the carrier of () -defined {fa} -defined Function-like one-to-one finite countable set
{fa} is finite countable set
{fa} --> a is Relation-like {fa} -defined {a} -valued Function-like constant finite total V38({fa},{a}) countable Element of bool [:{fa},{a}:]
{a} is finite countable set
[:{fa},{a}:] is Relation-like finite countable set
bool [:{fa},{a}:] is finite V30() countable set
c is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible set
dom c is Element of bool the carrier of ()
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is non halting Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is non halting Element of the InstructionsF of ()
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is non halting Element of the InstructionsF of ()
<*c,fa,a*> is set
[9,{},<*c,fa,a*>] is V13() V14() set
[[9,{}],<*c,fa,a*>] is non natural V13() set
{[9,{}],<*c,fa,a*>} is finite countable set
{{[9,{}],<*c,fa,a*>},{[9,{}]}} is finite V30() countable set
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is non halting Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is non halting Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is non halting Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set
InsCode (halt ()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((halt ())) is set
K29(K29((halt ()))) is set