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 SCMFSA_M:9;
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 A7: Initialized s = Initialize (Initialized s) by A5, SCMFSA_M:18;
DataPart (Initialized s) = DataPart (Initialized s) ;
then A8: 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;
A9: J c= (p +* Ig) +* J by FUNCT_4:25;
A10: p +* Ig halts_on Initialized s by A1, A7, SCMFSA7B:def 7;
then A11: 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);
A12: Ig ";" J c= p +* (Ig ";" J) by FUNCT_4:25;
Initialized s = Initialized (Initialized s) ;
then A13: Initialized s = Initialize (Initialized s) by A5, SCMFSA_M:18;
A14: DataPart (Initialized s) = DataPart (Initialized s) ;
A15: (Initialized s) . (intloc 0) = 1 by A5;
A16: 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, A14, SCMFSA8C:20 ;
then A17: 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 A18: LifeSpan (((p +* (Ig ";" J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(Initialized s)) by A1, A3, A14, 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, A7, SCMFSA8C:68;
then A19: 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, A3, A4, Th3;
then A20: p +* (Ig ";" J) halts_on Initialized s by A13, SCMFSA7B:def 7;
A21: 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 A20, 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, A11, Th5 ;
A22: 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 A10, 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 A23: (p +* Ig) +* J halts_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A19, 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 A19, A22, MEMSTR_0:79;
then A24: J is_closed_on Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))),(p +* Ig) +* J by A4, SCMFSA8B:3;
A25: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;
(IExec (Ig,p,s)) . (intloc 0) = 1 by A1, A3, SCMFSA8C:67;
then A26: 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, A4, A19, A22, A11, SCMFSA8C:72;
then A27: IC (Result (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s)))))) = IC (Result ((p +* J),(Initialized (IExec (Ig,p,s))))) ;
A28: 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, A19, A22, A26, SCMFSA8C:72;
A29: 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 A23, A28, EXTPRO_1:23 ;
A30: Ig is_halting_on Initialized s,p +* (Ig ";" J) by A1, A3, A14, 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 A31: Ig is_closed_on Initialized s,(p +* (Ig ";" J)) +* Ig by A3, SCMFSA8B:3;
A32: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A33: Ig +* (Ig ";" J) = Ig ";" J by SCMFSA6A:18;
A34: ((p +* (Ig ";" J)) +* Ig) +* (Ig ";" J) = (p +* (Ig ";" J)) +* (Ig +* (Ig ";" J)) by FUNCT_4:14;
A35: Ig c= (p +* (Ig ";" J)) +* Ig by FUNCT_4:25;
A36: (p +* Ig) +* (Ig ";" J) = p +* (Ig ";" J) by A33, FUNCT_4:14;
A37: Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) = Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))) by A10, A8, Th4, A6, A36;
Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
then (p +* (Ig ";" J)) +* Ig halts_on Initialized s by A30, 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 A31, A18, Th4, A35;
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 A33, A34
.= DataPart (Comput ((p +* (Ig ";" J)),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s)))))
.= DataPart (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) by A37 ;
then A38: 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 ;
A39: Ig is_closed_on Initialized s,p +* (Ig ";" J) by A3, A14, SCMFSA8B:3;
A40: J is_halting_on IExec (Ig,(p +* (Ig ";" J)),(Initialized s)),p +* (Ig ";" J) by A2, A4, A16, SCMFSA8B:5;
then A41: 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 A25, A39, A30, A18, A15, A17, Lm1, A12;
Reloc (J,(card Ig)) c= Ig ";" J by FUNCT_4:25;
then A42: Reloc (J,(card Ig)) c= p +* (Ig ";" J) by A12, XBOOLE_1:1;
A43: IC (Comput ((p +* (Ig ";" J)),(Initialized s),((LifeSpan ((p +* Ig),(Initialized s))) + 1))) = card Ig by A25, A39, A30, A18, A15, A17, A40, Lm1, A12;
then A44: 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 A24, A38, A41, A9, A42, SCMFSA8C:16;
A45: 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 A21
.= 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 A44, EXTPRO_1:4
.= DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A29 ;
A46: 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 A24, A38, A43, A41, A9, A42, SCMFSA8C:16;
A47: Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))) = Initialized (Result ((p +* Ig),(Initialized s))) by A10, EXTPRO_1:23;
A48: 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 A20, 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, A11, Th5
.= (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 A46, EXTPRO_1:4
.= (IC (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(Initialized s))))))))) + (card Ig) by A23, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A27, A47, SCMFSA6B:def 1 ;

A49: now :: thesis:

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

per cases by A50, SCMFSA_M:1;

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

then x <> IC by SCMFSA_2:56;
then A52: not x in dom (Start-At (l,SCM+FSA)) by A32, TARSKI:def 1;
(IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A45, A51, 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 A52, FUNCT_4:11; :: thesis:

end;

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

then x <> IC by SCMFSA_2:57;
then A54: not x in dom (Start-At (l,SCM+FSA)) by A32, TARSKI:def 1;
(IExec ((Ig ";" J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A45, A53, 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 A54, FUNCT_4:11; :: thesis:

end;

suppose A55: x = IC ; :: thesis:

then x in {(IC )} by TARSKI:def 1;
then A56: 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 A48, A55, 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 A55, A56, 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 A49, FUNCT_1:2; :: thesis: