let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for i being Element of the InstructionsF of T holds (il. (T,0)) .--> i is lower
let i be Element of the InstructionsF of T; :: thesis: (il. (T,0)) .--> i is lower
set F = (il. (T,0)) .--> i;
let l be Element of NAT ; :: according to AMI_WSTD:def 10 :: thesis: ( l in dom ((il. (T,0)) .--> i) implies for m being Element of NAT st m <= l,T holds
m in dom ((il. (T,0)) .--> i) )
assume A1: l in dom ((il. (T,0)) .--> i) ; :: thesis: for m being Element of NAT st m <= l,T holds
m in dom ((il. (T,0)) .--> i)
let m be Element of NAT ; :: thesis: ( m <= l,T implies m in dom ((il. (T,0)) .--> i) )
assume A2: m <= l,T ; :: thesis: m in dom ((il. (T,0)) .--> i)
consider k being Nat such that
A3: m = il. (T,k) by Th6;
A4: l = il. (T,0) by A1, TARSKI:def 1;
then ( 0 <= k & k <= 0 ) by A2, A3, Th8;
hence m in dom ((il. (T,0)) .--> i) by A1, A4, A3, XXREAL_0:1; :: thesis: verum