take
AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #)
; ( the carrier of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Memory & the Instruction-Counter of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = NAT & the Instructions of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Instr R & the haltF of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = [0 ,{} ,{} ] & the Object-Kind of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-OK R & the Execution of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Exec R )
[0 ,{} ,{} ] in SCM-Instr R
by SCMRING1:22;
hence
( the carrier of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Memory & the Instruction-Counter of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = NAT & the Instructions of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Instr R & the haltF of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = [0 ,{} ,{} ] & the Object-Kind of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-OK R & the Execution of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(In [0 ,{} ,{} ],(SCM-Instr R)),(SCM-OK R),(SCM-Exec R) #) = SCM-Exec R )
by AMI_2:30, FUNCT_7:def 1; verum