let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for I being Instruction of A holds
( I is halting iff Output I is empty )
let IL be non empty set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 IL,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
A4: dom s = the carrier of A by AMI_1:79;
A5: dom (Exec I,s) = the carrier of A by AMI_1:79;
assume Exec I,s <> s ; :: thesis: contradiction
then ex x being set st
( x in the carrier of A & (Exec I,s) . x <> s . x ) by A4, A5, FUNCT_1:9;
hence contradiction by A3, Def3; :: thesis: verum