thus SCM is IC-relocable :: thesis: verum

proof

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

per cases ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k being Nat st I = a =0_goto k or ex a being Data-Location ex k being Nat st I = a >0_goto k ) by AMI_3:24;

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

hence I is IC-relocable by AMI_3:26; :: thesis: verum

end;

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

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

end;

suppose ex a, b being Data-Location 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 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 st I = MultBy (a,b) ; :: thesis: I is IC-relocable

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

end;

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

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

end;

suppose A1: ex k being Nat st I = SCM-goto k ; :: 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; :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
set s2 = IncIC (s1,k);
consider k1 being Nat such that
A2: I = SCM-goto k1 by A1;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((SCM-goto (j + k1)),s1))) + k by A2, Th23
.= (j + k1) + k by AMI_3:7
.= IC (Exec ((SCM-goto ((j + i1) + k)),(IncIC (s1,k)))) by AMI_3:7
.= IC (Exec ((SCM-goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th23 ; :: thesis: verum

end;

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

then consider a being Data-Location, k1 being Nat such that
A3: I = a =0_goto k1 ;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;
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; :: 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 AMI_5:2;
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;

now :: thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))

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

suppose A5: s1 . a = 0 ; :: 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 + k1)),s1))) + k by A3, Th24
.= (j + k1) + k by A5, AMI_3:8
.= IC (Exec ((a =0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A4, A5, AMI_3:8
.= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th24 ; :: thesis: verum

end;

suppose A6: s1 . a <> 0 ; :: 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, Th24;
A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th24;
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, AMI_3:8
.= ((IC s1) + 1) + k
.= (IC (IncIC (s1,k))) + 1 by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, AMI_3:8 ; :: thesis: verum

end;

end;

end;

hence (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) ; :: thesis: verum

end;

suppose ex a being Data-Location ex k being Nat st I = a >0_goto k ; :: thesis: I is IC-relocable

then consider a being Data-Location, k1 being Nat such that
A10: I = a >0_goto k1 ;
reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;
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; :: 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 AMI_5:2;
then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A11: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11;

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

suppose A12: s1 . a > 0 ; :: 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 + k1)),s1))) + k by A10, Th25
.= (j + k1) + k by A12, AMI_3:9
.= IC (Exec ((a >0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A11, A12, AMI_3:9
.= IC (Exec ((a >0_goto ((j + k) + i1)),(IncIC (s1,k))))
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A10, Th25 ; :: thesis: verum

end;

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

A14: IncAddr (I,j) = a >0_goto (i1 + j) by A10, Th25;
A15: IncAddr (I,(j + k)) = a >0_goto (i1 + (j + k)) by A10, Th25;
IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A16: 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 A14, A13, AMI_3:9
.= ((IC s1) + 1) + k
.= (IC (IncIC (s1,k))) + 1 by A16
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A15, A13, A11, AMI_3:9 ; :: thesis: verum

end;

end;

end;

end;

end;