let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k,S),S c= Relocated g,k
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k,S),S c= Relocated g,k
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for g being FinPartState of S st S is realistic holds
Start-At ((IC g) + k,S),S c= Relocated g,k
let g be FinPartState of S; :: thesis: ( S is realistic implies Start-At ((IC g) + k,S),S c= Relocated g,k )
assume A1: S is realistic ; :: thesis: Start-At ((IC g) + k,S),S 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,S),S or [x,b₁] in Relocated g,k )
A2: Start-At ((IC g) + k,S),S = {[(IC S),((IC g) + k,S)]} by FUNCT_4:87;
A3: IC S in dom (Relocated g,k) by Th72;
A4: IC (Relocated g,k) = (IC g) + k,S by A1, Th73;
[(IC S),((IC g) + k,S)] 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,S),S or [x,b₁] in Relocated g,k ) by A2, TARSKI:def 1; :: thesis: verum