let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A st I is halting holds
Out_\_Inp I is empty
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over 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 Th3;
then Out_\_Inp I c= {} by A1, Th10;
hence Out_\_Inp I is empty ; :: thesis: verum