:: deftheorem Def7 defines Comput EXTPRO_1:def 7 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for p being NAT -defined the InstructionsF of b₂ -valued Function
for s being State of S
for k being Nat
for b₆ being State of S holds
( b₆ = Comput (p,s,k) iff ex f being sequence of (product (the_Values_of S)) st
( b₆ = f . k & f . 0 = s & ( for i being Nat holds f . (i + 1) = Following (p,(f . i)) ) ) );