let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_closed_on Initialized S,P
let S be State of SCM+FSA; for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_closed_on Initialized S,P
let I, J be Program of SCM+FSA; ( I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P implies I ';' J is_closed_on Initialized S,P )
assume that
A1:
I is_halting_on Initialized S,P
and
A2:
I is_closed_on Initialized S,P
and
A3:
J is_closed_on IExec (I,P,S),P
; I ';' J is_closed_on Initialized S,P
A4:
ProgramPart I = I
by RELAT_1:209;
A5:
ProgramPart J = J
by RELAT_1:209;
set IS = Initialized S;
set PS = P;
set s = (Initialized S) +* (Initialize (I ';' J));
set p = P +* (I ';' J);
A6:
I ';' J c= P +* (I ';' J)
by FUNCT_4:26;
A7:
Directed I c= I ';' J
by SCMFSA6A:55;
I ';' J c= P +* (I ';' J)
by FUNCT_4:26;
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:79;
A9:
DataPart (Initialized S) = DataPart ((Initialized S) +* (Initialize (I ';' J)))
by SCMFSA8A:11;
then A10:
I is_closed_on (Initialized S) +* (Initialize (I ';' J)),P +* (I ';' J)
by A2, SCMFSA8B:6;
A11:
I is_halting_on (Initialized S) +* (Initialize (I ';' J)),P +* (I ';' J)
by A1, A2, A9, SCMFSA8B:8;
then A12:
(P +* (I ';' J)) +* I halts_on ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)
by SCMFSA7B:def 8, A4;
set s1 = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I);
set p1 = (P +* (I ';' J)) +* I;
set JAt = Initialize J;
set s3 = (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J);
set p3 = ((P +* (I ';' J)) +* I) +* J;
A13:
J c= ((P +* (I ';' J)) +* I) +* J
by FUNCT_4:26;
set m1 = LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)));
set IJ = I ';' J;
A14:
ProgramPart (I ';' J) = I ';' J
by RELAT_1:209;
A15:
(Initialized S) . (intloc 0) = 1
by SCMFSA6C:3;
then
((Initialized S) +* (Initialize (I ';' J))) . (intloc 0) = 1
by A9, SCMFSA6A:38;
then A16:
((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I) = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I)
by SCMFSA8C:18;
DataPart (IExec (I,P,S)) =
DataPart (IExec (I,P,(Initialized S)))
by SCMFSA8C:17
.=
DataPart (IExec (I,(P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J)))))
by A1, A2, A9, A15, SCMFSA8C:46
.=
DataPart ((Result (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I)))) +* (((Initialized S) +* (Initialize (I ';' J))) | NAT))
by SCMFSA6B:def 1
.=
DataPart (Result (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialized I))))
by COMPOS_1:82
.=
DataPart (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I))))))
by A16, A12, EXTPRO_1:23
;
then
DataPart (IExec (I,P,S)) = DataPart ((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J))
by SCMFSA8A:11;
then A17:
J is_closed_on (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J),((P +* (I ';' J)) +* I) +* J
by A3, SCMFSA8B:6;
set PPR = Reloc (J,(card I));
set s4 = Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1));
reconsider kk = DataPart (Initialize J) as Function ;
A18:
DataPart ((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) = (DataPart (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I))))))) +* kk
by FUNCT_4:75;
let k be Element of NAT ; SCMFSA7B:def 7 IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),k)) in proj1 (I ';' J)
A19:
Initialize (Directed I) c= Initialize (I ';' J)
by PRE_CIRC:3, SCMFSA6A:55;
A20:
Initialize J c= (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)
by FUNCT_4:26;
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 A21:
(Initialized S) +* (Initialize (I ';' J)) = ((Initialized S) +* (Initialize (I ';' J))) +* (Initialize (Directed I))
by FUNCT_4:79;
then
IC (Comput (((P +* (I ';' J)) +* (Directed I)),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))) = card I
by SCMFSA8A:36, A10, A11;
then A22:
IC (Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))) = card I
by A8;
DataPart (Initialize J) = {}
by Th2;
then
DataPart (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) = DataPart ((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J))
by A18, LATTICE2:8, XBOOLE_1:2;
then A23:
DataPart (Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))) = DataPart ((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J))
by A10, A11, A21, SCMFSA8A:36, A8;
A24:
Reloc (J,(card I)) c= I ';' J
by FUNCT_4:26;
A25:
Reloc (J,(card I)) c= P +* (I ';' J)
by A6, XBOOLE_1:1, A24;
per cases
( k <= LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I))) or (LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1 <= k )
by NAT_1:13;
suppose A26:
k <= LifeSpan (
((P +* (I ';' J)) +* I),
(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))
;
IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),k)) in proj1 (I ';' J)A27:
dom I c= dom (I ';' J)
by SCMFSA6A:56;
A28:
IC (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),k)) in dom I
by A10, SCMFSA7B:def 7, A4;
IC (Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),k)) = IC (Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),k))
by A10, A11, A21, A26, COMPOS_1:24, SCMFSA8A:35, A8;
hence
IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),k)) in proj1 (I ';' J)
by A28, A27, A14;
verum end; suppose
(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1
<= k
;
IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),k)) in proj1 (I ';' J)then consider i being
Nat such that A29:
k = ((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1) + i
by NAT_1:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
reconsider jloc =
IC (Comput ((((P +* (I ';' J)) +* I) +* J),((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)),i)) as
Element of
NAT ;
A30:
(Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J) = ((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)) +* (Initialize J)
by A20, FUNCT_4:79;
(((P +* (I ';' J)) +* I) +* J) +* J = ((P +* (I ';' J)) +* I) +* J
by FUNCT_4:99;
then A31:
IC (Comput ((((P +* (I ';' J)) +* I) +* J),((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)),i)) in dom J
by A17, SCMFSA7B:def 7, A5, A30;
dom (Reloc (J,(card I))) =
dom (Reloc (J,(card I)))
.=
{ (j + (card I)) where j is Element of NAT : j in dom J }
by COMPOS_1:117
;
then A32:
jloc + (card I) in dom (Reloc (J,(card I)))
by A31;
A33:
dom (Reloc (J,(card I))) c= dom (I ';' J)
by A24, RELAT_1:25;
(IC (Comput ((((P +* (I ';' J)) +* I) +* J),((Comput (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)),(LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))))) +* (Initialize J)),i))) + (card I) =
IC (Comput ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1))),i))
by A22, A23, A20, A17, SCMFSA8C:42, A13, A25
.=
IC (Comput ((P +* (I ';' J)),((Initialized S) +* (Initialize (I ';' J))),(((LifeSpan (((P +* (I ';' J)) +* I),(((Initialized S) +* (Initialize (I ';' J))) +* (Initialize I)))) + 1) + i)))
by EXTPRO_1:5
;
hence
IC (Comput ((P +* (ProgramPart (I ';' J))),((Initialized S) +* (Initialize (I ';' J))),k)) in proj1 (I ';' J)
by A29, A32, A33, A14;
verum end;