let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N holds S is programmable
let IL be non empty set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N holds S is programmable
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: S is programmable
consider l being Instruction-Location of S;
consider I being Instruction of S;
take l .--> I ; :: according to AMI_1:def 27 :: thesis: ( not l .--> I is empty & l .--> I is autonomic )
thus ( not l .--> I is empty & l .--> I is autonomic ) by Lm1; :: thesis: verum