REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial V24() cardinal limit_cardinal countable denumerable Element of K27(REAL)
K27(REAL) is set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial V24() cardinal limit_cardinal countable denumerable set
K27(omega) is non trivial V24() set
K27(NAT) is non trivial V24() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
K28(2,2) is Relation-like V24() countable set
K28(K28(2,2),2) is Relation-like V24() countable set
K27(K28(K28(2,2),2)) is V24() V28() countable set
9 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
Segm 9 is countable Element of K27(omega)
K229() is set
SCM-Memory is set
K27(SCM-Memory) is set
K28(SCM-Memory,2) is Relation-like set
K27(K28(SCM-Memory,2)) is set
SCM-OK is Relation-like Function-like V36( SCM-Memory ,2) Element of K27(K28(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like total V212() set
SCM-OK * SCM-VAL is Relation-like Function-like set
product (SCM-OK * SCM-VAL) is functional with_common_domain product-like set
K230() is non empty set
K120((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is set
K28(K230(),K120((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))) is Relation-like set
K27(K28(K230(),K120((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))))) is set
SCM is non empty with_non-empty_values IC-Ins-separated strict strict V154(2) AMI-Struct over 2
the InstructionsF of SCM is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of SCM is non empty set
the_Values_of SCM is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like Function-like V36( the carrier of SCM,2) Element of K27(K28( the carrier of SCM,2))
K28( the carrier of SCM,2) is Relation-like set
K27(K28( the carrier of SCM,2)) is set
the ValuesF of SCM is Relation-like 2 -defined Function-like total V212() set
the Object-Kind of SCM * the ValuesF of SCM is Relation-like Function-like set
COMPLEX is set
RAT is set
INT is set
{} is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V25() V28() cardinal {} -element V39() Cardinal-yielding countable Function-yielding V158() V175() ext-real non negative V180() V181() V182() V183() V211() V212() set
the Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V25() V28() cardinal {} -element V39() Cardinal-yielding countable Function-yielding V158() V175() ext-real non negative V180() V181() V182() V183() V211() V212() set is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V25() V28() cardinal {} -element V39() Cardinal-yielding countable Function-yielding V158() V175() ext-real non negative V180() V181() V182() V183() V211() V212() set
SCM-Data-Loc is Element of K27(SCM-Memory)
1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V25() V28() cardinal {} -element V39() Cardinal-yielding countable Function-yielding V158() V175() ext-real non negative V180() V181() V182() V183() V211() V212() Element of NAT
NonZero SCM is Element of K27( the carrier of SCM)
K27( the carrier of SCM) is set
[0,{},{}] is V21() V22() set
[0,{}] is V21() set
{0,{}} is functional non empty V24() V28() countable set
{0} is functional non empty trivial V24() V28() 1 -element with_common_domain countable set
{{0,{}},{0}} is non empty V24() V28() countable set
[[0,{}],{}] is V21() set
{[0,{}],{}} is non empty V24() countable set
{[0,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[0,{}],{}},{[0,{}]}} is non empty V24() V28() countable set
{NAT} is non empty trivial V24() 1 -element countable set
0. SCM is V48( SCM ) Element of the carrier of SCM
Seg 1 is countable Element of K27(NAT)
{1} is non empty trivial V24() V28() 1 -element countable set
Seg 2 is countable Element of K27(NAT)
{1,2} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the carrier of R is non empty set
I is Int-like Element of the carrier of (SCM R)
Values I is non empty set
the_Values_of (SCM R) is Relation-like non-empty the carrier of (SCM R) -defined Function-like total set
the Object-Kind of (SCM R) is Relation-like Function-like V36( the carrier of (SCM R),2) Element of K27(K28( the carrier of (SCM R),2))
K28( the carrier of (SCM R),2) is Relation-like set
K27(K28( the carrier of (SCM R),2)) is set
the ValuesF of (SCM R) is Relation-like 2 -defined Function-like total V212() set
the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like Function-like set
(the_Values_of (SCM R)) . I is set
SCM-VAL R is Relation-like 2 -defined Function-like total V212() set
SCM-OK * (SCM-VAL R) is Relation-like Function-like set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the carrier of R is non empty set
I is Int-like Element of the carrier of (SCM R)
T is Int-like Element of the carrier of (SCM R)
i1 is Element of the carrier of R
j is Element of the carrier of R
(I,T) --> (i1,j) is Relation-like the carrier of (SCM R) -defined Function-like non empty V24() countable V212() set
the_Values_of (SCM R) is Relation-like non-empty the carrier of (SCM R) -defined Function-like total set
the Object-Kind of (SCM R) is Relation-like Function-like V36( the carrier of (SCM R),2) Element of K27(K28( the carrier of (SCM R),2))
K28( the carrier of (SCM R),2) is Relation-like set
K27(K28( the carrier of (SCM R),2)) is set
the ValuesF of (SCM R) is Relation-like 2 -defined Function-like total V212() set
the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like Function-like set
Values T is non empty set
(the_Values_of (SCM R)) . T is set
Values I is non empty set
(the_Values_of (SCM R)) . I is set
s1 is Element of Values I
k is Element of Values T
(I,T) --> (s1,k) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty V24() countable V212() set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
0. (SCM R) is V48( SCM R) Element of the carrier of (SCM R)
I is Int-like Element of the carrier of (SCM R)
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
0. (SCM R) is V48( SCM R) Element of the carrier of (SCM R)
I is Element of the carrier of (SCM R)
{(0. (SCM R))} is non empty trivial V24() 1 -element countable set
the carrier of (SCM R) \ {NAT} is Element of K27( the carrier of (SCM R))
K27( the carrier of (SCM R)) is set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
I is Int-like Element of the carrier of (SCM R)
T is Int-like Element of the carrier of (SCM R)
I := T is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*I,T*> is set
[1,{},<*I,T*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*I,T*>] is V21() set
{[1,{}],<*I,T*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*I,T*>},{[1,{}]}} is non empty V24() V28() countable set
InsCode (I := T) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((I := T)) is set
K41(K41((I := T))) is set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
I is Int-like Element of the carrier of (SCM R)
T is Int-like Element of the carrier of (SCM R)
AddTo (I,T) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*I,T*> is set
[2,{},<*I,T*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*I,T*>] is V21() set
{[2,{}],<*I,T*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*I,T*>},{[2,{}]}} is non empty V24() V28() countable set
InsCode (AddTo (I,T)) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((AddTo (I,T))) is set
K41(K41((AddTo (I,T)))) is set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
I is Int-like Element of the carrier of (SCM R)
T is Int-like Element of the carrier of (SCM R)
SubFrom (I,T) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*I,T*> is set
[3,{},<*I,T*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*I,T*>] is V21() set
{[3,{}],<*I,T*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*I,T*>},{[3,{}]}} is non empty V24() V28() countable set
InsCode (SubFrom (I,T)) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((SubFrom (I,T))) is set
K41(K41((SubFrom (I,T)))) is set
4 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
I is Int-like Element of the carrier of (SCM R)
T is Int-like Element of the carrier of (SCM R)
MultBy (I,T) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*I,T*> is set
[4,{},<*I,T*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*I,T*>] is V21() set
{[4,{}],<*I,T*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*I,T*>},{[4,{}]}} is non empty V24() V28() countable set
InsCode (MultBy (I,T)) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((MultBy (I,T))) is set
K41(K41((MultBy (I,T)))) is set
5 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
the carrier of R is non empty set
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
T is Int-like Element of the carrier of (SCM R)
I is Element of the carrier of R
T := I is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,I*> is set
[5,{},<*T,I*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*T,I*>] is V21() set
{[5,{}],<*T,I*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*T,I*>},{[5,{}]}} is non empty V24() V28() countable set
InsCode (T := I) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((T := I)) is set
K41(K41((T := I))) is set
6 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (I,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*I*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*I*>,{}] is V21() V22() set
[6,<*I*>] is V21() set
{6,<*I*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*I*>},{6}} is non empty V24() V28() countable set
[[6,<*I*>],{}] is V21() set
{[6,<*I*>],{}} is non empty V24() countable set
{[6,<*I*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*I*>],{}},{[6,<*I*>]}} is non empty V24() V28() countable set
InsCode (goto (I,R)) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((goto (I,R))) is set
K41(K41((goto (I,R)))) is set
7 is epsilon-transitive epsilon-connected ordinal natural non empty V24() cardinal V39() countable non with_non-empty_elements V175() ext-real positive non negative Element of NAT
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the carrier of (SCM R) is non empty set
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
T is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
I is Int-like Element of the carrier of (SCM R)
I =0_goto T is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*I*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*T*>,<*I*>] is V21() V22() set
[7,<*T*>] is V21() set
{7,<*T*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*T*>},{7}} is non empty V24() V28() countable set
[[7,<*T*>],<*I*>] is V21() set
{[7,<*T*>],<*I*>} is non empty V24() countable set
{[7,<*T*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*T*>],<*I*>},{[7,<*T*>]}} is non empty V24() V28() countable set
InsCode (I =0_goto T) is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41((I =0_goto T)) is set
K41(K41((I =0_goto T))) is set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
halt (SCM R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
halt the InstructionsF of (SCM R) is ins-loc-free Element of the InstructionsF of (SCM R)
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
the carrier of (SCM R) is non empty set
the carrier of R is non empty set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*r,u*>] is V21() set
{[4,{}],<*r,u*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*r,u*>},{[4,{}]}} is non empty V24() V28() countable set
P is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (P,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*P*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*P*>,{}] is V21() V22() set
[6,<*P*>] is V21() set
{6,<*P*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*P*>},{6}} is non empty V24() V28() countable set
[[6,<*P*>],{}] is V21() set
{[6,<*P*>],{}} is non empty V24() countable set
{[6,<*P*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*P*>],{}},{[6,<*P*>]}} is non empty V24() V28() countable set
e is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
x is Int-like Element of the carrier of (SCM R)
x =0_goto e is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*e*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*e*>,<*x*>] is V21() V22() set
[7,<*e*>] is V21() set
{7,<*e*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*e*>},{7}} is non empty V24() V28() countable set
[[7,<*e*>],<*x*>] is V21() set
{[7,<*e*>],<*x*>} is non empty V24() countable set
{[7,<*e*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*e*>],<*x*>},{[7,<*e*>]}} is non empty V24() V28() countable set
E is Int-like Element of the carrier of (SCM R)
v is Element of the carrier of R
E := v is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*E,v*> is set
[5,{},<*E,v*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*E,v*>] is V21() set
{[5,{}],<*E,v*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*E,v*>},{[5,{}]}} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of (SCM R) is non empty set
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
the carrier of R is non empty set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*r,u*>] is V21() set
{[4,{}],<*r,u*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*r,u*>},{[4,{}]}} is non empty V24() V28() countable set
P is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (P,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*P*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*P*>,{}] is V21() V22() set
[6,<*P*>] is V21() set
{6,<*P*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*P*>},{6}} is non empty V24() V28() countable set
[[6,<*P*>],{}] is V21() set
{[6,<*P*>],{}} is non empty V24() countable set
{[6,<*P*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*P*>],{}},{[6,<*P*>]}} is non empty V24() V28() countable set
e is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
x is Int-like Element of the carrier of (SCM R)
x =0_goto e is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*e*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*e*>,<*x*>] is V21() V22() set
[7,<*e*>] is V21() set
{7,<*e*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*e*>},{7}} is non empty V24() V28() countable set
[[7,<*e*>],<*x*>] is V21() set
{[7,<*e*>],<*x*>} is non empty V24() countable set
{[7,<*e*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*e*>],<*x*>},{[7,<*e*>]}} is non empty V24() V28() countable set
E is Int-like Element of the carrier of (SCM R)
v is Element of the carrier of R
E := v is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*E,v*> is set
[5,{},<*E,v*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*E,v*>] is V21() set
{[5,{}],<*E,v*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*E,v*>},{[5,{}]}} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of (SCM R) is non empty set
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
the carrier of R is non empty set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*r,u*>] is V21() set
{[4,{}],<*r,u*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*r,u*>},{[4,{}]}} is non empty V24() V28() countable set
P is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (P,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*P*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*P*>,{}] is V21() V22() set
[6,<*P*>] is V21() set
{6,<*P*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*P*>},{6}} is non empty V24() V28() countable set
[[6,<*P*>],{}] is V21() set
{[6,<*P*>],{}} is non empty V24() countable set
{[6,<*P*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*P*>],{}},{[6,<*P*>]}} is non empty V24() V28() countable set
e is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
x is Int-like Element of the carrier of (SCM R)
x =0_goto e is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*e*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*e*>,<*x*>] is V21() V22() set
[7,<*e*>] is V21() set
{7,<*e*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*e*>},{7}} is non empty V24() V28() countable set
[[7,<*e*>],<*x*>] is V21() set
{[7,<*e*>],<*x*>} is non empty V24() countable set
{[7,<*e*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*e*>],<*x*>},{[7,<*e*>]}} is non empty V24() V28() countable set
E is Int-like Element of the carrier of (SCM R)
v is Element of the carrier of R
E := v is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*E,v*> is set
[5,{},<*E,v*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*E,v*>] is V21() set
{[5,{}],<*E,v*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*E,v*>},{[5,{}]}} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of (SCM R) is non empty set
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
the carrier of R is non empty set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*r,u*>] is V21() set
{[4,{}],<*r,u*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*r,u*>},{[4,{}]}} is non empty V24() V28() countable set
P is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (P,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*P*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*P*>,{}] is V21() V22() set
[6,<*P*>] is V21() set
{6,<*P*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*P*>},{6}} is non empty V24() V28() countable set
[[6,<*P*>],{}] is V21() set
{[6,<*P*>],{}} is non empty V24() countable set
{[6,<*P*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*P*>],{}},{[6,<*P*>]}} is non empty V24() V28() countable set
e is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
x is Int-like Element of the carrier of (SCM R)
x =0_goto e is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*e*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*e*>,<*x*>] is V21() V22() set
[7,<*e*>] is V21() set
{7,<*e*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*e*>},{7}} is non empty V24() V28() countable set
[[7,<*e*>],<*x*>] is V21() set
{[7,<*e*>],<*x*>} is non empty V24() countable set
{[7,<*e*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*e*>],<*x*>},{[7,<*e*>]}} is non empty V24() V28() countable set
E is Int-like Element of the carrier of (SCM R)
v is Element of the carrier of R
E := v is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*E,v*> is set
[5,{},<*E,v*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*E,v*>] is V21() set
{[5,{}],<*E,v*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*E,v*>},{[5,{}]}} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of (SCM R) is non empty set
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
the carrier of R is non empty set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}} is non empty V24() V28() countable set
{4} is non empty trivial V24() V28() 1 -element countable set
{{4,{}},{4}} is non empty V24() V28() countable set
[[4,{}],<*r,u*>] is V21() set
{[4,{}],<*r,u*>} is non empty V24() countable set
{[4,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[4,{}],<*r,u*>},{[4,{}]}} is non empty V24() V28() countable set
P is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
goto (P,R) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*P*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
[6,<*P*>,{}] is V21() V22() set
[6,<*P*>] is V21() set
{6,<*P*>} is non empty V24() countable set
{6} is non empty trivial V24() V28() 1 -element countable set
{{6,<*P*>},{6}} is non empty V24() V28() countable set
[[6,<*P*>],{}] is V21() set
{[6,<*P*>],{}} is non empty V24() countable set
{[6,<*P*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[6,<*P*>],{}},{[6,<*P*>]}} is non empty V24() V28() countable set
e is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of NAT
x is Int-like Element of the carrier of (SCM R)
x =0_goto e is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*e*> is Relation-like Function-like FinSequence-like Cardinal-yielding FinSequence of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of the carrier of (SCM R)
[7,<*e*>,<*x*>] is V21() V22() set
[7,<*e*>] is V21() set
{7,<*e*>} is non empty V24() countable set
{7} is non empty trivial V24() V28() 1 -element countable set
{{7,<*e*>},{7}} is non empty V24() V28() countable set
[[7,<*e*>],<*x*>] is V21() set
{[7,<*e*>],<*x*>} is non empty V24() countable set
{[7,<*e*>]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[7,<*e*>],<*x*>},{[7,<*e*>]}} is non empty V24() V28() countable set
E is Int-like Element of the carrier of (SCM R)
v is Element of the carrier of R
E := v is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*E,v*> is set
[5,{},<*E,v*>] is V21() V22() set
[5,{}] is V21() set
{5,{}} is non empty V24() V28() countable set
{5} is non empty trivial V24() V28() 1 -element countable set
{{5,{}},{5}} is non empty V24() V28() countable set
[[5,{}],<*E,v*>] is V21() set
{[5,{}],<*E,v*>} is non empty V24() countable set
{[5,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[5,{}],<*E,v*>},{[5,{}]}} is non empty V24() V28() countable set
R is non empty V67() V92() V93() V94() unital V103() V107() V108() V109() V110() V111() V112() L11()
SCM R is non empty with_non-empty_values IC-Ins-separated strict V154(2) AMI-Struct over 2
the InstructionsF of (SCM R) is Relation-like non empty standard-ins V136() J/A-independent V139() set
the carrier of (SCM R) is non empty set
the carrier of R is non empty set
I is Element of the InstructionsF of (SCM R)
InsCode I is epsilon-transitive epsilon-connected ordinal natural V24() cardinal V39() countable V175() ext-real non negative Element of InsCodes the InstructionsF of (SCM R)
InsCodes the InstructionsF of (SCM R) is non empty set
K51( the InstructionsF of (SCM R)) is set
proj1 the InstructionsF of (SCM R) is non empty set
proj1 (proj1 the InstructionsF of (SCM R)) is set
K41(I) is set
K41(K41(I)) is set
T is Int-like Element of the carrier of (SCM R)
i1 is Int-like Element of the carrier of (SCM R)
T := i1 is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*T,i1*> is set
[1,{},<*T,i1*>] is V21() V22() set
[1,{}] is V21() set
{1,{}} is non empty V24() V28() countable set
{{1,{}},{1}} is non empty V24() V28() countable set
[[1,{}],<*T,i1*>] is V21() set
{[1,{}],<*T,i1*>} is non empty V24() countable set
{[1,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[1,{}],<*T,i1*>},{[1,{}]}} is non empty V24() V28() countable set
j is Int-like Element of the carrier of (SCM R)
k is Int-like Element of the carrier of (SCM R)
AddTo (j,k) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*j,k*> is set
[2,{},<*j,k*>] is V21() V22() set
[2,{}] is V21() set
{2,{}} is non empty V24() V28() countable set
{2} is non empty trivial V24() V28() 1 -element countable set
{{2,{}},{2}} is non empty V24() V28() countable set
[[2,{}],<*j,k*>] is V21() set
{[2,{}],<*j,k*>} is non empty V24() countable set
{[2,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[2,{}],<*j,k*>},{[2,{}]}} is non empty V24() V28() countable set
s1 is Int-like Element of the carrier of (SCM R)
s2 is Int-like Element of the carrier of (SCM R)
SubFrom (s1,s2) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*s1,s2*> is set
[3,{},<*s1,s2*>] is V21() V22() set
[3,{}] is V21() set
{3,{}} is non empty V24() V28() countable set
{3} is non empty trivial V24() V28() 1 -element countable set
{{3,{}},{3}} is non empty V24() V28() countable set
[[3,{}],<*s1,s2*>] is V21() set
{[3,{}],<*s1,s2*>} is non empty V24() countable set
{[3,{}]} is Relation-like Function-like constant non empty trivial V24() 1 -element countable V212() set
{{[3,{}],<*s1,s2*>},{[3,{}]}} is non empty V24() V28() countable set
r is Int-like Element of the carrier of (SCM R)
u is Int-like Element of the carrier of (SCM R)
MultBy (r,u) is V153(2, SCM R) Element of the InstructionsF of (SCM R)
<*r,u*> is set
[4,{},<*r,u*>] is V21() V22() set
[4,{}] is V21() set
{4,{}