thus SCM R is IC-relocable :: thesis: verum

proof

let I be Instruction of (SCM R); :: according to AMISTD_2:def 4 :: thesis: I is IC-relocable

per cases ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;

suppose I = [0,{},{}] ; :: thesis: I is IC-relocable

then I = halt (SCM R) ;
hence I is IC-relocable ; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = a := b ; :: thesis: I is IC-relocable

hence I is IC-relocable ; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = AddTo (a,b) ; :: thesis: I is IC-relocable

hence I is IC-relocable ; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = SubFrom (a,b) ; :: thesis: I is IC-relocable

hence I is IC-relocable ; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = MultBy (a,b) ; :: thesis: I is IC-relocable

hence I is IC-relocable ; :: thesis: verum

end;

suppose A1: ex i1 being Nat st I = goto (i1,R) ; :: thesis: I is IC-relocable

let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b₁ being set holds (IC (Exec ((IncAddr (I,j)),b₁))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b₁,k))))
let s1 be State of (SCM R); :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
consider i1 being Nat such that
A2: I = goto (i1,R) by A1;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((goto ((j + i1),R)),s1))) + k by A2, Th36
.= (j + i1) + k by SCMRING2:15
.= IC (Exec ((goto (((j + i1) + k),R)),(IncIC (s1,k)))) by SCMRING2:15
.= IC (Exec ((goto (((j + k) + i1),R)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th36 ; :: thesis: verum

end;

suppose ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 ; :: thesis: I is IC-relocable

then consider a being Data-Location of R, i1 being Nat such that
A3: I = a =0_goto i1 ;
let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b₁ being set holds (IC (Exec ((IncAddr (I,j)),b₁))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b₁,k))))
let s1 be State of (SCM R); :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
( a <> IC & dom ((IC ) .--> ((IC s1) + k)) = {(IC )} ) by Th2;
then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A4: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11;

per cases ( s1 . a = 0. R or s1 . a <> 0. R ) ;

suppose A5: s1 . a = 0. R ; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((a =0_goto (j + i1)),s1))) + k by A3, Th37
.= (j + i1) + k by A5, SCMRING2:16
.= IC (Exec ((a =0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A4, A5, SCMRING2:16
.= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th37 ; :: thesis: verum

end;

suppose A6: s1 . a <> 0. R ; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

A7: IncAddr (I,j) = a =0_goto (i1 + j) by A3, Th37;
A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th37;
IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A9: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13
.= (IC s1) + k by FUNCOP_1:72 ;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = ((IC s1) + 1) + k by A7, A6, SCMRING2:16
.= ((IC s1) + 1) + k
.= (IC (IncIC (s1,k))) + 1 by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, SCMRING2:16 ; :: thesis: verum

end;

end;

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis: I is IC-relocable

hence I is IC-relocable ; :: thesis: verum

end;

end;

end;