let p be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let Ig be good really-closed Program of SCM+FSA; :: thesis:
let J be really-closed Program of SCM+FSA; :: thesis:
set I = Ig;
assume that
A1: Ig is_halting_on Initialized s,p and
A2: J is_halting_on IExec (Ig,p,s),p ; :: thesis:
set Is = Initialized s;
set Ip = p;
A3: (Initialized s) . (intloc 0) = 1 by SCMFSA_M:9;
set s1 = Initialized s;
set p1 = p +* Ig;
A4: Ig c= p +* Ig by FUNCT_4:25;
set m1 = LifeSpan ((p +* Ig),(Initialized s));
Initialized s = Initialized (Initialized s) ;
then A5: Initialized s = Initialize (Initialized s) by A3, SCMFSA_M:18;
set s3 = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))));
set p3 = (p +* Ig) +* J;
A6: J c= (p +* Ig) +* J by FUNCT_4:25;
A7: p +* Ig halts_on Initialized s by A1, A5;
then A8: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ";" J);
A9: Ig ";" J c= p +* (Ig ";" J) by FUNCT_4:25;
Initialized s = Initialized (Initialized s) ;
then A10: Initialized s = Initialize (Initialized s) by A3, SCMFSA_M:18;
A11: DataPart (Initialized s) = DataPart (Initialized s) ;
A12: (Initialized s) . (intloc 0) = 1 by A3;
A13: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:3
.= DataPart (IExec (Ig,(p +* (Ig ";" J)),(Initialized s))) by A1, A3, A11, SCMFSA8C:20 ;
Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then A14: LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s)) by A1, A11, SCMFSA8C:72;
set JAt = Start-At (0,SCM+FSA);
(Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) . (intloc 0) = 1 by A3, A5, SCMFSA8C:68;
then A15: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by SCMFSA_M:18;
set m3 = LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))));
Ig ";" J is_halting_on Initialized s,p by A1, A2, Th2;
then A16: p +* (Ig ";" J) halts_on Initialized s by A10;
A17: IExec ((Ig ";" J),p,s) = Result ((p +* (Ig ";" J)),(Initialized s)) by SCMFSA6B:def 1
.= Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* (Ig ";" J)),(Initialized s)))) by A16, EXTPRO_1:23
.= Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A1, A2, A8, Th4 ;
A18: DataPart (IExec (Ig,p,s)) = DataPart (Result ((p +* Ig),(Initialized s))) by SCMFSA6B:def 1
.= DataPart (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A7, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))),p +* Ig by A2, SCMFSA8B:5;
then A19: (p +* Ig) +* J halts_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A15;
set IEJIs = IExec (J,p,(IExec (Ig,p,s)));
set IAt = Start-At (0,SCM+FSA);
A20: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
(IExec (Ig,p,s)) . (intloc 0) = 1 by A1, SCMFSA8C:67;
then A21: Initialized (IExec (Ig,p,s)) = Initialize (IExec (Ig,p,s)) by SCMFSA_M:18;
then Result (((p +* Ig) +* J),((Result ((p +* Ig),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))) = Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1)))) by A2, A15, A18, A8, SCMFSA8C:72;
then A22: IC (Result (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (Ig,p,s))))) ;
A23: Result ((p +* J),(Initialized (IExec (Ig,p,s)))) = Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))) by A2, A15, A18, A21, SCMFSA8C:72;
A24: IExec (J,p,(IExec (Ig,p,s))) = Result ((p +* J),(Initialized (IExec (Ig,p,s)))) by SCMFSA6B:def 1
.= Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) by A19, A23, EXTPRO_1:23 ;
A25: Ig is_halting_on Initialized s,p +* (Ig ";" J) by A1, A11, SCMFSA8B:5;
reconsider l = (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) as Element of NAT ;
reconsider s2t = s +* ((intloc 0) .--> 1) as State of SCM+FSA ;
A27: Ig +* (Ig ";" J) = Ig ";" J by SCMFSA6A:18;
A28: ((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J) = (p +* (Ig ";" J)) +* (Ig +* (Ig ";" J)) by FUNCT_4:14;
A29: Ig c= (p +* (Ig ";" J)) +* Ig by FUNCT_4:25;
A30: (p +* Ig) +* (Ig ";" J) = p +* (Ig ";" J) by A27, FUNCT_4:14;
A31: Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A7, Th3, A4, A30;
Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then (p +* (Ig ";" J)) +* Ig halts_on Initialized s by A25;
then Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A14, Th3, A29;
then DataPart (Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = DataPart (Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput ((((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput (((p +* (Ig ";" J)) +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A27, A28
.= DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A31 ;
then A32: DataPart ((Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71
.= DataPart ((Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71 ;
A33: J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A13, SCMFSA8B:5;
then A34: DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = DataPart (Initialized (Comput (((p +* (Ig ";" J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by A20, A25, A14, A12, Lm1, A9;
Reloc (J,(card Ig)) c= Ig ";" J by SCMFSA6A:38;
then A35: Reloc (J,(card Ig)) c= p +* (Ig ";" J) by A9, XBOOLE_1:1;
A36: IC (Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = card Ig by A20, A25, A14, A12, A33, Lm1, A9;
then A37: DataPart (Comput ((p +* (Ig ";" J)),(Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) = DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A32, A34, A6, A35, SCMFSA8C:16;
A38: DataPart (IExec ((Ig ";" J),p,s)) = DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) by A17
.= DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) by A37, EXTPRO_1:4
.= DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A24 ;
A39: IC (Comput ((p +* (Ig ";" J)),(Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))))))) = (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) + (card Ig) by A32, A36, A34, A6, A35, SCMFSA8C:16;
A40: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by A7, EXTPRO_1:23;
A41: IC (IExec ((Ig ";" J),p,s)) = IC (Result ((p +* (Ig ";" J)),(Initialized s))) by SCMFSA6B:def 1
.= IC (Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* (Ig ";" J)),(Initialized s))))) by A16, EXTPRO_1:23
.= IC (Comput ((p +* (Ig ";" J)),(Initialized s),(((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) by A1, A2, A8, Th4
.= (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))))) + (card Ig) by A39, EXTPRO_1:4
.= (IC (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) + (card Ig) by A19, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A22, A40, SCMFSA6B:def 1 ;

A42: now :: thesis:

let x be object ; :: thesis:
assume A43: x in dom (IExec ((Ig ";" J),p,s)) ; :: thesis:

per cases by A43, SCMFSA_M:1;

suppose A44: x is Int-Location ; :: thesis:

then x <> IC by SCMFSA_2:56;
then A45: not x in dom (Start-At (l,SCM+FSA)) by TARSKI:def 1;
(IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A38, A44, SCMFSA_M:2;
hence (IExec ((Ig ";" J),p,s)) . x = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A45, FUNCT_4:11; :: thesis:

end;

suppose A46: x is FinSeq-Location ; :: thesis:

then x <> IC by SCMFSA_2:57;
then A47: not x in dom (Start-At (l,SCM+FSA)) by TARSKI:def 1;
(IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A38, A46, SCMFSA_M:2;
hence (IExec ((Ig ";" J),p,s)) . x = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A47, FUNCT_4:11; :: thesis:

end;

suppose A48: x = IC ; :: thesis:

then x in {(IC )} by TARSKI:def 1;
then A49: x in dom (Start-At (l,SCM+FSA)) ;
thus (IExec ((Ig ";" J),p,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A41, A48, FUNCOP_1:72
.= ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A48, A49, FUNCT_4:13 ; :: thesis:

end;

end;

end;

dom (IExec ((Ig ";" J),p,s)) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) by PARTFUN1:def 2 ;
hence IExec ((Ig ";" J),p,s) = (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA)) by A42, FUNCT_1:2; :: thesis: