let p be Instruction-Sequence of SCM+FSA; :: thesis:
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,p and
A3: J is_halting_on IExec (I,p,s),p and
A4: I is_closed_on s,p and
A5: J is_closed_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 A6: Initialize ((intloc 0) .--> 1) c= s ; :: thesis:
then Start-At (0,SCM+FSA) c= s by MEMSTR_0:50;
then A7: Start-At (0,SCM+FSA) c= s ;
A8: s = s +* (Start-At (0,SCM+FSA)) by A7, FUNCT_4:98
.= Initialize s ;
then A9: p +* I halts_on s by A2, SCMFSA7B:def 7;
assume A10: I ";" J c= p ; :: thesis:
Directed I c= I ";" J by SCMFSA6A:16;
then Directed I c= p by A10, XBOOLE_1:1;
then A11: p +* (Directed I) = p by FUNCT_4:98;
Start-At (0,SCM+FSA) c= s by A6, MEMSTR_0:50;
then Start-At (0,SCM+FSA) c= s ;
then s = Initialize s by FUNCT_4:98;
hence A12: IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I by A2, A4, A11, 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;
A13: J c= (p +* I) +* J by FUNCT_4:25;
reconsider kk = DataPart (Start-At (0,SCM+FSA)) as Function ;
A14: DataPart (Start-At (0,SCM+FSA)) = {} by MEMSTR_0:20;
(Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) . (intloc 0) = s . (intloc 0) by A4, A8, SCMFSA8C:68;
then A15: 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 A14, FUNCT_4:98, XBOOLE_1:2;
hence A16: DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A2, A4, A8, A11, SCMFSA8A:22; :: thesis:
A17: Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
A18: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:10;
A19: s = s +* (Initialize ((intloc 0) .--> 1)) by A6, FUNCT_4:98;
A20: 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 A9, A19, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* I),s,(LifeSpan ((p +* I),s))),p +* I by A3, A5, SCMFSA8B:5;
then A21: (p +* I) +* J halts_on Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by A15, SCMFSA7B:def 7;
I ";" J c= p by A10;
then Reloc (J,(card I)) c= p by A17, XBOOLE_1:1;
then Reloc (J,(card I)) c= p ;
hence Reloc (J,(card I)) c= p ; :: thesis:
A22: Reloc (J,(card I)) c= p by A10, A17, XBOOLE_1:1;
intloc 0 in Int-Locations by AMI_2:def 16;
then A23: 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 A16, FUNCT_1:49
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A23, FUNCT_1:49
.= 1 by A18, 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 ;
A24: DataPart (IExec (I,p,s)) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) by A15, A20, MEMSTR_0:79;
then A25: J is_closed_on Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))),(p +* I) +* J by A5, SCMFSA8B:3;
A26: 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 A25, A12, A16, A22, A13, 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 A26;
then A27: CurInstr (p,(Comput (p,s,m))) = IncAddr ((halt SCM+FSA),(card I)) by A21, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
hence A28: p halts_on s by EXTPRO_1:29; :: thesis:

A29: now :: thesis:

let k be Element of NAT ; :: thesis:
assume ((LifeSpan ((p +* I),s)) + 1) + k < m ; :: thesis:
then A30: k < LifeSpan (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))))) by XREAL_1:6;
A31: 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 A32: CurInstr (p,(Comput (p,s,(((LifeSpan ((p +* I),s)) + 1) + k)))) = halt SCM+FSA ; :: thesis:
A33: 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 A32, A31, A25, A12, A16, A22, A13, SCMFSA8C:16;
then InsCode (CurInstr (((p +* I) +* J),(Comput (((p +* I) +* J),(Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))),k)))) = 0 by COMPOS_0:def 9, A33;
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 A21, A30, EXTPRO_1:def 15; :: thesis:

end;

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

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

hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A2, A4, A8, A11, 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
A35: ((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 A35;
hence CurInstr (p,(Comput (p,s,k))) <> halt SCM+FSA by A29, A34; :: thesis:

end;

end;

end;

then for k being Element of NAT st CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA holds
m <= k ;
then A36: LifeSpan (p,s) = m by A27, A28, EXTPRO_1:def 15;
Comput ((p +* I),s,(LifeSpan ((p +* I),s))) = Result ((p +* I),s) by A9, EXTPRO_1:23;
hence LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) by A36; :: thesis:
Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25, MEMSTR_0:50;
then A37: Initialize (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) = Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:98;
A38: Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) by FUNCT_4:25;

hereby :: thesis:

A39: 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 A25, A12, A16, A22, A13, SCMFSA8C:16;
assume A40: J is good ; :: thesis:
thus (Result (p,s)) . (intloc 0) = (Comput (p,s,m)) . (intloc 0) by A28, A36, 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 A39, SCMFSA_M:2
.= (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) . (intloc 0) by A5, A24, A37, A40, SCMFSA8B:3, SCMFSA8C:68
.= 1 by A18, A38, GRFUNC_1:2, SCMFSA_M:12 ; :: thesis:

end;