let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k) c= Relocated g,k
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k) c= Relocated g,k
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k) c= Relocated g,k
let g be FinPartState of S; :: thesis: ( S is realistic implies Start-At ((IC g) + k) c= Relocated g,k )
assume A1: S is realistic ; :: thesis: Start-At ((IC g) + k) c= Relocated g,k
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in Start-At ((IC g) + k) or [x,b₁] in Relocated g,k )
A2: Start-At ((IC g) + k) = {[(IC S),((IC g) + k)]} by FUNCT_4:87;
A3: IC S in dom (Relocated g,k) by Th51;
A4: IC (Relocated g,k) = (IC g) + k by A1, Th52;
IC (Relocated g,k) = (Relocated g,k) . (IC S) by A3, AMI_1:def 43;
then [(IC S),((IC g) + k)] in Relocated g,k by A3, A4, FUNCT_1:def 4;
hence for b₁ being set holds
( not [x,b₁] in Start-At ((IC g) + k) or [x,b₁] in Relocated g,k ) by A2, TARSKI:def 1; :: thesis: verum