take AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(SCM-OK R),(SCM-Exec R) #) ; :: thesis: ( the carrier of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(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),(SCM-OK R),(SCM-Exec R) #) = NAT & the Instructions of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(SCM-OK R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(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),(SCM-OK R),(SCM-Exec R) #) = SCM-Exec R )
thus ( the carrier of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(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),(SCM-OK R),(SCM-Exec R) #) = NAT & the Instructions of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(SCM-Instr R),(SCM-OK R),(SCM-Exec R) #) = SCM-Instr R & the Object-Kind of AMI-Struct(# SCM-Memory ,(In NAT ,SCM-Memory ),(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),(SCM-OK R),(SCM-Exec R) #) = SCM-Exec R ) by AMI_2:30, FUNCT_7:def 1; :: thesis: verum