let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being FinPartState of S
for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let F be FinPartState of S; :: thesis: for k being natural number st k > 0 holds
not il. S,0 in dom (Shift F,k)
let k be natural number ; :: thesis: ( k > 0 implies not il. S,0 in dom (Shift F,k) )
assume that
A1: k > 0 and
A2: il. S,0 in dom (Shift F,k) ; :: thesis: contradiction
dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;
then consider m being Element of NAT such that
A3: il. S,0 = il. S,(m + k) and
il. S,m in dom F by A2;
m + k = 0 by A3, AMISTD_1:25;
hence contradiction by A1; :: thesis: verum