take
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #)
; ( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Memory & the ZeroF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = NAT & the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-OK & the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-VAL R & the Execution of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Exec R )
thus
( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Memory & the ZeroF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = NAT & the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-OK & the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-VAL R & the Execution of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),SCM-OK,(SCM-VAL R),(SCM-Exec R) #) = SCM-Exec R )
by AMI_2:22, SUBSET_1:def 8; verum