let I be Instruction of SCM+FSA; :: according to AMISTD_2:def 4 :: thesis: I is IC-relocable
per cases ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex i1 being Nat st I = goto i1 or ex i1 being Nat ex a being Int-Location st I = a =0_goto i1 or ex i1 being Nat ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) or ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:93;
suppose I = [0,{},{}] ; :: thesis: I is IC-relocable
hence I is IC-relocable by SCMFSA_2:96; :: thesis: verum
end;
suppose ex a, b being Int-Location st I = a := b ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a, b being Int-Location st I = AddTo (a,b) ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a, b being Int-Location st I = SubFrom (a,b) ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a, b being Int-Location st I = MultBy (a,b) ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a, b being Int-Location st I = Divide (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 ; :: thesis: I is IC-relocable
let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; :: 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 by A1;
thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((goto (j + i1)),s1))) + k by A2, Th41
.= (j + i1) + k by SCMFSA_2:69
.= IC (Exec ((goto ((j + k) + i1)),(IncIC (s1,k)))) by SCMFSA_2:69
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th41 ; :: thesis: verum
end;
suppose ex i1 being Nat ex a being Int-Location st I = a =0_goto i1 ; :: thesis: I is IC-relocable
then consider a being Int-Location, i1 being Nat such that
A3: I = a =0_goto i1 ;
let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; :: 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 SCMFSA_2:56;
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 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 + i1)),s1))) + k by A3, Th42
.= (j + i1) + k by A5, SCMFSA_2:70
.= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k)))) by A4, A5, SCMFSA_2:70
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th42 ; :: 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, Th42;
A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th42;
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, SCMFSA_2:70
.= (IC (IncIC (s1,k))) + 1 by A9
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, SCMFSA_2:70 ; :: thesis: verum
end;
end;
end;
suppose ex i1 being Nat ex a being Int-Location st I = a >0_goto i1 ; :: thesis: I is IC-relocable
then consider i1 being Nat, a being Int-Location such that
A10: I = a >0_goto i1 ;
let j, k be Nat; :: according to AMISTD_2:def 3 :: thesis: for b1 being set holds (IC (Exec ((IncAddr (I,j)),b1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k))))
let s1 be State of SCM+FSA; :: 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 SCMFSA_2:56;
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 + i1)),s1))) + k by A10, Th43
.= (j + i1) + k by A12, SCMFSA_2:71
.= IC (Exec ((a >0_goto ((j + k) + i1)),(IncIC (s1,k)))) by A11, A12, SCMFSA_2:71
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A10, Th43 ; :: 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, Th43;
A15: IncAddr (I,(j + k)) = a >0_goto (i1 + (j + k)) by A10, Th43;
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, SCMFSA_2:71
.= (IC (IncIC (s1,k))) + 1 by A16
.= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A15, A13, A11, SCMFSA_2:71 ; :: thesis: verum
end;
end;
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: I is IC-relocable
hence I is IC-relocable ; :: thesis: verum
end;
end;