let I be good Program of SCM+FSA ; :: thesis:
let J be Program of SCM+FSA ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
assume that
A1: s . (intloc 0 ) = 1 and
A2: I is_halting_on s and
A3: J is_halting_on IExec I,s and
A4: I is_closed_on s and
A5: J is_closed_on IExec I,s ; :: thesis:
set s1 = s +* I;
set m1 = LifeSpan (s +* I);
set InJ = Initialized J;
set s3 = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J);
set m3 = LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J));
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At (insloc 0 );
set JAt = J +* (Start-At (insloc 0 ));
set Ins = NAT ;
assume A6: Initialized (I ';' J) c= s ; :: thesis:
A7: Start-At (insloc 0 ) c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:26;
(I ';' J) +* (Start-At (insloc 0 )) c= s by A6, SCMFSA6B:8;
then A8: Start-At (insloc 0 ) c= s by A7, XBOOLE_1:1;
then A9: s +* I = (s +* (Start-At (insloc 0 ))) +* I by FUNCT_4:79
.= (s +* I) +* (Start-At (insloc 0 )) by SCMFSA6B:14
.= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:15 ;
then A10: s +* I is halting by A2, SCMFSA7B:def 8;
A11: s +* I = s +* (Initialized I) by A6, SCMFSA6A:51;
reconsider kk = DataPart (J +* (Start-At (insloc 0 ))) as Function ;
(Computation (s +* I),(LifeSpan (s +* I))) . (intloc 0 ) = s . (intloc 0 ) by A4, A9, SCMFSA8C:97;
then A12: (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) = (Computation (s +* I),(LifeSpan (s +* I))) +* (J +* (Start-At (insloc 0 ))) by A1, SCMFSA8C:18;
then A13: DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) +* kk by FUNCT_4:75;
DataPart (J +* (Start-At (insloc 0 ))) = {} by Th2;
then A14: DataPart (Computation (s +* I),(LifeSpan (s +* I))) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A13, LATTICE2:8, XBOOLE_1:2;
A15: dom (Directed I) = dom I by FUNCT_4:105;
A16: Directed I c= I ';' J by SCMFSA6A:55;
A17: I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
(s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A15, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A6, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A16, A17, LATTICE2:8, XBOOLE_1:1
.= s by A6, LATTICE2:8 ;
then Directed I c= s by FUNCT_4:26;
then s +* (Directed I) = s by FUNCT_4:79;
then (s +* (Directed I)) +* (Start-At (insloc 0 )) = s by A8, FUNCT_4:79;
then A18: s +* ((Directed I) +* (Start-At (insloc 0 ))) = s by FUNCT_4:15;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A19: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A20: DataPart (IExec I,s) = DataPart ((Result (s +* (Initialized I))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized I))) by A19, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Computation (s +* I),(LifeSpan (s +* I))) by A10, A11, AMI_1:122 ;
then A21: DataPart (IExec I,s) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A12, SCMFSA8A:11;
then A22: J is_closed_on (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by A5, SCMFSA8B:6;
J is_halting_on Computation (s +* I),(LifeSpan (s +* I)) by A3, A5, A20, SCMFSA8B:8;
then A23: (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) is halting by A12, SCMFSA7B:def 8;
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A24: (I ';' J) +* (Start-At (insloc 0 )) c= s by A6, SCMFSA6B:8;
(Directed I) +* (Start-At (insloc 0 )) c= (I ';' J) +* (Start-At (insloc 0 )) by PRE_CIRC:3, SCMFSA6A:55;
then (Directed I) +* (Start-At (insloc 0 )) c= s by A24, XBOOLE_1:1;
then A25: s = s +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:79;
hence A26: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A2, A4, A9, SCMFSA8A:36; :: thesis:
thus A27: DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by A2, A4, A9, A14, A25, SCMFSA8A:36; :: thesis:
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) as Element of NAT ;
A28: J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then A29: I ';' J c= s by A6, XBOOLE_1:1;
ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
then ProgramPart (Relocated J,(card I)) c= s by A29, XBOOLE_1:1;
then A30: [(ProgramPart (Relocated J,(card I)))] c= Computation s,((LifeSpan (s +* I)) + 1) by AMI_1:81;
hence ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) ; :: thesis:
A31: intloc 0 in dom (Initialized J) by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:def 4;
then A32: intloc 0 in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = (DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) . (intloc 0 ) by A27, FUNCT_1:72, SCMFSA_2:127
.= ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) . (intloc 0 ) by A32, FUNCT_1:72, SCMFSA_2:127
.= (Initialized J) . (intloc 0 ) by A31, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis:

A33: now

let k be Element of NAT ; :: thesis:
assume ((LifeSpan (s +* I)) + 1) + k < m ; :: thesis:
then A34: k < LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by XREAL_1:8;
assume A35: CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + k)) = halt SCM+FSA ; :: thesis:
IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k)),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),k) by A22, A26, A27, A28, A30, SCMFSA8C:42
.= halt SCM+FSA by A35, AMI_1:51 ;
then InsCode (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k)) = 0 by SCMFSA_2:124, SCMFSA_4:22;
then CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),k) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A23, A34, AMI_1:def 46; :: thesis:

end;

IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A22, A26, A27, A28, A30, SCMFSA8C:42;
then IncAddr (CurInstr (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))),(card I) = CurInstr (Computation s,(((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))))) by AMI_1:51;
then A36: CurInstr (Computation s,m) = IncAddr (halt SCM+FSA ),(card I) by A23, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;

now

let k be Element of NAT ; :: thesis:
assume A37: k < m ; :: thesis:

per cases ;

suppose k <= LifeSpan (s +* I) ; :: thesis:

hence CurInstr (Computation s,k) <> halt SCM+FSA by A2, A4, A9, A18, SCMFSA8A:35; :: thesis:

end;

suppose LifeSpan (s +* I) < k ; :: thesis:

then (LifeSpan (s +* I)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A38: ((LifeSpan (s +* I)) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 13;
((LifeSpan (s +* I)) + 1) + kk = k by A38;
hence CurInstr (Computation s,k) <> halt SCM+FSA by A33, A37; :: thesis:

end;

then A39: for k being Element of NAT st CurInstr (Computation s,k) = halt SCM+FSA holds
m <= k ;
thus A40: s is halting by A36, AMI_1:def 20; :: thesis:
then A41: LifeSpan s = m by A36, A39, AMI_1:def 46;
hence LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) by A10, AMI_1:122; :: thesis:
A42: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
J +* (Start-At (insloc 0 )) c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
then A43: ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) +* (J +* (Start-At (insloc 0 ))) = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:79;

hereby :: thesis:

assume A44: J is good ; :: thesis:
A45: DataPart (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) = DataPart (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) by A22, A26, A27, A28, A30, SCMFSA8C:42;
thus (Result s) . (intloc 0 ) = (Computation s,m) . (intloc 0 ) by A40, A41, AMI_1:122
.= (Computation (Computation s,((LifeSpan (s +* I)) + 1)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) . (intloc 0 ) by AMI_1:51
.= (Computation ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)),(LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)))) . (intloc 0 ) by A45, SCMFSA6A:38
.= ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) . (intloc 0 ) by A5, A21, A43, A44, SCMFSA8B:6, SCMFSA8C:97
.= (Initialized J) . (intloc 0 ) by A31, A42, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis:

end;