let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Input I is empty
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of 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 Th20
.= {} ;
hence Input I is empty ; :: thesis: verum