let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for i being Element of the Instructions of T holds (il. T,0 ) .--> i is lower
let i be Element of the Instructions of T; :: thesis: (il. T,0 ) .--> i is lower
set F = (il. T,0 ) .--> i;
let l be Instruction-Location of T; :: according to AMISTD_1:def 20 :: thesis: ( l in dom ((il. T,0 ) .--> i) implies for m being Instruction-Location of T st m <= l holds
m in dom ((il. T,0 ) .--> i) )
assume A1: l in dom ((il. T,0 ) .--> i) ; :: thesis: for m being Instruction-Location of T st m <= l holds
m in dom ((il. T,0 ) .--> i)
let m be Instruction-Location of T; :: thesis: ( m <= l implies m in dom ((il. T,0 ) .--> i) )
assume A2: m <= l ; :: thesis: m in dom ((il. T,0 ) .--> i)
consider k being natural number such that
A3: m = il. T,k by Th26;
dom ((il. T,0 ) .--> i) = {(il. T,0 )} by FUNCOP_1:19;
then A4: l = il. T,0 by A1, TARSKI:def 1;
then ( 0 <= k & k <= 0 ) by A2, A3, Th28, NAT_1:2;
hence m in dom ((il. T,0 ) .--> i) by A1, A4, A3, XXREAL_0:1; :: thesis: verum