theorem Th18: :: EXTPRO_1:18

for N being non empty with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting 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 st P halts_at IC (Comput (P,s,k)) holds
Result (P,s) = Comput (P,s,k)