let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A holds
( I is halting iff Output I is empty )
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 EXTPRO_1:def 3 :: 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 ;
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 EXTPRO_1:def 3 :: 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 2;
then ex x being object st
( x in the carrier of A & (Exec (I,s)) . x <> s . x ) by A4, FUNCT_1:2;
hence contradiction by A3, Def3; :: thesis: verum