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 st I is halting holds
Input 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 st I is halting holds
Input I is empty
let I be Instruction of A; :: thesis: ( I is halting implies Input I is empty )
assume I is halting ; :: thesis: Input I is empty
then Input I = {} \ (Out_\_Inp I) by Th12
.= {} ;
hence Input I is empty ; :: thesis: verum