:: SCMRING3 semantic presentation

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,{}