REAL is V1() V45() set
NAT is V1() epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
K388() is V69() with_non-empty_values IC-Ins-separated strict V108(2) AMI-Struct over 2
2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
the U1 of K388() is set
the_Values_of K388() is Relation-like non-empty the U1 of K388() -defined Function-like V23( the U1 of K388()) set
the Object-Kind of K388() is Relation-like the U1 of K388() -defined 2 -valued Function-like V27( the U1 of K388(),2) Element of K6(K7( the U1 of K388(),2))
K7( the U1 of K388(),2) is Relation-like set
K6(K7( the U1 of K388(),2)) is set
the ValuesF of K388() is V1() Relation-like 2 -defined Function-like V23(2) set
the Object-Kind of K388() (#) the ValuesF of K388() is Relation-like the U1 of K388() -defined Function-like V23( the U1 of K388()) set
COMPLEX is V1() V45() set
NAT is V1() epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
K6(NAT) is set
K7(NAT,REAL) is Relation-like set
K6(K7(NAT,REAL)) is set
K6(K6(REAL)) is set
RAT is V1() V45() set
K6(RAT) is set
ExtREAL is V1() set
9 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Segm 9 is Element of K6(NAT)
K266() is set
SCM-Memory is set
K6(SCM-Memory) is set
K7(SCM-Memory,2) is Relation-like set
K6(K7(SCM-Memory,2)) is set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like V27( SCM-Memory ,2) Element of K6(K7(SCM-Memory,2))
SCM-VAL is V1() Relation-like 2 -defined Function-like V23(2) set
SCM-OK (#) SCM-VAL is Relation-like SCM-Memory -defined Function-like V23( SCM-Memory ) set
product (SCM-OK (#) SCM-VAL) is set
K267() is V1() set
K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) is set
K7(K267(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) is Relation-like set
K6(K7(K267(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))))) is set
the InstructionsF of K388() is V1() Relation-like V89() V90() V91() V93() set
INT is V1() V45() set
SCMPDS is V69() with_non-empty_values IC-Ins-separated strict strict V108(2) V176(2) V177(2) AMI-Struct over 2
K418(NAT,SCM-Memory) is Element of SCM-Memory
K547() is set
K567() is Relation-like K547() -defined K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) -valued Function-like V27(K547(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) Element of K6(K7(K547(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))))
K7(K547(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) is Relation-like set
K6(K7(K547(),K103((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))))) is set
AMI-Struct(# SCM-Memory,K418(NAT,SCM-Memory),K547(),SCM-OK,SCM-VAL,K567() #) is strict AMI-Struct over 2
the U1 of SCMPDS is set
the InstructionsF of SCMPDS is V1() Relation-like V89() V90() V91() V93() set
the_Values_of SCMPDS is Relation-like non-empty the U1 of SCMPDS -defined Function-like V23( the U1 of SCMPDS) set
the Object-Kind of SCMPDS is Relation-like the U1 of SCMPDS -defined 2 -valued Function-like V27( the U1 of SCMPDS,2) Element of K6(K7( the U1 of SCMPDS,2))
K7( the U1 of SCMPDS,2) is Relation-like set
K6(K7( the U1 of SCMPDS,2)) is set
the ValuesF of SCMPDS is V1() Relation-like 2 -defined Function-like V23(2) set
the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS is Relation-like the U1 of SCMPDS -defined Function-like V23( the U1 of SCMPDS) set
K2(K266(),INT) is V1() set
SCM-Data-Loc is Element of K6(SCM-Memory)
K2(SCM-Data-Loc,INT) is V1() set
1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
3 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer V88() V111() V112() V159() Element of NAT
the V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer V88() V111() V112() V159() set is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer V88() V111() V112() V159() set
0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() integer V88() V111() V112() V159() set
IC is Element of the U1 of SCMPDS
goto 1 is Element of the InstructionsF of SCMPDS
14 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
<*1*> is Relation-like Function-like set
K75(14,0,<*1*>) is set
- 1 is V11() V12() ext-real non positive integer set
goto (- 1) is Element of the InstructionsF of SCMPDS
<*(- 1)*> is Relation-like Function-like set
K75(14,0,<*(- 1)*>) is set
product (the_Values_of SCMPDS) is set
K7((product (the_Values_of SCMPDS)),NAT) is Relation-like set
K6(K7((product (the_Values_of SCMPDS)),NAT)) is set
GBP is Int-like Element of the U1 of SCMPDS
intpos 0 is Int-like Element of the U1 of SCMPDS
K397(0) is Int-like Element of the U1 of K388()
SBP is Int-like Element of the U1 of SCMPDS
intpos 1 is Int-like Element of the U1 of SCMPDS
K397(1) is Int-like Element of the U1 of K388()
i1 is Int-like Element of the U1 of SCMPDS
i2 is V11() V12() ext-real integer set
A is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() shiftable V160() set
D is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() shiftable V160() set
if>0 (i1,i2,A,D) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
card A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom A is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card A) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
(i1,i2) <=0_goto ((card A) + 2) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
5 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
<*i1,i2,((card A) + 2)*> is set
K75(5,0,<*i1,i2,((card A) + 2)*>) is set
card D is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom D is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card D) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Goto ((card D) + 1) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) V160() set
A ';' (Goto ((card D) + 1)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(A ';' (Goto ((card D) + 1))) ';' D is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
goto ((card D) + 1) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
<*((card D) + 1)*> is Relation-like Function-like set
K75(14,0,<*((card D) + 1)*>) is set
Load (goto ((card D) + 1)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() halt-free V98( SCMPDS ) V160() set
K385(0,(goto ((card D) + 1))) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
{0} is V1() functional set
K376({0},(goto ((card D) + 1))) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {(goto ((card D) + 1))} -valued Function-like constant V23({0}) V27({0},{(goto ((card D) + 1))}) Element of K6(K7({0},{(goto ((card D) + 1))}))
{(goto ((card D) + 1))} is V1() set
K7({0},{(goto ((card D) + 1))}) is Relation-like set
K6(K7({0},{(goto ((card D) + 1))})) is set
A ';' (Load (goto ((card D) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(A ';' (Load (goto ((card D) + 1)))) ';' D is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((i1,i2) <=0_goto ((card A) + 2)) ';' A is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(((i1,i2) <=0_goto ((card A) + 2)) ';' A) ';' (Goto ((card D) + 1)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((((i1,i2) <=0_goto ((card A) + 2)) ';' A) ';' (Goto ((card D) + 1))) ';' D is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((i1,i2) <=0_goto ((card A) + 2)) ';' (A ';' (Goto ((card D) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(((i1,i2) <=0_goto ((card A) + 2)) ';' (A ';' (Goto ((card D) + 1)))) ';' D is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i5 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() shiftable V160() set
((i1,i2) <=0_goto ((card A) + 2)) ';' i5 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
Load ((i1,i2) <=0_goto ((card A) + 2)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() halt-free V98( SCMPDS ) V160() set
K385(0,((i1,i2) <=0_goto ((card A) + 2))) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
K376({0},((i1,i2) <=0_goto ((card A) + 2))) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {((i1,i2) <=0_goto ((card A) + 2))} -valued Function-like constant V23({0}) V27({0},{((i1,i2) <=0_goto ((card A) + 2))}) Element of K6(K7({0},{((i1,i2) <=0_goto ((card A) + 2))}))
{((i1,i2) <=0_goto ((card A) + 2))} is V1() set
K7({0},{((i1,i2) <=0_goto ((card A) + 2))}) is Relation-like set
K6(K7({0},{((i1,i2) <=0_goto ((card A) + 2))})) is set
(Load ((i1,i2) <=0_goto ((card A) + 2))) ';' i5 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
A is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
D is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i1 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) shiftable V160() set
IExec (i1,A,D) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
i2 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() shiftable V160() set
i3 is Int-like Element of the U1 of SCMPDS
D . i3 is V11() V12() ext-real integer set
i4 is Int-like Element of the U1 of SCMPDS
(IExec (i1,A,D)) . i4 is V11() V12() ext-real integer set
i5 is V11() V12() ext-real integer set
DataLoc ((D . i3),i5) is Int-like Element of the U1 of SCMPDS
(D . i3) + i5 is V11() V12() ext-real integer set
K155(((D . i3) + i5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
[1,K155(((D . i3) + i5))] is set
{1,K155(((D . i3) + i5))} is V1() set
{1} is V1() V56() V57() set
{{1,K155(((D . i3) + i5))},{1}} is V1() V56() V57() set
D . (DataLoc ((D . i3),i5)) is V11() V12() ext-real integer set
if>0 (i3,i5,i1,i2) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() shiftable V160() set
IExec ((if>0 (i3,i5,i1,i2)),A,D) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
(IExec ((if>0 (i3,i5,i1,i2)),A,D)) . i4 is V11() V12() ext-real integer set
card i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom i1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
card i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom i2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card i1) + (card i2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
((card i1) + (card i2)) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Start-At ((((card i1) + (card i2)) + 2),SCMPDS) is V1() Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() ((card i1) + (card i2)) + 2 -started V160() set
K385((IC ),(((card i1) + (card i2)) + 2)) is V1() V2() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V33() V34() V35() V36() V37() V38() V39() V40() set
{(IC )} is V1() set
K376({(IC )},(((card i1) + (card i2)) + 2)) is V1() Relation-like non-empty non empty-yielding {(IC )} -defined NAT -valued RAT -valued INT -valued {(((card i1) + (card i2)) + 2)} -valued Function-like constant V23({(IC )}) V27({(IC )},{(((card i1) + (card i2)) + 2)}) V33() V34() V35() V36() Element of K6(K7({(IC )},{(((card i1) + (card i2)) + 2)}))
{(((card i1) + (card i2)) + 2)} is V1() V56() V57() set
K7({(IC )},{(((card i1) + (card i2)) + 2)}) is Relation-like set
K6(K7({(IC )},{(((card i1) + (card i2)) + 2)})) is set
dom (Start-At ((((card i1) + (card i2)) + 2),SCMPDS)) is V1() set
(IExec (i1,A,D)) +* (Start-At ((((card i1) + (card i2)) + 2),SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) ((card i1) + (card i2)) + 2 -started set
i1 is Int-like Element of the U1 of SCMPDS
i2 is V11() V12() ext-real integer set
i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
while>0 (i1,i2,i3) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
card i3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom i3 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card i3) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
(i1,i2) <=0_goto ((card i3) + 2) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
5 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
<*i1,i2,((card i3) + 2)*> is set
K75(5,0,<*i1,i2,((card i3) + 2)*>) is set
(card i3) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
- ((card i3) + 1) is V11() V12() ext-real non positive integer set
goto (- ((card i3) + 1)) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
<*(- ((card i3) + 1))*> is Relation-like Function-like set
K75(14,0,<*(- ((card i3) + 1))*>) is set
i3 ';' (goto (- ((card i3) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((i1,i2) <=0_goto ((card i3) + 2)) ';' (i3 ';' (goto (- ((card i3) + 1)))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((i1,i2) <=0_goto ((card i3) + 2)) ';' i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(((i1,i2) <=0_goto ((card i3) + 2)) ';' i3) ';' (goto (- ((card i3) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i1 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
Shift (i1,1) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V160() set
i2 is Int-like Element of the U1 of SCMPDS
i3 is V11() V12() ext-real integer set
while>0 (i2,i3,i1) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
card i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom i1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card i1) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
(i2,i3) <=0_goto ((card i1) + 2) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
5 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
<*i2,i3,((card i1) + 2)*> is set
K75(5,0,<*i2,i3,((card i1) + 2)*>) is set
(card i1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
- ((card i1) + 1) is V11() V12() ext-real non positive integer set
goto (- ((card i1) + 1)) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
<*(- ((card i1) + 1))*> is Relation-like Function-like set
K75(14,0,<*(- ((card i1) + 1))*>) is set
((i2,i3) <=0_goto ((card i1) + 2)) ';' i1 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
(((i2,i3) <=0_goto ((card i1) + 2)) ';' i1) ';' (goto (- ((card i1) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
Load (goto (- ((card i1) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() halt-free V98( SCMPDS ) V160() set
K385(0,(goto (- ((card i1) + 1)))) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
{0} is V1() functional set
K376({0},(goto (- ((card i1) + 1)))) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {(goto (- ((card i1) + 1)))} -valued Function-like constant V23({0}) V27({0},{(goto (- ((card i1) + 1)))}) Element of K6(K7({0},{(goto (- ((card i1) + 1)))}))
{(goto (- ((card i1) + 1)))} is V1() set
K7({0},{(goto (- ((card i1) + 1)))}) is Relation-like set
K6(K7({0},{(goto (- ((card i1) + 1)))})) is set
(((i2,i3) <=0_goto ((card i1) + 2)) ';' i1) ';' (Load (goto (- ((card i1) + 1)))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
Load ((i2,i3) <=0_goto ((card i1) + 2)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() halt-free V98( SCMPDS ) V160() set
K385(0,((i2,i3) <=0_goto ((card i1) + 2))) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
K376({0},((i2,i3) <=0_goto ((card i1) + 2))) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {((i2,i3) <=0_goto ((card i1) + 2))} -valued Function-like constant V23({0}) V27({0},{((i2,i3) <=0_goto ((card i1) + 2))}) Element of K6(K7({0},{((i2,i3) <=0_goto ((card i1) + 2))}))
{((i2,i3) <=0_goto ((card i1) + 2))} is V1() set
K7({0},{((i2,i3) <=0_goto ((card i1) + 2))}) is Relation-like set
K6(K7({0},{((i2,i3) <=0_goto ((card i1) + 2))})) is set
(Load ((i2,i3) <=0_goto ((card i1) + 2))) ';' i1 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
((Load ((i2,i3) <=0_goto ((card i1) + 2))) ';' i1) ';' (Load (goto (- ((card i1) + 1)))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
card (Load ((i2,i3) <=0_goto ((card i1) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom (Load ((i2,i3) <=0_goto ((card i1) + 2))) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
i1 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Initialize i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
Start-At (0,SCMPDS) is V1() Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() 0 -started V160() set
K385((IC ),0) is V1() V2() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V33() V34() V35() V36() V37() V38() V39() V40() V111() V112() set
{(IC )} is V1() set
K376({(IC )},0) is V1() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant V23({(IC )}) V27({(IC )},{0}) V33() V34() V35() V36() V111() V112() Element of K6(K7({(IC )},{0}))
{0} is V1() functional set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
i2 +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i3 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart i3 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
Data-Locations is Element of K6( the U1 of SCMPDS)
K6( the U1 of SCMPDS) is set
i3 | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
Initialize i3 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i3 +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i4 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) shiftable V160() set
stop i4 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() V88() V98( SCMPDS ) shiftable V160() set
K343(SCMPDS) is V1() V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V45() V88() non halt-free V97( SCMPDS ) V98( SCMPDS ) paraclosed parahalting shiftable V160() set
halt SCMPDS is V107(2, SCMPDS ) parahalting Element of the InstructionsF of SCMPDS
K339( the InstructionsF of SCMPDS) is V92( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
Load is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() V160() set
K385(0,(halt SCMPDS)) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
K376({0},(halt SCMPDS)) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {(halt SCMPDS)} -valued Function-like constant V23({0}) V27({0},{(halt SCMPDS)}) Element of K6(K7({0},{(halt SCMPDS)}))
{(halt SCMPDS)} is V1() set
K7({0},{(halt SCMPDS)}) is Relation-like set
K6(K7({0},{(halt SCMPDS)})) is set
i4 ';' K343(SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i1 +* (stop i4) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
LifeSpan ((i1 +* (stop i4)),(Initialize i2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
IExec (i4,i1,(Initialize i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart (IExec (i4,i1,(Initialize i2))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(IExec (i4,i1,(Initialize i2))) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
i5 is Int-like Element of the U1 of SCMPDS
i2 . i5 is V11() V12() ext-real integer set
i6 is V11() V12() ext-real integer set
DataLoc ((i2 . i5),i6) is Int-like Element of the U1 of SCMPDS
(i2 . i5) + i6 is V11() V12() ext-real integer set
K155(((i2 . i5) + i6)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
[1,K155(((i2 . i5) + i6))] is set
{1,K155(((i2 . i5) + i6))} is V1() set
{1} is V1() V56() V57() set
{{1,K155(((i2 . i5) + i6))},{1}} is V1() V56() V57() set
i2 . (DataLoc ((i2 . i5),i6)) is V11() V12() ext-real integer set
while>0 (i5,i6,i4) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) shiftable V160() set
stop (while>0 (i5,i6,i4)) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V45() V88() V98( SCMPDS ) shiftable V160() set
(while>0 (i5,i6,i4)) ';' K343(SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i1 +* (stop (while>0 (i5,i6,i4))) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
i7 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),i7) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
card i4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom i4 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card i4) + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
(i5,i6) <=0_goto ((card i4) + 2) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
5 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
<*i5,i6,((card i4) + 2)*> is set
K75(5,0,<*i5,i6,((card i4) + 2)*>) is set
(card i4) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
- ((card i4) + 1) is V11() V12() ext-real non positive integer set
goto (- ((card i4) + 1)) is V94( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
<*(- ((card i4) + 1))*> is Relation-like Function-like set
K75(14,0,<*(- ((card i4) + 1))*>) is set
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Shift (i4,1) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V160() set
i4 ';' (goto (- ((card i4) + 1))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) V160() set
((i5,i6) <=0_goto ((card i4) + 2)) ';' (i4 ';' (goto (- ((card i4) + 1)))) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) V160() set
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),(0 + 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Following ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0))) is Element of the InstructionsF of SCMPDS
IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)) . (IC ) is set
K72( the InstructionsF of SCMPDS,(i1 +* (stop (while>0 (i5,i6,i4)))),(IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS) is set
K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is set
the Execution of SCMPDS is Relation-like the InstructionsF of SCMPDS -defined K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like V27( the InstructionsF of SCMPDS,K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))
K7( the InstructionsF of SCMPDS,K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is Relation-like set
K6(K7( the InstructionsF of SCMPDS,K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))))) is set
the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)))) is Element of K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0))))) . (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),0)) is set
Following ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2)) is Element of the InstructionsF of SCMPDS
IC (Initialize i2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Initialize i2) . (IC ) is set
K72( the InstructionsF of SCMPDS,(i1 +* (stop (while>0 (i5,i6,i4)))),(IC (Initialize i2))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2))),(Initialize i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2))) is Element of K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2)))) . (Initialize i2) is set
Exec (((i5,i6) <=0_goto ((card i4) + 2)),(Initialize i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
the Execution of SCMPDS . ((i5,i6) <=0_goto ((card i4) + 2)) is Element of K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . ((i5,i6) <=0_goto ((card i4) + 2))) . (Initialize i2) is set
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
dom (Start-At (0,SCMPDS)) is V1() set
(Initialize i2) . i5 is V11() V12() ext-real integer set
DataLoc (((Initialize i2) . i5),i6) is Int-like Element of the U1 of SCMPDS
((Initialize i2) . i5) + i6 is V11() V12() ext-real integer set
K155((((Initialize i2) . i5) + i6)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
[1,K155((((Initialize i2) . i5) + i6))] is set
{1,K155((((Initialize i2) . i5) + i6))} is V1() set
{{1,K155((((Initialize i2) . i5) + i6))},{1}} is V1() V56() V57() set
(Initialize i2) . (DataLoc (((Initialize i2) . i5),i6)) is V11() V12() ext-real integer set
(Initialize i2) . (DataLoc ((i2 . i5),i6)) is V11() V12() ext-real integer set
(LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),(((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1) + 1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
dom (while>0 (i5,i6,i4)) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
k7 is Int-like Element of the U1 of SCMPDS
(Initialize i2) . k7 is V11() V12() ext-real integer set
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)) . k7 is V11() V12() ext-real integer set
DataPart (Initialize i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Initialize i2) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
(i1 +* (stop i4)) +* (stop i4) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
Initialize (Initialize i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
(Initialize i2) +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)) . (IC ) is set
succ 0 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() set
0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
Comput ((i1 +* (stop i4)),(Initialize i2),(LifeSpan ((i1 +* (stop i4)),(Initialize i2)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart (Comput ((i1 +* (stop i4)),(Initialize i2),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput ((i1 +* (stop i4)),(Initialize i2),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
Result ((i1 +* (stop i4)),(Initialize i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart (Result ((i1 +* (stop i4)),(Initialize i2))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Result ((i1 +* (stop i4)),(Initialize i2))) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) . (IC ) is set
CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)))) is Element of the InstructionsF of SCMPDS
IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))) . (IC ) is set
K72( the InstructionsF of SCMPDS,(i1 +* (stop (while>0 (i5,i6,i4)))),(IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))))) is Element of the InstructionsF of SCMPDS
(i1 +* (stop (while>0 (i5,i6,i4)))) . ((card i4) + 1) is Element of the InstructionsF of SCMPDS
(while>0 (i5,i6,i4)) . ((card i4) + 1) is set
Following ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Exec ((CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))))) is Element of K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)))))) . (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))) is set
Exec ((goto (- ((card i4) + 1))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
the Execution of SCMPDS . (goto (- ((card i4) + 1))) is Element of K103((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (goto (- ((card i4) + 1)))) . (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))) is set
k7 is Int-like Element of the U1 of SCMPDS
i3 . k7 is V11() V12() ext-real integer set
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))) . k7 is V11() V12() ext-real integer set
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),1)),(LifeSpan ((i1 +* (stop i4)),(Initialize i2))))) . k7 is V11() V12() ext-real integer set
IC (Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),(((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),(((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1) + 1))) . (IC ) is set
0 - ((card i4) + 1) is V1() V11() V12() ext-real non positive negative integer set
ICplusConst ((Comput ((i1 +* (stop (while>0 (i5,i6,i4)))),(Initialize i2),((LifeSpan ((i1 +* (stop i4)),(Initialize i2))) + 1))),(0 - ((card i4) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
i1 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
Data-Locations is Element of K6( the U1 of SCMPDS)
K6( the U1 of SCMPDS) is set
i2 | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
stop i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
K343(SCMPDS) is V1() V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V45() V88() non halt-free V97( SCMPDS ) V98( SCMPDS ) paraclosed parahalting shiftable V160() set
halt SCMPDS is V107(2, SCMPDS ) parahalting Element of the InstructionsF of SCMPDS
K339( the InstructionsF of SCMPDS) is V92( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
Load is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() 1 -element V88() V160() set
K385(0,(halt SCMPDS)) is V1() V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
{0} is V1() functional set
K376({0},(halt SCMPDS)) is V1() Relation-like {0} -defined the InstructionsF of SCMPDS -valued {(halt SCMPDS)} -valued Function-like constant V23({0}) V27({0},{(halt SCMPDS)}) Element of K6(K7({0},{(halt SCMPDS)}))
{(halt SCMPDS)} is V1() set
K7({0},{(halt SCMPDS)}) is Relation-like set
K6(K7({0},{(halt SCMPDS)})) is set
i3 ';' K343(SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
Initialize i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
Start-At (0,SCMPDS) is V1() Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() 0 -started V160() set
K385((IC ),0) is V1() V2() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V33() V34() V35() V36() V37() V38() V39() V40() V111() V112() set
{(IC )} is V1() set
K376({(IC )},0) is V1() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant V23({(IC )}) V27({(IC )},{0}) V33() V34() V35() V36() V111() V112() Element of K6(K7({(IC )},{0}))
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
i2 +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i1 +* (stop i3) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
dom (stop i3) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
i7 is Int-like Element of the U1 of SCMPDS
i2 . i7 is V11() V12() ext-real integer set
(Initialize i2) . i7 is V11() V12() ext-real integer set
dom (Start-At (0,SCMPDS)) is V1() set
i7 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
Comput ((i1 +* (stop i3)),(Initialize i2),i7) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
IC (Comput ((i1 +* (stop i3)),(Initialize i2),i7)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop i3)),(Initialize i2),i7)) . (IC ) is set
i7 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer set
Comput ((i1 +* (stop i3)),(Initialize i2),i7) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
IC (Comput ((i1 +* (stop i3)),(Initialize i2),i7)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop i3)),(Initialize i2),i7)) . (IC ) is set
IF1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
Comput ((i1 +* (stop i3)),(Initialize i2),IF1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop i3)),(Initialize i2),IF1)) . (IC ) is set
succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() set
(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
((IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))) --> ((goto 1),(goto (- 1))) is V1() Relation-like {(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))} -defined the InstructionsF of SCMPDS -valued Function-like V27({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))}, the InstructionsF of SCMPDS) Element of K6(K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))}, the InstructionsF of SCMPDS))
{(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))} is V1() set
K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))}, the InstructionsF of SCMPDS) is Relation-like set
K6(K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))}, the InstructionsF of SCMPDS)) is set
K385((IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(goto 1)) is V1() V2() Relation-like NAT -defined {(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
{(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))} is V1() set
K376({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))},(goto 1)) is V1() Relation-like {(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))} -defined the InstructionsF of SCMPDS -valued {(goto 1)} -valued Function-like constant V23({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))}) V27({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))},{(goto 1)}) Element of K6(K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))},{(goto 1)}))
{(goto 1)} is V1() set
K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))},{(goto 1)}) is Relation-like set
K6(K7({(IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))},{(goto 1)})) is set
K385((succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))),(goto (- 1))) is V1() V2() Relation-like {(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant set
{(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))} is V1() V56() V57() set
K376({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))},(goto (- 1))) is V1() Relation-like {(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))} -defined the InstructionsF of SCMPDS -valued {(goto (- 1))} -valued Function-like constant V23({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))}) V27({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))},{(goto (- 1))}) Element of K6(K7({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))},{(goto (- 1))}))
{(goto (- 1))} is V1() set
K7({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))},{(goto (- 1))}) is Relation-like set
K6(K7({(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))},{(goto (- 1))})) is set
K385((IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(goto 1)) +* K385((succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))),(goto (- 1))) is V1() Relation-like the InstructionsF of SCMPDS -valued Function-like set
(i1 +* (stop i3)) +* (((IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))))) --> ((goto 1),(goto (- 1)))) is V1() Relation-like the InstructionsF of SCMPDS -valued Function-like set
(i1 +* (stop i3)) +* ((IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1))),(goto 1)) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
j4 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
j4 +* ((succ (IC (Comput ((i1 +* (stop i3)),(Initialize i2),IF1)))),(goto (- 1))) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
j2 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
j5 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
j6 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
Comput ((i1 +* (stop i3)),(Initialize i2),j6) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
IC (Comput ((i1 +* (stop i3)),(Initialize i2),j6)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
(Comput ((i1 +* (stop i3)),(Initialize i2),j6)) . (IC ) is set
Comput (j2,(Initialize i2),IF1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
DataPart (Initialize i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Initialize i2) | (Data-Locations ) is Relation-like the U1 of SCMPDS -defined Data-Locations -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
j2 +* (stop i3) is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
Initialize (Initialize i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
(Initialize i2) +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
4 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
i1 is Element of the InstructionsF of SCMPDS
i2 is Element of the InstructionsF of SCMPDS
i1 ';' i2 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i3 is Element of the InstructionsF of SCMPDS
(i1 ';' i2) ';' i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
i4 is Element of the InstructionsF of SCMPDS
((i1 ';' i2) ';' i3) ';' i4 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() V160() set
card (((i1 ';' i2) ';' i3) ';' i4) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom (((i1 ';' i2) ';' i3) ';' i4) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
card ((i1 ';' i2) ';' i3) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom ((i1 ';' i2) ';' i3) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card ((i1 ';' i2) ';' i3)) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
card (i1 ';' i2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
dom (i1 ';' i2) is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() V139() set
(card (i1 ';' i2)) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
((card (i1 ';' i2)) + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
2 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
(2 + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative integer V56() Element of NAT
i1 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
i2 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i3 is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) shiftable V160() set
IExec (i3,i1,i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
Initialize (IExec (i3,i1,i2)) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
Start-At (0,SCMPDS) is V1() Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() 0 -started V160() set
K385((IC ),0) is V1() V2() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V33() V34() V35() V36() V37() V38() V39() V40() V111() V112() set
{(IC )} is V1() set
K376({(IC )},0) is V1() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant V23({(IC )}) V27({(IC )},{0}) V33() V34() V35() V36() V111() V112() Element of K6(K7({(IC )},{0}))
{0} is V1() functional set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
(IExec (i3,i1,i2)) +* (Start-At (0,SCMPDS)) is V1() Relation-like the U1 of SCMPDS -defined the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
i4 is Int-like Element of the U1 of SCMPDS
i2 . i4 is V11() V12() ext-real integer set
i5 is Int-like Element of the U1 of SCMPDS
i2 . i5 is V11() V12() ext-real integer set
i6 is Int-like Element of the U1 of SCMPDS
i2 . i6 is V11() V12() ext-real integer set
IF1 is V11() V12() ext-real integer set
i7 is V11() V12() ext-real integer set
DataLoc ((i2 . i4),i7) is Int-like Element of the U1 of SCMPDS
(i2 . i4) + i7 is V11() V12() ext-real integer set
K155(((i2 . i4) + i7)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative integer Element of NAT
[1,K155(((i2 . i4) + i7))] is set
{1,K155(((i2 . i4) + i7))} is V1() set
{1} is V1() V56() V57() set
{{1,K155(((i2 . i4) + i7))},{1}} is V1() V56() V57() set
i2 . (DataLoc ((i2 . i4),i7)) is V11() V12() ext-real integer set
IF1 + (i2 . (DataLoc ((i2 . i4),i7))) is V11() V12() ext-real integer set
while>0 (i4,i7,i3) is V1() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V45() V88() halt-free V98( SCMPDS ) shiftable V160() set
IExec ((while>0 (i4,i7,i3)),i1,i2) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
IExec ((while>0 (i4,i7,i3)),i1,(Initialize (IExec (i3,i1,i2)))) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
{i5} is V1() set
WH1 is Int-like Element of the U1 of SCMPDS
i2 . WH1 is V11() V12() ext-real integer set
WH1 is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) 0 -started set
WH1 . (DataLoc ((i2 . i4),i7)) is V11() V12() ext-real integer set
IF1 + (WH1 . (DataLoc ((i2 . i4),i7))) is V11() V12() ext-real integer set
{i6} is V1() set
WH1 . i4 is V11() V12() ext-real integer set
WH1 . i6 is V11() V12() ext-real integer set
WH1 . i5 is V11() V12() ext-real integer set
j1 is V1() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V23( NAT ) set
IExec (i3,j1,WH1) is Relation-like the U1 of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V23( the U1 of SCMPDS) set
(IExec (i3,j1,WH1)) . i4 is V11() V12() ext-real integer set
(IExec (i3,j1,WH1)) . (DataLoc ((i2 . i4),i7)) is V11() V12() ext-real integer