let i be Instruction of SCM+FSA; :: thesis: for s, t being State of SCM+FSA st s | () = t | () & s | () = t | () & IC s = IC t holds
( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )

let s, t be State of SCM+FSA; :: thesis: ( s | () = t | () & s | () = t | () & IC s = IC t implies ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () ) )
assume that
A1: s | () = t | () and
A2: s | () = t | () and
A3: IC s = IC t ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () ) by ; :: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
then consider a, b being Int-Location such that
A6: i = a := b by SCMFSA_2:30;
A7: UsedIntLoc i = {a,b} by ;
then A8: b in UsedIntLoc i by TARSKI:def 2;
then s . b = (s | ()) . b by FUNCT_1:49;
then A9: s . b = t . b by ;
thus IC (Exec (i,s)) = (IC t) + 1 by
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
( a = b or a <> b ) ;
then A10: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by ;
( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A11: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A13: UsedIntLoc i = {a,b} by ;
then A14: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A15: s . a = t . a by ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
A17: b in UsedIntLoc i by ;
then s . b = (s | ()) . b by FUNCT_1:49;
then A18: s . b = t . b by ;
( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A19: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A21: UsedIntLoc i = {a,b} by ;
then A22: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A23: s . a = t . a by ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
A25: b in UsedIntLoc i by ;
then s . b = (s | ()) . b by FUNCT_1:49;
then A26: s . b = t . b by ;
( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A27: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A29: UsedIntLoc i = {a,b} by ;
then A30: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A31: s . a = t . a by ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
A33: b in UsedIntLoc i by ;
then s . b = (s | ()) . b by FUNCT_1:49;
then A34: s . b = t . b by ;
( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A35: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
then consider a, b being Int-Location such that
A36: i = Divide (a,b) by SCMFSA_2:34;
A37: UsedIntLoc i = {a,b} by ;
then A38: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A39: s . a = t . a by ;
A40: UsedInt*Loc i = {} by ;
A41: b in UsedIntLoc i by ;
then s . b = (s | ()) . b by FUNCT_1:49;
then A42: s . b = t . b by ;
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)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
hence IC (Exec (i,s)) = (IC t) + 1 by
.= IC (Exec (i,t)) by ;
:: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
( (Exec (i,s)) . a = (s . a) mod (s . a) & (Exec (i,t)) . a = (t . a) mod (t . b) ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
thus (Exec (i,s)) | () = {} by
.= (Exec (i,t)) | () by ; :: thesis: verum
end;
suppose A44: a <> b ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
thus IC (Exec (i,s)) = (IC t) + 1 by
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A45: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by ;
( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
thus (Exec (i,s)) | () = {} by
.= (Exec (i,t)) | () by ; :: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 6 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
then consider l being Nat such that
A46: i = goto l by SCMFSA_2:35;
thus IC (Exec (i,s)) = l by
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A47: UsedIntLoc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A48: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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 ;
then A51: a in UsedIntLoc i by TARSKI:def 1;
then A52: s . a = (s | ()) . a by FUNCT_1:49;
then A53: s . a = t . a by ;
hereby :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ;
:: 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
.= IC (Exec (i,t)) by ;
:: thesis: verum
end;
end;
end;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A56: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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 ;
then A59: a in UsedIntLoc i by TARSKI:def 1;
then A60: s . a = (s | ()) . a by FUNCT_1:49;
then A61: s . a = t . a by ;
hereby :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ;
:: 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
.= IC (Exec (i,t)) by ;
:: thesis: verum
end;
end;
end;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A64: UsedInt*Loc i = {} by ;
hence (Exec (i,s)) | () = {} by RELAT_1:81
.= (Exec (i,t)) | () by ;
:: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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 ;
then A67: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A68: s . a = t . a by ;
thus IC (Exec (i,s)) = (IC t) + 1 by
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A69: UsedInt*Loc i = {f} by ;
then A70: f in UsedInt*Loc i by TARSKI:def 1;
then A71: s . f = (s | ()) . 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 ;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
s . f = t . f by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A75: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by ;
A76: UsedIntLoc i = {a,b} by ;
then A77: a in UsedIntLoc i by TARSKI:def 2;
then s . a = (s | ()) . a by FUNCT_1:49;
then A78: s . a = t . a by ;
A79: b in UsedIntLoc i by ;
then s . b = (s | ()) . b by FUNCT_1:49;
then A80: s . b = t . b by ;
A81: UsedInt*Loc i = {f} by ;
then A82: f in UsedInt*Loc i by TARSKI:def 1;
then s . f = (s | ()) . f by FUNCT_1:49;
then A83: s . f = t . f by ;
( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
( 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 ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A85: (Exec (i,t)) . a = len (t . f) by ;
A86: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by ;
A87: UsedInt*Loc i = {f} by ;
then A88: f in UsedInt*Loc i by TARSKI:def 1;
then A89: s . f = (s | ()) . f by FUNCT_1:49;
then s . f = t . f by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: ( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
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
.= IC (Exec (i,t)) by ; :: thesis: ( (Exec (i,s)) | () = (Exec (i,t)) | () & (Exec (i,s)) | () = (Exec (i,t)) | () )
A91: UsedIntLoc i = {a} by ;
then A92: a in UsedIntLoc i by TARSKI:def 1;
then A93: s . a = (s | ()) . 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 ;
( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: (Exec (i,s)) | () = (Exec (i,t)) | ()
A95: ex n being Nat st
( n = |.(t . a).| & (Exec (i,t)) . f = n |-> 0 ) by ;
s . a = t . a by ;
hence (Exec (i,s)) | () = (Exec (i,t)) | () by ; :: thesis: verum
end;
end;