take AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr R),(In ([0,{},{}],(SCM-Instr R))),(SCM-OK R),(SCM-Exec R) #) ; :: thesis: ( 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 ZeroF 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:18;
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 ZeroF 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:22, FUNCT_7:def 1; :: thesis: verum