REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)
K32(REAL) is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K32(NAT) is set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
Segm 9 is Element of K32(NAT)
K193() is set
SCM-Memory is set
K32(SCM-Memory) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
K33(SCM-Memory,2) is set
K32(K33(SCM-Memory,2)) is set
SCM-OK is Function-like V29( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like total set
SCM-OK * SCM-VAL is Relation-like set
K182((SCM-OK * SCM-VAL)) is set
K194() is non empty set
K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL))) is set
K33(K194(),K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))) is set
K32(K33(K194(),K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL))))) is set
K32(NAT) is set
INT is set
K193() \/ INT is set
SCM-Data-Loc is Element of K32(SCM-Memory)
SCM-Data-Loc \/ INT is set
SCMPDS-Instr is set
K33(SCMPDS-Instr,K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))) is set
K32(K33(SCMPDS-Instr,K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL))))) is set
SCMPDS is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the carrier of SCMPDS is non empty set
the InstructionsF of SCMPDS is non empty Relation-like V72() V73() V74() V76() set
K335(2,SCMPDS) is Relation-like non-empty the carrier of SCMPDS -defined Function-like total set
the Object-Kind of SCMPDS is Function-like V29( the carrier of SCMPDS,2) Element of K32(K33( the carrier of SCMPDS,2))
K33( the carrier of SCMPDS,2) is set
K32(K33( the carrier of SCMPDS,2)) is set
the U7 of SCMPDS is Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS * the U7 of SCMPDS is Relation-like set
SCM is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
K388(NAT,SCM-Memory) is Element of SCM-Memory
SCM-Exec is Function-like V29(K194(),K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))) Element of K32(K33(K194(),K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))))
AMI-Struct(# SCM-Memory,K388(NAT,SCM-Memory),K194(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the InstructionsF of SCM is non empty Relation-like V72() V73() V74() V76() set
the carrier of SCM is non empty set
K335(2,SCM) is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Function-like V29( the carrier of SCM,2) Element of K32(K33( the carrier of SCM,2))
K33( the carrier of SCM,2) is set
K32(K33( the carrier of SCM,2)) is set
the U7 of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the U7 of SCM is Relation-like set
RAT is set
{} is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
K247() is Function-like V29( SCMPDS-Instr ,K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))) Element of K32(K33(SCMPDS-Instr,K162(K182((SCM-OK * SCM-VAL)),K182((SCM-OK * SCM-VAL)))))
AMI-Struct(# SCM-Memory,K388(NAT,SCM-Memory),SCMPDS-Instr,SCM-OK,SCM-VAL,K247() #) is strict AMI-Struct over 2
IC is V57( SCMPDS ) Element of the carrier of SCMPDS
RetIC is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
RetSP is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
NonZero SCMPDS is Element of K32( the carrier of SCMPDS)
K32( the carrier of SCMPDS) is set
{0} is Element of K32(NAT)
i00 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
dl. i00 is Int-like Element of the carrier of SCM
[1,i00] is set
i00 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
DataLoc (i00,i01) is Int-like Element of the carrier of SCMPDS
i00 + i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((i00 + i01)) is Int-like Element of the carrier of SCMPDS
dl. (i00 + i01) is Int-like Element of the carrier of SCM
[1,(i00 + i01)] is set
abs (i00 + i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
[1,(abs (i00 + i01))] is Element of K33(NAT,NAT)
K33(NAT,NAT) is set
[1,(i00 + i01)] is Element of K33(NAT,NAT)
i00 is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
IC i00 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i00 . (IC ) is set
i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i02 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i01 + i02 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
- i02 is V24() V25() integer ext-real set
ICplusConst (i00,(- i02)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i03 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i03 + (- i02) is V24() V25() integer ext-real set
abs (i03 + (- i02)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(0) is Int-like Element of the carrier of SCMPDS
dl. 0 is Int-like Element of the carrier of SCM
[1,0] is set
(1) is Int-like Element of the carrier of SCMPDS
dl. 1 is Int-like Element of the carrier of SCM
[1,1] is set
() is Int-like Element of the carrier of SCMPDS
() is Int-like Element of the carrier of SCMPDS
i00 is Element of the InstructionsF of SCMPDS
i01 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
i01 ';' i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card (i01 ';' i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (i01 ';' i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card i01) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Load i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
i01 ';' (Load i00) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card (i01 ';' (Load i00)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (i01 ';' (Load i00)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card (Load i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (Load i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card i01) + (card (Load i00)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i00 is Element of the InstructionsF of SCMPDS
i01 is Element of the InstructionsF of SCMPDS
i00 ';' i01 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card (i00 ';' i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (i00 ';' i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
Load i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
Load i01 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
(Load i00) ';' (Load i01) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card ((Load i00) ';' (Load i01)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((Load i00) ';' (Load i01)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card (Load i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (Load i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card (Load i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (Load i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (Load i00)) + (card (Load i01)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
1 + (card (Load i01)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i00 is Element of the InstructionsF of SCMPDS
i01 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
i01 ';' i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(i01 ';' i00) . (card i01) is set
dom (i01 ';' i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
Load i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
dom (Load i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
0 + (card i01) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(i01 ';' i00) . (0 + (card i01)) is set
i01 ';' (Load i00) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(i01 ';' (Load i00)) . (0 + (card i01)) is set
(Load i00) . 0 is set
card (i01 ';' i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(card i01) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
i00 is Element of the InstructionsF of SCMPDS
i01 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
i01 ';' i00 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom i01 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
i02 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(i01 ';' i00) ';' i02 is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((i01 ';' i00) ';' i02) . (card i01) is set
dom (i01 ';' i00) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(i01 ';' i00) . (card i01) is set
() := 0 is Element of the InstructionsF of SCMPDS
() := 7 is Element of the InstructionsF of SCMPDS
(() := 0) ';' (() := 7) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
saveIC ((),RetIC) is Element of the InstructionsF of SCMPDS
((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
goto 2 is Element of the InstructionsF of SCMPDS
(((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
halt SCMPDS is Element of the InstructionsF of SCMPDS
((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((),3) <=0_goto 9 is Element of the InstructionsF of SCMPDS
(((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((),6) := ((),3) is Element of the InstructionsF of SCMPDS
((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
Divide ((),2,(),3) is Element of the InstructionsF of SCMPDS
(((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((),7) := ((),3) is Element of the InstructionsF of SCMPDS
((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
4 + RetSP is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((),(4 + RetSP)) := ((),1) is Element of the InstructionsF of SCMPDS
(((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
AddTo ((),1,4) is Element of the InstructionsF of SCMPDS
((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
- 7 is V24() V25() integer ext-real set
goto (- 7) is Element of the InstructionsF of SCMPDS
((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((),2) := ((),6) is Element of the InstructionsF of SCMPDS
(((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
return () is Element of the InstructionsF of SCMPDS
((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) ';' (return ()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
() is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
card () is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom () is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
15 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
card (((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card ((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((() := 0) ';' (() := 7)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((() := 0) ';' (() := 7)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((() := 0) ';' (() := 7))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card ((() := 0) ';' (() := 7))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((card ((() := 0) ';' (() := 7))) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(2 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((2 + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card (((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((card (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3)))) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9))) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((((card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9))) + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
5 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(5 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((5 + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((5 + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((((5 + 1) + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
10 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
card ((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((card ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC)))) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4)))) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4)))) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((((card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4)))) + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
10 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(10 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((10 + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((10 + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((((10 + 1) + 1) + 1) + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
() . 0 is set
() . 1 is set
() . 2 is set
() . 3 is set
() . 4 is set
() . 5 is set
() . 6 is set
() . 7 is set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 8 is set
() . 9 is set
10 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 10 is set
11 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 11 is set
12 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 12 is set
13 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 13 is set
14 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real positive Element of NAT
() . 14 is set
card ((() := 0) ';' (() := 7)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((() := 0) ';' (() := 7)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
card (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
3 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
4 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
5 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
6 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
7 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
8 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
9 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
10 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
11 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
12 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
card ((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom ((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
13 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(((),2) := ((),6)) ';' (return ()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(saveIC ((),RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(() := 7) ';' ((saveIC ((),RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' ((((),2) := ((),6)) ';' (return ())) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((() := 0) ';' (() := 7)) ';' ((saveIC ((),RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
(() := 0) ';' ((() := 7) ';' ((saveIC ((),RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ())))))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
Load (() := 0) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
card (Load (() := 0)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom (Load (() := 0)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(Load (() := 0)) ';' (() := 7) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
((Load (() := 0)) ';' (() := 7)) ';' ((saveIC ((),RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' ((((),3) <=0_goto 9) ';' ((((),6) := ((),3)) ';' ((Divide ((),2,(),3)) ';' ((((),7) := ((),3)) ';' ((((),(4 + RetSP)) := ((),1)) ';' ((AddTo ((),1,4)) ';' ((saveIC ((),RetIC)) ';' ((goto (- 7)) ';' ((((),2) := ((),6)) ';' (return ()))))))))))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
Load (return ()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() 1 -element V71() set
((((((((((((((() := 0) ';' (() := 7)) ';' (saveIC ((),RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((),3) <=0_goto 9)) ';' (((),6) := ((),3))) ';' (Divide ((),2,(),3))) ';' (((),7) := ((),3))) ';' (((),(4 + RetSP)) := ((),1))) ';' (AddTo ((),1,4))) ';' (saveIC ((),RetIC))) ';' (goto (- 7))) ';' (((),2) := ((),6))) ';' (Load (return ())) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V32() V71() set
p is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
p . 0 is Element of the InstructionsF of SCMPDS
p . 1 is Element of the InstructionsF of SCMPDS
p . 2 is Element of the InstructionsF of SCMPDS
p . 3 is Element of the InstructionsF of SCMPDS
p . 4 is Element of the InstructionsF of SCMPDS
p . 5 is Element of the InstructionsF of SCMPDS
p . 6 is Element of the InstructionsF of SCMPDS
p . 7 is Element of the InstructionsF of SCMPDS
p . 8 is Element of the InstructionsF of SCMPDS
p . 9 is Element of the InstructionsF of SCMPDS
p . 10 is Element of the InstructionsF of SCMPDS
p . 11 is Element of the InstructionsF of SCMPDS
p . 12 is Element of the InstructionsF of SCMPDS
p . 13 is Element of the InstructionsF of SCMPDS
p . 14 is Element of the InstructionsF of SCMPDS
7 + RetIC is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((7 + RetIC)) is Int-like Element of the carrier of SCMPDS
dl. (7 + RetIC) is Int-like Element of the carrier of SCM
[1,(7 + RetIC)] is set
(9) is Int-like Element of the carrier of SCMPDS
dl. 9 is Int-like Element of the carrier of SCM
[1,9] is set
(10) is Int-like Element of the carrier of SCMPDS
dl. 10 is Int-like Element of the carrier of SCM
[1,10] is set
p is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
x is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total 0 -started set
Comput (p,x,4) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
IC (Comput (p,x,4)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (p,x,4)) . (IC ) is set
(Comput (p,x,4)) . () is V24() V25() integer ext-real set
(Comput (p,x,4)) . () is V24() V25() integer ext-real set
(Comput (p,x,4)) . ((7 + RetIC)) is V24() V25() integer ext-real set
(Comput (p,x,4)) . (9) is V24() V25() integer ext-real set
x . (9) is V24() V25() integer ext-real set
(Comput (p,x,4)) . (10) is V24() V25() integer ext-real set
x . (10) is V24() V25() integer ext-real set
IC x is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
x . (IC ) is set
p /. (IC x) is Element of the InstructionsF of SCMPDS
p . (IC x) is Element of the InstructionsF of SCMPDS
Comput (p,x,1) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
IC (Comput (p,x,1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (p,x,1)) . (IC ) is set
p /. (IC (Comput (p,x,1))) is Element of the InstructionsF of SCMPDS
p . (IC (Comput (p,x,1))) is Element of the InstructionsF of SCMPDS
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Comput (p,x,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Comput (p,x,0) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Following (p,(Comput (p,x,0))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
CurInstr (p,(Comput (p,x,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (p,x,0)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (p,x,0)) . (IC ) is set
p /. (IC (Comput (p,x,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (p,(Comput (p,x,0)))),(Comput (p,x,0))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is set
K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Function-like V29( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is set
K32(K33( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,0))))) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,0))))) . (Comput (p,x,0)) is set
Following (p,x) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
CurInstr (p,x) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (p,x)),x) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,x))) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,x))) . x is set
Exec ((() := 0),x) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(() := 0)) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(() := 0)) . x is set
succ (IC x) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real set
CurInstr (p,(Comput (p,x,1))) is Element of the InstructionsF of SCMPDS
p . 1 is Element of the InstructionsF of SCMPDS
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Comput (p,x,(1 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Following (p,(Comput (p,x,1))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Exec ((CurInstr (p,(Comput (p,x,1)))),(Comput (p,x,1))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,1))))) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,1))))) . (Comput (p,x,1)) is set
Exec ((() := 7),(Comput (p,x,1))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(() := 7)) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(() := 7)) . (Comput (p,x,1)) is set
(Comput (p,x,1)) . () is V24() V25() integer ext-real set
(Comput (p,x,1)) . (9) is V24() V25() integer ext-real set
(Comput (p,x,1)) . (10) is V24() V25() integer ext-real set
Comput (p,x,2) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
IC (Comput (p,x,2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (p,x,2)) . (IC ) is set
p /. (IC (Comput (p,x,2))) is Element of the InstructionsF of SCMPDS
p . (IC (Comput (p,x,2))) is Element of the InstructionsF of SCMPDS
succ (IC (Comput (p,x,1))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer V64() ext-real set
CurInstr (p,(Comput (p,x,2))) is Element of the InstructionsF of SCMPDS
p . 2 is Element of the InstructionsF of SCMPDS
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Comput (p,x,(2 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Following (p,(Comput (p,x,2))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
Exec ((CurInstr (p,(Comput (p,x,2)))),(Comput (p,x,2))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,2))))) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (p,(Comput (p,x,2))))) . (Comput (p,x,2)) is set
Exec ((saveIC ((),RetIC)),(Comput (p,x,2))) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(saveIC ((),RetIC))) is Element of K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K164( the InstructionsF of SCMPDS,K162(K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K182(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(saveIC ((),RetIC))) . (Comput (p,x,2)) is set
(Comput (p,x,2)) . () is V24() V25() integer ext-real set
(Comput (p,x,2)) . () is V24() V25() integer ext-real set
(Comput (p,x,2)) . (9) is V24() V25() integer ext-real set
(Comput (p,x,2)) . (10) is V24() V25() integer ext-real set
Comput (p,x,3) is Relation-like the carrier of SCMPDS -defined Function-like K335(2,SCMPDS) -compatible total set
IC (Comput (p,x,3)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (p,x,3)) . (IC ) is set
p /. (IC (Comput (p,x,3))) is Element of the InstructionsF of SCMPDS
p . (IC (Comput (p,x,3))) is Element of the InstructionsF of SCMPDS
succ (IC (Comput (p,x,2))) is non empty epsilon-transitive epsilon-connected ordinal nat