let P be Instruction-Sequence of SCM+FSA; :: thesis:
let S be State of SCM+FSA; :: thesis:
let I, J be 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 and
A3: I is_closed_on Initialized S,P and
A4: J is_closed_on IExec (I,P,S),P ; :: thesis:
set s = Initialize (Initialized S);
set p = P +* (I ";" J);
A5: 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 A5, XBOOLE_1:1;
then A6: (P +* (I ";" J)) +* (Directed I) = P +* (I ";" J) by FUNCT_4:98;
A7: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A8: I is_halting_on Initialize (Initialized S),P +* (I ";" J) by A1, A3, SCMFSA8B:5;
then A9: (P +* (I ";" J)) +* I halts_on Initialize (Initialize (Initialized S)) by SCMFSA7B:def 7;
set s1 = Initialize (Initialize (Initialized S));
set p1 = (P +* (I ";" J)) +* I;
A10: (Initialized S) . (intloc 0) = 1 by SCMFSA_M:9;
then (Initialize (Initialized S)) . (intloc 0) = 1 by A7, SCMFSA_M:2;
then A11: 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;
A12: 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)))))))));
A13: 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, A3, A7, A10, 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 A11, A9, 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, A4, SCMFSA8B:5;
then A14: ((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))))))) by SCMFSA7B:def 7;
DataPart (IExec (I,P,S)) = DataPart (Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S)))))))) by A13, MEMSTR_0:79;
then A15: J is_closed_on Initialize (Comput (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))),(LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))))),((P +* (I ";" J)) +* I) +* J by A4, SCMFSA8B:3;
A16: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
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);
A17: Reloc (J,(card I)) c= P +* (I ";" J) by A5, A16, 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 ;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A18: 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 7 :: 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:
A19: I is_closed_on Initialize (Initialized S),P +* (I ";" J) by A3, A7, SCMFSA8B:3;
then A20: IC (Comput ((P +* (I ";" J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ";" J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A8, A6, SCMFSA8A:22;
A21: 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 A18, 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 A19, A8, A6, 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 A20, A15, A17, A12, 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 A21;
then CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize (Initialized S)),m))) = IncAddr ((halt SCM+FSA),(card I)) by A14, 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: