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 ;
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 ) ;
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;
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;
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;
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 ) )
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 A12, 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 A12, SCMFSA_2:64; :: thesis: verum
end;
end;
end;
A17: b in UsedIntLoc i by A13, TARSKI:def 2;
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;
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;
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 ) )
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: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 A20, SCMFSA_2:65; :: thesis: verum
end;
end;
end;
A25: b in UsedIntLoc i by A21, TARSKI:def 2;
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;
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;
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 ) )
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 A28, 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 A28, SCMFSA_2:66; :: thesis: verum
end;
end;
end;
A33: b in UsedIntLoc i by A29, TARSKI:def 2;
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;
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;
hereby :: thesis: verum
per cases ( a = b or a <> b ) ;
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;
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;
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 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;
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;
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 A54: s . a = 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))
hence IC (Exec (i,s)) = l by A49, SCMFSA_2:70
.= IC (Exec (i,t)) by A49, A53, A54, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose A55: s . a <> 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))
hence IC (Exec (i,s)) = (IC s) + 1 by A49, SCMFSA_2:70
.= IC (Exec (i,t)) by A3, A49, A53, A55, SCMFSA_2:70 ;
:: thesis: verum
end;
end;
end;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A49, SCMFSA_2:70;
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;
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;
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 A62: s . a > 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))
hence IC (Exec (i,s)) = l by A57, SCMFSA_2:71
.= IC (Exec (i,t)) by A57, A61, A62, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose A63: s . a <= 0 ; :: thesis: IC (Exec (i,s)) = IC (Exec (i,t))
hence IC (Exec (i,s)) = (IC s) + 1 by A57, SCMFSA_2:71
.= IC (Exec (i,t)) by A3, A57, A61, A63, SCMFSA_2:71 ;
:: thesis: verum
end;
end;
end;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A57, SCMFSA_2:71;
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;
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;
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 ) )
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, A70, A71, A68, A72, 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 A65, SCMFSA_2:72; :: thesis: verum
end;
end;
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
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
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;
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;
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;
end;