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

end;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;

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_{1} being set holds (IC (Exec ((IncAddr (I,j)),b_{1}))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b_{1},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;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

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_{1} being set holds (IC (Exec ((IncAddr (I,j)),b_{1}))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b_{1},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;

end;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

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))))end;

hence
(IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k))))
; :: thesis: verumper cases
( s1 . a = 0 or s1 . a <> 0 )
;

end;

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;.= (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

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;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

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_{1} being set holds (IC (Exec ((IncAddr (I,j)),b_{1}))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b_{1},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;

end;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

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 )
;

end;

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;.= (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

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;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