let p be Instruction-Sequence of SCM+FSA; :: thesis:
let I be good really-closed Program of SCM+FSA; :: thesis:
let J be really-closed 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,p and
A3: J is_halting_on IExec (I,p,s),p ; :: thesis:
set s1 = s;
set p1 = p +* I;
set m1 = LifeSpan ((p +* I),s);
set s4 = Comput (p,s,((LifeSpan ((p +* I),s)) + 1));
set p4 = p;
assume A4: Initialize ((intloc 0) .--> 1) c= s ; :: thesis:
then Start-At (0,SCM+FSA) c= s by MEMSTR_0:50;
then A5: Start-At (0,SCM+FSA) c= s ;
A6: s = s +* (Start-At (0,SCM+FSA)) by A5, FUNCT_4:98
.= Initialize s ;
then A7: p +* I halts_on s by A2;
assume A8: I ";" J c= p ; :: thesis:
Directed I c= I ";" J by SCMFSA6A:16;
then Directed I c= p by A8, XBOOLE_1:1;
then A9: p +* (Directed I) = p by FUNCT_4:98;
Start-At (0,SCM+FSA) c= s by A4, MEMSTR_0:50;
then Start-At (0,SCM+FSA) c= s ;
then s = Initialize s by FUNCT_4:98;
hence A10: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A2, A9, SCMFSA8A:22; :: thesis:
set JAt = Start-At (0,SCM+FSA);
set InJ = Initialize ((intloc 0) .--> 1);
set s3 = Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))));
set p3 = (p +* I) +* J;
A11: J c= (p +* I) +* J by FUNCT_4:25;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A12: DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
(Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . (intloc 0) = s . (intloc 0) by A6, SCMFSA8C:68;
then A13: Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = Initialize (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A1, SCMFSA_M:18;
then DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) = (DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) +* kk by FUNCT_4:71;
then DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A12, FUNCT_4:98, XBOOLE_1:2;
hence A14: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A2, A6, A9, SCMFSA8A:22; :: thesis:
A15: Reloc (J,(card I)) c= I ";" J by SCMFSA6A:38;
A16: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:10;
A17: s = s +* (Initialize ((intloc 0) .--> 1)) by A4, FUNCT_4:98;
DataPart (IExec (I,p,s)) = DataPart (Result ((p +* I),(Initialized s))) by SCMFSA6B:def 1
.= DataPart (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A7, A17, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* I),s,(LifeSpan ((p +* I),s))),p +* I by A3, SCMFSA8B:5;
then A18: (p +* I) +* J halts_on Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A13;
I ";" J c= p by A8;
then Reloc (J,(card I)) c= p by A15, XBOOLE_1:1;
then Reloc (J,(card I)) c= p ;
hence Reloc (J,(card I)) c= p ; :: thesis:
A19: Reloc (J,(card I)) c= p by A8, A15, XBOOLE_1:1;
intloc 0 in Int-Locations by AMI_2:def 16;
then A20: intloc 0 in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = (DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))) . (intloc 0) by A14, FUNCT_1:49
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A20, FUNCT_1:49
.= 1 by A16, FUNCT_4:13, SCMFSA_M:12 ;
:: thesis:
set m3 = LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))));
reconsider m = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))) as Element of NAT by ORDINAL1:def 12;
A21: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))))) by EXTPRO_1:4;
IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))),(card I)) = CurInstr (p,(Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))))))) by A10, A14, A19, A11, SCMFSA8C:16;
then IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))),(card I)) = CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))))) by A21;
then A22: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A18, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A23: p halts_on s by EXTPRO_1:29; :: thesis:

A24: now :: thesis:

let k be Element of NAT ; :: thesis:
assume ((LifeSpan ((p +* I),s)) + 1) + k < m ; :: thesis:
then A25: k < LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))) by XREAL_1:6;
A26: Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)) = Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),k) by EXTPRO_1:4;
assume A27: CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA ; :: thesis:
A28: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
IncAddr ((CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k)))),(card I)) = halt SCM+FSA by A27, A26, A10, A14, A19, A11, SCMFSA8C:16;
then InsCode (CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k)))) = 0 by A28, COMPOS_0:def 9;
then CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k))) = halt SCM+FSA by SCMFSA_2:95;
hence contradiction by A18, A25, EXTPRO_1:def 15; :: thesis:

end;

let k be Nat; :: thesis:
assume A29: k < m ; :: thesis:

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

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A2, A6, A9, SCMFSA8A:21; :: thesis:

end;

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

then (LifeSpan ((p +* I),s)) + 1 <= k by NAT_1:13;
then consider kk being Nat such that
A30: ((LifeSpan ((p +* I),s)) + 1) + kk = k by NAT_1:10;
reconsider kk = kk as Element of NAT by ORDINAL1:def 12;
((LifeSpan ((p +* I),s)) + 1) + kk = k by A30;
hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A24, A29; :: thesis:

end;

end;

end;

then for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A31: LifeSpan (p,s) = m by A22, A23, EXTPRO_1:def 15;
Comput ((p +* I),s,(LifeSpan ((p +* I),s))) = Result ((p +* I),s) by A7, EXTPRO_1:23;
hence LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) by A31; :: thesis:
Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25, MEMSTR_0:50;
then A32: Initialize (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) = Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:98;
A33: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25;

hereby :: thesis:

A34: DataPart (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) = DataPart (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) by A10, A14, A19, A11, SCMFSA8C:16;
assume A35: J is good ; :: thesis:
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A23, A31, EXTPRO_1:23
.= (Comput (p,(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) . (intloc 0) by EXTPRO_1:4
.= (Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),(LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))))))) . (intloc 0) by A34, SCMFSA_M:2
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A32, A35, SCMFSA8C:68
.= 1 by A16, A33, GRFUNC_1:2, SCMFSA_M:12 ; :: thesis:

end;