let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 = (Initialized S) +* (Initialize (I ';' J));
set p = P +* (ProgramPart (I ';' J));
A5: ProgramPart I = I by RELAT_1:209;
A6: ProgramPart J = J by RELAT_1:209;
ProgramPart (I ';' J) = I ';' J by RELAT_1:209;
then A7: I ';' J c= P +* (ProgramPart (I ';' J)) by FUNCT_4:26;
Directed I c= I ';' J by SCMFSA6A:55;
then Directed I c= P +* (ProgramPart (I ';' J)) by A7, XBOOLE_1:1;
then A8: (P +* (ProgramPart (I ';' J))) +* (Directed I) = P +* (ProgramPart (I ';' J)) by FUNCT_4:79;
A9: DataPart (Initialized S) = DataPart ((Initialized S) +* (Initialize (I ';' J))) by SCMFSA8A:11;
then A10: I is_halting_on (Initialized S) +* (Initialize (I ';' J)),P +* (ProgramPart (I ';' J)) by A1, A3, SCMFSA8B:8;
then A11: (P +* (ProgramPart (I ';' J))) +* I halts_on ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I) by SCMFSA7B:def 8, A5;
set s1 = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I);
set p1 = (P +* (ProgramPart (I ';' J))) +* I;
A12: (Initialized S) . (intloc 0) = 1 by SCMFSA6C:3;
then ((Initialized S) +* (Initialize (I ';' J))) . (intloc 0) = 1 by A9, SCMFSA6A:38;
then A13: ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I) = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I) by SCMFSA8C:18;
set JAt = Initialize J;
set s3 = (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J);
set p3 = ((P +* (ProgramPart (I ';' J))) +* I) +* J;
A14: J c= ((P +* (ProgramPart (I ';' J))) +* I) +* J by FUNCT_4:26;
set m3 = LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)));
A15: DataPart (IExec (I,P,S)) = DataPart (IExec (I,P,(Initialized S))) by SCMFSA8C:17
.= DataPart (IExec (I,(P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))))) by A1, A3, A9, A12, SCMFSA8C:46
.= DataPart ((Result (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I)))) +* (((Initialized S) +* (Initialize (I ';' J))) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I)))) by COMPOS_1:82
.= DataPart (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) by A13, A11, EXTPRO_1:23 ;
then J is_halting_on Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I))))),(P +* (ProgramPart (I ';' J))) +* I by A2, A4, SCMFSA8B:8;
then A16: ((P +* (ProgramPart (I ';' J))) +* I) +* J halts_on (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J) by SCMFSA7B:def 8, A6;
DataPart (IExec (I,P,S)) = DataPart ((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) by A15, SCMFSA8A:11;
then A17: J is_closed_on (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J),((P +* (ProgramPart (I ';' J))) +* I) +* J by A4, SCMFSA8B:6;
A18: Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
set m1 = LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)));
set s4 = Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1));
set p4 = P +* (ProgramPart (I ';' J));
A19: Initialize (Directed I) c= Initialize (I ';' J) by PRE_CIRC:3, SCMFSA6A:55;
Initialize (I ';' J) c= (Initialized S) +* (Initialize (I ';' J)) by FUNCT_4:26;
then Initialize (Directed I) c= (Initialized S) +* (Initialize (I ';' J)) by A19, XBOOLE_1:1;
then A20: (Initialized S) +* (Initialize (I ';' J)) = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize (Directed I)) by FUNCT_4:79;
A21: Reloc (J,(card I)) c= P +* (ProgramPart (I ';' J)) by A7, A18, XBOOLE_1:1;
reconsider m = ((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1) + (LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)))) as Element of NAT ;
reconsider kk = DataPart (Initialize J) as Function ;
A22: DataPart ((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) = (DataPart (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I))))))) +* kk by FUNCT_4:75;
take m ; :: according to EXTPRO_1:def 7,SCMFSA7B:def 8 :: thesis: ( IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m)) in proj1 (P +* (ProgramPart (I ';' J))) & CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m))) = halt SCM+FSA )
IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m)) in NAT ;
hence IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m)) in dom (P +* (ProgramPart (I ';' J))) by PARTFUN1:def 4; :: thesis: CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m))) = halt SCM+FSA
A23: Initialize J c= (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J) by FUNCT_4:26;
A24: I is_closed_on (Initialized S) +* (Initialize (I ';' J)),P +* (ProgramPart (I ';' J)) by A3, A9, SCMFSA8B:6;
then A25: IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))) = card I by A10, A20, SCMFSA8A:36, A8;
A26: Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),(((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1) + (LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)))))) = Comput ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))),(LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J))))) by EXTPRO_1:5;
DataPart (Initialize J) = {} by Th2;
then DataPart (Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) = DataPart ((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) by A22, LATTICE2:8, XBOOLE_1:2;
then DataPart (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))) = DataPart ((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) by A24, A10, A20, SCMFSA8A:36, A8;
then IncAddr ((CurInstr ((((P +* (ProgramPart (I ';' J))) +* I) +* J),(Comput ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)),(LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)))))))),(card I)) = CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))),(LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J))))))) by A25, A23, A17, SCMFSA8C:42, A21, A14;
then IncAddr ((CurInstr ((((P +* (ProgramPart (I ';' J))) +* I) +* J),(Comput ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)),(LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)))))))),(card I)) = CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),(((LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1) + (LifeSpan ((((P +* (ProgramPart (I ';' J))) +* I) +* J),((Comput (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (ProgramPart (I ';' J))) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)))))))) by A26;
then CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m))) = IncAddr ((halt SCM+FSA),(card I)) by A16, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
hence CurInstr ((P +* (ProgramPart (I ';' J))),(Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),m))) = halt SCM+FSA ; :: thesis: verum