let P be Instruction-Sequence of SCM+FSA; :: thesis: for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_halting_on Initialized S,P
let S be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_halting_on Initialized S,P
let I, J be Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P implies I ';' J is_halting_on Initialized S,P )
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: I ';' J is_halting_on Initialized S,P
set s = Initialize (Initialized S);
set p = P +* (I ';' J);
A7: 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 A7, XBOOLE_1:1;
then A8: (P +* (I ';' J)) +* (Directed I) = P +* (I ';' J) by FUNCT_4:98;
A9: DataPart (Initialized S) = DataPart (Initialize (Initialized S)) by MEMSTR_0:79;
then A10: I is_halting_on Initialize (Initialized S),P +* (I ';' J) by A1, A3, SCMFSA8B:5;
then A11: (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;
A12: (Initialized S) . (intloc 0) = 1 by SCMFSA6A:38;
then (Initialize (Initialized S)) . (intloc 0) = 1 by A9, SCMFSA6A:7;
then A13: Initialize (Initialize (Initialized S)) = Initialized (Initialize (Initialized S)) by SCMFSA8C:4;
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;
A14: 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)))))))));
A15: 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, A9, A12, 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 A13, A11, 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 A16: ((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 A15, MEMSTR_0:79;
then A17: 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;
A18: 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);
A21: Reloc (J,(card I)) c= P +* (I ';' J) by A7, A18, 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 ;
A22: 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 proj1 (P +* (I ';' J)) & CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize (Initialized S)),m))) = halt SCM+FSA )
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: CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize (Initialized S)),m))) = halt SCM+FSA
A24: I is_closed_on Initialize (Initialized S),P +* (I ';' J) by A3, A9, SCMFSA8B:3;
then A25: IC (Comput ((P +* (I ';' J)),(Initialize (Initialized S)),((LifeSpan (((P +* (I ';' J)) +* I),(Initialize (Initialize (Initialized S))))) + 1))) = card I by A10, A8, SCMFSA8A:22;
A26: 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 A22, 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 A24, A10, A8, 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 A25, A17, A21, A14, 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 A26;
then CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize (Initialized S)),m))) = IncAddr ((halt SCM+FSA),(card I)) by A16, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_1:11 ;
hence CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize (Initialized S)),m))) = halt SCM+FSA ; :: thesis: verum