let I be Instruction of SCM+FSA; :: according to AMISTD_2:def 19 :: thesis: I is IC-good

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 Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of 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:120;

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

hence I is IC-good by AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

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

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

end;

suppose ex a, b being Int-Location st I = AddTo (a,b) ; :: thesis: I is IC-good

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

end;

suppose ex a, b being Int-Location st I = SubFrom (a,b) ; :: thesis: I is IC-good

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

end;

suppose ex a, b being Int-Location st I = MultBy (a,b) ; :: thesis: I is IC-good

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

end;

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

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

end;

suppose A1: ex i1 being Element of NAT st I = goto i1 ; :: thesis: I is IC-good

let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for b₁ being set holds (IC (Exec (I,b₁))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (b₁,k))))
let s1 be State of SCM+FSA; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))
set s2 = IncrIC (s1,k);
consider i1 being Element of NAT such that
A2: I = goto i1 by A1;
IC (Exec (I,s1)) = i1 by A2, SCMFSA_2:95;
hence (IC (Exec (I,s1))) + k = IC (Exec ((goto (i1 + k)),(IncrIC (s1,k)))) by SCMFSA_2:95
.= IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A2, Th89 ;
:: thesis: verum

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; :: thesis: I is IC-good

then consider a being Int-Location , i1 being Element of NAT such that
A3: I = a =0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for b₁ being set holds (IC (Exec (I,b₁))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (b₁,k))))
let s1 be State of SCM+FSA; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))
set s2 = IncrIC (s1,k);
A5: dom ((IC SCM+FSA) .--> ((IC s1) + k)) = {(IC SCM+FSA)} by FUNCOP_1:19;
a <> IC SCM+FSA by SCMFSA_2:81;
then not a in dom ((IC SCM+FSA) .--> ((IC s1) + k)) by A5, TARSKI:def 1;
then A6: s1 . a = (IncrIC (s1,k)) . a by FUNCT_4:12;

now

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

suppose A7: s1 . a = 0 ; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))

then IC (Exec (I,s1)) = i1 by A3, SCMFSA_2:96;
hence (IC (Exec (I,s1))) + k = IC (Exec ((a =0_goto (i1 + k)),(IncrIC (s1,k)))) by A6, A7, SCMFSA_2:96
.= IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A3, Th90 ;
:: thesis: verum

end;

suppose A8: s1 . a <> 0 ; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))

dom ((IC SCM+FSA) .--> ((IC s1) + k)) = {(IC SCM+FSA)} by FUNCOP_1:19;
then IC SCM+FSA in dom ((IC SCM+FSA) .--> ((IC s1) + k)) by TARSKI:def 1;
then A9: IC (IncrIC (s1,k)) = ((IC SCM+FSA) .--> ((IC s1) + k)) . (IC SCM+FSA) by FUNCT_4:14
.= (IC s1) + k by FUNCOP_1:87 ;
A10: IC (Exec (I,s1)) = succ (IC s1) by A3, A8, SCMFSA_2:96
.= (IC s1) + 1 ;
IC (Exec (I,(IncrIC (s1,k)))) = succ (IC (IncrIC (s1,k))) by A3, A6, A8, SCMFSA_2:96
.= ((IC s1) + k) + 1 by A9 ;
hence (IC (Exec (I,s1))) + k = succ (IC (IncrIC (s1,k))) by A3, A6, A8, A10, SCMFSA_2:96
.= IC (Exec ((a =0_goto (i1 + k)),(IncrIC (s1,k)))) by A6, A8, SCMFSA_2:96
.= IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A3, Th90 ;
:: thesis: verum

end;

end;

end;

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

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; :: thesis: I is IC-good

then consider a being Int-Location , i1 being Element of NAT such that
A11: I = a >0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 18 :: thesis: for b₁ being set holds (IC (Exec (I,b₁))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (b₁,k))))
let s1 be State of SCM+FSA; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))
set s2 = IncrIC (s1,k);
A13: dom ((IC SCM+FSA) .--> ((IC s1) + k)) = {(IC SCM+FSA)} by FUNCOP_1:19;
a <> IC SCM+FSA by SCMFSA_2:81;
then not a in dom ((IC SCM+FSA) .--> ((IC s1) + k)) by A13, TARSKI:def 1;
then A14: s1 . a = (IncrIC (s1,k)) . a by FUNCT_4:12;

now

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

suppose A15: s1 . a > 0 ; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))

then IC (Exec (I,s1)) = i1 by A11, SCMFSA_2:97;
hence (IC (Exec (I,s1))) + k = IC (Exec ((a >0_goto (i1 + k)),(IncrIC (s1,k)))) by A14, A15, SCMFSA_2:97
.= IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A11, Th91 ;
:: thesis: verum

end;

suppose A16: s1 . a <= 0 ; :: thesis: (IC (Exec (I,s1))) + k = IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k))))

dom ((IC SCM+FSA) .--> ((IC s1) + k)) = {(IC SCM+FSA)} by FUNCOP_1:19;
then IC SCM+FSA in dom ((IC SCM+FSA) .--> ((IC s1) + k)) by TARSKI:def 1;
then A17: IC (IncrIC (s1,k)) = ((IC SCM+FSA) .--> ((IC s1) + k)) . (IC SCM+FSA) by FUNCT_4:14
.= (IC s1) + k by FUNCOP_1:87 ;
A18: IC (Exec (I,s1)) = succ (IC s1) by A11, A16, SCMFSA_2:97
.= (IC s1) + 1 ;
IC (Exec (I,(IncrIC (s1,k)))) = succ (IC (IncrIC (s1,k))) by A11, A14, A16, SCMFSA_2:97
.= ((IC s1) + k) + 1 by A17 ;
hence (IC (Exec (I,s1))) + k = succ (IC (IncrIC (s1,k))) by A11, A14, A16, A18, SCMFSA_2:97
.= IC (Exec ((a >0_goto (i1 + k)),(IncrIC (s1,k)))) by A14, A16, SCMFSA_2:97
.= IC (Exec ((IncAddr (I,k)),(IncrIC (s1,k)))) by A11, Th91 ;
:: thesis: verum

end;

end;

end;

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

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := (f,a) ; :: thesis: I is IC-good

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

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = (f,a) := b ; :: thesis: I is IC-good

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

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: I is IC-good

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

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: I is IC-good

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

end;

end;