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 4
.= dom (Exec i,t) by PARTFUN1:def 4 ;
A5: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A6: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A7: InsCode i <= 11 + 1 by SCMFSA_2:35;

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, A6, A5, NAT_1:8, NAT_1:33;

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:122;
then Exec i,s = s by AMI_1:def 8;
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, AMI_1:def 8; :: 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:54;
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:72;
then A12: s . b = t . b by A1, A11, FUNCT_1:72;
thus IC (Exec i,s) = succ (IC t) by A3, A9, SCMFSA_2:89
.= IC (Exec i,t) by A9, SCMFSA_2:89 ; :: 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:89;
( (Exec i,s) . a = s . b & (Exec i,t) . a = t . b ) by A9, SCMFSA_2:89;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A10, A12, A13, GRFUNC_1:91; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A14, RELAT_1:110 ;
:: 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:55;
thus IC (Exec i,s) = succ (IC t) by A3, A15, SCMFSA_2:90
.= IC (Exec i,t) by A15, SCMFSA_2:90 ; :: 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:72;
then A18: s . a = t . a by A1, A17, FUNCT_1:72;

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:90; :: 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:90; :: 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:72;
then A21: s . b = t . b by A1, A20, FUNCT_1:72;
( (Exec i,s) . a = (s . a) + (s . b) & (Exec i,t) . a = (t . a) + (t . b) ) by A15, SCMFSA_2:90;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A16, A18, A21, A19, GRFUNC_1:91; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A22, RELAT_1:110 ;
:: 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:56;
thus IC (Exec i,s) = succ (IC t) by A3, A23, SCMFSA_2:91
.= IC (Exec i,t) by A23, SCMFSA_2:91 ; :: 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:72;
then A26: s . a = t . a by A1, A25, FUNCT_1:72;

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:91; :: 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:91; :: 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:72;
then A29: s . b = t . b by A1, A28, FUNCT_1:72;
( (Exec i,s) . a = (s . a) - (s . b) & (Exec i,t) . a = (t . a) - (t . b) ) by A23, SCMFSA_2:91;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A24, A26, A29, A27, GRFUNC_1:91; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A30, RELAT_1:110 ;
:: 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:57;
thus IC (Exec i,s) = succ (IC t) by A3, A31, SCMFSA_2:92
.= IC (Exec i,t) by A31, SCMFSA_2:92 ; :: 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:72;
then A34: s . a = t . a by A1, A33, FUNCT_1:72;

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:92; :: 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:92; :: 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:72;
then A37: s . b = t . b by A1, A36, FUNCT_1:72;
( (Exec i,s) . a = (s . a) * (s . b) & (Exec i,t) . a = (t . a) * (t . b) ) by A31, SCMFSA_2:92;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A32, A34, A37, A35, GRFUNC_1:91; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A38, RELAT_1:110 ;
:: 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:58;
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:72;
then A42: s . a = t . a by A1, A41, FUNCT_1:72;
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:72;
then A45: s . b = t . b by A1, A44, FUNCT_1:72;

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:94
.= IC (Exec i,t) by A39, A46, SCMFSA_2:94 ;
:: 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:94;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A40, A42, A46, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A43, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A43, RELAT_1:110 ; :: 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:93
.= IC (Exec i,t) by A39, SCMFSA_2:93 ; :: 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:93;
( (Exec i,s) . a = (s . a) div (s . b) & (Exec i,t) . a = (t . a) div (t . b) ) by A39, A47, SCMFSA_2:93;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A40, A42, A45, A48, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A43, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A43, RELAT_1:110 ; :: 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:59;
thus IC (Exec i,s) = l by A49, SCMFSA_2:95
.= IC (Exec i,t) by A49, SCMFSA_2:95 ; :: 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:110
.= (Exec i,t) | (UsedIntLoc i) by A50, RELAT_1:110 ;
:: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A51, RELAT_1:110 ;
:: 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:60;
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:72;
then A56: s . a = t . a by A1, A54, FUNCT_1:72;

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:96
.= IC (Exec i,t) by A52, A56, A57, SCMFSA_2:96 ;
:: 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:96
.= IC (Exec i,t) by A3, A52, A56, A58, SCMFSA_2:96 ;
:: thesis: verum

end;

end;

end;

( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A52, SCMFSA_2:96;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A4, A53, A54, A55, FUNCT_1:72, GRFUNC_1:90; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A59, RELAT_1:110 ;
:: 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:61;
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:72;
then A64: s . a = t . a by A1, A62, FUNCT_1:72;

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:97
.= IC (Exec i,t) by A60, A64, A65, SCMFSA_2:97 ;
:: 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:97
.= IC (Exec i,t) by A3, A60, A64, A66, SCMFSA_2:97 ;
:: thesis: verum

end;

end;

end;

( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A60, SCMFSA_2:97;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A4, A61, A62, A63, FUNCT_1:72, GRFUNC_1:90; :: 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:110
.= (Exec i,t) | (UsedInt*Loc i) by A67, RELAT_1:110 ;
:: 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:62;
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:72;
then A71: s . a = t . a by A1, A70, FUNCT_1:72;
thus IC (Exec i,s) = succ (IC t) by A3, A68, SCMFSA_2:98
.= IC (Exec i,t) by A68, SCMFSA_2:98 ; :: 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:72;
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:98;

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:72; :: 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:98; :: thesis: verum

end;

end;

end;

s . f = t . f by A2, A73, A74, FUNCT_1:72;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A69, A71, A75, A76, GRFUNC_1:91; :: 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:98;
hence (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A2, A4, A72, A73, A74, FUNCT_1:72, GRFUNC_1:90; :: 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:63;
thus IC (Exec i,s) = succ (IC t) by A3, A77, SCMFSA_2:99
.= IC (Exec i,t) by A77, SCMFSA_2:99 ; :: 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:99;
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:72;
then A81: s . a = t . a by A1, A80, FUNCT_1:72;
A82: b in UsedIntLoc i by A79, TARSKI:def 2;
then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:72;
then A83: s . b = t . b by A1, A82, FUNCT_1:72;
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:72;
then A86: s . f = t . f by A2, A85, FUNCT_1:72;
( (Exec i,s) . a = s . a & (Exec i,s) . b = s . b ) by A77, SCMFSA_2:99;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A79, A81, A83, A78, GRFUNC_1:91; :: 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:99;
hence (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A4, A84, A81, A83, A86, GRFUNC_1:90; :: 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:64;
thus IC (Exec i,s) = succ (IC t) by A3, A87, SCMFSA_2:100
.= IC (Exec i,t) by A87, SCMFSA_2:100 ; :: 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:100;
A89: ( UsedIntLoc i = {a} & (Exec i,s) . a = len (s . f) ) by A87, Th22, SCMFSA_2:100;
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:72;
then s . f = t . f by A2, A91, FUNCT_1:72;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A4, A89, A88, GRFUNC_1:90; :: 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:100;
hence (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A2, A4, A90, A91, A92, FUNCT_1:72, GRFUNC_1:90; :: 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:65;
thus IC (Exec i,s) = succ (IC t) by A3, A93, SCMFSA_2:101
.= IC (Exec i,t) by A93, SCMFSA_2:101 ; :: 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:72;
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:101;
( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A93, SCMFSA_2:101;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A4, A94, A95, A96, FUNCT_1:72, GRFUNC_1:90; :: 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:101;
s . a = t . a by A1, A95, A96, FUNCT_1:72;
hence (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A4, A97, A98, GRFUNC_1:90; :: thesis: verum

end;

end;