let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_U_Inp I is empty
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for I being Instruction of A st I is halting holds
Out_U_Inp I is empty
let I be Instruction of A; :: thesis: ( I is halting implies Out_U_Inp I is empty )
assume A1: for s being State of A holds Exec I,s = s ; :: according to AMI_1:def 8 :: thesis: Out_U_Inp I is empty
assume not Out_U_Inp I is empty ; :: thesis: contradiction
then consider o being Object of A such that
A2: o in Out_U_Inp I by SUBSET_1:10;
consider s being State of A, a being Element of ObjectKind o such that
A3: Exec I,(s +* o,a) <> (Exec I,s) +* o,a by A2, Def5;
Exec I,(s +* o,a) = s +* o,a by A1
.= (Exec I,s) +* o,a by A1 ;
hence contradiction by A3; :: thesis: verum