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;