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