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 ;

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

( 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 ;

InsCode i <= 12 by SCMFSA_2:16;

then not not InsCode i = 0 & ... & not InsCode i = 12 ;

per cases then
( 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 )
;

end;

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 A5:
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, A5, EXTPRO_1:def 3; :: thesis: verum

end;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, A5, EXTPRO_1:def 3; :: thesis: verum

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:30;

A7: UsedIntLoc i = {a,b} by A6, Th14;

then A8: b in UsedIntLoc i by TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A9: s . b = t . b by A1, A8, FUNCT_1:49;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A6, SCMFSA_2:63

.= IC (Exec (i,t)) by A6, 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 A10: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A6, SCMFSA_2:63;

( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by A6, SCMFSA_2:63;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A7, A9, A10, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A11: UsedInt*Loc i = {} by A6, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A11, RELAT_1:81 ;

:: thesis: verum

end;A6: i = a := b by SCMFSA_2:30;

A7: UsedIntLoc i = {a,b} by A6, Th14;

then A8: b in UsedIntLoc i by TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A9: s . b = t . b by A1, A8, FUNCT_1:49;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A6, SCMFSA_2:63

.= IC (Exec (i,t)) by A6, 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 A10: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A6, SCMFSA_2:63;

( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by A6, SCMFSA_2:63;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A7, A9, A10, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A11: UsedInt*Loc i = {} by A6, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A11, RELAT_1:81 ;

:: thesis: verum

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

A12: i = AddTo (a,b) by SCMFSA_2:31;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A12, SCMFSA_2:64

.= IC (Exec (i,t)) by A12, 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) )

A13: UsedIntLoc i = {a,b} by A12, Th14;

then A14: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A15: s . a = t . a by A1, A14, FUNCT_1:49;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A18: s . b = t . b by A1, A17, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by A12, SCMFSA_2:64;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A13, A15, A18, A16, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A19: UsedInt*Loc i = {} by A12, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A19, RELAT_1:81 ;

:: thesis: verum

end;A12: i = AddTo (a,b) by SCMFSA_2:31;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A12, SCMFSA_2:64

.= IC (Exec (i,t)) by A12, 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) )

A13: UsedIntLoc i = {a,b} by A12, Th14;

then A14: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A15: s . a = t . a by A1, A14, FUNCT_1:49;

A16: 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 ) )

A17:
b in UsedIntLoc i
by A13, TARSKI:def 2;end;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A18: s . b = t . b by A1, A17, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by A12, SCMFSA_2:64;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A13, A15, A18, A16, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A19: UsedInt*Loc i = {} by A12, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A19, RELAT_1:81 ;

:: thesis: verum

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

A20: i = SubFrom (a,b) by SCMFSA_2:32;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A20, SCMFSA_2:65

.= IC (Exec (i,t)) by A20, 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) )

A21: UsedIntLoc i = {a,b} by A20, Th14;

then A22: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A23: s . a = t . a by A1, A22, FUNCT_1:49;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A26: s . b = t . b by A1, A25, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by A20, SCMFSA_2:65;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A21, A23, A26, A24, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A27: UsedInt*Loc i = {} by A20, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A27, RELAT_1:81 ;

:: thesis: verum

end;A20: i = SubFrom (a,b) by SCMFSA_2:32;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A20, SCMFSA_2:65

.= IC (Exec (i,t)) by A20, 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) )

A21: UsedIntLoc i = {a,b} by A20, Th14;

then A22: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A23: s . a = t . a by A1, A22, FUNCT_1:49;

A24: 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 ) )

A25:
b in UsedIntLoc i
by A21, TARSKI:def 2;end;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A26: s . b = t . b by A1, A25, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by A20, SCMFSA_2:65;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A21, A23, A26, A24, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A27: UsedInt*Loc i = {} by A20, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A27, RELAT_1:81 ;

:: thesis: verum

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

A28: i = MultBy (a,b) by SCMFSA_2:33;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A28, SCMFSA_2:66

.= IC (Exec (i,t)) by A28, 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) )

A29: UsedIntLoc i = {a,b} by A28, Th14;

then A30: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A31: s . a = t . a by A1, A30, FUNCT_1:49;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A34: s . b = t . b by A1, A33, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by A28, SCMFSA_2:66;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A29, A31, A34, A32, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A35: UsedInt*Loc i = {} by A28, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A35, RELAT_1:81 ;

:: thesis: verum

end;A28: i = MultBy (a,b) by SCMFSA_2:33;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A28, SCMFSA_2:66

.= IC (Exec (i,t)) by A28, 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) )

A29: UsedIntLoc i = {a,b} by A28, Th14;

then A30: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A31: s . a = t . a by A1, A30, FUNCT_1:49;

A32: 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 ) )

A33:
b in UsedIntLoc i
by A29, TARSKI:def 2;end;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A34: s . b = t . b by A1, A33, FUNCT_1:49;

( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by A28, SCMFSA_2:66;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A29, A31, A34, A32, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A35: UsedInt*Loc i = {} by A28, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A35, RELAT_1:81 ;

:: thesis: verum

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

A36: i = Divide (a,b) by SCMFSA_2:34;

A37: UsedIntLoc i = {a,b} by A36, Th14;

then A38: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A39: s . a = t . a by A1, A38, FUNCT_1:49;

A40: UsedInt*Loc i = {} by A36, Th32;

A41: b in UsedIntLoc i by A37, TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A42: s . b = t . b by A1, A41, FUNCT_1:49;

end;A36: i = Divide (a,b) by SCMFSA_2:34;

A37: UsedIntLoc i = {a,b} by A36, Th14;

then A38: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A39: s . a = t . a by A1, A38, FUNCT_1:49;

A40: UsedInt*Loc i = {} by A36, Th32;

A41: b in UsedIntLoc i by A37, TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A42: s . b = t . b by A1, A41, FUNCT_1:49;

hereby :: thesis: verum
end;

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

end;

suppose A43:
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)) =
(IC t) + 1
by A3, A36, SCMFSA_2:68

.= IC (Exec (i,t)) by A36, A43, 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 A36, A43, SCMFSA_2:68;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A37, A39, A43, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A40, RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A40, RELAT_1:81 ; :: thesis: verum

end;.= IC (Exec (i,t)) by A36, A43, 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 A36, A43, SCMFSA_2:68;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A37, A39, A43, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A40, RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A40, RELAT_1:81 ; :: thesis: verum

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) )

thus IC (Exec (i,s)) =
(IC t) + 1
by A3, A36, SCMFSA_2:67

.= IC (Exec (i,t)) by A36, 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) )

A45: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by A36, SCMFSA_2:67;

( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by A36, A44, SCMFSA_2:67;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A37, A39, A42, A45, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A40, RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A40, RELAT_1:81 ; :: thesis: verum

end;.= IC (Exec (i,t)) by A36, 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) )

A45: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by A36, SCMFSA_2:67;

( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by A36, A44, SCMFSA_2:67;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A37, A39, A42, A45, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A40, RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A40, RELAT_1:81 ; :: thesis: verum

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 Nat such that

A46: i = goto l by SCMFSA_2:35;

thus IC (Exec (i,s)) = l by A46, SCMFSA_2:69

.= IC (Exec (i,t)) by A46, 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) )

A47: UsedIntLoc i = {} by A46, Th15;

hence (Exec (i,s)) | (UsedIntLoc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedIntLoc i) by A47, RELAT_1:81 ;

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

A48: UsedInt*Loc i = {} by A46, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A48, RELAT_1:81 ;

:: thesis: verum

end;A46: i = goto l by SCMFSA_2:35;

thus IC (Exec (i,s)) = l by A46, SCMFSA_2:69

.= IC (Exec (i,t)) by A46, 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) )

A47: UsedIntLoc i = {} by A46, Th15;

hence (Exec (i,s)) | (UsedIntLoc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedIntLoc i) by A47, RELAT_1:81 ;

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

A48: UsedInt*Loc i = {} by A46, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A48, RELAT_1:81 ;

:: thesis: verum

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 Nat, a being Int-Location such that

A49: i = a =0_goto l by SCMFSA_2:36;

A50: UsedIntLoc i = {a} by A49, Th16;

then A51: a in UsedIntLoc i by TARSKI:def 1;

then A52: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A53: s . a = t . a by A1, A51, FUNCT_1:49;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A50, A51, A52, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A56: UsedInt*Loc i = {} by A49, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A56, RELAT_1:81 ;

:: thesis: verum

end;A49: i = a =0_goto l by SCMFSA_2:36;

A50: UsedIntLoc i = {a} by A49, Th16;

then A51: a in UsedIntLoc i by TARSKI:def 1;

then A52: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A53: s . a = t . a by A1, A51, 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) )

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a )
by A49, SCMFSA_2:70;
end;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A50, A51, A52, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A56: UsedInt*Loc i = {} by A49, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A56, RELAT_1:81 ;

:: thesis: verum

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 Nat, a being Int-Location such that

A57: i = a >0_goto l by SCMFSA_2:37;

A58: UsedIntLoc i = {a} by A57, Th16;

then A59: a in UsedIntLoc i by TARSKI:def 1;

then A60: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A61: s . a = t . a by A1, A59, FUNCT_1:49;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A58, A59, A60, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A64: UsedInt*Loc i = {} by A57, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A64, RELAT_1:81 ;

:: thesis: verum

end;A57: i = a >0_goto l by SCMFSA_2:37;

A58: UsedIntLoc i = {a} by A57, Th16;

then A59: a in UsedIntLoc i by TARSKI:def 1;

then A60: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A61: s . a = t . a by A1, A59, 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) )

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a )
by A57, SCMFSA_2:71;
end;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A58, A59, A60, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A64: UsedInt*Loc i = {} by A57, Th32;

hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81

.= (Exec (i,t)) | (UsedInt*Loc i) by A64, RELAT_1:81 ;

:: thesis: verum

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

A65: i = b := (f,a) by SCMFSA_2:38;

A66: UsedIntLoc i = {a,b} by A65, Th17;

then A67: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A68: s . a = t . a by A1, A67, FUNCT_1:49;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A65, SCMFSA_2:72

.= IC (Exec (i,t)) by A65, 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) )

A69: UsedInt*Loc i = {f} by A65, Th33;

then A70: f in UsedInt*Loc i by TARSKI:def 1;

then A71: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

A72: ( ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . b = (s . f) /. m ) & ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . b = (t . f) /. n ) ) by A65, SCMFSA_2:72;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A66, A68, A72, A73, 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 A65, SCMFSA_2:72;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A69, A70, A71, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

end;A65: i = b := (f,a) by SCMFSA_2:38;

A66: UsedIntLoc i = {a,b} by A65, Th17;

then A67: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A68: s . a = t . a by A1, A67, FUNCT_1:49;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A65, SCMFSA_2:72

.= IC (Exec (i,t)) by A65, 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) )

A69: UsedInt*Loc i = {f} by A65, Th33;

then A70: f in UsedInt*Loc i by TARSKI:def 1;

then A71: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

A72: ( ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . b = (s . f) /. m ) & ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . b = (t . f) /. n ) ) by A65, SCMFSA_2:72;

A73: 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 ) )end;

s . f = t . f
by A2, A70, A71, FUNCT_1:49;hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A66, A68, A72, A73, 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 A65, SCMFSA_2:72;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A69, A70, A71, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

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

A74: i = (f,a) := b by SCMFSA_2:39;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A74, SCMFSA_2:73

.= IC (Exec (i,t)) by A74, 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) )

A75: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by A74, SCMFSA_2:73;

A76: UsedIntLoc i = {a,b} by A74, Th17;

then A77: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A78: s . a = t . a by A1, A77, FUNCT_1:49;

A79: b in UsedIntLoc i by A76, TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A80: s . b = t . b by A1, A79, FUNCT_1:49;

A81: UsedInt*Loc i = {f} by A74, Th33;

then A82: f in UsedInt*Loc i by TARSKI:def 1;

then s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

then A83: s . f = t . f by A2, A82, FUNCT_1:49;

( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by A74, SCMFSA_2:73;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A76, A78, A80, A75, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

( ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . f = (s . f) +* (m,(s . b)) ) & ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . f = (t . f) +* (n,(t . b)) ) ) by A74, SCMFSA_2:73;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A81, A78, A80, A83, GRFUNC_1:29; :: thesis: verum

end;A74: i = (f,a) := b by SCMFSA_2:39;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A74, SCMFSA_2:73

.= IC (Exec (i,t)) by A74, 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) )

A75: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by A74, SCMFSA_2:73;

A76: UsedIntLoc i = {a,b} by A74, Th17;

then A77: a in UsedIntLoc i by TARSKI:def 2;

then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

then A78: s . a = t . a by A1, A77, FUNCT_1:49;

A79: b in UsedIntLoc i by A76, TARSKI:def 2;

then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49;

then A80: s . b = t . b by A1, A79, FUNCT_1:49;

A81: UsedInt*Loc i = {f} by A74, Th33;

then A82: f in UsedInt*Loc i by TARSKI:def 1;

then s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

then A83: s . f = t . f by A2, A82, FUNCT_1:49;

( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by A74, SCMFSA_2:73;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A76, A78, A80, A75, GRFUNC_1:30; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

( ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . f = (s . f) +* (m,(s . b)) ) & ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . f = (t . f) +* (n,(t . b)) ) ) by A74, SCMFSA_2:73;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A81, A78, A80, A83, GRFUNC_1:29; :: thesis: verum

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

A84: i = a :=len f by SCMFSA_2:40;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A84, SCMFSA_2:74

.= IC (Exec (i,t)) by A84, 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) )

A85: (Exec (i,t)) . a = len (t . f) by A84, SCMFSA_2:74;

A86: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by A84, Th18, SCMFSA_2:74;

A87: UsedInt*Loc i = {f} by A84, Th34;

then A88: f in UsedInt*Loc i by TARSKI:def 1;

then A89: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

then s . f = t . f by A2, A88, FUNCT_1:49;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A86, A85, 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 A84, SCMFSA_2:74;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A87, A88, A89, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

end;A84: i = a :=len f by SCMFSA_2:40;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A84, SCMFSA_2:74

.= IC (Exec (i,t)) by A84, 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) )

A85: (Exec (i,t)) . a = len (t . f) by A84, SCMFSA_2:74;

A86: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by A84, Th18, SCMFSA_2:74;

A87: UsedInt*Loc i = {f} by A84, Th34;

then A88: f in UsedInt*Loc i by TARSKI:def 1;

then A89: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49;

then s . f = t . f by A2, A88, FUNCT_1:49;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A86, A85, 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 A84, SCMFSA_2:74;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A87, A88, A89, FUNCT_1:49, GRFUNC_1:29; :: thesis: verum

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

A90: i = f :=<0,...,0> a by SCMFSA_2:41;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A90, SCMFSA_2:75

.= IC (Exec (i,t)) by A90, 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) )

A91: UsedIntLoc i = {a} by A90, Th18;

then A92: a in UsedIntLoc i by TARSKI:def 1;

then A93: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

A94: ( UsedInt*Loc i = {f} & ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . f = m |-> 0 ) ) by A90, Th34, SCMFSA_2:75;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A90, SCMFSA_2:75;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A91, A92, A93, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A95: ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . f = n |-> 0 ) by A90, SCMFSA_2:75;

s . a = t . a by A1, A92, A93, FUNCT_1:49;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A94, A95, GRFUNC_1:29; :: thesis: verum

end;A90: i = f :=<0,...,0> a by SCMFSA_2:41;

thus IC (Exec (i,s)) = (IC t) + 1 by A3, A90, SCMFSA_2:75

.= IC (Exec (i,t)) by A90, 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) )

A91: UsedIntLoc i = {a} by A90, Th18;

then A92: a in UsedIntLoc i by TARSKI:def 1;

then A93: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49;

A94: ( UsedInt*Loc i = {f} & ex m being Nat st

( m = |.(s . a).| & (Exec (i,s)) . f = m |-> 0 ) ) by A90, Th34, SCMFSA_2:75;

( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A90, SCMFSA_2:75;

hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A91, A92, A93, FUNCT_1:49, GRFUNC_1:29; :: thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i)

A95: ex n being Nat st

( n = |.(t . a).| & (Exec (i,t)) . f = n |-> 0 ) by A90, SCMFSA_2:75;

s . a = t . a by A1, A92, A93, FUNCT_1:49;

hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A94, A95, GRFUNC_1:29; :: thesis: verum