set D = Int-Locations \/ FinSeq-Locations ;
let I be InitHalting keepInt0_1 Program of ; :: thesis:
let J be InitHalting Program of ; :: thesis:
let s be State of ; :: thesis:
set s1 = s +* I;
set s3 = (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J);
set m1 = LifeSpan (s +* I);
set m3 = LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J));
A1: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
assume A2: Initialized (I ';' J) c= s ; :: thesis:
then A3: s = s +* (Initialized (I ';' J)) by FUNCT_4:79;
set s4 = Computation s,((LifeSpan (s +* I)) + 1);
A4: ( Directed I c= I ';' J & I ';' J c= Initialized (I ';' J) ) by SCMFSA6A:26, SCMFSA6A:55;
reconsider m = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J))) as Element of NAT ;
A5: dom (Directed I) = dom I by FUNCT_4:105;
A6: (s +* I) +* (Directed I) = s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A5, FUNCT_4:20
.= (s +* (Initialized (I ';' J))) +* (Directed I) by A2, LATTICE2:8
.= s +* ((Initialized (I ';' J)) +* (Directed I)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by A4, LATTICE2:8, XBOOLE_1:1
.= s by A2, LATTICE2:8 ;
then A7: Directed I c= s by FUNCT_4:26;
Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;
then dom (Initialized J) c= dom ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by GRFUNC_1:8;
then A8: dom (Initialized J) c= the carrier of SCM+FSA by AMI_1:79;
A9: ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
(I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) c= s by A2, FUNCT_4:15;
then A10: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A1, XBOOLE_1:1;
A11: Initialized I c= s +* I by A2, SCMFSA6A:52;
then A12: ProgramPart (s +* I) halts_on s +* I by Th5;
hence A13: IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) by A10, A6, Th21, FUNCT_4:26; :: thesis:

A14: now

let x be set ; :: thesis:
assume x in dom (DataPart (Initialized J)) ; :: thesis:
then A15: x in (dom (Initialized J)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then A16: x in dom (Initialized J) by XBOOLE_0:def 4;
A17: x in Int-Locations \/ FinSeq-Locations by A15, XBOOLE_0:def 4;

per cases by A16, SCMFSA6A:44;

suppose A18: x in dom J ; :: thesis:

dom J c= NAT by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of SCM+FSA by A18, AMI_1:def 4;
(DataPart (Initialized J)) . l = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . l by A17, SCMFSA6A:37;
hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x ; :: thesis:

end;

suppose A19: x = intloc 0 ; :: thesis:

thus (DataPart (Initialized J)) . x = (Initialized J) . x by A17, FUNCT_1:72, SCMFSA_2:127
.= 1 by A19, SCMFSA6A:46
.= (Computation (s +* I),(LifeSpan (s +* I))) . x by A11, A19, Def3
.= (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x by A17, FUNCT_1:72, SCMFSA_2:127 ; :: thesis:

end;

suppose x = IC SCM+FSA ; :: thesis:

hence (DataPart (Initialized J)) . x = (DataPart (Computation (s +* I),(LifeSpan (s +* I)))) . x by A15, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis:

end;

A30: now

let k be Element of NAT ; :: thesis:
assume ((LifeSpan (s +* I)) + 1) + k < m ; :: thesis:
then A31: k < LifeSpan ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) by XREAL_1:8;
assume A32: 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 A13, A23, A27, A24, Th12
.= halt SCM+FSA by A32, 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 A21, A31, AMI_1:def 46; :: thesis:

end;

now

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

per cases ;

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

hence CurInstr (Computation s,k) <> halt SCM+FSA by A11, A6, Th23; :: 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
A34: ((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 A34;
hence CurInstr (Computation s,k) <> halt SCM+FSA by A30, A33; :: thesis:

end;

then for k being Element of NAT st CurInstr (Computation s,k) = halt SCM+FSA holds
m <= k ;
then A35: LifeSpan s = m by A28, A29, AMI_1:def 46;
s +* I = s +* (Initialized I) by A2, SCMFSA6A:51;
then Initialized I c= s +* I by FUNCT_4:26;
then ProgramPart (s +* I) halts_on s +* I by Th5;
hence LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) by A35, Th5, AMI_1:122; :: thesis:
A36: Initialized J c= (Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J) by FUNCT_4:26;

hereby :: thesis:

A37: 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 A13, A23, A27, A24, Th12;
assume A38: J is keeping_0 ; :: thesis:
thus (Result s) . (intloc 0 ) = (Computation s,m) . (intloc 0 ) by A29, A35, 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 A37, SCMFSA6A:38
.= ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) . (intloc 0 ) by A20, A38, SCMFSA6B:def 4
.= (Initialized J) . (intloc 0 ) by A25, A36, GRFUNC_1:8
.= 1 by SCMFSA6A:46 ; :: thesis:

end;