let i be Instruction of SCM+FSA; :: thesis: for s, t being State of SCM+FSA st s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t holds
( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
let s, t be State of SCM+FSA; :: thesis: ( s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t implies ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) )
assume that
A1: s | (UsedIntLoc i) = t | (UsedIntLoc i) and
A2: s | (UsedInt*Loc i) = t | (UsedInt*Loc i) and
A3: IC s = IC t ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
set UFi = UsedInt*Loc i;
set Ui = UsedIntLoc i;
set Et = Exec (i,t);
set Es = Exec (i,s);
A4: dom (Exec (i,s)) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (Exec (i,t)) by PARTFUN1:def 2 ;
A7: InsCode i <= 12 by SCMFSA_2:16;

per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A7, NAT_1:36;

suppose InsCode i = 0 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then A8: i = halt SCM+FSA by SCMFSA_2:95;
then Exec (i,s) = s by EXTPRO_1:def 3;
hence ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) by A1, A2, A3, A8, EXTPRO_1:def 3; :: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location such that
A9: i = a := b by SCMFSA_2:30;
A10: UsedIntLoc i = {a,b} by A9, Th18;
then A11: b in UsedIntLoc i by TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A12: s . b = t . b by A1, A11, FUNCT_1:49;
thus IC (Exec (i,s)) = succ (IC t) by A3, A9, SCMFSA_2:63
.= IC (Exec (i,t)) by A9, SCMFSA_2:63 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
( a = b or a <> b ) ;
then A13: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A9, SCMFSA_2:63;
( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by A9, SCMFSA_2:63;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A10, A12, A13, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A14: UsedInt*Loc i = {} by A9, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A14, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location such that
A15: i = AddTo (a,b) by SCMFSA_2:31;
thus IC (Exec (i,s)) = succ (IC t) by A3, A15, SCMFSA_2:64
.= IC (Exec (i,t)) by A15, SCMFSA_2:64 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A16: UsedIntLoc i = {a,b} by A15, Th18;
then A17: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A18: s . a = t . a by A1, A17, FUNCT_1:49;

A19: now

per cases ( a = b or a <> b ) ;

case a = b ; :: thesis: ( (Exec (i,s)) . b = (s . a) + (s . b) & (Exec (i,t)) . b = (t . a) + (t . b) )

hence ( (Exec (i,s)) . b = (s . a) + (s . b) & (Exec (i,t)) . b = (t . a) + (t . b) ) by A15, SCMFSA_2:64; :: thesis: verum

end;

case a <> b ; :: thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b )

hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A15, SCMFSA_2:64; :: thesis: verum

end;

end;

end;

A20: b in UsedIntLoc i by A16, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A21: s . b = t . b by A1, A20, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by A15, SCMFSA_2:64;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A16, A18, A21, A19, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A22: UsedInt*Loc i = {} by A15, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A22, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location such that
A23: i = SubFrom (a,b) by SCMFSA_2:32;
thus IC (Exec (i,s)) = succ (IC t) by A3, A23, SCMFSA_2:65
.= IC (Exec (i,t)) by A23, SCMFSA_2:65 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A24: UsedIntLoc i = {a,b} by A23, Th18;
then A25: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A26: s . a = t . a by A1, A25, FUNCT_1:49;

A27: now

per cases ( a = b or a <> b ) ;

case a = b ; :: thesis: ( (Exec (i,s)) . b = (s . a) - (s . b) & (Exec (i,t)) . b = (t . a) - (t . b) )

hence ( (Exec (i,s)) . b = (s . a) - (s . b) & (Exec (i,t)) . b = (t . a) - (t . b) ) by A23, SCMFSA_2:65; :: thesis: verum

end;

case a <> b ; :: thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b )

hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A23, SCMFSA_2:65; :: thesis: verum

end;

end;

end;

A28: b in UsedIntLoc i by A24, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A29: s . b = t . b by A1, A28, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by A23, SCMFSA_2:65;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A24, A26, A29, A27, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A30: UsedInt*Loc i = {} by A23, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A30, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location such that
A31: i = MultBy (a,b) by SCMFSA_2:33;
thus IC (Exec (i,s)) = succ (IC t) by A3, A31, SCMFSA_2:66
.= IC (Exec (i,t)) by A31, SCMFSA_2:66 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A32: UsedIntLoc i = {a,b} by A31, Th18;
then A33: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A34: s . a = t . a by A1, A33, FUNCT_1:49;

A35: now

per cases ( a = b or a <> b ) ;

case a = b ; :: thesis: ( (Exec (i,s)) . b = (s . a) * (s . b) & (Exec (i,t)) . b = (t . a) * (t . b) )

hence ( (Exec (i,s)) . b = (s . a) * (s . b) & (Exec (i,t)) . b = (t . a) * (t . b) ) by A31, SCMFSA_2:66; :: thesis: verum

end;

case a <> b ; :: thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b )

hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A31, SCMFSA_2:66; :: thesis: verum

end;

end;

end;

A36: b in UsedIntLoc i by A32, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A37: s . b = t . b by A1, A36, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by A31, SCMFSA_2:66;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A32, A34, A37, A35, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A38: UsedInt*Loc i = {} by A31, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A38, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location such that
A39: i = Divide (a,b) by SCMFSA_2:34;
A40: UsedIntLoc i = {a,b} by A39, Th18;
then A41: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A42: s . a = t . a by A1, A41, FUNCT_1:49;
A43: UsedInt*Loc i = {} by A39, Th36;
A44: b in UsedIntLoc i by A40, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A45: s . b = t . b by A1, A44, FUNCT_1:49;

hereby :: thesis: verum

per cases ( a = b or a <> b ) ;

suppose A46: a = b ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

hence IC (Exec (i,s)) = succ (IC t) by A3, A39, SCMFSA_2:68
.= IC (Exec (i,t)) by A39, A46, SCMFSA_2:68 ;
:: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
( (Exec (i,s)) . a = (s . a) mod (s . a) & (Exec (i,t)) . a = (t . a) mod (t . b) ) by A39, A46, SCMFSA_2:68;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A40, A42, A46, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A43, RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A43, RELAT_1:81 ; :: thesis: verum

end;

suppose A47: a <> b ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

thus IC (Exec (i,s)) = succ (IC t) by A3, A39, SCMFSA_2:67
.= IC (Exec (i,t)) by A39, SCMFSA_2:67 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A48: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by A39, SCMFSA_2:67;
( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by A39, A47, SCMFSA_2:67;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A40, A42, A45, A48, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A43, RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A43, RELAT_1:81 ; :: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 6 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider l being Element of NAT such that
A49: i = goto l by SCMFSA_2:35;
thus IC (Exec (i,s)) = l by A49, SCMFSA_2:69
.= IC (Exec (i,t)) by A49, SCMFSA_2:69 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A50: UsedIntLoc i = {} by A49, Th19;
hence (Exec (i,s)) | (UsedIntLoc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedIntLoc i) by A50, RELAT_1:81 ;
:: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A51: UsedInt*Loc i = {} by A49, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A51, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider l being Element of NAT , a being Int-Location such that
A52: i = a =0_goto l by SCMFSA_2:36;
A53: UsedIntLoc i = {a} by A52, Th20;
then A54: a in UsedIntLoc i by TARSKI:def 1;
then A55: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A56: s . a = t . a by A1, A54, FUNCT_1:49;

hereby :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

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

suppose A57: s . a = 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = l by A52, SCMFSA_2:70
.= IC (Exec (i,t)) by A52, A56, A57, SCMFSA_2:70 ;
:: thesis: verum

end;

suppose A58: s . a <> 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = succ (IC s) by A52, SCMFSA_2:70
.= IC (Exec (i,t)) by A3, A52, A56, A58, SCMFSA_2:70 ;
:: thesis: verum

end;

end;

end;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A52, SCMFSA_2:70;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A53, A54, A55, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A59: UsedInt*Loc i = {} by A52, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A59, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider l being Element of NAT , a being Int-Location such that
A60: i = a >0_goto l by SCMFSA_2:37;
A61: UsedIntLoc i = {a} by A60, Th20;
then A62: a in UsedIntLoc i by TARSKI:def 1;
then A63: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A64: s . a = t . a by A1, A62, FUNCT_1:49;

hereby :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

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

suppose A65: s . a > 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = l by A60, SCMFSA_2:71
.= IC (Exec (i,t)) by A60, A64, A65, SCMFSA_2:71 ;
:: thesis: verum

end;

suppose A66: s . a <= 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = succ (IC s) by A60, SCMFSA_2:71
.= IC (Exec (i,t)) by A3, A60, A64, A66, SCMFSA_2:71 ;
:: thesis: verum

end;

end;

end;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A60, SCMFSA_2:71;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A61, A62, A63, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A67: UsedInt*Loc i = {} by A60, Th36;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A67, RELAT_1:81 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location , f being FinSeq-Location such that
A68: i = b := (f,a) by SCMFSA_2:38;
A69: UsedIntLoc i = {a,b} by A68, Th21;
then A70: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A71: s . a = t . a by A1, A70, FUNCT_1:49;
thus IC (Exec (i,s)) = succ (IC t) by A3, A68, SCMFSA_2:72
.= IC (Exec (i,t)) by A68, SCMFSA_2:72 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A72: UsedInt*Loc i = {f} by A68, Th37;
then A73: f in UsedInt*Loc i by TARSKI:def 1;
then A74: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
A75: ( ex m being Element of NAT st
( m = abs (s . a) & (Exec (i,s)) . b = (s . f) /. m ) & ex n being Element of NAT st
( n = abs (t . a) & (Exec (i,t)) . b = (t . f) /. n ) ) by A68, SCMFSA_2:72;

A76: now

per cases ( a = b or a <> b ) ;

case a = b ; :: thesis: (Exec (i,s)) . b = (Exec (i,t)) . b

thus (Exec (i,s)) . b = (Exec (i,t)) . b by A2, A73, A74, A71, A75, FUNCT_1:49; :: thesis: verum

end;

case a <> b ; :: thesis: ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a )

hence ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A68, SCMFSA_2:72; :: thesis: verum

end;

end;

end;

s . f = t . f by A2, A73, A74, FUNCT_1:49;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A69, A71, A75, A76, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by A68, SCMFSA_2:72;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A72, A73, A74, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a, b being Int-Location , f being FinSeq-Location such that
A77: i = (f,a) := b by SCMFSA_2:39;
thus IC (Exec (i,s)) = succ (IC t) by A3, A77, SCMFSA_2:73
.= IC (Exec (i,t)) by A77, SCMFSA_2:73 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A78: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by A77, SCMFSA_2:73;
A79: UsedIntLoc i = {a,b} by A77, Th21;
then A80: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A81: s . a = t . a by A1, A80, FUNCT_1:49;
A82: b in UsedIntLoc i by A79, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A83: s . b = t . b by A1, A82, FUNCT_1:49;
A84: UsedInt*Loc i = {f} by A77, Th37;
then A85: f in UsedInt*Loc i by TARSKI:def 1;
then s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
then A86: s . f = t . f by A2, A85, FUNCT_1:49;
( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by A77, SCMFSA_2:73;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A79, A81, A83, A78, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
( ex m being Element of NAT st
( m = abs (s . a) & (Exec (i,s)) . f = (s . f) +* (m,(s . b)) ) & ex n being Element of NAT st
( n = abs (t . a) & (Exec (i,t)) . f = (t . f) +* (n,(t . b)) ) ) by A77, SCMFSA_2:73;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A84, A81, A83, A86, GRFUNC_1:29; :: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a being Int-Location , f being FinSeq-Location such that
A87: i = a :=len f by SCMFSA_2:40;
thus IC (Exec (i,s)) = succ (IC t) by A3, A87, SCMFSA_2:74
.= IC (Exec (i,t)) by A87, SCMFSA_2:74 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A88: (Exec (i,t)) . a = len (t . f) by A87, SCMFSA_2:74;
A89: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by A87, Th22, SCMFSA_2:74;
A90: UsedInt*Loc i = {f} by A87, Th38;
then A91: f in UsedInt*Loc i by TARSKI:def 1;
then A92: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
then s . f = t . f by A2, A91, FUNCT_1:49;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A89, A88, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by A87, SCMFSA_2:74;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A90, A91, A92, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

then consider a being Int-Location , f being FinSeq-Location such that
A93: i = f :=<0,...,0> a by SCMFSA_2:41;
thus IC (Exec (i,s)) = succ (IC t) by A3, A93, SCMFSA_2:75
.= IC (Exec (i,t)) by A93, SCMFSA_2:75 ; :: thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
A94: UsedIntLoc i = {a} by A93, Th22;
then A95: a in UsedIntLoc i by TARSKI:def 1;
then A96: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
A97: ( UsedInt*Loc i = {f} & ex m being Element of NAT st
( m = abs (s . a) & (Exec (i,s)) . f = m |-> 0 ) ) by A93, Th38, SCMFSA_2:75;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A93, SCMFSA_2:75;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A94, A95, A96, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A98: ex n being Element of NAT st
( n = abs (t . a) & (Exec (i,t)) . f = n |-> 0 ) by A93, SCMFSA_2:75;
s . a = t . a by A1, A95, A96, FUNCT_1:49;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A97, A98, GRFUNC_1:29; :: thesis: verum

end;

end;