REAL is V4() V45() set
NAT is V4() epsilon-transitive epsilon-connected ordinal V45() cardinal limit_cardinal countable denumerable Element of K32(REAL)
K32(REAL) is V45() set
K531() is V81() with_non-empty_values IC-Ins-separated strict V163(2) AMI-Struct over 2
2 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
SCM-Memory is set
K561(NAT,SCM-Memory) is Element of SCM-Memory
K410() is V4() set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like total V29( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))
K33(SCM-Memory,2) is Relation-like set
K32(K33(SCM-Memory,2)) is set
SCM-VAL is V4() Relation-like 2 -defined Function-like total set
SCM-Exec is V4() Relation-like K410() -defined K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) -valued Function-like total V29(K410(),K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) Element of K32(K33(K410(),K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))))
SCM-OK (#) SCM-VAL is Relation-like SCM-Memory -defined Function-like total set
product (SCM-OK (#) SCM-VAL) is functional with_common_domain product-like set
K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) is V4() functional set
K33(K410(),K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) is Relation-like set
K32(K33(K410(),K162((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))))) is set
AMI-Struct(# SCM-Memory,K561(NAT,SCM-Memory),K410(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the carrier of K531() is V4() set
the_Values_of K531() is V4() Relation-like non-empty non empty-yielding the carrier of K531() -defined Function-like total set
the Object-Kind of K531() is V4() Relation-like the carrier of K531() -defined 2 -valued Function-like total V29( the carrier of K531(),2) Element of K32(K33( the carrier of K531(),2))
K33( the carrier of K531(),2) is Relation-like set
K32(K33( the carrier of K531(),2)) is set
the ValuesF of K531() is V4() Relation-like 2 -defined Function-like total set
the Object-Kind of K531() (#) the ValuesF of K531() is V4() Relation-like the carrier of K531() -defined Function-like total set
COMPLEX is V4() V45() set
NAT is V4() epsilon-transitive epsilon-connected ordinal V45() cardinal limit_cardinal countable denumerable set
K32(NAT) is V45() set
K32(NAT) is V45() set
K33(NAT,REAL) is Relation-like V45() set
K32(K33(NAT,REAL)) is V45() set
K32(K32(REAL)) is V45() set
RAT is V4() V45() set
K32(RAT) is V45() set
ExtREAL is V4() set
INT is V4() V45() set
K33(REAL,REAL) is Relation-like V45() set
K32(K33(REAL,REAL)) is V45() set
K397() is V81() V109() L8()
the carrier of K397() is V4() set
9 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
Segm 9 is countable Element of K32(NAT)
K409() is set
K32(SCM-Memory) is set
the InstructionsF of K531() is V4() Relation-like standard-ins V145() V146() V148() set
SCMPDS is V81() with_non-empty_values IC-Ins-separated strict strict V163(2) AMI-Struct over 2
the carrier of SCMPDS is V4() set
the InstructionsF of SCMPDS is V4() Relation-like standard-ins V145() V146() V148() set
the_Values_of SCMPDS is V4() Relation-like non-empty non empty-yielding the carrier of SCMPDS -defined Function-like total set
the Object-Kind of SCMPDS is V4() Relation-like the carrier of SCMPDS -defined 2 -valued Function-like total V29( the carrier of SCMPDS,2) Element of K32(K33( the carrier of SCMPDS,2))
K33( the carrier of SCMPDS,2) is Relation-like set
K32(K33( the carrier of SCMPDS,2)) is set
the ValuesF of SCMPDS is V4() Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS is V4() Relation-like the carrier of SCMPDS -defined Function-like total set
K33(COMPLEX,COMPLEX) is Relation-like V45() set
K32(K33(COMPLEX,COMPLEX)) is V45() set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is Relation-like V45() set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is V45() set
K33(K33(REAL,REAL),REAL) is Relation-like V45() set
K32(K33(K33(REAL,REAL),REAL)) is V45() set
K33(RAT,RAT) is Relation-like V45() set
K32(K33(RAT,RAT)) is V45() set
K33(K33(RAT,RAT),RAT) is Relation-like V45() set
K32(K33(K33(RAT,RAT),RAT)) is V45() set
K33(INT,INT) is Relation-like V45() set
K32(K33(INT,INT)) is V45() set
K33(K33(INT,INT),INT) is Relation-like V45() set
K32(K33(K33(INT,INT),INT)) is V45() set
K33(NAT,NAT) is Relation-like V45() set
K33(K33(NAT,NAT),NAT) is Relation-like V45() set
K32(K33(K33(NAT,NAT),NAT)) is V45() set
0 is V4() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer ext-real non negative V35() V36() V37() V38() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable V143() set
1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
3 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
0 is V4() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer ext-real non negative V35() V36() V37() V38() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable V143() Element of NAT
14 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
IC is V88( SCMPDS ) Element of the carrier of SCMPDS
halt SCMPDS is V162(2, SCMPDS ) parahalting Element of the InstructionsF of SCMPDS
halt the InstructionsF of SCMPDS is V147( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
4 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
5 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
6 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
{0,4,5,6,14} is countable Element of K32(NAT)
product (the_Values_of SCMPDS) is V4() functional with_common_domain product-like set
K33((product (the_Values_of SCMPDS)),NAT) is Relation-like V45() set
K32(K33((product (the_Values_of SCMPDS)),NAT)) is V45() set
<*> REAL is V4() Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer ext-real non negative V35() V36() V37() V38() V45() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable V143() FinSequence of REAL
K362((<*> REAL)) is V24() V25() ext-real Element of REAL
Fib 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Fib 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
{0} is V4() V5() functional 1 -element with_common_domain countable Element of K32(NAT)
A is Element of the InstructionsF of SCMPDS
D is Element of the InstructionsF of SCMPDS
A ';' D is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
a1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
(A ';' D) ';' a1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
((A ';' D) ';' a1) . 0 is set
((A ';' D) ';' a1) . 1 is set
D ';' a1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
A ';' (D ';' a1) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
Load A is V4() V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V45() 1 -element countable V143() V153( SCMPDS ) set
(Load A) ';' (D ';' a1) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
dom (Load A) is V4() V5() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal 1 -element V56() countable V74() set
(Load A) . 0 is set
Load D is V4() V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V45() 1 -element countable V143() V153( SCMPDS ) set
dom (Load D) is V4() V5() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal 1 -element V56() countable V74() set
card (D ';' a1) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal V56() countable Element of NAT
dom (D ';' a1) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal V56() countable V74() set
card a1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal V56() countable Element of NAT
dom a1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal V56() countable V74() set
(card a1) + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
card (Load A) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal V56() countable Element of NAT
0 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
((Load A) ';' (D ';' a1)) . (0 + 1) is set
(D ';' a1) . 0 is set
(Load D) ';' a1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() set
((Load D) ';' a1) . 0 is set
(Load D) . 0 is set
A is Int-like Element of the carrier of SCMPDS
D is Int-like Element of the carrier of SCMPDS
a1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
a1 . A is V24() V25() integer ext-real set
a1 . D is V24() V25() integer ext-real set
a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
a1 . A is V24() V25() integer ext-real set
a1 . D is V24() V25() integer ext-real set
abs (a1 . A) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
abs (a1 . D) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
max ((abs (a1 . A)),(abs (a1 . D))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
a1 . A is V24() V25() integer ext-real set
a1 . D is V24() V25() integer ext-real set
a1 is V4() Relation-like product (the_Values_of SCMPDS) -defined NAT -valued Function-like total V29( product (the_Values_of SCMPDS), NAT ) V35() V36() V37() V38() Element of K32(K33((product (the_Values_of SCMPDS)),NAT))
a2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a1 . a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
a1 . a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
j1 . A is V24() V25() integer ext-real set
j1 . D is V24() V25() integer ext-real set
abs (j1 . A) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
abs (j1 . D) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
max ((abs (j1 . A)),(abs (j1 . D))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a1 . a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a2 . A is V24() V25() integer ext-real set
a2 . D is V24() V25() integer ext-real set
abs (a2 . A) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
abs (a2 . D) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
max ((abs (a2 . A)),(abs (a2 . D))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a3 . A is V24() V25() integer ext-real set
a3 . D is V24() V25() integer ext-real set
abs (a3 . A) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
abs (a3 . D) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
max ((abs (a3 . A)),(abs (a3 . D))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
A is Int-like Element of the carrier of SCMPDS
D is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
D . A is V24() V25() integer ext-real set
a1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
D is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
D . A is V24() V25() integer ext-real set
- (D . A) is V24() V25() integer ext-real set
a1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
D is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
D . A is V24() V25() integer ext-real set
D is V4() Relation-like product (the_Values_of SCMPDS) -defined NAT -valued Function-like total V29( product (the_Values_of SCMPDS), NAT ) V35() V36() V37() V38() Element of K32(K33((product (the_Values_of SCMPDS)),NAT))
a1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
D . a1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
D . a2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a3 . A is V24() V25() integer ext-real set
- (a3 . A) is V24() V25() integer ext-real set
a1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
D . a1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
a1 . A is V24() V25() integer ext-real set
- (a1 . A) is V24() V25() integer ext-real set
a2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a2 . A is V24() V25() integer ext-real set
- (a2 . A) is V24() V25() integer ext-real set
SCM-Data-Loc is Element of K32(SCM-Memory)
F2() is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F5() is Int-like Element of the carrier of SCMPDS
F2() . F5() is V24() V25() integer ext-real set
F6() is V24() V25() integer ext-real set
DataLoc ((F2() . F5()),F6()) is Int-like Element of the carrier of SCMPDS
(F2() . F5()) + F6() is V24() V25() integer ext-real set
abs ((F2() . F5()) + F6()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
K4(1,(abs ((F2() . F5()) + F6()))) is set
F4() is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
while<0 (F5(),F6(),F4()) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
F3() is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec ((while<0 (F5(),F6(),F4())),F3(),F2()) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2())) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() countable 0 -started set
K528((IC ),0) is V5() INT -valued V35() V36() V37() V38() Cardinal-yielding set
K1((IC )) is V4() V5() 1 -element set
K519(K1((IC )),0) is V4() Relation-like K1((IC )) -defined INT -valued K1(0) -valued Function-like total V29(K1((IC )),K1(0)) V35() V36() V37() V38() Cardinal-yielding Element of K32(K33(K1((IC )),K1(0)))
K1(0) is V4() V5() functional 1 -element with_common_domain set
K33(K1((IC )),K1(0)) is Relation-like set
K32(K33(K1((IC )),K1(0))) is set
(IExec ((while<0 (F5(),F6(),F4())),F3(),F2())) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),F3(),F2())))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F1(a3) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 . F5() is V24() V25() integer ext-real set
j1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec ((while<0 (F5(),F6(),F4())),j1,a3) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec ((while<0 (F5(),F6(),F4())),j1,a3)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec ((while<0 (F5(),F6(),F4())),j1,a3)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),j1,a3)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Initialize a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
a3 +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
a3 . (DataLoc ((F2() . F5()),F6())) is V24() V25() integer ext-real set
j2 is Int-like Element of the carrier of SCMPDS
(IExec ((while<0 (F5(),F6(),F4())),j1,a3)) . j2 is V24() V25() integer ext-real set
a3 . j2 is V24() V25() integer ext-real set
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F1(j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
j1 . F5() is V24() V25() integer ext-real set
j2 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec ((while<0 (F5(),F6(),F4())),j2,j1) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec ((while<0 (F5(),F6(),F4())),j2,j1)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j2 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec (F4(),j2,j1) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
j1 . (DataLoc ((F2() . F5()),F6())) is V24() V25() integer ext-real set
(IExec (F4(),j2,j1)) . F5() is V24() V25() integer ext-real set
Initialize (IExec (F4(),j2,j1)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec (F4(),j2,j1)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
DataLoc ((j1 . F5()),F6()) is Int-like Element of the carrier of SCMPDS
(j1 . F5()) + F6() is V24() V25() integer ext-real set
abs ((j1 . F5()) + F6()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
K4(1,(abs ((j1 . F5()) + F6()))) is set
WB is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F1(WB) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
WB . (DataLoc ((j1 . F5()),F6())) is V24() V25() integer ext-real set
F1((Initialize (IExec (F4(),j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
H1( Initialize (IExec (F4(),j2,j1))) + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
WB is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
WB . F5() is V24() V25() integer ext-real set
WB . (DataLoc ((j1 . F5()),F6())) is V24() V25() integer ext-real set
WH is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec (F4(),WH,WB) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(IExec (F4(),WH,WB)) . F5() is V24() V25() integer ext-real set
F1(WB) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Initialize (IExec (F4(),WH,WB)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec (F4(),WH,WB)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec (F4(),WH,WB)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 . (DataLoc ((j1 . F5()),F6())) is V24() V25() integer ext-real set
IExec ((while<0 (F5(),F6(),F4())),j2,j1) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IExec ((while<0 (F5(),F6(),F4())),j2,(Initialize (IExec (F4(),j2,j1)))) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(Initialize (IExec (F4(),j2,j1))) . F5() is V24() V25() integer ext-real set
Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec ((while<0 (F5(),F6(),F4())),j2,j1)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F1(j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 . F5() is V24() V25() integer ext-real set
j2 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec ((while<0 (F5(),F6(),F4())),j2,j1) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec ((while<0 (F5(),F6(),F4())),j2,j1)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
F1(F2()) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F1(a3) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
a3 . F5() is V24() V25() integer ext-real set
j1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec ((while<0 (F5(),F6(),F4())),j1,a3) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec ((while<0 (F5(),F6(),F4())),j1,a3)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec ((while<0 (F5(),F6(),F4())),j1,a3)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
F1((Initialize (IExec ((while<0 (F5(),F6(),F4())),j1,a3)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos 1 is Int-like Element of the carrier of SCMPDS
K540(1) is Int-like Element of the carrier of K531()
K4(1,1) is set
intpos 2 is Int-like Element of the carrier of SCMPDS
K540(2) is Int-like Element of the carrier of K531()
K4(1,2) is set
intpos 3 is Int-like Element of the carrier of SCMPDS
K540(3) is Int-like Element of the carrier of K531()
K4(1,3) is set
GBP is Int-like Element of the carrier of SCMPDS
intpos 0 is Int-like Element of the carrier of SCMPDS
K540(0) is Int-like Element of the carrier of K531()
K4(1,0) is set
GBP := 0 is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
<*GBP,0*> is V4() Relation-like NAT -defined Function-like V45() 2 -element FinSequence-like FinSubsequence-like countable set
K15(2,0,<*GBP,0*>) is set
(intpos 1) := 0 is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
<*(intpos 1),0*> is V4() Relation-like NAT -defined Function-like V45() 2 -element FinSequence-like FinSubsequence-like countable set
K15(2,0,<*(intpos 1),0*>) is set
(GBP := 0) ';' ((intpos 1) := 0) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) paraclosed parahalting shiftable set
j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
- j1 is V24() V25() integer ext-real non positive set
(intpos 2) := (- j1) is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
<*(intpos 2),(- j1)*> is V4() Relation-like NAT -defined Function-like V45() 2 -element FinSequence-like FinSubsequence-like countable set
K15(2,0,<*(intpos 2),(- j1)*>) is set
((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- j1)) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) paraclosed parahalting shiftable set
j2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j2 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
(intpos 3) := (j2 + 1) is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
<*(intpos 3),(j2 + 1)*> is V4() Relation-like NAT -defined Function-like V45() 2 -element FinSequence-like FinSubsequence-like countable set
K15(2,0,<*(intpos 3),(j2 + 1)*>) is set
(((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- j1))) ';' ((intpos 3) := (j2 + 1)) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) paraclosed parahalting shiftable set
AddTo (GBP,1,(intpos 3),0) is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
AddTo (GBP,2,1) is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
8 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
<*GBP,2,1*> is V4() Relation-like NAT -defined Function-like V45() 3 -element FinSequence-like FinSubsequence-like countable set
K15(8,0,<*GBP,2,1*>) is set
(AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1)) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) paraclosed parahalting shiftable set
AddTo (GBP,3,1) is No-StopCode shiftable parahalting Element of the InstructionsF of SCMPDS
<*GBP,3,1*> is V4() Relation-like NAT -defined Function-like V45() 3 -element FinSequence-like FinSubsequence-like countable set
K15(8,0,<*GBP,3,1*>) is set
((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) paraclosed parahalting shiftable set
while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1)))) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := (- j1))) ';' ((intpos 3) := (j2 + 1))) ';' (while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
j1 is V4() Relation-like product (the_Values_of SCMPDS) -defined NAT -valued Function-like total V29( product (the_Values_of SCMPDS), NAT ) V35() V36() V37() V38() Element of K32(K33((product (the_Values_of SCMPDS)),NAT))
j2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
j1 . j2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
j1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
j2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
j3 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
WH is Int-like Element of the carrier of SCMPDS
j2 . WH is V24() V25() integer ext-real set
WB is Int-like Element of the carrier of SCMPDS
j2 . WB is V24() V25() integer ext-real set
j1 is Int-like Element of the carrier of SCMPDS
j2 . j1 is V24() V25() integer ext-real set
j4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos j3 is Int-like Element of the carrier of SCMPDS
K540(j3) is Int-like Element of the carrier of K531()
K4(1,j3) is set
j2 . (intpos j3) is V24() V25() integer ext-real set
- j2 is V24() V25() integer ext-real non positive set
j4 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
while<0 (WB,j3,j3) is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V45() countable V143() halt-free V153( SCMPDS ) shiftable set
IExec ((while<0 (WB,j3,j3)),j1,j2) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(IExec ((while<0 (WB,j3,j3)),j1,j2)) . WH is V24() V25() integer ext-real set
WB is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len WB is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum WB is V24() V25() integer ext-real Element of INT
Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() countable 0 -started set
K528((IC ),0) is V5() INT -valued V35() V36() V37() V38() Cardinal-yielding set
K1((IC )) is V4() V5() 1 -element set
K519(K1((IC )),0) is V4() Relation-like K1((IC )) -defined INT -valued K1(0) -valued Function-like total V29(K1((IC )),K1(0)) V35() V36() V37() V38() Cardinal-yielding Element of K32(K33(K1((IC )),K1(0)))
K1(0) is V4() V5() functional 1 -element with_common_domain set
K33(K1((IC )),K1(0)) is Relation-like set
K32(K33(K1((IC )),K1(0))) is set
(IExec ((while<0 (WB,j3,j3)),j1,j2)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
DataLoc ((j2 . WB),j3) is Int-like Element of the carrier of SCMPDS
(j2 . WB) + j3 is V24() V25() integer ext-real set
abs ((j2 . WB) + j3) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
K4(1,(abs ((j2 . WB) + j3))) is set
i3 is V4() Relation-like product (the_Values_of SCMPDS) -defined NAT -valued Function-like total V29( product (the_Values_of SCMPDS), NAT ) V35() V36() V37() V38() Element of K32(K33((product (the_Values_of SCMPDS)),NAT))
j1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
j1 . (intpos j3) is V24() V25() integer ext-real set
(j1 . (intpos j3)) + j2 is V24() V25() integer ext-real set
j1 . WH is V24() V25() integer ext-real set
j1 . j1 is V24() V25() integer ext-real set
(i3,j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j1 . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
- (j1 . (DataLoc ((j2 . WB),j3))) is V24() V25() integer ext-real set
j1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
j1 . (intpos j3) is V24() V25() integer ext-real set
(j1 . (intpos j3)) + j2 is V24() V25() integer ext-real set
j1 . WH is V24() V25() integer ext-real set
j1 . j1 is V24() V25() integer ext-real set
j1 . WB is V24() V25() integer ext-real set
j1 . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
IF is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len IF is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum IF is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len IF) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
IF is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len IF is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum IF is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len IF) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
j2 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
IExec (j3,j2,j1) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize (IExec (j3,j2,j1)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(IExec (j3,j2,j1)) +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
WB is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos WB is Int-like Element of the carrier of SCMPDS
K540(WB) is Int-like Element of the carrier of K531()
K4(1,WB) is set
j1 . (intpos WB) is V24() V25() integer ext-real set
j2 . (intpos WB) is V24() V25() integer ext-real set
WH is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len WH is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum WH is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len WH) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
0 + j3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos (0 + j3) is Int-like Element of the carrier of SCMPDS
K540((0 + j3)) is Int-like Element of the carrier of K531()
K4(1,(0 + j3)) is set
(IExec (j3,j2,j1)) . WB is V24() V25() integer ext-real set
((j1 . (intpos j3)) + j2) + 1 is V24() V25() integer ext-real set
(IExec (j3,j2,j1)) . j1 is V24() V25() integer ext-real set
(IExec (j3,j2,j1)) . WH is V24() V25() integer ext-real set
WB is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len WB is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(j4 + 1) + (len WB) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
Sum WB is V24() V25() integer ext-real Element of INT
(IExec (j3,j2,j1)) . (intpos j3) is V24() V25() integer ext-real set
(j1 . (intpos j3)) + 1 is V24() V25() integer ext-real set
(Initialize (IExec (j3,j2,j1))) . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
(i3,(Initialize (IExec (j3,j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(i3,j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
WH is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len WH is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum WH is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len WH) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
(i3,j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
- (j1 . (DataLoc ((j2 . WB),j3))) is V24() V25() integer ext-real set
- (j1 . (intpos j3)) is V24() V25() integer ext-real set
(Initialize (IExec (j3,j2,j1))) . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
(i3,(Initialize (IExec (j3,j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
- ((Initialize (IExec (j3,j2,j1))) . (DataLoc ((j2 . WB),j3))) is V24() V25() integer ext-real set
- ((j1 . (intpos j3)) + 1) is V24() V25() integer ext-real set
(- (j1 . (intpos j3))) - 1 is V24() V25() integer ext-real set
(i3,j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(i3,(Initialize (IExec (j3,j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(i3,j1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(i3,(Initialize (IExec (j3,j2,j1)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(Initialize (IExec (j3,j2,j1))) . (intpos j3) is V24() V25() integer ext-real set
((Initialize (IExec (j3,j2,j1))) . (intpos j3)) + j2 is V24() V25() integer ext-real set
(Initialize (IExec (j3,j2,j1))) . WH is V24() V25() integer ext-real set
(Initialize (IExec (j3,j2,j1))) . j1 is V24() V25() integer ext-real set
WH is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos WH is Int-like Element of the carrier of SCMPDS
K540(WH) is Int-like Element of the carrier of K531()
K4(1,WH) is set
(Initialize (IExec (j3,j2,j1))) . (intpos WH) is V24() V25() integer ext-real set
(IExec (j3,j2,j1)) . (intpos WH) is V24() V25() integer ext-real set
j2 . (intpos WH) is V24() V25() integer ext-real set
((IExec (j3,j2,j1)) . (intpos j3)) + j2 is V24() V25() integer ext-real set
(j2 . (intpos j3)) + j2 is V24() V25() integer ext-real set
j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos j1 is Int-like Element of the carrier of SCMPDS
K540(j1) is Int-like Element of the carrier of K531()
K4(1,j1) is set
j2 . (intpos j1) is V24() V25() integer ext-real set
j1 is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum j1 is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len j1) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
(i3,(Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
(Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2))) . (intpos j3) is V24() V25() integer ext-real set
((Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2))) . (intpos j3)) + j2 is V24() V25() integer ext-real set
(Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2))) . WH is V24() V25() integer ext-real set
(Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2))) . j1 is V24() V25() integer ext-real set
j1 is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum j1 is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len j1) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
j1 is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len j1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum j1 is V24() V25() integer ext-real Element of INT
(IExec ((while<0 (WB,j3,j3)),j1,j2)) . (intpos (0 + j3)) is V24() V25() integer ext-real set
(IExec ((while<0 (WB,j3,j3)),j1,j2)) . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
(Initialize (IExec ((while<0 (WB,j3,j3)),j1,j2))) . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
j2 is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len j2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum j2 is V24() V25() integer ext-real Element of INT
(j4 + 1) + (len j2) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
j2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable set
dom WB is countable V74() Element of K32(NAT)
WB . j2 is V24() V25() integer ext-real set
IF is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j4 + IF is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos (j4 + IF) is Int-like Element of the carrier of SCMPDS
K540((j4 + IF)) is Int-like Element of the carrier of K531()
K4(1,(j4 + IF)) is set
j2 . (intpos (j4 + IF)) is V24() V25() integer ext-real set
j1 . j2 is V24() V25() integer ext-real set
j2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
IF is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len IF is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j2 . (intpos j3) is V24() V25() integer ext-real set
(j2 . (intpos j3)) + j2 is V24() V25() integer ext-real set
j2 . WH is V24() V25() integer ext-real set
Sum IF is V24() V25() integer ext-real Element of INT
j2 . j1 is V24() V25() integer ext-real set
(j4 + 1) + (len IF) is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
(i3,j2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j2 . (DataLoc ((j2 . WB),j3)) is V24() V25() integer ext-real set
j1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
j3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
j3 . GBP is V24() V25() integer ext-real set
j3 . (intpos 3) is V24() V25() integer ext-real set
Initialize j3 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() countable 0 -started set
K528((IC ),0) is V5() INT -valued V35() V36() V37() V38() Cardinal-yielding set
K1((IC )) is V4() V5() 1 -element set
K519(K1((IC )),0) is V4() Relation-like K1((IC )) -defined INT -valued K1(0) -valued Function-like total V29(K1((IC )),K1(0)) V35() V36() V37() V38() Cardinal-yielding Element of K32(K33(K1((IC )),K1(0)))
K1(0) is V4() V5() functional 1 -element with_common_domain set
K33(K1((IC )),K1(0)) is Relation-like set
K32(K33(K1((IC )),K1(0))) is set
j3 +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3))) . GBP is V24() V25() integer ext-real set
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3))) . (intpos 1) is V24() V25() integer ext-real set
j3 . (intpos 1) is V24() V25() integer ext-real set
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3))) . (intpos 2) is V24() V25() integer ext-real set
j3 . (intpos 2) is V24() V25() integer ext-real set
(j3 . (intpos 2)) + 1 is V24() V25() integer ext-real set
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3))) . (intpos 3) is V24() V25() integer ext-real set
j4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos j4 is Int-like Element of the carrier of SCMPDS
K540(j4) is Int-like Element of the carrier of K531()
K4(1,j4) is set
j3 . (intpos j4) is V24() V25() integer ext-real set
(j3 . (intpos 1)) + (j3 . (intpos j4)) is V24() V25() integer ext-real set
j4 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS) is functional with_common_domain product-like set
K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is V4() functional set
the Execution of SCMPDS is V4() Relation-like the InstructionsF of SCMPDS -defined K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like total V29( the InstructionsF of SCMPDS,K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K162((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 . (AddTo (GBP,1,(intpos 3),0)) is Relation-like Function-like Element of K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (AddTo (GBP,1,(intpos 3),0))) . (Initialize j3) is set
(Initialize j3) . (intpos 3) is V24() V25() integer ext-real set
(Initialize j3) . GBP is V24() V25() integer ext-real set
((Initialize j3) . GBP) + 1 is V24() V25() integer ext-real set
abs (((Initialize j3) . GBP) + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
DataLoc (((Initialize j3) . GBP),1) is Int-like Element of the carrier of SCMPDS
K4(1,(abs (((Initialize j3) . GBP) + 1))) is set
(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . GBP is V24() V25() integer ext-real set
((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . GBP) + 2 is V24() V25() integer ext-real set
abs (((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . GBP) + 2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
DataLoc (((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . GBP),2) is Int-like Element of the carrier of SCMPDS
K4(1,(abs (((Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . GBP) + 2))) is set
(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . (intpos 3) is V24() V25() integer ext-real set
(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . (intpos 3) is V24() V25() integer ext-real set
Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3)))) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . (AddTo (GBP,2,1)) is Relation-like Function-like Element of K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (AddTo (GBP,2,1))) . (Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) is set
(Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))))) . (intpos 3) is V24() V25() integer ext-real set
(Initialize j3) . (intpos 1) is V24() V25() integer ext-real set
0 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
intpos (0 + 1) is Int-like Element of the carrier of SCMPDS
K540((0 + 1)) is Int-like Element of the carrier of K531()
K4(1,(0 + 1)) is set
(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . (intpos 1) is V24() V25() integer ext-real set
DataLoc (((Initialize j3) . (intpos 3)),0) is Int-like Element of the carrier of SCMPDS
((Initialize j3) . (intpos 3)) + 0 is V24() V25() integer ext-real set
abs (((Initialize j3) . (intpos 3)) + 0) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
K4(1,(abs (((Initialize j3) . (intpos 3)) + 0))) is set
(Initialize j3) . (DataLoc (((Initialize j3) . (intpos 3)),0)) is V24() V25() integer ext-real set
((Initialize j3) . (intpos 1)) + ((Initialize j3) . (DataLoc (((Initialize j3) . (intpos 3)),0))) is V24() V25() integer ext-real set
j4 + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos (j4 + 0) is Int-like Element of the carrier of SCMPDS
K540((j4 + 0)) is Int-like Element of the carrier of K531()
K4(1,(j4 + 0)) is set
(Initialize j3) . (intpos (j4 + 0)) is V24() V25() integer ext-real set
((Initialize j3) . (intpos 1)) + ((Initialize j3) . (intpos (j4 + 0))) is V24() V25() integer ext-real set
0 + 2 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
intpos (0 + 2) is Int-like Element of the carrier of SCMPDS
K540((0 + 2)) is Int-like Element of the carrier of K531()
K4(1,(0 + 2)) is set
(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . (intpos 2) is V24() V25() integer ext-real set
(Initialize j3) . (intpos 2) is V24() V25() integer ext-real set
(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . GBP is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))))) . GBP is V24() V25() integer ext-real set
DataLoc (((IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . GBP),3) is Int-like Element of the carrier of SCMPDS
((IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . GBP) + 3 is V24() V25() integer ext-real set
abs (((IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . GBP) + 3) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
K4(1,(abs (((IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . GBP) + 3))) is set
0 + 3 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
intpos (0 + 3) is Int-like Element of the carrier of SCMPDS
K540((0 + 3)) is Int-like Element of the carrier of K531()
K4(1,(0 + 3)) is set
(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . (intpos 2) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))))) . (intpos 2) is V24() V25() integer ext-real set
(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . (intpos 1) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))))) . (intpos 1) is V24() V25() integer ext-real set
Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3)))) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . (AddTo (GBP,3,1)) is Relation-like Function-like Element of K162((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (AddTo (GBP,3,1))) . (IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) is set
(Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))))) . GBP is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))))) . (intpos 1) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))))) . (intpos 2) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))))) . (intpos 3) is V24() V25() integer ext-real set
i3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
intpos i3 is Int-like Element of the carrier of SCMPDS
K540(i3) is Int-like Element of the carrier of K531()
K4(1,i3) is set
(IExec ((((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))),j1,(Initialize j3))) . (intpos i3) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,3,1)),(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))))) . (intpos i3) is V24() V25() integer ext-real set
(IExec (((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))),j1,(Initialize j3))) . (intpos i3) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,2,1)),(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))))) . (intpos i3) is V24() V25() integer ext-real set
(Exec ((AddTo (GBP,1,(intpos 3),0)),(Initialize j3))) . (intpos i3) is V24() V25() integer ext-real set
(Initialize j3) . (intpos i3) is V24() V25() integer ext-real set
j3 . (intpos i3) is V24() V25() integer ext-real set
j1 is V4() Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
j2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
j2 . (intpos 1) is V24() V25() integer ext-real set
j2 . GBP is V24() V25() integer ext-real set
j2 . (intpos 2) is V24() V25() integer ext-real set
j2 . (intpos 3) is V24() V25() integer ext-real set
Initialize j2 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V45() countable 0 -started set
K528((IC ),0) is V5() INT -valued V35() V36() V37() V38() Cardinal-yielding set
K1((IC )) is V4() V5() 1 -element set
K519(K1((IC )),0) is V4() Relation-like K1((IC )) -defined INT -valued K1(0) -valued Function-like total V29(K1((IC )),K1(0)) V35() V36() V37() V38() Cardinal-yielding Element of K32(K33(K1((IC )),K1(0)))
K1(0) is V4() V5() functional 1 -element with_common_domain set
K33(K1((IC )),K1(0)) is Relation-like set
K32(K33(K1((IC )),K1(0))) is set
j2 +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),j1,(Initialize j2)) is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(IExec ((while<0 (GBP,2,(((AddTo (GBP,1,(intpos 3),0)) ';' (AddTo (GBP,2,1))) ';' (AddTo (GBP,3,1))))),j1,(Initialize j2))) . (intpos 1) is V24() V25() integer ext-real set
j4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
j3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
- j3 is V24() V25() integer ext-real non positive set
j4 + 1 is V4() epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive non negative V45() cardinal V56() countable Element of NAT
WB is Relation-like NAT -defined INT -valued Function-like V35() V36() V37() V45() FinSequence-like FinSubsequence-like countable FinSequence of INT
len WB is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative V45() cardinal countable Element of NAT
Sum WB is V24() V25() integer ext-real Element of INT
i1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Initialize i1 is V4() Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
i1 +* (Start-At (0,SCMPDS)) is V4() Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
i1 . (intpos 2) is V24() V25() integer ext-real