let p be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let J be Program of SCM+FSA; :: thesis:
let Ig be good 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 and
A3: Ig is_closed_on Initialized s,p and
A4: J is_closed_on IExec (Ig,p,s),p ; :: thesis:
set Is = Initialized s;
set Ip = p;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA6A:38;
set s1 = Initialized s;
set p1 = p +* Ig;
A6: Ig c= p +* Ig by FUNCT_4:25;
set m1 = LifeSpan ((p +* Ig),(Initialized s));
Initialized s = Initialized (Initialized s) ;
then A10: Initialized s = Initialize (Initialized s) by A5, SCMFSA8C:4;
DataPart (Initialized s) = DataPart (Initialized s) ;
then A11: Ig is_closed_on Initialized s,p +* Ig by A3, SCMFSA8B:3;
set s3 = Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))));
set p3 = (p +* Ig) +* J;
A12: J c= (p +* Ig) +* J by FUNCT_4:25;
A13: p +* Ig halts_on Initialized s by A1, A10, SCMFSA7B:def 7;
then A14: 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);
A15: Ig ';' J c= p +* (Ig ';' J) by FUNCT_4:25;
Initialized s = Initialized (Initialized s) ;
then A16: Initialized s = Initialize (Initialized s) by A5, SCMFSA8C:4;
A17: DataPart (Initialized s) = DataPart (Initialized s) ;
A18: (Initialized s) . (intloc 0) = 1 by A5;
A19: 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, A5, A17, SCMFSA8C:20 ;
then A20: J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J) by A2, A4, SCMFSA8B:5;
Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then A22: LifeSpan (((p +* (Ig ';' J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s)) by A1, A3, A17, 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, A10, SCMFSA8C:68;
then A23: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialize (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by SCMFSA8C:4;
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, A3, A4, Th4;
then A25: p +* (Ig ';' J) halts_on Initialized s by A16, SCMFSA7B:def 7;
A26: 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 A25, 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, A3, A4, A14, Th6 ;
A27: 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 A13, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))),p +* Ig by A2, A4, SCMFSA8B:5;
then A28: (p +* Ig) +* J halts_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A23, SCMFSA7B:def 7;
set IEJIs = IExec (J,p,(IExec (Ig,p,s)));
set IAt = Start-At (0,SCM+FSA);
DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))) by A23, A27, MEMSTR_0:79;
then A31: J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J by A4, SCMFSA8B:3;
A32: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
(IExec (Ig,p,s)) . (intloc 0) = 1 by A1, A3, SCMFSA8C:67;
then A33: Initialized (IExec (Ig,p,s)) = Initialize (IExec (Ig,p,s)) by SCMFSA8C:4;
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, A4, A23, A27, A14, SCMFSA8C:72;
then A34: IC (Result (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (Ig,p,s))))) ;
A35: 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, A4, A23, A27, A33, SCMFSA8C:72;
A36: 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 A28, A35, EXTPRO_1:23 ;
A37: Ig is_halting_on Initialized s,p +* (Ig ';' J) by A1, A3, A17, 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 ;
DataPart (Initialized s) = DataPart (Initialized s) ;
then A40: Ig is_closed_on Initialized s,(p +* (Ig ';' J)) +* Ig by A3, SCMFSA8B:3;
A41: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A42: Ig +* (Ig ';' J) = Ig ';' J by SCMFSA6A:18;
A44: ((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J) = (p +* (Ig ';' J)) +* (Ig +* (Ig ';' J)) by FUNCT_4:14;
A48: Ig c= (p +* (Ig ';' J)) +* Ig by FUNCT_4:25;
A49: (p +* Ig) +* (Ig ';' J) = p +* (Ig ';' J) by A42, FUNCT_4:14;
EO: Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A13, A11, Th5, A6, A49;
Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then (p +* (Ig ';' J)) +* Ig halts_on Initialized s by A37, SCMFSA7B:def 7;
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 A40, A22, Th5, A48;
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 A42, A44
.= DataPart (Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by FUNCT_4:93
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by EO ;
then A50: 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 ;
A51: Ig is_closed_on Initialized s,p +* (Ig ';' J) by A3, A17, SCMFSA8B:3;
A52: J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J) by A2, A4, A19, SCMFSA8B:5;
then A53: 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 A32, A51, A37, A22, A18, A20, Lm1, A15;
Reloc (J,(card Ig)) c= Ig ';' J by FUNCT_4:25;
then A54: Reloc (J,(card Ig)) c= p +* (Ig ';' J) by A15, XBOOLE_1:1;
A55: IC (Comput ((p +* (Ig ';' J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = card Ig by A32, A51, A37, A22, A18, A20, A52, Lm1, A15;
then A56: 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 A31, A50, A53, A12, A54, SCMFSA8C:16;
A58: 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 A26
.= 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 A56, EXTPRO_1:4
.= DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A36 ;
A59: 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 A31, A50, A55, A53, A12, A54, SCMFSA8C:16;
A60: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by A13, EXTPRO_1:23;
A61: 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 A25, 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, A3, A4, A14, Th6
.= (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 A59, EXTPRO_1:4
.= (IC (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) + (card Ig) by A28, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A34, A60, SCMFSA6B:def 1 ;

A62: now

let x be set ; :: thesis:
assume A63: x in dom (IExec ((Ig ';' J),p,s)) ; :: thesis:

per cases by A63, SCMFSA6A:5;

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

then x <> IC by SCMFSA_2:56;
then A65: not x in dom (Start-At (l,SCM+FSA)) by A41, TARSKI:def 1;
(IExec ((Ig ';' J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A58, A64, SCMFSA6A:7;
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 A65, FUNCT_4:11; :: thesis:

end;

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

then x <> IC by SCMFSA_2:57;
then A67: not x in dom (Start-At (l,SCM+FSA)) by A41, TARSKI:def 1;
(IExec ((Ig ';' J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A58, A66, SCMFSA6A:7;
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 A67, FUNCT_4:11; :: thesis:

end;

suppose A68: x = IC ; :: thesis:

then x in {(IC )} by TARSKI:def 1;
then A69: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:13;
thus (IExec ((Ig ';' J),p,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A61, A68, 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 A68, A69, 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 A62, FUNCT_1:2; :: thesis: