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 A1: ( s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & 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 Es = Exec i,s;
set Et = Exec i,t;
set Ui = UsedIntLoc i;
set UFi = UsedInt*Loc i;
A2: dom (Exec i,s) = the carrier of SCM+FSA by AMI_1:79
.= dom (Exec i,t) by AMI_1:79 ;
A3: InsCode i <= 11 + 1 by SCMFSA_2:35;
A4: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A5: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;

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 A3, A4, 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 i = halt SCM+FSA by SCMFSA_2:122;
then ( Exec i,s = s & Exec i,t = t ) 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; :: 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
A6: i = a := b by SCMFSA_2:54;
thus IC (Exec i,s) = Next (IC t) by A1, A6, SCMFSA_2:89
.= IC (Exec i,t) by A6, 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) )
A7: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {} ) by A6, Th18, Th36;
then A8: ( a in UsedIntLoc i & b in UsedIntLoc i ) by TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b ) by FUNCT_1:72;
then A9: ( s . a = t . a & s . b = t . b ) by A1, A8, FUNCT_1:72;
( a = b or a <> b ) ;
then ( (Exec i,s) . a = s . b & (Exec i,s) . b = s . b & (Exec i,t) . a = t . b & (Exec i,t) . b = t . b ) by A6, SCMFSA_2:89;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A7, A9, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A7, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A7, 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
A10: i = AddTo a,b by SCMFSA_2:55;
thus IC (Exec i,s) = Next (IC t) by A1, A10, SCMFSA_2:90
.= IC (Exec i,t) by A10, 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) )
A11: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {} ) by A10, Th18, Th36;
then A12: ( a in UsedIntLoc i & b in UsedIntLoc i ) by TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b ) by FUNCT_1:72;
then A13: ( s . a = t . a & s . b = t . b ) by A1, A12, FUNCT_1:72;
A14: ( (Exec i,s) . a = (s . a) + (s . b) & (Exec i,t) . a = (t . a) + (t . b) ) by A10, SCMFSA_2:90;

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 A10, 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 A10, SCMFSA_2:90; :: thesis: verum

end;

end;

end;

hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A11, A13, A14, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A11, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A11, 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
A15: i = SubFrom a,b by SCMFSA_2:56;
thus IC (Exec i,s) = Next (IC t) by A1, A15, SCMFSA_2:91
.= IC (Exec i,t) by A15, 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) )
A16: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {} ) by A15, Th18, Th36;
then A17: ( a in UsedIntLoc i & b in UsedIntLoc i ) by TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b ) by FUNCT_1:72;
then A18: ( s . a = t . a & s . b = t . b ) by A1, A17, FUNCT_1:72;
A19: ( (Exec i,s) . a = (s . a) - (s . b) & (Exec i,t) . a = (t . a) - (t . b) ) by A15, SCMFSA_2:91;

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: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 A15, SCMFSA_2:91; :: thesis: verum

end;

end;

end;

hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A16, A18, A19, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A16, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A16, 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
A20: i = MultBy a,b by SCMFSA_2:57;
thus IC (Exec i,s) = Next (IC t) by A1, A20, SCMFSA_2:92
.= IC (Exec i,t) by A20, 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) )
A21: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {} ) by A20, Th18, Th36;
then A22: ( a in UsedIntLoc i & b in UsedIntLoc i ) by TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b ) by FUNCT_1:72;
then A23: ( s . a = t . a & s . b = t . b ) by A1, A22, FUNCT_1:72;
A24: ( (Exec i,s) . a = (s . a) * (s . b) & (Exec i,t) . a = (t . a) * (t . b) ) by A20, SCMFSA_2:92;

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 A20, 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 A20, SCMFSA_2:92; :: thesis: verum

end;

end;

end;

hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A21, A23, A24, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A21, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A21, 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
A25: i = Divide a,b by SCMFSA_2:58;
A26: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {} ) by A25, Th18, Th36;
then A27: ( a in UsedIntLoc i & b in UsedIntLoc i ) by TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b ) by FUNCT_1:72;
then A28: ( s . a = t . a & s . b = t . b ) by A1, A27, FUNCT_1:72;

hereby :: thesis: verum

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

suppose A29: 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) = Next (IC t) by A1, A25, SCMFSA_2:94
.= IC (Exec i,t) by A25, A29, 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 A25, A29, SCMFSA_2:94;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A26, A28, A29, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A26, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A26, RELAT_1:110 ; :: thesis: verum

end;

suppose A30: 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) = Next (IC t) by A1, A25, SCMFSA_2:93
.= IC (Exec i,t) by A25, 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) )
( (Exec i,s) . a = (s . a) div (s . b) & (Exec i,t) . a = (t . a) div (t . b) & (Exec i,s) . b = (s . a) mod (s . b) & (Exec i,t) . b = (t . a) mod (t . b) ) by A25, A30, SCMFSA_2:93;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A26, A28, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A26, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A26, 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 Instruction-Location of SCM+FSA such that
A31: i = goto l by SCMFSA_2:59;
thus IC (Exec i,s) = l by A31, SCMFSA_2:95
.= IC (Exec i,t) by A31, 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) )
A32: ( UsedIntLoc i = {} & UsedInt*Loc i = {} ) by A31, Th19, Th36;
hence (Exec i,s) | (UsedIntLoc i) = {} by RELAT_1:110
.= (Exec i,t) | (UsedIntLoc i) by A32, RELAT_1:110 ;
:: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A32, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A32, 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 Instruction-Location of SCM+FSA , a being Int-Location such that
A33: i = a =0_goto l by SCMFSA_2:60;
A34: ( UsedIntLoc i = {a} & UsedInt*Loc i = {} ) by A33, Th20, Th36;
then A35: a in UsedIntLoc i by TARSKI:def 1;
then A36: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:72;
then A37: s . a = t . a by A1, A35, 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 A38: s . a = 0 ; :: thesis: IC (Exec i,s) = IC (Exec i,t)

hence IC (Exec i,s) = l by A33, SCMFSA_2:96
.= IC (Exec i,t) by A33, A37, A38, SCMFSA_2:96 ;
:: thesis: verum

end;

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

hence IC (Exec i,s) = Next (IC s) by A33, SCMFSA_2:96
.= IC (Exec i,t) by A1, A33, A37, A39, SCMFSA_2:96 ;
:: thesis: verum

end;

end;

end;

( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A33, SCMFSA_2:96;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A2, A34, A35, A36, FUNCT_1:72, GRFUNC_1:90; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A34, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A34, 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 Instruction-Location of SCM+FSA , a being Int-Location such that
A40: i = a >0_goto l by SCMFSA_2:61;
A41: ( UsedIntLoc i = {a} & UsedInt*Loc i = {} ) by A40, Th20, Th36;
then A42: a in UsedIntLoc i by TARSKI:def 1;
then A43: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:72;
then A44: s . a = t . a by A1, A42, 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 A45: s . a > 0 ; :: thesis: IC (Exec i,s) = IC (Exec i,t)

hence IC (Exec i,s) = l by A40, SCMFSA_2:97
.= IC (Exec i,t) by A40, A44, A45, SCMFSA_2:97 ;
:: thesis: verum

end;

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

hence IC (Exec i,s) = Next (IC s) by A40, SCMFSA_2:97
.= IC (Exec i,t) by A1, A40, A44, A46, SCMFSA_2:97 ;
:: thesis: verum

end;

end;

end;

( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A40, SCMFSA_2:97;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A2, A41, A42, A43, FUNCT_1:72, GRFUNC_1:90; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = {} by A41, RELAT_1:110
.= (Exec i,t) | (UsedInt*Loc i) by A41, 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
A47: i = b := f,a by SCMFSA_2:62;
thus IC (Exec i,s) = Next (IC t) by A1, A47, SCMFSA_2:98
.= IC (Exec i,t) by A47, 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) )
A48: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {f} ) by A47, Th21, Th37;
then A49: ( a in UsedIntLoc i & b in UsedIntLoc i & f in UsedInt*Loc i ) by TARSKI:def 1, TARSKI:def 2;
then A50: ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b & s . f = (s | (UsedInt*Loc i)) . f ) by FUNCT_1:72;
then A51: ( s . a = t . a & s . b = t . b & s . f = t . f ) by A1, A49, FUNCT_1:72;
consider m being Element of NAT such that
A52: ( m = abs (s . a) & (Exec i,s) . b = (s . f) /. m ) by A47, SCMFSA_2:98;
consider n being Element of NAT such that
A53: ( n = abs (t . a) & (Exec i,t) . b = (t . f) /. n ) by A47, SCMFSA_2:98;
A54: ( (Exec i,s) . f = s . f & (Exec i,t) . f = t . f ) by A47, SCMFSA_2:98;

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 A51, A52, A53; :: 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 A47, SCMFSA_2:98; :: thesis: verum

end;

end;

end;

hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A48, A51, A52, A53, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A1, A2, A48, A49, A50, A54, 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
A55: i = f,a := b by SCMFSA_2:63;
thus IC (Exec i,s) = Next (IC t) by A1, A55, SCMFSA_2:99
.= IC (Exec i,t) by A55, 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) )
A56: ( UsedIntLoc i = {a,b} & UsedInt*Loc i = {f} ) by A55, Th21, Th37;
then A57: ( a in UsedIntLoc i & b in UsedIntLoc i & f in UsedInt*Loc i ) by TARSKI:def 1, TARSKI:def 2;
then ( s . a = (s | (UsedIntLoc i)) . a & s . b = (s | (UsedIntLoc i)) . b & s . f = (s | (UsedInt*Loc i)) . f ) by FUNCT_1:72;
then A58: ( s . a = t . a & s . b = t . b & s . f = t . f ) by A1, A57, FUNCT_1:72;
consider m being Element of NAT such that
A59: ( m = abs (s . a) & (Exec i,s) . f = (s . f) +* m,(s . b) ) by A55, SCMFSA_2:99;
consider n being Element of NAT such that
A60: ( n = abs (t . a) & (Exec i,t) . f = (t . f) +* n,(t . b) ) by A55, SCMFSA_2:99;
( (Exec i,s) . a = s . a & (Exec i,s) . b = s . b & (Exec i,t) . a = t . a & (Exec i,t) . b = t . b ) by A55, SCMFSA_2:99;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A56, A58, GRFUNC_1:91; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A2, A56, A58, A59, A60, 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
A61: i = a :=len f by SCMFSA_2:64;
thus IC (Exec i,s) = Next (IC t) by A1, A61, SCMFSA_2:100
.= IC (Exec i,t) by A61, 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) )
A62: ( UsedIntLoc i = {a} & UsedInt*Loc i = {f} ) by A61, Th22, Th38;
then A63: ( a in UsedIntLoc i & f in UsedInt*Loc i ) by TARSKI:def 1;
then A64: ( s . a = (s | (UsedIntLoc i)) . a & s . f = (s | (UsedInt*Loc i)) . f ) by FUNCT_1:72;
then A65: ( s . a = t . a & s . f = t . f ) by A1, A63, FUNCT_1:72;
A66: ( (Exec i,s) . a = len (s . f) & (Exec i,s) . f = s . f & (Exec i,t) . a = len (t . f) & (Exec i,t) . f = t . f ) by A61, SCMFSA_2:100;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A2, A62, A65, GRFUNC_1:90; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A1, A2, A62, A63, A64, A66, 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
A67: i = f :=<0,...,0> a by SCMFSA_2:65;
thus IC (Exec i,s) = Next (IC t) by A1, A67, SCMFSA_2:101
.= IC (Exec i,t) by A67, 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) )
A68: ( UsedIntLoc i = {a} & UsedInt*Loc i = {f} ) by A67, Th22, Th38;
then A69: ( a in UsedIntLoc i & f in UsedInt*Loc i ) by TARSKI:def 1;
then A70: ( s . a = (s | (UsedIntLoc i)) . a & s . f = (s | (UsedInt*Loc i)) . f ) by FUNCT_1:72;
then A71: ( s . a = t . a & s . f = t . f ) by A1, A69, FUNCT_1:72;
consider m being Element of NAT such that
A72: ( m = abs (s . a) & (Exec i,s) . f = m |-> 0 ) by A67, SCMFSA_2:101;
consider n being Element of NAT such that
A73: ( n = abs (t . a) & (Exec i,t) . f = n |-> 0 ) by A67, SCMFSA_2:101;
( (Exec i,s) . a = s . a & (Exec i,t) . a = t . a ) by A67, SCMFSA_2:101;
hence (Exec i,s) | (UsedIntLoc i) = (Exec i,t) | (UsedIntLoc i) by A1, A2, A68, A69, A70, FUNCT_1:72, GRFUNC_1:90; :: thesis: (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i)
thus (Exec i,s) | (UsedInt*Loc i) = (Exec i,t) | (UsedInt*Loc i) by A2, A68, A71, A72, A73, GRFUNC_1:90; :: thesis: verum

end;

end;