( (halt SCM) `1_3 = 0 & ( for a, b being Data-Location holds (a := b) `1_3 = 1 ) & ( for a, b being Data-Location holds (AddTo (a,b)) `1_3 = 2 ) & ( for a, b being Data-Location holds (SubFrom (a,b)) `1_3 = 3 ) & ( for a, b being Data-Location holds (MultBy (a,b)) `1_3 = 4 ) & ( for a, b being Data-Location holds (Divide (a,b)) `1_3 = 5 ) & ( for i being Element of NAT holds (SCM-goto i) `1_3 = 6 ) & ( for a being Data-Location
for i being Element of NAT holds (a =0_goto i) `1_3 = 7 ) & ( for a being Data-Location
for i being Element of NAT holds (a >0_goto i) `1_3 = 8 ) ) by AMI_3:26;