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 EXTPRO_1:def 3 :: 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