let P be Instruction-Sequence of SCM+FSA; :: thesis:
let S be State of SCM+FSA; :: thesis:
let I, J be really-closed Program of SCM+FSA; :: thesis:
assume that
A1: I is_halting_on Initialized S,P and
A2: J is_halting_on IExec (I,P,S),P ; :: thesis:
set s = Initialize (Initialized S);
set p = P +* (I ";" J);
A3: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
Directed I c= I ";" J by SCMFSA6A:16;
then Directed I c= P +* (I ";" J) by A3, XBOOLE_1:1;
then A4: (P +* (I ";" J)) +* (Directed I) = P +* (I ";" J) by FUNCT_4:98;
A5: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A6: I is_halting_on Initialize (Initialized S),P +* (I ";" J) by A1, SCMFSA8B:5;
then A7: (P +* (I ";" J)) +* I halts_on Initialize (Initialize (Initialized S)) ;
set s1 = Initialize (Initialize (Initialized S));
set p1 = (P +* (I ";" J)) +* I;
A8: (Initialized S) . (intloc 0) = 1 by SCMFSA_M:9;
then (Initialize (Initialized S)) . (intloc 0) = 1 by A5, SCMFSA_M:2;
then A9: Initialize (Initialize (Initialized S)) = Initialized (Initialize (Initialized S)) by SCMFSA_M:18;
set JAt = Start-At (0,SCM+FSA);
set s3 = Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))));
set p3 = ((P +* (I ";" J)) +* I) +* J;
A10: J c= ((P +* (I ";" J)) +* I) +* J by FUNCT_4:25;
set m3 = LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))));
DataPart (IExec (I,P,S)) = DataPart (IExec (I,P,(Initialized S))) by SCMFSA8C:3
.= DataPart (IExec (I,(P +* (I ";" J)),(Initialize (Initialized S)))) by A1, A5, A8, SCMFSA8C:20
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S))))) by SCMFSA6B:def 1
.= DataPart (Result (((P +* (I ";" J)) +* I),(Initialized (Initialize (Initialized S)))))
.= DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) by A9, A7, EXTPRO_1:23 ;
then J is_halting_on Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))),(P +* (I ";" J)) +* I by A2, SCMFSA8B:5;
then A11: ((P +* (I ";" J)) +* I) +* J halts_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) ;
A12: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
set m1 = LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))));
set s4 = Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1));
set p4 = P +* (I ";" J);
A13: Reloc (J,(card I)) c= P +* (I ";" J) by A3, A12, XBOOLE_1:1;
reconsider m = ((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))) as Element of NAT by ORDINAL1:def 12;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A14: DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) = (DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) +* kk by FUNCT_4:71;
take m ; :: according to EXTPRO_1:def 8,SCMFSA7B:def 6 :: thesis:
IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m)) in NAT ;
hence IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m)) in dom (P +* (I ";" J)) by PARTFUN1:def 2; :: thesis:
A15: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A6, A4, SCMFSA8A:22;
A16: Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))) = Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))))))) by EXTPRO_1:4;
DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
then DataPart (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A14, FUNCT_4:98, XBOOLE_1:2;
then DataPart (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A6, A4, SCMFSA8A:22;
then IncAddr ((CurInstr ((((P +* (I ";" J)) +* I) +* J),(Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))))))))) by A15, A13, A10, SCMFSA8C:16;
then IncAddr ((CurInstr ((((P +* (I ";" J)) +* I) +* J),(Comput ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))),(LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),(((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1) + (LifeSpan ((((P +* (I ";" J)) +* I) +* J),(Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))))))))) by A16;
then CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = IncAddr ((halt SCM+FSA),(card I)) by A11, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = halt SCM+FSA ; :: thesis: