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 ;
A5: 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 A5, 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 A6: 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, A6, 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
A7: i = a := b by SCMFSA_2:30;
A8: UsedIntLoc i = {a,b} by A7, Th14;
then A9: b in UsedIntLoc i by TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A10: s . b = t . b by A1, A9, FUNCT_1:49;
thus IC (Exec (i,s)) = succ (IC t) by A3, A7, SCMFSA_2:63
.= IC (Exec (i,t)) by A7, 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 A11: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A7, SCMFSA_2:63;
( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by A7, SCMFSA_2:63;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A8, A10, A11, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A12: UsedInt*Loc i = {} by A7, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A12, 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
A13: i = AddTo (a,b) by SCMFSA_2:31;
thus IC (Exec (i,s)) = succ (IC t) by A3, A13, SCMFSA_2:64
.= IC (Exec (i,t)) by A13, 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) )
A14: UsedIntLoc i = {a,b} by A13, Th14;
then A15: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A16: s . a = t . a by A1, A15, FUNCT_1:49;

A17: now :: thesis: ( ( a = b & (Exec (i,s)) . b = (s . a) + (s . b) & (Exec (i,t)) . b = (t . a) + (t . b) ) or ( a <> b & (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) )

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 A13, 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 A13, SCMFSA_2:64; :: thesis: verum

end;

end;

end;

A18: b in UsedIntLoc i by A14, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A19: s . b = t . b by A1, A18, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by A13, SCMFSA_2:64;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A14, A16, A19, A17, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A20: UsedInt*Loc i = {} by A13, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A20, 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
A21: i = SubFrom (a,b) by SCMFSA_2:32;
thus IC (Exec (i,s)) = succ (IC t) by A3, A21, SCMFSA_2:65
.= IC (Exec (i,t)) by A21, 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) )
A22: UsedIntLoc i = {a,b} by A21, Th14;
then A23: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A24: s . a = t . a by A1, A23, FUNCT_1:49;

A25: now :: thesis: ( ( a = b & (Exec (i,s)) . b = (s . a) - (s . b) & (Exec (i,t)) . b = (t . a) - (t . b) ) or ( a <> b & (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) )

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 A21, 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 A21, SCMFSA_2:65; :: thesis: verum

end;

end;

end;

A26: b in UsedIntLoc i by A22, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A27: s . b = t . b by A1, A26, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by A21, SCMFSA_2:65;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A22, A24, A27, A25, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A28: UsedInt*Loc i = {} by A21, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A28, 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
A29: i = MultBy (a,b) by SCMFSA_2:33;
thus IC (Exec (i,s)) = succ (IC t) by A3, A29, SCMFSA_2:66
.= IC (Exec (i,t)) by A29, 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) )
A30: UsedIntLoc i = {a,b} by A29, Th14;
then A31: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A32: s . a = t . a by A1, A31, FUNCT_1:49;

A33: now :: thesis: ( ( a = b & (Exec (i,s)) . b = (s . a) * (s . b) & (Exec (i,t)) . b = (t . a) * (t . b) ) or ( a <> b & (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) )

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 A29, 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 A29, SCMFSA_2:66; :: thesis: verum

end;

end;

end;

A34: b in UsedIntLoc i by A30, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A35: s . b = t . b by A1, A34, FUNCT_1:49;
( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by A29, SCMFSA_2:66;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A30, A32, A35, A33, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A36: UsedInt*Loc i = {} by A29, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A36, 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
A37: i = Divide (a,b) by SCMFSA_2:34;
A38: UsedIntLoc i = {a,b} by A37, Th14;
then A39: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A40: s . a = t . a by A1, A39, FUNCT_1:49;
A41: UsedInt*Loc i = {} by A37, Th32;
A42: b in UsedIntLoc i by A38, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A43: s . b = t . b by A1, A42, FUNCT_1:49;

hereby :: thesis: verum

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

suppose A44: 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, A37, SCMFSA_2:68
.= IC (Exec (i,t)) by A37, A44, 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 A37, A44, SCMFSA_2:68;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A38, A40, A44, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A41, RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A41, RELAT_1:81 ; :: thesis: verum

end;

suppose A45: 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, A37, SCMFSA_2:67
.= IC (Exec (i,t)) by A37, 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) )
A46: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by A37, SCMFSA_2:67;
( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by A37, A45, SCMFSA_2:67;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A38, A40, A43, 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 A41, RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A41, 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
A47: i = goto l by SCMFSA_2:35;
thus IC (Exec (i,s)) = l by A47, SCMFSA_2:69
.= IC (Exec (i,t)) by A47, 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) )
A48: UsedIntLoc i = {} by A47, Th15;
hence (Exec (i,s)) | (UsedIntLoc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedIntLoc i) by A48, RELAT_1:81 ;
:: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A49: UsedInt*Loc i = {} by A47, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A49, 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
A50: i = a =0_goto l by SCMFSA_2:36;
A51: UsedIntLoc i = {a} by A50, Th16;
then A52: a in UsedIntLoc i by TARSKI:def 1;
then A53: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A54: s . a = t . a by A1, A52, 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 A55: s . a = 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = l by A50, SCMFSA_2:70
.= IC (Exec (i,t)) by A50, A54, A55, SCMFSA_2:70 ;
:: thesis: verum

end;

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

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

end;

end;

end;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A50, SCMFSA_2:70;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A51, A52, A53, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A57: UsedInt*Loc i = {} by A50, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A57, 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
A58: i = a >0_goto l by SCMFSA_2:37;
A59: UsedIntLoc i = {a} by A58, Th16;
then A60: a in UsedIntLoc i by TARSKI:def 1;
then A61: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A62: s . a = t . a by A1, A60, 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 A63: s . a > 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))

hence IC (Exec (i,s)) = l by A58, SCMFSA_2:71
.= IC (Exec (i,t)) by A58, A62, A63, SCMFSA_2:71 ;
:: thesis: verum

end;

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

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

end;

end;

end;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A58, SCMFSA_2:71;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A59, A60, A61, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A65: UsedInt*Loc i = {} by A58, Th32;
hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81
.= (Exec (i,t)) | (UsedInt*Loc i) by A65, 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
A66: i = b := (f,a) by SCMFSA_2:38;
A67: UsedIntLoc i = {a,b} by A66, Th17;
then A68: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A69: s . a = t . a by A1, A68, FUNCT_1:49;
thus IC (Exec (i,s)) = succ (IC t) by A3, A66, SCMFSA_2:72
.= IC (Exec (i,t)) by A66, 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) )
A70: UsedInt*Loc i = {f} by A66, Th33;
then A71: f in UsedInt*Loc i by TARSKI:def 1;
then A72: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
A73: ( 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 A66, SCMFSA_2:72;

A74: now :: thesis: ( ( a = b & (Exec (i,s)) . b = (Exec (i,t)) . b ) or ( a <> b & (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) )

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, A71, A72, A69, A73, 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 A66, SCMFSA_2:72; :: thesis: verum

end;

end;

end;

s . f = t . f by A2, A71, A72, FUNCT_1:49;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A67, A69, A73, A74, 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 A66, SCMFSA_2:72;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A70, A71, A72, 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
A75: i = (f,a) := b by SCMFSA_2:39;
thus IC (Exec (i,s)) = succ (IC t) by A3, A75, SCMFSA_2:73
.= IC (Exec (i,t)) by A75, 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) )
A76: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by A75, SCMFSA_2:73;
A77: UsedIntLoc i = {a,b} by A75, Th17;
then A78: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
then A79: s . a = t . a by A1, A78, FUNCT_1:49;
A80: b in UsedIntLoc i by A77, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;
then A81: s . b = t . b by A1, A80, FUNCT_1:49;
A82: UsedInt*Loc i = {f} by A75, Th33;
then A83: f in UsedInt*Loc i by TARSKI:def 1;
then s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
then A84: s . f = t . f by A2, A83, FUNCT_1:49;
( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by A75, SCMFSA_2:73;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A77, A79, A81, A76, 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 A75, SCMFSA_2:73;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A82, A79, A81, A84, 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
A85: i = a :=len f by SCMFSA_2:40;
thus IC (Exec (i,s)) = succ (IC t) by A3, A85, SCMFSA_2:74
.= IC (Exec (i,t)) by A85, 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) )
A86: (Exec (i,t)) . a = len (t . f) by A85, SCMFSA_2:74;
A87: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by A85, Th18, SCMFSA_2:74;
A88: UsedInt*Loc i = {f} by A85, Th34;
then A89: f in UsedInt*Loc i by TARSKI:def 1;
then A90: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;
then s . f = t . f by A2, A89, FUNCT_1:49;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A87, A86, 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 A85, SCMFSA_2:74;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A88, A89, A90, 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
A91: i = f :=<0,...,0> a by SCMFSA_2:41;
thus IC (Exec (i,s)) = succ (IC t) by A3, A91, SCMFSA_2:75
.= IC (Exec (i,t)) by A91, 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) )
A92: UsedIntLoc i = {a} by A91, Th18;
then A93: a in UsedIntLoc i by TARSKI:def 1;
then A94: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;
A95: ( UsedInt*Loc i = {f} & ex m being Element of NAT st
( m = abs (s . a) & (Exec (i,s)) . f = m |-> 0 ) ) by A91, Th34, SCMFSA_2:75;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A91, SCMFSA_2:75;
hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A92, A93, A94, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)
A96: ex n being Element of NAT st
( n = abs (t . a) & (Exec (i,t)) . f = n |-> 0 ) by A91, SCMFSA_2:75;
s . a = t . a by A1, A93, A94, FUNCT_1:49;
hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A95, A96, GRFUNC_1:29; :: thesis: verum

end;

end;