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;
A1: dom ((il. T,0 ) .--> i) = {(il. T,0 )} by FUNCOP_1:19;
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 A2: 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)
A3: l = il. T,0 by A1, A2, TARSKI:def 1;
let m be Instruction-Location of T; :: thesis: ( m <= l implies m in dom ((il. T,0 ) .--> i) )
assume A4: m <= l ; :: thesis: m in dom ((il. T,0 ) .--> i)
consider k being natural number such that
A5: m = il. T,k by Th26;
( 0 <= k & k <= 0 ) by A3, A4, A5, Th28, NAT_1:2;
hence m in dom ((il. T,0 ) .--> i) by A2, A3, A5, XXREAL_0:1; :: thesis: verum