let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_\_Inp I is empty
let A be non empty IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct of N; :: thesis: for I being Instruction of A st I is halting holds
Out_\_Inp I is empty
let I be Instruction of A; :: thesis: ( I is halting implies Out_\_Inp I is empty )
assume A1: I is halting ; :: thesis: Out_\_Inp I is empty
Out_\_Inp I c= Output I by Th10;
then Out_\_Inp I c= {} by A1, Th18;
hence Out_\_Inp I is empty by XBOOLE_1:3; :: thesis: verum