set SAt = Start-At (0,SCM+FSA);
set D = Int-Locations \/ FinSeq-Locations;
let I be good Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s & J is_halting_on IExec (I,s) & I is_closed_on s & J is_closed_on IExec (I,s) & Initialized (I ';' J) c= s holds
( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
let J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s & J is_halting_on IExec (I,s) & I is_closed_on s & J is_closed_on IExec (I,s) & Initialized (I ';' J) c= s holds
( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
let s be State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & I is_halting_on s & J is_halting_on IExec (I,s) & I is_closed_on s & J is_closed_on IExec (I,s) & Initialized (I ';' J) c= s implies ( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) ) )
assume that
A1: s . (intloc 0) = 1 and
A2: I is_halting_on s and
A3: J is_halting_on IExec (I,s) and
A4: I is_closed_on s and
A5: J is_closed_on IExec (I,s) ; :: thesis: ( not Initialized (I ';' J) c= s or ( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) ) )
A6: Start-At (0,SCM+FSA) c= (I ';' J) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
set s1 = s +* I;
set m1 = LifeSpan ((ProgramPart (s +* I)),(s +* I));
set s4 = Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1));
T4: ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = ProgramPart s by AMI_1:123;
A7: (Directed I) +* (Start-At (0,SCM+FSA)) c= (I ';' J) +* (Start-At (0,SCM+FSA)) by PRE_CIRC:3, SCMFSA6A:55;
assume A8: Initialized (I ';' J) c= s ; :: thesis: ( IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
then (I ';' J) +* (Start-At (0,SCM+FSA)) c= s by SCMFSA6B:8;
then A9: Start-At (0,SCM+FSA) c= s by A6, XBOOLE_1:1;
then A10: s +* I = (Initialize s) +* I by FUNCT_4:79
.= Initialize (s +* I) by COMPOS_1:83
.= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
then A11: ProgramPart (s +* I) halts_on s +* I by A2, SCMFSA7B:def 8;
(I ';' J) +* (Start-At (0,SCM+FSA)) c= s by A8, SCMFSA6B:8;
then (Directed I) +* (Start-At (0,SCM+FSA)) c= s by A7, XBOOLE_1:1;
then A12: s = s +* ((Directed I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
hence A13: IC (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I by A2, A4, A10, SCMFSA8A:36; :: thesis: ( DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
set JAt = Initialize J;
set InJ = Initialized J;
set s3 = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J);
reconsider kk = DataPart (Initialize J) as Function ;
A14: DataPart (Initialize J) = {} by Th2;
(Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) . (intloc 0) = s . (intloc 0) by A4, A10, SCMFSA8C:97;
then A15: (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialize J) by A1, SCMFSA8C:18;
then DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = (DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))))) +* kk by FUNCT_4:75;
then DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A14, LATTICE2:8, XBOOLE_1:2;
hence A16: DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A2, A4, A10, A12, SCMFSA8A:36; :: thesis: ( ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A17: dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
A18: ProgramPart (Relocated (J,(card I))) c= I ';' J by FUNCT_4:26;
A19: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
A20: s +* I = s +* (Initialized I) by A8, SCMFSA6A:51;
A21: DataPart (IExec (I,s)) = DataPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) by A17, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) by A11, A20, EXTPRO_1:23 ;
then J is_halting_on Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))) by A3, A5, SCMFSA8B:8;
then A22: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by A15, SCMFSA7B:def 8;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then I ';' J c= s by A8, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= s by A18, XBOOLE_1:1;
then A23: ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) by AMI_1:81;
hence ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) ; :: thesis: ( (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
intloc 0 in Int-Locations by SCMFSA_2:def 4;
then A24: intloc 0 in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = (DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))) . (intloc 0) by A16, FUNCT_1:72, SCMFSA_2:127
.= ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) . (intloc 0) by A24, FUNCT_1:72, SCMFSA_2:127
.= (Initialized J) . (intloc 0) by A19, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: ( ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )
A25: I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)));
A26: dom (Directed I) = dom I by FUNCT_4:105;
reconsider m = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))) as Element of NAT ;
A27: Directed I c= I ';' J by SCMFSA6A:55;
(s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A26, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A8, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A27, A25, LATTICE2:8, XBOOLE_1:1
.= s by A8, LATTICE2:8 ;
then Directed I c= s by FUNCT_4:26;
then s +* (Directed I) = s by FUNCT_4:79;
then (s +* (Directed I)) +* (Start-At (0,SCM+FSA)) = s by A9, FUNCT_4:79;
then A28: s +* ((Directed I) +* (Start-At (0,SCM+FSA))) = s by FUNCT_4:15;
A29: DataPart (IExec (I,s)) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) by A15, A21, SCMFSA8A:11;
then A30: J is_closed_on (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by A5, SCMFSA8B:6;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) by AMI_1:123;
V: Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))) by EXTPRO_1:5;
TX3: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) by AMI_1:123;
TX4: ProgramPart s = ProgramPart (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) by T4, AMI_1:123;
A31: Initialize J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))))))) by A30, A13, A16, A23, TX3, TX4, T4, SCMFSA8C:42;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))),(card I)) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))))) by V;
then A32: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A22, EXTPRO_1:def 14
.= halt SCM+FSA by SCMFSA_4:8 ;
hence A33: ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: ( LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 ) )

A34: now

let k be Element of NAT ; :: thesis: ( ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k < m implies not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA )
assume ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k < m ; :: thesis: not CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA
then A35: k < LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))) by XREAL_1:8;
V: Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k) by EXTPRO_1:5;
assume A36: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,(((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + k)))) = halt SCM+FSA ; :: thesis: contradiction
TT4: ProgramPart s = ProgramPart (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k)) by T4, AMI_1:123;
TX3k: ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)) by AMI_1:123;
IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)))),(card I)) = CurInstr ((ProgramPart s),(Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),k))) by A30, A13, A16, A31, A23, T, TX3k, TT4, SCMFSA8C:42
.= halt SCM+FSA by A36, V ;
then InsCode (CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k)))) = 0 by SCMFSA_2:124, SCMFSA_4:22;
then CurInstr ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),(Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),k))) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A22, A35, EXTPRO_1:def 14; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < m implies CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b₁))) <> halt SCM+FSA )
assume A37: k < m ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b₁))) <> halt SCM+FSA

per cases ( k <= LifeSpan ((ProgramPart (s +* I)),(s +* I)) or LifeSpan ((ProgramPart (s +* I)),(s +* I)) < k ) ;

suppose k <= LifeSpan ((ProgramPart (s +* I)),(s +* I)) ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b₁))) <> halt SCM+FSA

hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCM+FSA by A2, A4, A10, A28, SCMFSA8A:35; :: thesis: verum

end;

suppose LifeSpan ((ProgramPart (s +* I)),(s +* I)) < k ; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,b₁))) <> halt SCM+FSA

then (LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A38: ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + kk = k by A38;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) <> halt SCM+FSA by A34, A37; :: thesis: verum

end;

end;

end;

then for k being Element of NAT st CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA holds
m <= k ;
then A39: LifeSpan ((ProgramPart s),s) = m by A32, A33, EXTPRO_1:def 14;
Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I)))) = Result ((ProgramPart (s +* I)),(s +* I)) by A11, EXTPRO_1:23;
hence LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) by A39; :: thesis: ( J is good implies (Result ((ProgramPart s),s)) . (intloc 0) = 1 )
J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then A40: ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) +* (J +* (Start-At (0,SCM+FSA))) = (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:79;
A41: Initialized J c= (Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J) by FUNCT_4:26;

hereby :: thesis: verum

A42: DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) = DataPart (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) by A30, A13, A16, A31, A23, T4, SCMFSA8C:42;
assume A43: J is good ; :: thesis: (Result ((ProgramPart s),s)) . (intloc 0) = 1
thus (Result ((ProgramPart s),s)) . (intloc 0) = (Comput ((ProgramPart s),s,m)) . (intloc 0) by A33, A39, EXTPRO_1:23
.= (Comput ((ProgramPart s),(Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by EXTPRO_1:5
.= (Comput ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J))),((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)))))) . (intloc 0) by A42, SCMFSA6A:38
.= ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) . (intloc 0) by A5, A29, A40, A43, SCMFSA8B:6, SCMFSA8C:97
.= (Initialized J) . (intloc 0) by A19, A41, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis: verum

end;