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 holds
( I is halting iff Output 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 holds
( I is halting iff Output I is empty )
let I be Instruction of A; :: thesis: ( I is halting iff Output I is empty )
thus ( I is halting implies Output I is empty ) :: thesis: ( Output I is empty implies I is halting )

proof

assume A1: for s being State of A holds Exec I,s = s ; :: according to AMI_1:def 8 :: thesis: Output I is empty
assume not Output I is empty ; :: thesis: contradiction
then consider o being Object of A such that
A2: o in Output I by SUBSET_1:10;
ex s being State of A st s . o <> (Exec I,s) . o by A2, Def3;
hence contradiction by A1; :: thesis: verum

end;

assume A3: Output I is empty ; :: thesis: I is halting
let s be State of A; :: according to AMI_1:def 8 :: thesis: Exec I,s = s
assume A4: Exec I,s <> s ; :: thesis: contradiction
( dom s = the carrier of A & dom (Exec I,s) = the carrier of A ) by PARTFUN1:def 4;
then ex x being set st
( x in the carrier of A & (Exec I,s) . x <> s . x ) by A4, FUNCT_1:9;
hence contradiction by A3, Def3; :: thesis: verum